Prooftoys currently has primitive support for working with real numbers using addition, subtraction, multiplication, and division, with axioms and basic rules of inference.

**Axioms.**
The axioms refer only to addition, multiplication, negation
(~~neg~~), and reciprocal (~~recip~~). Subtraction
and division are defined in terms of negation and reciprocal.

In addition there are axioms stating that the result of the basic operations on real numbers give real numbers as a result (except for the reciprocal of zero), though they are not shown here.

The first axiom, commutativity of addition
(`axiomCommutativePlus`

), shown as
~~x + y = y + x~~, means "for all *real numbers*
~~x~~ and ~~y~~, ~~x + y = y + x~~.
Since Prooftoys can work with other kinds of values, the full
statements of the axioms say explicitly that they are only guaranteed
for real numbers. In this case the full statement is:
~~R x & R y => x + y = y + x~~, or with parentheses to clarify
grouping, ~~((R x) & (R y)) => (x + y = y + x)~~.

~~R x~~ means "~~x~~ is a real number".
The conditions about real numbers are not normally shown in the
Prooftoys displays, to help reduce visual clutter. The symbols
~~&~~ and ~~=>~~ represent the mathematical
"and" and "implies" relationships, explained further in the
Logic through Pictures page.

**Doing arithmetic.**
The `axiomArithmetic`

axiom schema evaluates basic
arithmetic expressions with numeric arguments. It works with the
operations ~~+, -, *, /, neg, =, !=, >, >=, <, ≤~~, and the
predicate `R`

when given numeric literals as arguments.
(When dividing, it accepts only inputs that give exact integer
results.)

**Numeric constants.**
Prooftoys supports (integer) real number constants in the usual
syntax, e.g. `(x - 2)`

. Be sure when subtracting a numeric
constant as in the example to leave a space between the
`-`

and the number, otherwise the parser will the
`-`

as part of the number `-2`

and
`x`

as a function applied to `-2`

.

**With the proof builder.**
In the interactive proof builder, find axioms by pressing the
`x`

key on your keyboard without selecting any existing
proof step. They are under the letter `x`

to reduce
clutter in the initial display of available theorems and rules of
inference.

**Subtraction and division.**
The operators `-`

and `/`

are defined, but there
are no rules of inference for them, so it is more convenient to expand
their definitions where they occur. You can expand the definitions by
selecting an expression that uses them, such as ~~(y - 2)~~ or
~~(x / z)~~ and requesting the `apply`

rule.

**Rules of inference.** Based on the axioms are a set of simple
rules of inference for real numbers. You can select an expression in
a proof step and apply one of these to it, associating `+`

or `*`

to the left or to the right, commuting the
arguments, applying the distributive law or using it in reverse to
group common factors (`associatePlusToLeft`

,
`associatePlusToRight`

, `associateTimesToLeft`

,
`associateTimesToRight`

, `distribute`

, and
`group`

).

There are also rules related to 1, 0, negation and reciprocal:
`plusZeroElim`

, `plusZeroIntro`

,
`timesOneElim`

, `timesOneIntro`

,
`plusNegElim`

, `timesRecipElim`

, and
`timesZeroElim`

.

Some of the steps in the example use the Prooftoys "replace" rule. With this rule one or more occurrences of an expression can be replaced by one that is equal to it. If the equation is conditional (has hypotheses), the resulting statement must satisfy all of its conditions, so it may be necessary to add them to any existing hypotheses.

This example solves a pair of simple simultaneous equations using the current Prooftoys axioms and rules of inference.

Notes: In lines with hypotheses, like

the number 1 is an abbreviation for the assumption introduced on line 1, and the number 2 is an abbreviation for the assumption introduced on line 2. So if line 1 assumes~~14. 1, 2: x = 4~~

~~14. (x = y * 2) & (x + y = 6) => x = 4~~

For additional background it may be helpful to read Basic logic through pictures and the Introduction page.