Page 145 - Textos de Matemática Vol. 40

3.5. Supervaluation 133 II. T-elem.
(2) x = y → T(x =˙ y),
(3) ¬x = y → T(¬˙ (x =˙ y)), (4) N(x) → T(N˙ x),
(5) ¬N(x) → T(¬˙ (N˙ x)).
III. T-imp.
(6) T(φ˙ →˙ ψ˙) → (T(φ˙) → T(ψ˙)).
IV. T-univ.
(7) (∀x.T(φ˙)) → T(∀˙ (λx.φ˙)).
V. T-log.
(8) T(φ˙), if φ is a logical axiom.
As for FON, we leave out (trivial) self-reference, but define T˙ as λx.x.
By T-log, we have T(φ˙) as an axiom of SON whenever φ is a LFt formula which is an instantiation of an axiom of predicate logic with equality. Moreover, in the following, we study LFt formulae φ which are provable by use of pure logic only, i.e., by use of axioms and rules of predicate logic with equality. In this case, we write
PL ⊢ φ.
The following Lemma collects the elementary facts which we need about SON, [Can96]. In particular, the first one, provable by induction on the length of the derivation, is crucial.
Lemma 3.5.1. 1. For LFt formulae φ for which PL ⊢ φ holds, we have: SON ⊢ T ( φ˙ ) .
2. SON ⊢ (∀x.T(φ˙)) ↔ T(∀˙ (λx.φ˙)),
3. SON ⊢ T(φ˙) ∧ T(ψ˙) ↔ T(φ˙ ∧˙ ψ˙),
4. SON ⊢ (∃x.T(φ)) → T(∃˙ (λx.φ˙)),
5. SON ⊢ T(φ˙) ∨ T(ψ˙) → T(φ˙ ∨˙ ψ˙).
Note that we have equivalences in the case of conjunction and universal
quantification, while for disjunction and existential quantification only one di- rection holds.
Induction.
Concerning induction principles, we are mainly interested in truth induc- tion (T-IN) because in SON, it is equivalent to the scheme of formulae induction (LFt -IN), i.e., induction over N for arbitrary LFt formulae.