Our language for this is given by the grammar
statement : bool_exp ;
bool_exp : ( ¬ bool_exp) | ( bool_exp b_operator bool_exp )
| ( quantifier variable . bool_exp )
| ( num_exp relation num_exp ) ;
| [ ¬ bool_exp) | [ bool_exp b_operator bool_exp )
| [ quantifier variable . bool_exp )
| [ num_exp relation num_exp ) ;
| { ¬ bool_exp} | { bool_exp b_operator bool_exp }
| { quantifier variable . bool_exp }
| { num_exp relation num_exp } ;
b_operator : ∧ | ∨ | ⊃ ;
quantifier : ∀ | ∃ ;
variable : letter | variable ! ;
variable : v | w | x | y | z ;
relation : = | ≤ ;
num_exp : 0 | variable | num_exp ' | ( num_exp a_operator num_exp ) ;
a_operator : + | · ;There are now two types of expressions, boolean and numerical. The numerical ones are meant to have natural numbers as values. The ’ takes a numerical expression and increments it. We sometimes refer to \({ x ' }\) as the successor of \({ x }\).
This language doesn’t allow the usual decimal notation for natural numbers so the way to represent the natural numbers we’d normally call 0, 1, 2, 3, … is as 0, 0’, 0’‘, 0’’‘, etc. We can also add and multiply numerical expressions, which gives us a few more options. So we don’t have to represent 2023 as a 0 followed by 2023 apostrophes, for example. We could also write it as \[ ( 0''' + \{ [ 0' + ( \{ 0'' + [ ( 0''' + \{ [ 0''' + ( 0' · 0'''' ) ] · 0'''' \} ) · 0'''' ] \} · 0'''' ) · 0'''' ) ] · 0'''' \} ) . \] If you’re wondering where this came from it’s just the base 4 representation \[ ( 3 + \{ [ 1 + ( \{ 2 + [ ( 3 + \{ [ 3 + ( 1 · 4 ) ] · 4 \} ) · 4 ] \} · 4 ) ] · 4 \} ) \] with 1, 2, 3 and 4 replaced by 0’, 0’‘, 0’’‘, and 0’’’‘. There’s nothing special about 4. We could have used decimal instead but it’s hard to look at 0’’’’’’’’’’ and see what number it is. We could also have used binary but then the expression would be quite long, though not nearly as long as a 0 followed by 2023 apostrophes!
It would have been possible to use decimal or binary representations directly but then we’d have build much of elementary arithmetic into the axioms and rules of inference. This can be done, as we saw when we considered languages expressing divisibility properties. In addition to requiring a very complicated set of rules of inference that approach would miss the point. We want to build a formal system in which to prove statements in elementary arithmetic. If we need to assume large parts of elementary arithmetic to show that our rules of inference are sound then what’s the point? It’s better to assume as little prior knowledge of arithmetic as we can get away with.
New to this module, but presumably familiar, are the binary relations \({ = }\) and \({ ≤ }\). They take a pair of numerical expressions and give a Boolean expression. This is unlike the Boolean operators, which combine Boolean expressions to give a Boolean expression or the arithmetic operators \({ + }\) and \({ · }\) which combine numerical expressions into numerical ones.
Other than this our language for arithmetic is borrowed from first order logic, but the role of predicates is now played by Boolean expressions and the role of parameters is played by numerical expressions.
If you’re wondering why the subtraction and division operators are missing, that’s a consequence of using first order logic. First order logic, as mentioned earlier, does not cope well with names for non-existent objects. We would quickly encounter problems if we allowed expressions like \({ 0 - 0' }\) or \({ 0' / 0 }\) into our language. Of course \({ 0 - 0' }\) exists, but not as a natural number.
There is some redundancy in this language. We would suffer no loss of expressiveness if we removed the \({ ≤ }\) relation, for example. The statement \[ ( x ≤ z ) , \] for example, has the same meaning as \[ \{ ∃ y . [ ( x + y ) = z ] \} , \] since \({ x ≤ z }\) if and only if there is a natural number \({ y }\) such that \({ x + y = z }\).