Page 103 - Textos de Matemática Vol. 40

3.1. Truth theories in the total setting 91
For readability reasons we use in the following freely an infix notation for terms containing the dotted constants. So x =˙ y, for instance, has to be written formally as =˙ x y.
The axioms of FON (Frege structures over TON) are the axioms of TON extended to the new language plus the following axioms:
I. Closure under prime formulae of TON.
(1) x = y ↔ T(x =˙ y),
(2) ¬x = y ↔ T(¬˙ (x =˙ y)), (3) N(x) ↔ T(N˙ x),
(4) ¬N(x) ↔ T(¬˙ (N˙ x)).
II. Closure under composed formulae.
(5) T(x) ↔ T(¬˙ (¬˙ x)),
(6) T(x)∧T(y)↔T(x∧˙y),
(7) T(¬˙ x)∨T(¬˙ y)↔T(¬˙ (x∧˙ y)), (8) (∀x.T(f x)) ↔ T(∀˙ f),
(9) (∃x.T(¬˙ (f x))) ↔ T(¬˙ (∀˙ f)).
III. Consistency.
(10) ¬(T(x) ∧ T(¬˙ x)).
The axioms I. – II. express that T is closed under formula construction by =, N, T, ∧, ∀, and negation where T may be used only positively.
We will use the following abbreviations:
F(t) :⇔ P(t) :⇔ C(t) :⇔
T(¬˙ t), T(t) ∨ F(t), ∀x.P(t x).
T(t) may be read as “t is true”, F(t) as “t is false”, P(t) as “t is a proposition”, and C(t) as “t is a class”. In the literature, C(t) is often characterized as a propositional function.
By use of the Recursion Theorem 1.2.2, we can diagonalize ¬˙ and obtain the existence of objects which are not propositions.
Lemma 3.1.1. FON ⊢ ¬∀x.P(x).
Proof. Set l := rec (λx.¬˙ x), i.e., l = ¬˙ l. So l may be seen as a formalization of the liar sentence. Now, T(l) is equivalent to T(¬˙ l). Thus P(l) would contradict the axiom of consistency. ⊣