Page 105 - Textos de Matemática Vol. 40

3.1. Truth theories in the total setting 93 Definition 3.1.2. By induction on the build up of an LFt formula, we define:
˙ t=s ≡
˙ N(t) ≡
˙ T(t) ≡
˙
¬φ ≡
˙ φ∧ψ ≡
˙ ∀x.φ ≡
t=˙s ˙
Nt ˙
Tt ≡ t ¬˙φ˙
˙˙ φ˙∧ψ
˙
∀ (λx.φ˙ )
Since we work in classical logic, we can introduce abbreviations for the other connectives on the term level in the usual way:
(t∨˙ s):=¬˙ (¬˙ t∧˙ ¬˙ s), (t→˙ s):=¬˙ t∨˙ s, and (∃˙x.t):=¬˙ (∀˙x.¬˙ t).
Using the “dot”-notation φ˙ we would like to indicate the difference of this representation compared with a G¨odelization φ.
¿From a technical point of view, the representation is particularly con- venient with respect to variables and substitution: since terms and variables stay essentially untouched in the term representing a formula, φ˙[t/x] should
˙
be equal to φ[t/x]. However, in the case of the universal quantifier we set ˙ ˙
∀x.φ := ∀ (λx.φ˙ ). In the total setting we may define λ terms in a way that they are compatable with substitution, but for the partial case, we discuss in the following subsections, this is not possible. In any case—total and partial—, we can show the following Lemma, expressing that truth holds under substitution.
Lemma 3.1.3. For all terms t and formulae φ of LFt the following holds: ˙
FON ⊢ T(φ˙[t/x]) ↔ T(φ[t/x]).
Proof. The proof is by induction on the build up of φ. The interesting case is the universal quantification, where we can assume y ̸∈ FV(t, x).
˙
By definition and axiom II.(8) the formula T((∀y.φ)[t/x]) is equivalent to
∀y.T((λy.φ˙)[t/x]y). But(λy.φ˙)[t/x]yisequaltoφ˙[t/x]andweget∀y.T(φ˙[t/x]). ˙
The induction hypothesis yields ∀y.T(φ[t/x]) and by axiom II.(8) we have the ˙
equivalence with T((∀y.φ)[t/x]). ⊣
In the following, we have to pay special attention to formulae in which the truth predicate occurs only positively. The formal definition of T-positiveness is given simultaneously with T-negativeness: