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 absent2. 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