Prooftoys technical notes
Table of contents
Substitution for variables is one of the fundamental operations in virtually all forms of mathematical proofs and mathematical problem solving. How can we understand that substitution is a valid step in a proof?
If a mathematical statement has a variable in it, we say the statement is true if it is true for all possible values of the variable; otherwise we say it is not true. If the variable is a boolean variable, we say the statement is true if it is true regardless of whether the variable is true or false.
So if a variable appears more than once in a true statement, we know the statement will be true as long as each occurrence is assigned the same value. Since an expression with the same inputs always gives the same result, substituting an expression for every occurrence of a variable in a true statement gives another true statement.
In a true statement, if we systematically replace every occurrence of a variable with an expression (the same expression everywhere), the result of this substitution is another true statement, because the expression has the same value everywhere it appears.
The simple tautology
a ⇒ a is a true statement,
true ⇒ true and
false ⇒ false. A statement like
(shining sun) ⇒ (shining sun) is also
true whether the sun is actually shining or not. The substituted
expression itself can have variables, as in
x < y ⇒ x < y. No matter what values
y have, the value
x < y is going to be the same in both spots, so the whole statement
is still true.
The result of substituting an expression for all instances of a variable in a statement is called an instance of the original statement, so we say that substituting one or more expressions for variables in a tautology gives an instance of the tautology.
If a mathematical statement contains bound variables substitution has to be done a bit more carefully, but the idea remains the same.
First, if the a variable
v in the statement appears as a bound
variable, in a part that looks like
v is left alone
and not changed in that part of the statement.
Second, if the replacement term contains any free variables, those variables must remain free after the substitution. This is always achievable, and Prooftoys ensures it by automatically renaming bound variables in the original statement as needed.
Facts about real numbers are conditional. For example the commutative
law of addition for real numbers is
R x & R y => x + y = y + x,
which only asserts the equality for real numbers. Most steps in
proofs about the real numbers are also conditional. So when we apply
a fact about real numbers to a step in a proof about real numbers by
replacement or rewriting, often both of the inputs to the rewriting
After any substitution, the inputs to replacement have the form:
a_1 => (t_1 = t_2) and
a_2 => c. After replacing an occurrence
c, the result looks like
a_1 => (a_2 => c_1), where
c_1 is the result of the replacement in
Replacement and rewriting steps in Prooftoys use the tautology
(b ⇒ c)) ≡ (a ∧ b ⇒ c) to collect the assumptions together.
Also, most inference steps check if the result is conditional
b) and remove duplicated assumptions and any occurrences of
simplify the result.
Managing type assumptions
When the result of rewriting has assumptions such as
R (x + y), that
the result of some arithmetic operations is real, it uses known
arithmetic facts to break it down into assumptions that the values of
each variable is real. The example breaks down to
R x & R y. It
also can prove that numeric literals are real numbers, so
R (x + 3)
breaks down into just
About the Prooftoys logic
The core of Mathtoys is a Web-based, visual proof assistant based on Alonzo Church’s simple type theory as developed by Peter Andrews under the name Q0. Simple type theory is suitable for construction of most of mathematics, comparable in this respect to first-order logic plus set theory. It uses a minimum of simple, understandable concepts, expressing them with a handful of axioms and inference rules.
Prooftoys uses a slightly different axiomatization than Q0, and will transition to definitions of boolean operators that directly expose their truth tables. But the theorems and inference remain the same as in Q0.
The well-established HOL family of theorem provers are also based on simple type theory, though there are significant differences as well, including major differences in the style of proofs they are designed to support.
Project task tracking is in Pivotal Tracker, though currently much out of date.