- This is the continuation of Help:Tutorial
Implementation of some of the Peano axioms
First, we must teach JHilbert that stuff like "naturals" and "formulas" exist:
var (nat x y z)
kind commands tell JHilbert that we will use terms whose values are natural numbers (abbreviated to "nat") or formulas. Wait a minute, didn't I tell you before that formulas aren't terms? The answer is that JHilbert's metamathematical meaning of "term" is more general than terms in Peano arithmetic. In JHilbert, all expressions are terms, and their meaning can be distinguished by their kind.
var command defines three variables,
z. They are placeholders for any JHilbert terms of kind "nat".
Next, we want to teach JHilbert the first four Peano axioms, that is, the axioms involving equality. So, we first need to define the equality symbol:
term command here defines the new symbol "=". This new symbol can now be used to create expressions from two natural numbers, such as
(= x y). Hmm, shouldn't that be
(x = y)? In fact, both are possible. JHilbert makes no assumption where orders of symbols, like operators and relation symbols, are a matter of convention, depending on the symbol itself. The "natural" order for JHilbert is Polish notation, but you can place the term symbol (here the equal sign) later if you don't have a variable with the same name as otherwise the term symbol will "shadow" the variable. If you don't use Polish notation, JHilbert will reorder the expression internally. The
formula identifier of the
term command tells JHilbert that expressions with
= are of kind "formula". Now we can state the equality axioms:
stmt (eqsymmetric () ((x = y)) (y = x)) # 2nd Peano axiom
These are the first three Peano axioms, which we have given the names
eqtransitive respectively. The empty bracket after their names are for disjoint variable constraints, which are beyond the scope of this tutorial. Then, there follow the hypotheses required to invoke the statements later in proofs. The first Peano axioms does not have any hypotheses (empty bracket), the second has one hypothesis, and the third Peano axiom has two hypotheses. Finally, the
stmt commands are concluded with the consequents of the statement. Remember that the variables, such as
x, are just placeholders for any natural numbers. So
eqreflexive yields, not only
(x = x) but also
(y = y) and (once we have defined addition)
((x + x) = (x + x)). It does not yield
(y = z) as the same variables must be replaced with the same expressions (proper substitution). It does not yield
((y = z) = (y = z)) either, because, while we have the same expression,
(y = z) twice, it is not of the right kind ("formula" vs. "nat").
And what about the fourth axiom? Well, in the small universe we have been teaching JHilbert, there are only equations between natural numbers. So we do not need to specifically state the fourth axiom. One could also say that the fourth axiom is implied by the definition of
Next, we define our very first natural number, zero:
Neat, huh? Compare this with the definition of
=. Just like
0 is a JHilbert term symbol, but this one doesn't take any expressions to make a
nat, it just is a
nat. We call such terms constants.
Next, we define the successor function:
stmt (succfunc () ((x = y)) ((succ x) = (succ y))) # 6th Peano axiom, b
To encode the sixth axiom, we needed two commands. One
term to introduce the successor function, and one
stmt to establish that
succ is actually a function (i.e., application of
to the same values always yields the same results).
The seventh Peano axiom says that zero is not the successor of any natural number. As we have no concept for "not" handy right now, we just ignore the seventh axiom, to keep matters simple for this tutorial. The axiom is not needed to prove .
The eighth axiom is just the reverse of the
The ninth axiom would require some kind of set theory, so we ignore this axiom as well.
Now that we have zero, we can define some more natural numbers as well:
def ((2) (succ (1)))
def ((3) (succ (2)))
def ((4) (succ (3)))
We have now defined the natural numbers from
, each as the successor of the respective previous number. The
def command creates a term (the kind of which is inferred from the definiens) which can be transparently replaced. So,
(4) will, if necessary, be transparently replaced with
(succ (succ (succ (succ 0)))) by JHilbert. This is a very convenient feature if one wants to create abbreviations for unwieldy expressions. Definitions can also be made to depend on variables, creating a whole family of abbreviations.
Finally, we define addition:
stmt (addsym () () ((x + y) = (y + x)))
stmt (addzero () () (x = (x + (0))))
stmt (addsucc () () ((succ (x + y)) = (x + (succ y))))
addsucc recursively define addition for a fixed first summand. To do so likewise for a fixed second summand, we simply introduce the commutative law of addition as
This completes our partial implementation of the Peano axioms.
- The proof of can be found in the main namespace: Tutorial
Interface module parsed successfully