The logical symbols, i.e. the Boolean operators and quantifiers, have the same meaning as in logic. There are two types of quantifiers though. The bounded quantifiers are just a useful shorthand. \[ \{ ∀ x < c : P \} \] means the same as \[ \{ ∀ x . [ ( x < c ) ⊃ P ] \} \] and similarly for the existential quantifier.
The arithmetic operators \({ + }\) and \({ - }\) mean addition and multiplication, respectively. 0 means 0. The apostrophe is the successor operator, that is the operator which takes a natural number and increments it. The successor operator occurs so often that I’ve broken with my usual practice of allowing only fully parenthesised expressions. This won’t cause any problems because it’s the only exception.
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!
Note that some expressions are of numerical type, which in this case means they should be though of as natural numbers, and some are of Boolean type.
Numerical expressions include const_exps,
variables and num_exps.
const_exps, i.e. constant expressions, are those
constructed without the use of variables. Every
const_exp is a num_exp, but not every
num_exp is a const_exp. The expression \[
( 0''' + \{ [ 0' + ( \{ 0'' + [ (
0''' + \{ [ 0''' + ( 0' ·
0'''' ) ] · 0'''' \} ) ·
0'''' ] \} · 0'''' ) ·
0'''' ) ] · 0'''' \} ) .
\] for \({ 2023 }\) considered
earlier is a const_exp, and therefore also a
num_exp. \({ ( x + y ' )
}\) is a num_exp which is not a
const_exp.
Boolean expressions include comparison,
bndd_exp and bool_exp. Every
comparison is a bndd_exp and every
bndd_exp is a bool_exp but not every
bool_exp is a bndd_exp and not every
bndd_exp is a comparison.
comparisons have to be constructed without the use of
Boolean operators or quantifiers. bndd_exps can use Boolean
operators and quantifiers, but only bounded quantifiers.
The point of bounded expressions is that for any given value of the free variables occurring in them we can, at least in principle, check whether they’re true. Whenever we see a quantifier we only need to check those numbers up to the given bound. With an ordinary quantifier we might need to check all natural numbers, which cannot be done in finite time.
It would have been possible to use decimal or binary representations as part of the language 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.
Note that there Boolean operators, which combine Boolean expressions to give a Boolean expression, and there are arithmetic operators, which combine numerical expressions to give a numerical expression, and there are comparison relations, which combine numerical expressions to give a Boolean expression, but there is no way of combining Boolean expressions to get a numerical expression.