Sunday, March 31, 2019

ITP2019

ITP2019

A Proof Assistant for Beginners

Abstract

Prooftoys is a web-based visual proof assistant, written in JavaScript to run in modern web browsers. It reflects the author’s belief that it is time for computer tools to become a welcome improvement pencil and paper in in basic proof-based mathematical problem-solving.

Its purpose is to support non-experts in exploration and self-education in logic and axiomatic mathematical reasoning, using the real numbers as a starting point. The design is driven by an overriding concern for simplicity and a less difficult learning process. It also strives for compatibility with textbook presentations of mathematical concepts.

This paper introduces the system, its logic, implementation, and user interaction. It aims to acquaint a technical audience with aspects of interest, though the system itself is designed for less technical users. The source code repository https://github.com/crisperdue/prooftoys contains the full source code and documentation, and the project Web site http://prooftoys.org/ is updated frequently with recent versions of the working system.

Introduction

To a new user, Prooftoys is a list of steps in a proof, displayed on a Web page. The list might be open for the user to extend and modify, or it might be locked down to be viewed but not changed. It might be on the Prooftoys web site (http://prooftoys.org/proofbuilder.html), or anywhere else on the web. It can operate in all of these modes.

All aspects of the system are under continuing development, so some parts should be expected to evolve in the future.

Prooftoys at work

Proof displays

In the user interface a proof is just a sequence of proof steps, each being an axiom, a definition, a fact already known true, or the result of applying some rule of inference to some input values, which may be proof steps, parts of proof steps, terms in the language, or other values.

Sample proof display A live version is at http://prooftoys.org/proofbuilder.html?fact=SubclassInter&details=true

Each step is numbered, with a statement of the step followed by some description of its derivation. Hovering over the step number highlights key step(s) and/or parts of the steps involved in deriving the step. Assumptions of types, using “ind”.

Assumptions of the form R x (that certain variables are real-valued) are omitted by default from the displays, and repetitive displays in the left side of a step may be reduced to just an ellipsis if they are identical to the previous step.

Proof step details

Almost all proofs use theorems that have already been proved, and most proof steps are really compositions of many smaller steps. Proof displays give the user easy access to proofs of theorems and details of proof steps by clicking within some part of the description of the step that is highlighted in blue.

So in the proof above, clicking on the word “use” in step 2, then digging down to details of details eventually takes us to:

proof display step details

This reveals the final phase of the proof of the key tautology for step 2.

Proof editing

  • “Point and click” selection – of steps and arbitrary terms
  • Simple editing of existing proof, with deletion and inlining of details

Selecting, drilling down. Viewing proofs

Levels of difficulty

Saving and restoring work

Logical concepts

The logic is based on Alonzo Church’s simple type theory as developed by Peter Andrews under the name Q0.

Prooftoys has the same theorems as Q0 and the same rule of inference, which allows replacement of an arbitrary term with one always equal to it. The axioms are like the five axioms of Q0, but two are generalizations that in Q0 are proved as theorems. The definitions of the boolean operators (except boolean equality) are defined by their truth tables by axiomatizing if-then-else. Prooftoys implements Q0 as a Hilbert-style system in the sense that it does not support a concept of hypotheses except as conjunctions of assumptions that form the antecedent of a conditional statement.

The logical core supports simple constant definitions that take the form of equalities with the defined name on the left and its definition on the right, with the usual restrictions on freshness of the name and absence of free variables in the right-hand side.

The real numbers are treated as a subset of the logical base type of individuals, and are axiomatized as a complete ordered field. This approach gives the math in Prooftoys a significantly different feel than other systems based on type theory. In particular, statements about the real numbers must explicitly include assumptions that certain variables have values in ℝ, where in other systems numbers are introduced as new types of the logic itself

Given that the reals are treated as a subset of the individuals, the integers, rationals, and natural numbers naturally become subsets of the reals, and there is much less need for explicit presentation of types of variables. On the other hand, closure of operations must be stated explicitly, and assumptions that an expression has a real value must be proved.

Logical kernel

The inference component of Prooftoys is built as a logical kernel, with additional functionality implemented by additional JavaScript functions that call the kernel functions and each other. JavaScript does not offer guarantees that new code will not bypass the kernel, but this aspect of the design still greatly improves the trustworthiness of the system.

The logical kernel supports assertion of axioms, starting with the logical axioms, and builds proofs withe Q0 primitive inference rule R, which takes a proved statement, a path specifying a term within that statement, and an equation as input. It returns a new proved statement as its result.

An empty path refers to an entire statement, and each component of a path indicates which part of the top-level term to traverse. A function invocation has a function part and an argument part, and a lambda term has a bound variable and a body. A path is a sequence of zero or more of these indications.

The kernel also supports assertion of axioms by an assert function that takes a statement in the logic as its only argument.

New proof steps (“steps”) are built up from axioms, constant definitions, and use of rule R. Each proved statement is linked to the name of the inference function that produced it, and all the arguments passed to that function, so the step can be reproduced.

Additional inference rules are implemented as side-effect-free JavaScript functions that accept arguments and return a proof step.

A step may depend on other steps, or on facts already proved as part of the system. Or it may not depend on other steps, for example being an axiom or theorem, or a step that proves a tautology from its statement.

Additional inference rules are implemented as JavaScript functions that accept arguments such as terms of the language and previously proved statements.

Notation

Identifiers are composed of alphanumerics with an optional numeric subscript indicated by appending _<digits>. Sequences of most other printing (currently ASCII) characters are considered to be operators. There are also integer literals within the limits of exact arithmetic in JavaScript.

Variable names are single-character identifiers, possibly subscripted. Operators and all other identifiers are reserved for constants, and operators can be declared internally as infix with a precedence. At present there is not an explicit syntax for entering an explicit type (such as individual) through the language.

Any expression can be enclosed in parentheses for grouping, a sequence of proof steps.
In this sense, the proof editornd an operator enclosed by itself in parentheses is allowed to represent its designed to support forward reasoning.

[[Move this:]] Backward reasoning from a goal toassociated constant. Notations of the form {<var>. <term>} and [<var>. <term>] indicate lambda expressions. For example {x. p x} its proof is also supported idiomatically by sthe same as λ x. p x in lambda notarting with with a step of the form conditions ⇒ goal, where goal is the conclusion part of the desired theorem. on. Terms with quantifiers use this notation, e.g. forall {x. p x ⇒ q x} ⇒ subclass p q. The syntax with braces is intentionally suggestive of set/class notation, but brackets have the same meaning.

Convenient inference

Tautology checking

The tautology checker is a function that takes a propositional calculus statement as its argument and attempts to prove the statement true. The result is a proved duplicate of the input. Like all proved statements in Prooftoys, the result is connected to the steps from which it was derived.

Rewriting

Rewriting could be considered the characteristic form of reasoning in Prooftoys. When a basic math text describes use of a basic law such as commutativity, it is effectively referring to rewriting.

Prooftoys matches a statement of equality (or logical equivalence) with an occurrence of an arbitrary term in some statement. If it finds a substitution into the equality that makes its left-hand side identical to the term it is matched against, the rewrite applies this substitution to the equality and replaces the occurrence with the right-hand side of the resulting equality.

The equality can be conditional, and if so the replacement step adds the antecedent (after substitution) to any assumptions as it replaces the occurrence of the term.

The system uses rewriting to accomplish other traditional forms of reasoning as well, described below.

Forward and backward reasoning

(goals and subgoals?)

The user interacts with the proof editor primarily by entering one step after another, producing a sequence of proof steps. In this sense, the proof editor is designed to support forward reasoning.

It is also straightforward to reason backward from a goal. For example a proof of a theorem of the form conditions ⇒ conclusion could start with an already-proved fact that has the same form but different conditions, even a tautology such as conclusion ⇒ conclusion.

Other convenient inferences

Simplification

Auto-simplification

Supporting mechanisms

Fact registration and lookup

Matching / substitution finding

Higher-order matching

Assumption management

Some basic and ubiquitous issues related to assumptions are handled internally to some of the rules of inference, such as rewriting rules. Among these are

It deduplication ofes assumptions, removal ofes assumptions trivially known to be true, such as “3 is a real number”, and handling of closure of operations by reducing reduces type assumptions on terms such as R (x + y) to R x & R y, and puts assumptions into a standard order for consistency between steps.

Working with real numbers

Comparison with other tools

Metamath, Mizar, (no tactic proofs)

Wednesday, April 19, 2017

Mathtoys update

Mathtoys has evolved considerably since my last update, and the changes post frequently to the site. There has been a fundamental change in the primary approach to solving an algebra problem, which itself changes some aspects of the user experience, and a handful of other notable changes in the user experience.


Straight-through problem solving in Mathtoys

Mathtoys has always proved every user step with its internal proof engine.
Older versions of Mathtoys nicely supported inference from the problem statement to a "solution", so that if the givens were true, the solution statement must be true.  These were all valid proofs, but the results were really "candidate" solutions, and in principle they required some sort of formal check that the solution was correct. This is easy enough to do by going back to the problem statement, replacing the variable with the candidate solution value, and checking that the result is a true statement.  On the other hand this is not necessary for many algebra problems, if you are confident that all the steps have been done correctly.

Recent versions of Mathtoys work directly with equivalences where possible. Steps display with a mathematical "equivalence" symbol "≡", indicating that the line is equivalent to the one above it and thus true for exactly the same values of the problem variables. When the final result is equivalent to the problem statement, the problem is solved without need for any further work, and you have a "straight-through" solution with no going back to check.

In some cases it is not possible to work with equivalent steps, but Mathtoys tries to do this when it can.  Of course if you solve a math problem by hand it is a good practice to go back and check for errors you may have made along the way.

Solving simultaneous equations

Mathtoys also solves simultaneous linear equations "straight-through" as well, using equivalences. This means that a problem statement says that all of the equations are true using a mathematical "and" also known as a "conjunction". If you choose to solve example simultaneous equations on the web site, you will see that the equations are connected with the mathematical "∧" symbol.

As you work through a problem, Mathtoys shows that each set of equations is equivalent to the set in the previous step and displays the "≡" symbol to indicate this.

Step suggestions

Until recently Mathtoys offered you a menu of things to do next, sometimes with an indication of what the result would look like. New in the user interface, Mathtoys may offer you some specific suggestions of exact next steps you can choose from as you work on a problem.  Some steps have descriptions in a menu, as before, but for many you get to see exactly what the next step could be if you choose it.

Solution status display

As your work on a problem approaches the desired form, Mathtoys now notices the progress and informs you wth a message. This applies especially to simultaneous equations, where each equation can make its own progress toward a solution.

Vacuously true statements

You can think of a vacuously true statement as a sort of mathematical joke. For example, if Santa Claus does not have any pigs, it is mathematically true that “All of Santa’s pigs can fly”! Vacuously true statements can also play a role in mathematical fallacies, which are incorrect arguments that may look reasonable until you take a closer look at them.

You might want to review the previous posting on the meaning of "implies". The key to understanding vacuous statements is that if the “antecedent” (left side) of an implication is false, the whole statement is true no matter whether the right side (“consequent”) is reasonable or not. In our little example, it is true that all of Santa’s pigs can fly, even if no pig in the entire world can fly. And I guess all purple cows are math whizzes, too — unless of course there really is a purple cow somewhere.

In the truth table for the implication operator (P ⇒ Q), if you look at the rows where P is false, you will see that the whole implication is true regardless of whether Q is true or not. So any implication with "false" on the left side is true; and we say "false implies anything".

The definition of "⇒" gives just the results we need to do mathematics — just watch out for statements that are vacuously true!

Friday, January 2, 2015

The math problem inside every math problem

A great deal of high school math is about solving problems. Yet for mathematicians throughout history and right up to the present, math is about proofs. Are students doing one kind of math, while mathematicians are doing something quite different? Not really. The kind of math that professional mathematicians do is much more challenging and abstract than a high school math problem, but in its essence the math is the same no matter who does it.

How is this possible? The steps in solving a math problem feel like the steps in a proof, but in some ways the process feels different. What is the theorem to be proved, and where is it? It turns out that theorem and its proof are both hiding just a bit inside the math problem.

Let’s look first at solving equations, perhaps the most classic form of algebra problem. A very simple equation to solve could be something like:

4 ⋅ x + 3 = 15

which has the solution:

x = 3

We could solve it by subtracting 3 from both sides and then dividing both sides by 4. The steps would look something like this:

4 ⋅ x + 3 - 3 = 15 − 3
4 ⋅ x = 12
(4 ⋅ x) / 4 = 12 / 4
x = 3

There is indeed a proof lurking inside the solution to this problem! How can this be? None of the statements in the proof is a theorem. A theorem should always be true, like the commutative law is true for all real numbers. None of these statements is true unless x is equal to 3, though each is true if x is indeed equal to 3.

We could say there are two theorems here. Stated in words, one is that for all real numbers x, if 4 ⋅ x + 3 = 15 then x = 3. Mathematical notation for this is:

4 ⋅ x + 3 = 15 ⇒ x = 3

(You can read the arrow as “implies”.)

When we solve equations, we usually work in this manner, starting with the problem statement and applying rules to get a sequence of statements, each true based on earlier steps.

The problem statement is assumed at each step. So the statements being proved along the way technically are like this:

4 ⋅ x + 3 = 15 ⇒ 4 ⋅ x + 3 - 3 = 15 − 3
4 ⋅ x + 3 = 15 ⇒ 4 ⋅ x = 12
4 ⋅ x + 3 = 15 ⇒ (4 ⋅ x) / 4 = 12 / 4
4 ⋅ x + 3 = 15 ⇒ x = 3

And the final step is the first theorem being proved. Repeating the assumption every time is tedious, so you can see why the assumptions are generally not written at each step in solving a problem!

The other theorem is that for all real numbers x, if x = 3 then 4 ⋅ x + 3 = 15. In mathematical notation this is:

x = 3 ⇒ 4 ⋅ x + 3 = 15

For many problems like this one, we can confirm this theorem just by “plugging in” the value 3 for x in the equation 4 ⋅ x + 3 = 15. In math textbooks this is sometimes called “checking your work”. It can help you avoid mistakes, and in some problems is necessary even if all of your steps are done correctly! We will say more about that in another posting.

Mathematical notation also lets us combine the two statements into a single theorem. In mathematical notation it looks like this:

4 ⋅ x + 3 = 15 ⇔ x = 3

This has an arrow pointing in both directions, and means that 4 ⋅ x + 3 = 15 ⇒ x = 3 and also that x = 3 ⇒ 4 ⋅ x + 3 = 15. That is why the arrow in this one points in both directions. In mathematics, a statement of this kind is called an equivalence.

Solving equations is mathematically the same as finding an equivalence between the given equation (or equations) and the "solution". In the solution, each variable should be shown equal to some expression, and the expression should be reasonably simple — the simpler the better.

There are other kinds of math problems too, including simplification of expressions. More on this later.

Wednesday, December 31, 2014

The meaning of “implies”

Nothing is more essential to mathematical thinking than deduction, the art of working out the consequences — the implications — of precise assumptions.

This posting takes a closer look at the mathematical meaning of “implies” through an example in basic algebra. It assumes that you know just a little bit about propositional logic and its “implication” operator, as explained for example in Logic through Pictures.

Let’s look at the statement that

if x is equal to 1 then x squared is also equal to 1.

In mathematical notation we write this as

x = 1 ⇒ x2 = 1

and this is a true mathematical statement just as you would expect. We typically read the arrow here in English as “implies”, reading the whole statement as “x equals 1 implies x squared equals 1”. We are going to look more closely at the precise mathematical meaning of this implication arrow.

The mathematical meaning of a true statement with variables is that any possible value can be used as the value of each variable, giving a true statement in every case. So in this example the statement should be true for x = 0, x = 1, x = 2, and so on. And if we are talking about the real numbers, it should also be true for ½, the square root of 2, and so on.

For each possible value of x we consider the value of x = 1 and the value of x2 = 1. Each of these will be either true or false. The implication arrow is a function that takes two “truth values” (either T or F) as inputs, and gives a truth value as its result.

Since x = 1 ⇒ x2 = 1 is a true statement, its value must be T (true) for all possible values of x. Let’s take a look at the truth table for the ⇒ operator.

P Q P ⇒ Q
F F T
F T T
T F F
T T T

Its value is T for all inputs except P = T and Q = F. In our true statement we will see that all three of the cases that give a value of T occur for certain values of x.

Suppose the value of x is 1. Then the expression x = 1 is true and the expression x2 = 1 is also true. The value of T ⇒ T is T, and 1 = 1 ⇒ 12 = 1 is true as expected.

Next suppose x is -1. The expression x = 1 is false, but the expression x2 = 1 is true. The value of F ⇒ T is T, so -1 = 1 ⇒ (-1)2 = 1 is also true.

Now suppose x is 0. Then the expression x = 1 is false and the expression x2 = 1 is also false. The truth value of F ⇒ F is T, and 0 = 1 ⇒ 02 = 1 is true, also as expected. The inputs to “⇒” are false for x = 2, x = 3, x = ½, and all other values of x as well.

As long as there is no value of x that causes x = 1 to be true and x2 = 1 to be false, the implication is true. For this statement there are no such cases, and we see in detail how our original statement is true, looking at all possible cases and using the “truth table” for the “⇒“ operator.

What is high school algebra for?

Basic algebra is a core part of virtually all high school level educational programs. There are areas of controversy over teaching of math, but the value of studying basic algebra itself is not one of them. The skills and understanding of high school algebra provide a base for much practical and important mathematics, and advanced areas of math build on basic algebra, including probability, statistics, calculus, real and complex analysis to mention only a few.



Still, algebra is only one face of mathematics. Ever since the ancient Greeks, math has had other important faces as well. Euclidean geometry is recognized to this day as a shining example of systematic mathematical reasoning and taught in standard school programs. With the arrival of the computer and the Internet, new kinds of mathematics have come to have great practical importance, including discrete mathematics and mathematics of computation. And mathematics itself has exploded in many directions, especially over the last century or so.


With the computer have also come questions about the math students learn in school. For example now that we have calculators, how important is it to learn to calculate by hand? Powerful computer algebra software now can solve many kinds of math problems, often beyond the abilities of all but the most capable humans. Textbook problems in basic algebra are among the simplest problems of these kinds.


In spite of all this there is still a consensus in favor of basic algebra in schools. It does not seem to be just conservatism or inertia. Where does this continued belief in high school algebra come from? High school algebra can contribute in a number of areas, including:


  • Problem-solving skills. Math has always been a tool for solving problems, and algebra provides excellent arenas in which to state problems, consider the means available, and systematically solve those problems.
  • Fundamental concepts of mathematics. Among these are variables, constants, terms, functions, domain, range, relations and equations.
  • Interpreting mathematical expressions and statements. This means understanding for example the structure of a term, how it transforms its inputs to its outputs, the graphs of equations, and the conditions when mathematical statements are true or false.
  • Understanding and using properties of numbers and operations. These include ordering of numbers, operations such as commutativity, associativity, and distributivity; symmetry, transitivity, and so on.
  • Describing the world mathematically. Typically this means transforming questions about the world into mathematical statements that can allow the questions to be solved or analyzed.
  • Reasoning mathematically. Proper mathematical reasoning is deductive, and the fundamental rules of deductive reasoning apply to all branches of mathematics, both simple and advanced.

Some of the posts on this blog discuss how basic algebra can illustrate principles of mathematical reasoning often overlooked in textbooks and courses in the subject. These principles can also be readily implemented in interactive computer software such as Mathtoys that can support its users in correct reasoning.