Interface:Tutorial

From Wikiproofs
Jump to: navigation, search
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 (nat)
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:

term (formula (= nat nat))

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 (eqreflexive () () (x = x)) # 1st Peano axiom

stmt (eqsymmetric () ((x = y)) (y = x)) # 2nd Peano axiom

stmt (eqtransitive () ((x = y) (y = z)) (x = z)) # 3rd 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:

term (nat (0)) # 5th Peano axiom

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:

term (nat (succ nat)) # 6th Peano axiom, a
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:

stmt (succinj () (((succ x) = (succ y))) (x = y)) # 8th Peano axiom

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 ((1) (succ (0)))
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:

term (nat (+ nat nat))
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