We introduced Robinson’s arithmetic . It is a weak (and sound) theory that proves all true
sentences. We also introduced Peano Arithmetic
.
is sound and designed to “capture” all true first-order statements about
. (The incompleteness theorems will show that it does not suceed: There are true statements that
does not prove.)
We showed that represents all c.e. sets and binumerates all recursive sets, in particular all primitive recursive functions.
actually proves that the representations of primitive recursive functions define functions, so in any (maybe non-standard) model of
it makes sense to talk, for example, of the exponential function, or the function enumerating the primes.
We proved the fixed point lemma and deduced from it Tarski’s theorem on the undefinability of truth, thus formally solving the liar’s paradox.