Before learning about more handy rules of inference, let’s clarify a bit the notation in the next sections.
Capital letters A, B, and C here are not variables in the logic. They are pattern variables to be replaced with arbitrary boolean terms (with true/false values). Letters F and G represent terms whose values are functions. Capital letters X and Y are also pattern variables, for arbitrary terms of any type.
Rewriting and replacement are core parts of inference in Prooftoys, and have their own page.
From: Proof step with one or more free variables. To: Proof step with a term substituted for each variable.
From: forall {x. A}.
To: A with a term of your choice substituted for x.
From: {x. A} X.
To: A, with term X substituted for x throughout
This can be done anywhere in any formula.
In the simple cases, all forms of substitution above work in the way you might expect from examples in any high school math textbook. There is a restriction in cases where the term undergoing substitution contains “bound” variables of its own.
For details on this see link TBD.
X = X
The value of any expression is equal to itself.
From: forall {x. B}
To: B
(Result of instantiating with x.)
From: B
To: forall {x. B}
From: X = Y
To: {x. X} = {x. Y}
(Consequence of {x. X} = {x. X}, then replacing the second X with
Y.)
From: g = {x. X}
To: g x = X
This is useful for converting a definition from the basic form to the
usual form seen in first-order logics. For a function g of more
than one variable, this rule can apply multiple times.
From: g x = X
To: g = {x. X}
This is useful for converting a definition from the basic form to the usual form seen in first-order logics. Like unbinding, this rule can be applied multiple times for functions of multiple arguments.
If a conditional fact has an assumption with a variable that only appears (free) in that assumption and nowhere else in the statement of the fact, in almost all cases, that assumption can safely be removed. We can suggest the working of the inference like this:
From: a_1 and a_2 and … ⇒ C
To: a_2 and … ⇒ C
The one limitation is that there must be some value for the variable that can make the irrelevant assumption true. So to use this rule in a proof, there must be a proof that such a value exists. Prooftoys doesn’t yet support this rule in its general form, but it supports a couple of common cases. These are useful cases, and Prooftoys can work out the existence fact on its own. The cases are:
<var> = <term>; and R <var>
In both cases, the variable var does not appear in the
fact outside this one assumption.
For every assumption of these kinds, the existence of a value satisfying it is provable, so we can remove the assumption from the proof step.
A couple of often-useful inference rules in Prooftoys combine a couple of steps together and rewrite the result. These may take two steps and “conjoin” them using the boolean “and” operation. Then they rewrite a tautology to make it match the conjunction and infer a conclusion.
Proof steps that use these rules tend to have the word “consequence” in their description.
[[More to be written here.]]