This is a small tutorial on the JHilbert extension in which we prove the statement "two plus two equals four" from a small set of simple axioms.

If you're really, really impatient, you can skip all the preliminary blah blah and jump right forward to the #Implementation of some of the Peano axioms.

Why this tutorial?

While JHilbert is a relatively simple piece of software compared with other formal logic suites such as Coq or Isabelle, it is also more complex than most other MediaWiki extensions, so a tutorial to provide a gentle introduction for newcomers seems in order. Besides, most people prefer learning by example (at least initially) to just ingesting the specs.

Prerequisites

In order to reproduce the effects of the JHilbert code in this tutorial, you'll need a MediaWiki installation with the JHilbert extension properly installed and a JHilbert server running on your MediaWiki host. See Extension:JHilbert#Installation for details.

Understandably, the mediawiki.org site does not have the JHilbert extension installed. Therefore, all JHilbert code on this page will be placed between <pre>…</pre> tags instead of between the <jh>…</jh> tags provided by the JHilbert extension.

Unfortunately, the author does not know of any public MediaWiki installation with activated JHilbert extension. Until such time as a JHilbert enabled site goes live, you'll have to use a private MediaWiki installation.

Why ${\displaystyle 2+2=4}$?

So, why choose the statement "${\displaystyle 2+2=4}$" for a tutorial? For one, because it's simple! At least it seems so at first glance. Almost all, say, eight-year old children with access to formal education know that ${\displaystyle 2+2=4}$. On the other hand, it is not natural knowledge. Children have to be taught addition of small integers. It usually doesn't come to them naturally. In this sense, 2+2=4 is a true cultural achievement.

To illustrate how complicated even a trivial statement like ${\displaystyle 2+2=4}$ can get, check out Norman Megill's metamath proof of ${\displaystyle 2+2=4}$. His proof database is founded on very general axioms. The advantage of this is that you can formalise virtually all the fancy stuff mathematicians are working with, such as vector spaces and complex numbers. With all the other proofs here to help, the metamath proof of a simple statement like ${\displaystyle 2+2=4}$ is reasonably short (ten metamath steps). But if you were to unravel the proof back to the initial axioms, you'd have to untangle 2452 subtheorems totalling 25933 steps. An awe-inspiring demonstration of the human power of abstraction.

For this tutorial, we will, of course, keep things much, much simpler.

What is ${\displaystyle 2+2=4}$ anyway?

At the beginning of each formalisation is the question what the stuff we're talking about actually means. Per se, ${\displaystyle 2+2=4}$ is just a string of symbols. We recognise four different symbols in this string: ${\displaystyle 2}$, ${\displaystyle 4}$, ${\displaystyle +}$ and ${\displaystyle =}$.

The first two symbols, ${\displaystyle 2}$ and ${\displaystyle 4}$, are instances of natural numbers, that is, the numbers ${\displaystyle 0,1,2,3,4,5,\ldots }$. (In school, you may have learned that zero does not belong in the natural numbers. While the inclusion of zero implies certain slight variations in the handling of certain definitions, this is effectively just convention. For this tutorial, the natural numbers will contain zero.) Note that this is just one of the simpler explanations for what ${\displaystyle 2}$ and ${\displaystyle 4}$ should mean. We could just as well have stipulated that ${\displaystyle 2}$ and ${\displaystyle 4}$ should be complex numbers (which would clearly go beyond the scope of a tutorial). As there are many natural numbers, we need some way to express which ones are ${\displaystyle 2}$ and ${\displaystyle 4}$.

The next symbol, ${\displaystyle +}$, the symbol for addition, is able to take two natural numbers to make a new one. We might say, ${\displaystyle +}$ is a function which enables us to create the term ${\displaystyle 2+2}$ whose value is a natural number. Of course, many such functions exist: multiplication, exponentiation, and so on. So we'll have to make the meaning of ${\displaystyle +}$ precisely clear. Note that ${\displaystyle 2+2}$ is by no means a simplest possible term, as ${\displaystyle 2}$ and ${\displaystyle 4}$ already constitute primitive terms.

The last symbol, ${\displaystyle =}$, the symbol for equality, is also able to take two natural numbers, or, more general, two terms whose values are natural numbers to make something new. However, ${\displaystyle 2+2=4}$ is not a term in the sense of arithmetic. Rather, it is a formula: something for which the question "Is it true that …?" makes sense. So, while "Is it true that ${\displaystyle 2+2}$?" is not a sensible question to ask, "Is it true that ${\displaystyle 2+2=4}$?" is.

So, let's sum up what we need:

1. A formalisation of the natural numbers, and of formulas involving natural numbers (equality is enough for our purposes).
2. A precise description of the natural numbers ${\displaystyle 2}$ and ${\displaystyle 4}$.
3. A precise definition of the addition operation.

Sounds difficult to formalise? It is! Fortunately, we do not need to rack our brains as someone else has already done it for us.

The Peano axioms

Some material in this section was taken from the article Peano axioms from Wikipedia, the free encyclopedia.

In 1889, Italian mathematician Guiseppe Peano found the following nine formal statements to describe the natural numbers and equality. For all natural numbers ${\displaystyle x,y,z}$:

