We discuss Robinson's model theoretic proof of Tarski's theorem on undefinability of truth. We present two other “diagonal-free” proofs of Tarski's theorem, and we compare undefinability of truth to other forms of undefinability in nonstandard models of arithmetic.

We give new proofs of both incompleteness theorems. We do not use the diagonalization lemma, but work with some quickly growing functions instead.

For a primitive recursive consistent and strong enough theory T we construct an independent statement which has some clear metamathematical meaning.

We transform the proof of the second incompleteness theorem given in [3] to a proof-theoretic version, avoiding the use of the arithmetized completeness theorem. We give also new proofs of old results: The Arithmetical Hierarchy Theorem and Tarski's Theorem on undefinability of truth; the proofs in which the construction of a sentence by means of diagonalization lemma is not needed.

We shall prove the second incompleteness theorem via Kolmogorov complexity.

We give a proof of Gödel's first incompleteness theorem based on Berry's paradox, and from it we also derive the second incompleteness theorem model-theoretically.

We prove that any 1-closed (see def 1.1) model of the Π 2 consequences of PA satisfies ¬Cons PA which gives a proof of the second Godel incompleteness theorem without the use of the Godel diagonal lemma. We prove a few other theorems by the same method.