Working with real numbers

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.

Worked example

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

Notes: In lines with hypotheses, like

14. 1, 2: x = 4
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 x = y * 2 and line 2 assumes x + y = 6, the whole line amounts to:
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.