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

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:

`==`

(equivalence, displays as "~~==~~")`=>`

(implication, displays as "~~=>~~")`|`

(or)`&`

(and)`= != < <= > >=`

(equality and relational operators)

These display as~~= != < ≤ > ≥~~respectively.`+ -`

`* /`

**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.

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 Q_{0} 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 Q_{0} 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.

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:**

**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.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:~~x / 4 = y~~(assumption)

2.~~1: x = 4 * y~~

3.~~y = 5~~(assumption)

4.~~1, 3: x = 20~~

2.and line 4 similarly is just a shorthand for:~~x / 4 = y => x = 4 * y~~

4.~~(x / 4 = y & y = 5) => x = 20~~

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.

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**