Introduction to Prooftoys Proofs

This page introduces you to the language used in the Prooftoys system, viewing and exploring proofs, and using the interactive proof builder.

The language

For more complete information see the language documentation in the project Wiki.

Aside from variables and constants, the language has only function calls and function expressions. The parser and printer support infix operators, which are represented internally as function calls.

Infix operators. Infix operators available in order of increasing precedence are:

Negation ("not"). Negation is represented by not, and acts like any other function. So "x is not red" might be expressed in Prooftoys as not (red x). Like the Prooftoys functions for "and", "or", its input is a true/false value and so is the value of its result.

Function calls. Ordinary function calls look like (f x) or f x. An expression such as sin x / 2 has the same meaning as (sin x) / 2, not sin(x / 2). We say that function calls have higher precedence than infix operators, just as multiplication has higher precedence than addition, so that when some parentheses are omitted in an expression such as x + 2 * y, it has the same meaning as x + (2 * y).

Forall and exists. These quantifiers are entered as forall and exists, and display as the usual mathematical symbols and . In Prooftoys the typical math notation x P(x) is entered as forall {x. P x} or forall {x. (P x)} and displays as forall {x. P x} or forall {x. (P x)}.

Function expressions. These have the form {x. P x}. In an example like this one, assuming P returns a true/false value, the notation can be read like the common notation for sets, "the set of x such that P of x". In fact the P x part can be any expression, and the whole thing can always be read as "the function of x whose value is P x".

The most common use of function expressions is with the quantifiers forall (forall) and exists (exists) as in the examples above, although usually in these cases our attention focuses on the quantifier itself and not on the the function expression.

Inference in Prooftoys

Prooftoys supports the usual forms of classical inference and has a number of common rules predefined (though not yet inference with existential quantifiers).

Its one fundamental rule of inference is the Q0 Rule R that allows replacement of any occurrence of a term by a term that is equal to it. The Prooftoys replace rule is the same as the Q0 derived Rule R', which does the same sort of replacement when the equation is conditional. In other words it allows C to be replaced by D if H => (C = D). It turns out that most equations in basic textbook algebra problems have this form when written out in full, which makes this rule especially useful. See the section Working with Real Numbers.

Viewing and exploring proofs

Examples of many of the currently-implemented rules of inference are available here. Selecting a theorem or inference rule below displays an example of usage of the rule or theorem. Axioms, theorems, and rules of inference often have parameters.

Some often-used practical rules of inference are universal generalization ("add forall"), universal instantiation ("instantiate forall"), and reasoning by cases ("proof by cases"). There is also a tautology checker which can prove arbitrary tautologies.

To see how a rule operates internally, click on its name in the proof line that uses it.

Note: Proof displays are supported in modern browsers such as Chrome, Firefox, Safari, and Internet Explorer 9.

Select a rule or theorem to prove:

Demo screencast

Assumptions. Most math problems start with assumptions, and whethere the assumptions are stated explicitly or not, the assumptions are often required to properly justify many of the steps in a problem solution.

The Prooftoys language has a compact notation for referring to assumptions. For example if an assumption is made in line 1 of a proof, later steps can refer to that assumption using the number 1, something like this:

1. x / 4 = y (assumption)
2. 1: x = 4 * y
3. y = 5 (assumption)
4. 1, 3: x = 20
Here Line 2 refers to the assumption on line 1, and line 4 refers to the assumptions on lines 1 and 3. Line 2 is a shorthand for:
2. x / 4 = y => x = 4 * y
and line 4 similarly is just a shorthand for:
4. (x / 4 = y & y = 5) => x = 20

Using the proof builder

The proof builder lets you interactively build proofs using all of the publicly-available theorems and rules of inference. It can make working with proofs easier, apply rules of inference correctly, show what inference rules do and how they work.

To start, click on the text entry field. It will pop up a menu of all axioms, theorems, and theorem schemas available. You can start typing the name you want or select it from the list. Clicking on the desired item or typing <Enter> when it is selected will choose it.

Once you have chosen the axiom or theorem to use, the system checks whether it takes parameters. If so, you will be offered a small form to fill in. Enter expressions in the language as needed and type <Enter> to submit the form. The system will prove the theorem as needed and display it in the proof. A common first step in solving a math problem is to use the assume theorem schema. Type any expression, and it will be "assumed" for you. The new theorem just says that your assumption implies itself, which is obvious but works well with the rules of inference.

Once there is at least one step in your proof you can choose rules of inference that take existing proof steps as input. To use a rule of inference, select a step that it depends on. If a rule of inference operates on a specific location in a step, you must select the subexpression to operate on. For example rules r and replace require you to select the subexpression you want to replace. Click again on a step to deselect it, to enter an axiom or theorem.

Building a simple proof

Let us consider a very simple example applying forward reasoning with implications ("modus ponens") to a pair of assumptions. Here is a display of the proof you are going to build.

In the Proof Builder area below, you can create the same proof. To enter an assumption click in the text entry field and select the rule assume hypothetically. Type in p, and press <Enter>. You will see the first line of your proof.

Next use the rule assume hypothetically again, typing in p => q as your second assumption.

For the inference step, click on the step number "1" at the very beginning in the first line of the proof display. The whole line will highlight itself (in yellow) and stay highlighted as you move the mouse away. Now use the dropdown list control to select a rule of inference to use. When you select [p] and [p => q] to [q] from the list, a small form will appear with "1" as the hypothesis step. Enter 2 as the number of the implication step to apply the rule to. Press <Enter>. You should see the conclusion q added to the proof.

Note that in this rule [p], [p => q], and [q] are patterns. The rule needs two steps as its inputs, which must match the patterns [p] and [p => q]. p can be any expression, but it must be the same in both of the input steps. The result of the inference will be the expression that matches with q in the second input step. The brackets just indicate the boundaries of each of the patterns.

To make the assumptions explicit, you might wish to select the last line of the proof and choose the assumptions explicit rule, which causes the hypotheses to be displayed explicitly as preconditions. Again, select the entire step by clicking on the step number.

Going beyond what is displayed in the sample, you could choose add forall to add universal quantifiers to the formula. Do this twice to quantify over both p and q.

Proof Builder demo screencast

Proof Builder