Page 104 - Textos de Matemática Vol. 40

92 Chapter 3. Truth Theories
This Lemma shows that we cannot have a truth definition for the whole language. In particular, we cannot add full self-reference. That means that we are not allowed to add a term T˙ such that ¬T(x) ↔ T(¬˙ (T˙ x)). But we may introduce a rather trivial version of self-reference just by defining T˙ as the identity function λx.x. With this, we get the following clauses:2
Self-reference.
T(x) ↔ T(T˙ x),
T(¬˙ x) ↔ T(¬˙ (T˙ x)),
Induction. In the context of Frege structures, we can consider at least three natural forms of induction over N.
1. Class induction on N (C-IN)
C(f) ∧ T(f 0) ∧ (∀x : N.T(f x) → T(f (x′))) → ∀x : N.T(f x).
2. Truth induction on N (T-IN)
T(f 0) ∧ (∀x : N.T(f x) → T(f (x′))) → ∀x : N.T(f x).
3. Formulae induction on N (LFt -IN)
φ(0) ∧ (∀x : N.φ(x) → φ(x′)) → ∀x : N.φ(x)
for arbitrary LFt formulae φ.
Our theories FON, FON + (C-IN), FON + (T-IN), and FON + (LFt -IN) are essentially equivalent to the theories MF−, MFc, MFp, and MF, respectively, of Cantini in [Can96].
3.1.2 Abstraction
One of the essential features of Frege structures is the possibility to represent formulae by terms without a G¨odelization of the language.
In a straightforward way, we can associate a term with every formula in FON.
2In Cantini’s theory MF−, these two formulae are added as axioms, while T˙ is an additional abbreviated term, cf. footnote 1.