2013
Reading
Colin Howson, [1997] Logic with trees Chapter 9 & 11
Tutorial
Notation
It is common in this setting (which is arithmetic) to use functional terms like s(x), s(1), s(0) to mean the successor of x, 1, and 0, respectively. Equally common is the notation x', 1', and 0' to mean the same thing. The latter is quicker and shorter (though not semi-nmemonic)-- we will use it here.
Formal Arithmetic
Formal Number Theory is the formalization of ordinary elementary arithmetic. It deals with addition (+), multiplication (here, .), it has a constant (0), and the successor function ('). And it uses Identity. The successor function takes 0 to 0' (ie 1), then 0'' is 2. And so on. In many formal systems, 1 is defined as 0' and 2 as 1' (or 0'') and so on. Our system allows in the numerals 0,1,2,3 as constants (but not 4,5,6 etc.-- we need only enough numerals for illustration), then any definitions have to be explicitly introduced. Then the formal theory proves a number of theorems like
x'=x+1.
The end result is that number theory can be done as a first order theory within predicate logic.
Of particular interest, intellectually, is the use of an axiom schema (that of induction).
Axioms or First Principles need to be decidable. That is, there should be a mechanical way of answering yes/no to the question of whether a particular formula is an axiom. Often axiom systems have only a finite number of axioms (say 5 or 6 of them) and these are decidable by virtue of the fact that we only have to look through them to see whether a presented formula is among them (and thus is or is not an axiom). But it is possible for an axiom system to have an infinite number of axioms. Obviously we cannot complete looking through these individually. But if the infinite among them all fit a certain pattern, we can see whether or not a presented formula fits the pattern (and thus is or is not an axiom). So, purely as an illustration, some theory might have an axiom schema (or pattern) to the effect that
any formula with form φ[x] is an axiom, where φ[x] here means any well formed formula with at least one occurrence of the free variable x.
with this example, the formulas F(x),G(x),H(x), etc are all axioms (infinitely many of them). We can decide which formulas are axioms (even, here, with infinitely many axioms).
The induction axiom schema, permitting infinitely many axioms, will be similar to this.
In sum
Formal Number Theory has five proper symbols {=,',+, .,0} and six proper axioms
∀x∀y(x'=y'→x=y),
∀x~(x'=0),
∀x(x+0=x),
∀x∀y(x+y'=(x+y)'),
∀x(x.0=0),
∀x∀y(x.y'=x.y+x)
And the axiom (metalanguage) schema of induction. If φ[n] is any formula in the object language with free variable n then
(φ[0]∧∀n(φ[n]→φ[n'])) → ∀nφ[n]
is an axiom.
What the schema says in English, roughly, is
If (φ[0]∧∀n(φ[n]→φ[n'])) then ∀nφ[n]
which is
If φ[0]and∀n(φ[n]→φ[n'])) then ∀nφ[n]
which is
If you have a formula φ[x], with free variable x, proved for the case of 0 substituted for that x and∀n(φ[n]→φ[n'])) then ∀nφ[n]
which is
If you have a formula φ[x], with free variable x, proved for the case of 0 substituted for that x and you have for all n (φ[n]→φ[n'])) then ∀nφ[n]
which is
If you have a formula φ[x], with free variable x, proved for the case of 0 substituted for that x and you have for all n (if φ[n]then φ[n'])) then ∀nφ[n]
which is
If you have a formula φ[x], with free variable x, proved for the case of 0 substituted for that x and you have for all n (if φ[with n for x]then φ[with n'for x])) then ∀nφ[n]
which is
If you have a formula φ[x], with free variable x, proved for the case of 0 substituted for that x and you have for all n (if φ[with n for x]then φ[with n'for x])) then you can have All n φ[n for x]
[Notation. There is just the mildest of stresses here between explaining induction and running the software. For explanation of Induction it is useful to use 'n' as a variable and to write, for example, ∀n . The reason for this is that we are talking number theory here and 'n' reminds us of that. But, in our running software, 'n' is not a variable so ∀n is not well-formed. We use 'w','x','y', and 'z' as variables (with or without subscripts). So, in the Exercises, for example, you will see the use Induction using one of our real variables.]
Peano Arithmetic
Of great historical and philosophical interest in is so-called Peano Arithmetic. It is just formal number theory as explained above.
Doing Formal Number Theory/ Peano Arithmetic in Trees.
We can do arithmetic with trees. We just write the axioms as starting formulas or 'premises' together with the negation of the desired theorem. The Axiom of Induction Schema will need special treatment. You will need to take the desired instantiation of it as and axiom (we have made that choice for you in the exercises below)
Exercise 1
Hints for reasoning with identities:- Often with these kinds of proofs you can have four or five identity statements and it is easy to start going round in circles. A couple of good ideas are a) don't be rewriting both sides of an equation at once, if you get either the left or the right to equal what you want confine yourself to rewriting the other side, and b) the idea is to 'terminate' with what you want, if you can get any notion of 'weight' or 'complexity' (perhaps in terms of numbers of connectives) of the formulas you are producing, be careful with increasing weight, you may end up increasing weight forever.
1.
∀x∀y(x'=y'→x=y),
∀x~(x'=0),
∀x(x+0=x),
∀x∀y(x+y'=(x+y)'),
∀x(x.0=0),
∀x∀y(x.y'=x.y+x),
∴
∀x(x+0'=x')
You can see this (the conclusion) has nothing to do with multiplication, so it might be a little less cluttered to prove
∀x∀y(x'=y'→x=y),
∀x~(x'=0),
∀x(x+0=x),
∀x∀y(x+y'=(x+y)'),
∴
∀x(x+0'=x')
2.
∀x∀y(x'=y'→x=y),
∀x~(x'=0),
∀x(x+0=x),
∀x∀y(x+y'=(x+y)'),
∀x(x.0=0),
∀x∀y(x.y'=x.y+x),
((0=(0+0))∧∀x((x=(0+x))→(x'=(0+x'))))→∀x(x=(0+x)) (*Induction*)
∴
∀x(x=0+x)
Less cluttered
∀x∀y(x'=y'→x=y),
∀x~(x'=0),
∀x(x+0=x),
∀x∀y(x+y'=(x+y)'),
((0=(0+0))∧∀x((x=(0+x))→(x'=(0+x'))))→∀x(x=(0+x)) (*Induction*)
∴
∀x((x=0+x)
3.
∀x∀y(x'=y'→x=y),
∀x~(x'=0),
∀x(x+0=x),
∀x∀y(x+y'=(x+y)'),
∀x(x.0=0),
∀x∀y(x.y'=x.y+x),
(((x'+0)=(x+0)')∧∀y(((x'+y)=(x+y)')→((x'+y')=(x+y')')))→∀y((x'+y)=(x+y)') (*Induction*)
∴
∀x∀x(x'+y=(x+y)'))
Less cluttered
∀x∀y(x'=y'→x=y),
∀x~(x'=0),
∀x(x+0=x),
∀x∀y(x+y'=(x+y)'),
∀x(x.0=0),
∀x∀y(x.y'=x.y+x),
(((x'+0)=(x+0)')∧∀y(((x'+y)=(x+y)')→((x'+y')=(x+y')')))→∀y((x'+y)=(x+y)') (*Induction*)
∴
∀x∀x(x'+y=(x+y)'))
If you decide to use the web application you can launch it from here Deriver [Howson] — username 'logic' password 'logic'. Then either copy and paste into the Journal or use the Deriver File Menu to Open Web Page with this address https://softoption.us/test/treesStandAlone/howson/CombinedTutorialsHowson.html . Then select the desired formula(s) and Start Tree off the Actions Menu.
Preferences
You will need to set some Preferences for this. Set identity to true (and that will give you the identity rules) set firstOrder to true (to get first order theories); and you can check that the parser is set to Howson.