Page 144 - Textos de Matemática Vol. 40

132 Chapter 3. Truth Theories
Theorem3.4.22. 1. |FSU+(C-IN)|=|ID<ω|=φ100=Γ0, 2. |FSU + (T-IN) | = |ID<ωω | = φ1ω0,
3. |FSU + (LU -IN) | = |ID<ε0 | = φ1ε00.
3.5 Supervaluation
In [Can90], Cantini has already presented a truth theory over Peano arithmetic which is proof-theoretically equivalent to ID1. It is based on supervaluation. The idea of supervaluation is due to van Fraassen [vF68, vF70]. It expresses that formulae which follow by pure logic are true independently of the logical complexity and syntactical structure of their subformulae.
In [Can96, Chapter 12], Cantini introduced an corresponding truth theory for applicative theories, called VFp. For it, the truth axioms of Frege structures
˙
are replaced by axioms for supervaluation. For example, we have T(φ → φ) for
arbitrary formulae φ. It is easy to observe that this is, in general, not provable for T negative formulae in Frege structures.
Cantini shows the proof-theoretic lower bound by an embedding of IDacc. 1
The upper bound is shown by a provability interpretation in the theory KPu, a version of Kripke-Platek set theory equivalent to ID1 introduced and studied by Ja¨ger [J¨ag82].
Here, we will introduce the theory SON+(LFt -IN) which is Cantini’s VFp,
but refine the proof-theoretic lower bound, by giving an syntactical interpreta-
tion of ID instead of IDacc. As for the embedding of ID within Frege structures, 111
this result shows the special syntactical expressiveness of truth theories over ap- plicative theories.
The theory SON.
We define the theory SON (supervaluation over theories of operation and numbers), which corresponds to the theory VF− of Cantini in [Can96, § 59]. The language SON is the same as LFt , but we make freely use of the additional (definable) constant →˙ . As in definition 3.1.2, we can associate with every formula φ a term φ˙.
The axioms of SON are those of TON extended to the new language, plus the following ones:
I. T-out.
(1) T(φ˙)→φ.
The Section on supervaluation is based on [Kah01] and essentially a translation of [Kah97a, Section 2.2.7].