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.

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

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