This is a small tutorial on how to use the JHilbert, the automated proof verifier driving this wiki. We shall 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 to the implementation of some of the Peano axioms.
Why this tutorial?
While JHilbert is a 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.
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. Wikiproofs is such an installation.
So, why choose the statement "" 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 . 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 can get, check out Norman Megill's metamath proof of . 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 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 anyway?
At the beginning of each formalisation is the question what the stuff we're talking about actually means. Per se, is just a string of symbols. We recognise four different symbols in this string: , , and .
The first two symbols, and , are instances of natural numbers, that is, the numbers . (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 and should mean. We could just as well have stipulated that and 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 and .
The next symbol, , the symbol for addition, is able to take two natural numbers to make a new one. We might say, is a function which enables us to create the term 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 precisely clear. Note that is by no means a simplest possible term, as and already constitute primitive terms.
The last symbol, , 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, 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 ?" is not a sensible question to ask, "Is it true that ?" is.
So, let's sum up what we need:
- A formalisation of the natural numbers, and of formulas involving natural numbers (equality is enough for our purposes).
- A precise description of the natural numbers and .
- 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 :
- If , then .
- If and , then .
- If for some , then is a natural number.
- is a natural number.
- There is a function (the successor function) such that is a natural number.
- The function is injective.
- If is a set such that and for all we have , then all natural numbers are contained in .
Addition can then be defined for all natural numbers using the induction principle to which the ninth axiom gives rise: and , and likewise for the left summand. The number is simply the successor of the successor of , and 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 .
- This tutorial continues in the Interface namespace: Interface:Tutorial