Page 113 - Textos de Matemática Vol. 40

3.2. Truth theories in the partial setting 101
˙ ˙ ˙
For conjunctions φ ∧ ψ we define φ∧ψ by ∀(λy.dN (λz.φ˙)(λz.ψ)y00) with
˙ ˙
y,z ̸∈ FV(φ,ψ). For the universal quantification we set ∀x.φ := ∀(λx.φ˙).
Note that φ˙ is not compatible with substitution, because of the use of λ- abstraction. In the presence of (AllN), we have that truth is preserved under substitution, if we substitute a defined term:
Lemma 3.2.4. For all closed terms t and formulae φ of LFd the following holds: ˙
FDA + (AllN) ⊢ t ↓ → (T(φ˙ [t/x]) ↔ T(φ[t/x])).
Proof. The proof is analogous to the proof of Lemma 3.1.3, and we check the case of negated conjunction only, assuming that the closed term t is defined.
In the following chain of equivalences the first one holds by definition, the second by axiom II.(9), and the third by case distinction on y.
˙ T(¬(φ∧ψ)[t/x]) ↔
˙ ˙
T(¬˙ (∀(λy.dN (λz.φ˙)(λz.ψ)y00)[t/x]))
↔ ∃y.T(¬˙ (dN (λz.φ˙)[t/x] (λz.ψ˙)[t/x] y 0 0))
↔ T(¬˙ (dN (λz.φ˙)[t/x] (λz.ψ˙)[t/x] 0 0 0))
∨ ∃y.y ̸= 0 ∧ T(¬˙ (dN (λz.φ˙)[t/x] (λz.ψ˙)[t/x] y 0 0)). To get the equivalence of this disjunction with
T(¬˙ ((λz.φ˙)[t/x]0))∨T(¬˙ ((λz.ψ˙)[t/x]0))
we need on the one hand the assumption (AllN) in the second disjunct. On the
other hand, the assumption t ↓ is needed, because otherwise the term (λz.φ˙)[t/x]
or (λz.ψ˙)[t/x] could become undefined while λz.φ˙ and λz.ψ˙ are always defined.
Since (λz.s)[t/x] 0 ≃ s[t/x][0/z] holds for arbitrary closed terms t, the last line ˙
is equivalent to T(¬˙φ[t/x]) ∨ T(¬ψ[t/x]), and the induction hypothesis yields ˙ ˙
T(¬φ[t/x]) ∨ T(¬ψ[t/x]). Tracing back on the same lines we get the equivalence ˙
with T(¬(φ[t/x] ∨ ψ[t/x]). ⊣ Now we can prove the central Proposition for Frege structures for the class
of weakly T-positive formulae.
Proposition 3.2.5. If φ is a weakly T-positive formula of LFd , then
FDA + (AllN) ⊢ T(φ˙) ↔ φ.