Page 146 - Textos de Matemática Vol. 40

134 Chapter 3. Truth Theories Proposition 3.5.2. (T-IN) and (LFt -IN) are equivalent over SON.
Proof. Of course, we have to show the derivation of (LFt -IN) from (T-IN) only. The proof is a part of the proof of Theorem 59.6 in [Can96], and runs as follows: We set
ClosN(ψ) :⇔ ψ(0) ∧ ∀x : N.ψ(x) → ψ(sN x), ψ′(x) :⇔ ClosN(ψ) → ψ(x).
It follows that PL ⊢ ClosN(ψ′). ¿From this, we get by Lemma 3.5.1.1 that SON ˙
proves T(ClosN(ψ′)). Writing ClosN(ψ′) out in full and applying Lemma 3.5.1.3 yields the premiss of (T-IN) for ψ′. Thus, we get by this induction principle
˙
∀x : N.T(ψ′(x)). The axiom T-out yields ∀x : N.ψ′(x) which is, writing φ′(x) out in full, (LFt -IN) for the formula ψ. Since ψ was arbitrary, the proof is finished. ⊣
¿From [Can96], we get the proof-theoretic equivalence of ID1 and SON + (T-IN), which is essentially his theory VFp. Together with the previous Propo- sition, we have:
Theorem 3.5.3. SON + (T-IN) ≡ SON + (LFt -IN) ≡ ID1.
However, the lower bound is shown by an embedding of IDacc. In the
1
following we will show that, in fact, ID1 can be embedded within SON+(T-IN).
For completeness, we will mention the maybe surprising fact that the re- striction to class induction (C-IN) will not exceed the proof-theoretic strength of Peano arithmetic, cf. [Can96].
Theorem 3.5.4. SON + (C-IN) ≡ PA.
The embedding of ID1. In addition to Cantini’s result, we will show in
the following that SON + (T-IN ) (and (LFt -IN )) also admits a syntactical embed-
ding of ID itself. In contrast to IDacc, the syntactic power of ID is much bigger 111
by allowing the definition of fixed points of arbitrary positive operator forms.
The steps of the proof follow essentially Cantini’s proof of the embedding of
IDacc [Can96, Theorem 59.4], which has to be generalized from binary relations 1
to arbitrary positive operator forms.
Let the positive operator form φ(R,x) be defined, as for FON, as a T-
positive formula which contains the relation variable R only positively. Then, we have:
Lemma 3.5.5. If φ(R,x) is a positive operator form and ψ(x) and χ(x) are arbitrary LFt -formula with the one free variable x, we have:
1. PL ⊢ φ(ψ, x) ∧ (∀x.ψ(x) → χ(x)) → φ(χ, x).
˙ ˙ 2. SON ⊢ φ(T(ψ(·)), x) → T(φ(ψ, x)).