Program Semantics and Classical Logic

continuity while the second lemma proves a generalisation related to weak
anticontinuity. Lemma 6 will be applied immediately in the proof of lemma
8 below, but the application of lemma 7 will have to wait a bit, until we come
to the proof of Scott’s Induction Rule.

Lemma 6 Let Aα be continuous in ξ1 , . . . , ξn, then

[ V (A, α[RJ7ξι,..., Rn∙∕ξ_n]) = V (A,α[RT∕ξι,     R£∕ξn])

m

Proof. Repeated application of continuity gives us that

[ ... [ V (A, a[R™ ∕ξι,..., Rnmⁿ ∕ξn]) = V (A, a[Rω ∕ξι,..., R ∕ξn])

m1 mn

That the lefthand side of this equation is equal to

^[ V (A, a[R1^m ∕ξ1,...,Rn^m∕ξn])
m

follows by the monotonicity of A in each of the variables ξ₁,..., ξ_n.   □

Lemma 7 Let Aα be continuous in ξ1 , . . . , ξn , while B is weakly anticontin-
uous in ζα, and ξ1 , . . . , ξn are not free in B. For each k (1 ≤ k ≤ n), let
R⁰_k ⊆ R¹_k ⊆ . . . ⊆ R_k^m ⊆ . . . be a chain, then

^\ V([A∕ζ]B, a[R1^m∕ξ1,..., Rn^m∕ξn]) ⊆V([A∕ζ]B,a[R1^ω∕ξ1,...,Rn^ω∕ξn])
m

Proof. For each m ∈ N let S^m  = V(A, a[R₁^m ∕ξ₁ , . . . , R_n^m ∕ξ_n ]). From the

monotonicity of A in each ξk we obtain that S⁰ ⊆ S¹ ⊆ . . . ⊆ S^m ⊆ ....

Hence, by the usual Substitution Theorem and the weak anticontinuity of B
in ζ,

\ V ([A∕ζ]B, a[RT∕ξι,..., Rn∙∕ξJ) = \ V (B, a[S ^m∕ζ ]) ⊆ V (B, a[S^ω ∕ζ ])
mm

From Lemma 6 it follows that S^ω = V(A, a [R₁^ω∕ξ₁, . . . , R_n^ω∕ξ_n ]) for each m,
so that

V(B, a[S^ω∕ζ]) =V([A∕ζ]B,a[R1^ω∕ξ1,...,Rn^ω∕ξn])

□

18

<<   15   16   17   18   19   20   21   >>

More intriguing information