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. The name is absent
2. Inflation Targeting and Nonlinear Policy Rules: The Case of Asymmetric Preferences (new title: The Fed's monetary policy rule and U.S. inflation: The case of asymmetric preferences)
3. A Theoretical Growth Model for Ireland
4. The name is absent
5. The Variable-Rate Decision for Multiple Inputs with Multiple Management Zones
6. Modeling industrial location decisions in U.S. counties
7. Volunteering and the Strategic Value of Ignorance
8. Improving Business Cycle Forecasts’ Accuracy - What Can We Learn from Past Errors?
9. Ronald Patterson, Violinist; Brooks Smith, Pianist
10. News Not Noise: Socially Aware Information Filtering