Page 108 - Textos de Matemática Vol. 40

96 Chapter 3. Truth Theories
Let a model M of TON be given. We assume that M is the universe of M containing distinct elements =˙ , ¬˙ , ∧˙ , N˙ and ∀˙ . Moreover, we will identify the terms of LFt with their interpretation in M. Let N be the interpretation of N.
Now we can define a P-positive operator form Γ(P,x) which consists of the disjunction of the following clauses:
1. ∃y, z.x = (y =˙ z) ∧ y = z,
2. ∃y, z.x = ¬˙ (y =˙ z) ∧ y ̸= z,
3. ∃y.x=N˙y∧N(y),
4. ∃y.x=¬˙(N˙y)∧¬N(y),
5. ∃y.x=¬˙(¬˙y)∧P(y),
6. ∃y,z.x=(y∧˙ z)∧P(y)∧P(z),
7. ∃y,z.x=¬˙ (y∧˙ z)∧(P(¬˙ y)∨P(¬˙ z)), 8. ∃f.x=∀˙f∧∀y.P(fy),
9. ∃f.x=¬˙(∀˙f)∧∃y.P(¬˙(fy)).
Interpreting the truth predicate T by a least fixed point of Γ(P,x) the verification of the FON axioms is straightforward. However, the leastness of the fixed point is essential to verify the axiom of consistency. Thus, while the operator Γ can be easily formalized in ID1, consistency can be directly verified only in the theory ID1.
However, there is a possibility to deal with consistency by use of fixed point theories with ordinals. Such theories, introduced by Ja¨ger [J¨ag93], were widely used in the proof-theoretic analysis of explicit mathematics, cf. [FJ93, JS95a, JS95b, FJ96, GS96, JS96, MS98, FS00, Str00b]. In the following we give a sketch for the analysis of FON + (LFt -IN) which would proceed with the following steps:
1. Introduce a theory Γ-ID1 consisting of a fixed point axiom for the operator Γ plus an additional axiom stating the consistency of the fixed point. So Γ-ID1 extends PA by the new fixed point constant PΓ and the two axioms:
∀x.Γ(PΓ, x) ↔ PΓ(x), ∀x.¬(PΓ(x) ∧ PΓ(¬˙ x)).
2. Define a semi-formal system ω-PAwΩ, i.e., the theory PAwΩ of [J¨ag93] but involving a ω-rule for the natural numbers. The main feature of this theory is that it provides ordinals which allow us to form fixed points in stages.