Define the canonical term for a natural number by and for , .
Show that for with we have . Be careful to state any induction hypothesis carefully.
An atomic formula is one of the form or , where are terms. A negated atomic formula is one of the form where is atomic.
Given that or for every atomic sentence , show that proves all true sentences.
We write for the -formula . It is not true that , but where is the statement . and is the statement . The injective property of the pairing function is, however, provable in .
and . Prove these!
Prove in that .
(Hint: Given , a model of the theory above, first show that there is such that ; then find such that .)
A formula of is existential if it is of the form where is quantifier-free.
Prove that every existential formula of is provably equivalent in to one of the form
where are terms in the language . (Use an induction on the different ways of building a quantifier-free formula from atomic and negated atomic ones.)