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. This page tries to give quick opportunities to play around with proofs and even the proof builder.

For more systematic reading about the system and its logic, try some of the pages in the Prooftoys Wiki.

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 Microsoft Edge. Internet Explorer is not being updated to current Web technologies and is no longer supported by Prooftoys.

Select a rule or theorem to prove:

Demo screencast

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.

Proof Builder