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 A1, . . . , An be terms of type s ×
s → t
which are continuous in the type s × s → t variables X1 , . . . , Xn . Fix a
model and an assignment a. For each k (1 ≤ k ≤ n) let R0 = 0 and Rmm + =
V(Ak, α[Rm∕Xι,..., Rm∕Xn]). Then V(Ak, a[R /Xι,..., Rωn/Xn]) = Rk for
each
k and

n

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

Proof. First, we check by induction on m that Rk0 ⊆ Rk1 ⊆ . . . ⊆ Rkm ⊆ . . .,
for each
k. Trivially, 0 = Rk0 ⊆ Rk1 . Suppose that Rkm ⊆ Rkm+1 for each k.
Since
Ak is monotonic in X1 , . . . , Xn it holds that

Rkm+1 =V(Ak,a[R1m/X1,...,Rnm/Xn])

V(Ak,a[R1m+1/X1,...,Rnm+1/Xn])=Rkm+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

[ Rkm+1 = [ Rkm = Rkk
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



More intriguing information

1. Initial Public Offerings and Venture Capital in Germany
2. Imitation in location choice
3. The name is absent
4. Wirtschaftslage und Reformprozesse in Estland, Lettland, und Litauen: Bericht 2001
5. Endogenous Determination of FDI Growth and Economic Growth:The OECD Case
6. Language discrimination by human newborns and by cotton-top tamarin monkeys
7. The name is absent
8. The Challenge of Urban Regeneration in Deprived European Neighbourhoods - a Partnership Approach
9. Foreign direct investment in the Indian telecommunications sector
10. The name is absent