There is some redundancy in this language. As already mentioned, the bounded quantifier expressions are just shorthand for longer expressions involving ordinary quantifiers.
Also 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 }\). Alternatively, we could remove \({ = }\) and write \[ ( x = z ) \] as \[ [ ( x ≤ z ) ∧ ( z ≤ x ) ] . \] In fact it’s possible to express any four of our relations in terms of the remaining one.
We also have more non-terminal symbols in our grammar than are strictly necessary to specify this language. We don’t really need to consider constant expressions separately from other numerical expressions, for example, or bounded expressions separately from other Boolean expressions. In fact you can safely ignore those distinctions for most of this chapter, but it will sometimes be useful to have them available.
One thing conspicuously missing from our language is any notation for sets of natural numbers. We can still talk about at least some sets, by specifying conditions for membership, but we can’t name sets, we can’t assert the existence of a set with given properties and we can’t assert that all sets have a given property. This is the “elementary” in “elementary arithmetic”.
The grammar above is ambiguous, but not very ambiguous. For example
\({ ( 0'' + 0'' ) }\),
i.e. \({ 2 + 2 }\), is a
num_exp. We can see this either by using the fact that it’s
a const_exp and every const_exp is a
num_exp, or by using the fact that 0'' is a
num_exp and that joining two num_exps with a
+ gives a num_exp. Strictly speaking these are
different parsings of the expression but they have the same meaning and
there won’t be any cases where it matters which parsing we choose. It is
possible to disambiguate the grammar, but it doesn’t really seem
worthwhile.
A more minimalist version of the language, while it would make proving theorems in our formal system more painful, would be useful if were going to prove a number of theorems about it, but I’m rarely going to do that, although I will state a number of them and give a rough idea of the proof of some.