Program Semantics and Classical Logic

The reason why we are interested in continuity at all is the so-called Knaster-
Tarski theorem, which says that intersections of fixpoints as we have used
them in the translation of the recursion construct can be ‘approximated from
below’. The following lemma is a version of the Knaster-Tarski theorem in
our modeltheoretic setting. It will be crucial in proving the induction theorem
we are after.

Lemma 8 (Knaster-Tarski) Let B and A₁, . . . , A_n be terms of type s ×
s → t which are continuous in the type s × s → t variables X₁ , . . . , X_n . Fix a
model and an assignment a. For each k (1 ≤ k ≤ n) let R0 = 0 and Rmm ⁺ =
V(Ak, α[Rm∕Xι,..., Rm∕X_n]). Then V(Ak, a[R /Xι,..., R^ω_n/Xn]) = Rk for
each k and

n

V (λr. ∀X₁ ...X_n(∕∖ Xi = Ai →B(r)),a) = V (B,aR/Xι,...,Rk /Xn])
i=1

Proof. First, we check by induction on m that R_k⁰ ⊆ R_k¹ ⊆ . . . ⊆ R_k^m ⊆ . . .,
for each k. Trivially, 0 = R_k⁰ ⊆ R_k¹ . Suppose that R_k^m ⊆ R_k^m+1 for each k.
Since A_k is monotonic in X₁ , . . . , X_n it holds that

Rk^m+1 =V(Ak,a[R1^m/X1,...,Rn^m/Xn]) ⊆

V(Ak,a[R1^m+1/X1,...,Rn^m+1/Xn])=Rk^m+2

which proves the statement. It follows from Lemma 6 that

V(Ak, a[Rk/Xι,..., Rk/Xn]) = [ V(Ak, a[Rm∕Xι,..., Rm/Xn]) =
m

^[ Rk^m+1 = ^[ Rk^m = Rk^k
mm

Next, observe that

λr.∀X1...Xn(^{^n} Xi =Ai → B(r))
i=1

is equivalent with

λr. ∀Y (∃X1 ...Xn(^{^n} Xi = Ai∧Y = B) → Y (r))
i=1

19

<<   <   16   17   18   19   20   21   22   >   >>