Page 107 - Textos de Matemática Vol. 40

3.1. Truth theories in the total setting 95 Proposition 3.1.8. Let φ(R, x) be a positive operator form. Then there exists a
term tφ of LFt such that
FON ⊢ ∀x.T(tφ x) ↔ φ(T(tφ ·), x).
Proof. We define tφ by use of the Recursion Theorem 1.2.2: ˙
tφ := rec (λy, x.φ(T(y ·), x)). ˙
So we have tφ x = φ(T(tφ ·),x) and get
T(tφ x) ↔ T(φ(T(tφ ·), x))
↔ φ(T(tφ ·), x).
Note, the T-positiveness of φ is crucial when applying Proposition 3.1.5. ⊣
By Proposition 3.1.5, we can reduce induction for T free formulae in FON to (C-IN). Thus, the standard translation ·N of Peano Arithmetic into TON + (Lt-IN), [JS95b], carries over to FON + (C-IN). Using the previous Proposition, we easily can extend this interpretation to the fixed points constants of ID#1 and ID1. So we get:
Proposition 3.1.9. There exists a translation ·N from the language of PA or LID, respectively, into the language LFt such that
1. PA⊢φ ⇒ FON+(C-IN)⊢φN, 2. ID#1 ⊢φ ⇒ FON+(T-IN)⊢φN, 3. ID1 ⊢φ ⇒ FON+(LFt -IN)⊢φN.
Please note that the Recursion Theorem in applicative theories does not help to define least fixed points. For this reason, there is no possibility to define a truth theory based on applicative theories which allows an embedding of ID1 in the same manner. However, later we will define a truth theory based on supervaluation which allows a syntactical embedding of ID1, see Section 3.5.
3.1.4 Model construction
Flagg and Myhill [FM87b] give a general model construction for Frege struc- tures by defining truth as a fixed point satisfying the corresponding closure conditions (cf. also the original definition in [Acz80]). These models can be directly formalized in ID1, but the leastness condition is essential to verify the axiom of consistency.
˙