# Interface:Tutorial

*This is the continuation of Help:Tutorial*

## Implementation of some of the Peano axioms[edit]

First, we must teach JHilbert that stuff like "naturals" and "formulas" exist:

kind (formula)

var (nat x y z)

The two `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.

Finally, the `var`

command defines three variables, `x`

, `y`

, and `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:

The `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 `eqreflexive`

, `eqsymmetric`

and `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 `succfunc`

statement:

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 to
, 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))))

The statements `addzero`

and `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 `addsym`

.

This completes our partial implementation of the Peano axioms.

*The proof of can be found in the main namespace: Tutorial*

Interface module parsed successfully