Page 147 - Textos de Matemática Vol. 40

3.5. Supervaluation 135
The proof is straightforward by induction of the build up of φ and, for the second Claim, by use of Lemma 3.5.1.
In the following, we will use as abbreviations: Closφ(ψ) :⇔ ∀x.φ(ψ, x) → ψ(x),
ψ′(x) :⇔ Closφ(ψ) → ψ(x).
In close analogy to the proof of Proposition 3.5.2, we can show the φ- closure of ψ′ by use of pure logic only. From that, we get the φ-closure of T(ψ˙′) in SON.
Lemma 3.5.6. If φ(R, x) is a positive operator form and ψ(x) an arbitrary LFt - formula with the one free variable x, we have:
1. PL ⊢ Closφ(ψ′(·)).
˙
2. SON ⊢ Closφ(T(ψ′(·))).
Proof. We have to show ∀x.φ(ψ′,x) → ψ′(x) by use of pure logic only, i.e., PL ⊢ ∀x.φ(ψ′, x) → (Closφ(ψ′) → ψ(x)).
Let us assume φ(ψ′,x) and Closφ(ψ). By the definition of ψ′, we get ∀y.ψ′(y) → ψ(y) from the latter. Lemma 3.5.5.1 yields φ(ψ,x), which is the premiss of Closφ(ψ). Thus, we get ψ(x). Since this proof uses pure logic only, we have shown the first assertion.
˙
By Lemma 3.5.1.1, we get from the first assertion that T(Closφ(ψ′)) holds in SON. By Lemma 3.5.1.2, axiom III.(6), and Lemma 3.5.5.2, we can move the truth predicate inside the formula and get Closφ(T(ψ˙′)). ⊣
Now, we can define least fixed points for positive operator forms in SON. Proposition 3.5.7. Let φ(R, x) be a positive operator form. Then there exists a
LFt formula Pφ(x) such that for all LFt formulae ψ, the following holds: SON ⊢ ∀x.φ(Pφ, x) → Pφ(x),
SON ⊢ (∀y.φ(ψ, y) → ψ(y)) → ∀x.Pφ(x) → ψ(x). Proof. We set
Pφ(x) :⇔ ∀z.Closφ(T(z ·)) → T(z x).
For the first assertion, let us assume φ(Pφ,x). We have to show Pφ(x), i.e., ∀z.Closφ(T(z ·)) → T(z x). So we assume, additionally, Closφ(T(z ·)). From the definition of Pφ(x), we get from this that ∀y.Pφ(y) → T(z y) holds. Now, we apply Lemma 3.5.5.1 and get from the first assumption φ(T(z ·), x). Using the second assumption again, we finally have T(z x).