Program Semantics and Classical Logic

Proof. If C = {Fι}P{F2} then C^t = ∀ij. (F₁^t(i) ∧ P^t(<i,ji)) → F₂^t(j) and
X occurs in P. Using that P^t is continuous in X and applying Lemma 11
repeatedly, we find that C^t is anticontinuous in X. If C = P₁ ⊆ P₂ then C^t =
∀r. P₁^t (r) → P₂^t (r). The following series of equivalences and implications give
the required proof.

V(∀r.P1^t(r) → P2^t(r),a[Rⁿ/X]) = 1

n

for all n: V (∀r. P₁^t (r) → P₂^t (r), a[Rⁿ/X]) = 1
for all n: V(P1^t, a[Rⁿ/X]) ⊆ V(P2^t, a[Rⁿ/X])

^[ V(P1^t, a[Rⁿ/X]) ⊆ ^[V(P2^t,a[Rⁿ/X])

nn

V(P^t,a[R^ω/X] ⊆ V(P2^t,a[R^ω/X])

V(∀r.P₁^t(r) → P₂^t(r),a[R^ω/X]) = 1

The main rule of Scott Induction can now be proved. We first formulate a
general logical variant, from which the Rule itself follows as a corollary.

Theorem 13 Let B and A1, . . . , An be terms of type s × s → t which are
continuous in the type s × s → t variables X₁,..., X_n and let φ be a for-
mula which is weakly anticontinuous in the s × s → t variable X such that
X₁,..., X_n are not free in φ. For readability, write φ(A) instead of [A/X]<^.
Then

φ([λr. false/Xi,..., λr. false/X_n]B)
∀X1... Xnfc(B) → φ([A√X1,..., An/Xn]B) AX
φ(λr. ∀X1... Xn(Vn=ι Xi = Ai → B(r)))

Proof. For each k, let R = 0 and Rm+¹ = V(A_k, a[Rm/X₁₅..., Rmm/Xn]).
The first premise says that V([B/Xfc, a[R⁰/X₁... Rn/X_n]) = 1 and the sec-
ond premise implies that

V([B/Xfc, a[Rm/X1... Rm/Xn]) = 1 only if

V([B/Xfc, a[Rm⁺¹/X1... Rm⁺ /Xn]) = 1.

We conclude that T_m V([B/X]φ, a[Rmm/X₁... Rm¹ /X_n]) = 1 and use Lemma 7
to derive that V([B/Xfc, a[Rm/X₁... Rm/X_n]) = 1. From this the Theorem
follows with Lemma 8.   □

23

<<   20   21   22   23   24   25   26   >>

More intriguing information