1. ${\displaystyle x=x}$.
2. If ${\displaystyle x=y}$, then ${\displaystyle y=x}$.
3. If ${\displaystyle x=y}$ and ${\displaystyle y=z}$, then ${\displaystyle x=z}$.
4. If ${\displaystyle x=a}$ for some ${\displaystyle a}$, then ${\displaystyle a}$ is a natural number.
5. ${\displaystyle 0}$ is a natural number.
6. There is a function ${\displaystyle \mathrm {succ} }$ (the successor function) such that ${\displaystyle \mathrm {succ} (x)}$ is a natural number.
7. ${\displaystyle \mathrm {succ} (x)\neq 0}$.
8. The function ${\displaystyle \mathrm {succ} }$ is injective.
9. If ${\displaystyle A}$ is a set such that ${\displaystyle 0\in A}$ and for all ${\displaystyle a\in A}$ we have ${\displaystyle \mathrm {succ} (a)\in A}$, then all natural numbers are contained in ${\displaystyle A}$.

Addition can then be defined for all natural numbers using the induction principle to which the ninth axiom gives rise: ${\displaystyle x+0=x}$ and ${\displaystyle \mathrm {succ} (x+y)=x+\mathrm {succ} (y)}$, and likewise for the left summand. The number ${\displaystyle 2}$ is simply the successor of the successor of ${\displaystyle 0}$, and ${\displaystyle 4}$ is defined likewise.

We are going to teach JHilbert (some of) the Peano axioms in the next section. As you can see, we also need concepts like "If … then", "and", "not" and even set theory to implement these axioms. However, to keep things simple, we will not define these concepts but rather emulate them with JHilbert intrinsics where possible, and drop the axioms for which this is not easily possible. The remaining axioms will be enough to prove that ${\displaystyle 2+2=4}$.

Implementation of some of the Peano axioms

Start a new page on your JHilbert enabled wiki in the Interface namespace, say Interface:Peano axioms. We shall teach JHilbert some of these axioms now.

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 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 ${\displaystyle \mathrm {succ} }$ 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 ${\displaystyle 2+2=4}$.

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 ${\displaystyle 1}$ to ${\displaystyle 4}$, 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. Hit the "Preview" button and see if everything checks out. You should see the notice "Interface module parsed successfully" at the bottom of the page. Note that you'll get an error message if you mistyped something. If everything is all right, save the page.

The proof of ${\displaystyle 2+2=4}$

Ready to prove ${\displaystyle 2+2=4}$, the statement you ever since your childhood wondered whether it was really, really true, from our Peano axioms? Well, then, create a new page in the main namespace (without a prefix), such as 2+2=4. First, we need to load all that stuff we did in Interface:Peano axioms:

import (NAT Interface:Peano_axioms () ())

Be sure to replace all spaces in the original interface name with underscores, otherwise the JHilbert server will think "axioms" is a parser token separate from "Interface:Peano". The other parameters (NAT and the two empty brackets) are of no importance here. They can be used in multiple import proof modules, or multiple param interface modules, to create funky weird-o-magicks like parameterised interfaces and theory adapters, which all, you guessed it, are beyond the scope of this little tutorial. So:

Let's go straight to the proof then:

thm (2+2=4 () () (((2) + (2)) = (4)) (

As you can see, the thm command looks just like a stmt command, except that it doesn't stop after the consequent. That single open bracket is crying for a proof. Proofs are maintained using a proof stack of expressions. The proof stack starts out empty, so let's push something onto it:

        (2) addzero

So, first we push the expression (2) on the stack. The next item in the list is not an expression but the name of a statement, namely addzero. The consequent of addzero is (x = (x + (0)) and there are no hypotheses in this statement. As we have mentioned before, each variable can actually take any expression of the correct kind. To know which expression is the desired one, addzero looks on the stack, finds the (2), pops it from the stack and substitutes it for x. So now, we have ((2) = ((2) + (0)) on the stack. Great! We have proven that ${\displaystyle 2=2+0}$. To reach ${\displaystyle 4=2+2}$, we bump up that equation with the successor function:

        succfunc

The succfunc statement requires one hypothesis, (x = y). So it pops one element from the stack and finds: ((2) = ((2) + (0)). That's a perfect match if we substitute (2) for x and ((2) + (0)) for y. This process is called unification. Note that succfunc does not look on the stack any further despite depending on two variables because these two variables have already been determined by the unification. So now we have on the stack: ((succ (2)) = (succ ((2) + (0)))). Note that (succ (2)) is just (3). So we need succfunc just once more to reach (4). First, however, we must use addsucc to move the annoying successor function deeper into the brackets:

        (2) (0) addsucc
        eqtransitive

The first line pushes the expression ((succ ((2) + (0))) = ((2) + (succ (0)))) on the stack. So we have now two expressions on the stack:

1. ((3) = (succ ((2) + (0))))
2. ((succ ((2) + (0))) = ((2) + (succ (0))))

This means we have proved these two expressions, and they look like they could be combined to the single expression ((3) = ((2) + (1))) (with (succ (0)) already simplified to (1)). That's just what eqtransitive does: it needs two expressions, the two on the stack match, so they are popped. Unification determines all variables, so we get the combined expression on the stack. All we've got to do now is doing the same thing once more to go from (3) to (4):

        succfunc
        (2) (1) addsucc
        eqtransitive

This time, we have of course to instantiate addsuc with (1) for y, as otherwise eqtransitive would not be able to properly unify the stack contents with its hypotheses. Now we're practically done, for we have ((4) = ((2) + (2))) on the stack. At the end of the proof, the stack must contain exactly one element which matches the consequent of the theorem. We do have only one element, but the consequent is (((2) + (2)) = (4)). So all that is left to do is to flip the equation:

       eqsymmetric # 2 + 2 = 4
))

That's it. You can now preview and save (do not forget the closing parentheses).