Program Semantics and Classical Logic

for each ` ∈ N ∪ {ω}, each m ∈ N and each k (1 ≤ k ≤ n) the relation
R. by setting R0,k = 0 and Rmk⁺¹ = V(Ak, α[Rm√Xι,..., Rm_n∕X_n, R'∕ξ])•
Then R⁰_k ⊆ R'_k ⊆ ... ⊆ Rnk ⊆ ... for each k and '. Moreover, it
,,     ,

is easily proved by induction on m, using the monotonicity of the Ak and
the definition of Rmk that Rmk ⊆ Rm+₁,k if ' ∈ N, so that we also have
chains Rmk ⊆ Rmk ⊆ ... ⊆ Rmk ⊆ .... We prove by induction on m that
S' Rmk = Rmk. This is trivial for m = 0. Suppose the statement holds for
m. Then, using the continuity of the A_k and the induction hypothesis, we
find that

^R'^m,k^{+1  =}

'

[ V(Ak, a[Rm1∕X1,..., Rm/Xn, R'∕ξ]) =
'

U Rm1∕X1,... ,∪ Rmn/Xn, U R'∕ξ ) =

'   ''

V(Ak, a Rω^m,1∕X1,..., Rω^m,n∕Xn, R^ω ∕ξ ) =

^Rω^m,⁺k ¹

Since Rω^ω,k = m  ' R'^m,k = '  m R'^m,k it follows that (*) Rω^ω,k =  'R'^ω,k. Now

we reason as follows, using Lemma 8 twice and using (*) and the continuity
of B in ξ

^[V(λr.∀X1 .. .Xn(^{^n} Xi = Ai → B(r)), a[R^'∕ξ]) =

'                        i=1

^[ V(B, a[R'^ω,1∕X1,..., R'^ω,n∕Xn, R^'∕ξ]) =
'

R'^ω,1∕X1,...,   R'^ω,n∕Xn,   R^'∕ξ

'   ''

V(B,a Rω^ω,1∕X1,..., Rω^ω,n∕Xn, R^ω∕ξ ) =

V(λr.∀X1...Xn(^{^n} Xi =Ai → B(r)), a[R^ω ∕ξ])

i=1

This concludes the proof □

That translations of programs are continuous is now easily proved. The
proposition will allow us to apply the Knaster-Tarski theorem to those trans-
lations.

21

<<   <   18   19   20   21   22   23   24   >   >>