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. Towards a Strategy for Improving Agricultural Inputs Markets in Africa
2. The name is absent
3. Improving behaviour classification consistency: a technique from biological taxonomy
4. Rent-Seeking in Noxious Weed Regulations: Evidence from US States
5. Regional science policy and the growth of knowledge megacentres in bioscience clusters
6. Workforce or Workfare?
7. On the Integration of Digital Technologies into Mathematics Classrooms
8. Public Debt Management in Brazil
9. DEMAND FOR MEAT AND FISH PRODUCTS IN KOREA
10. A Brief Introduction to the Guidance Theory of Representation