Proof. If C = {Fι}P{F2} then Ct = ∀ij. (F1t(i) ∧ Pt(<i,ji)) → F2t(j) and
X occurs in P. Using that Pt is continuous in X and applying Lemma 11
repeatedly, we find that Ct is anticontinuous in X. If C = P1 ⊆ P2 then Ct =
∀r. P1t (r) → P2t (r). The following series of equivalences and implications give
the required proof.
V(∀r.P1t(r) → P2t(r),a[Rn/X]) = 1
< ⇒
< ⇒
< ⇒ (P1, P2 are continuous)
<⇒
n
for all n: V (∀r. P1t (r) → P2t (r), a[Rn/X]) = 1
for all n: V(P1t, a[Rn/X]) ⊆ V(P2t, a[Rn/X])
[ V(P1t, a[Rn/X]) ⊆ [V(P2t,a[Rn/X])
nn
V(Pt,a[Rω/X] ⊆ V(P2t,a[Rω/X])
V(∀r.P1t(r) → P2t(r),a[Rω/X]) = 1
The main rule of Scott Induction can now be proved. We first formulate a
general logical variant, from which the Rule itself follows as a corollary.
Theorem 13 Let B and A1, . . . , An be terms of type s × s → t which are
continuous in the type s × s → t variables X1,..., Xn and let φ be a for-
mula which is weakly anticontinuous in the s × s → t variable X such that
X1,..., Xn are not free in φ. For readability, write φ(A) instead of [A/X]<^.
Then
φ([λr. false/Xi,..., λr. false/Xn]B)
∀X1... Xnfc(B) → φ([A√X1,..., An/Xn]B) AX
φ(λr. ∀X1... Xn(Vn=ι Xi = Ai → B(r)))
Proof. For each k, let R = 0 and Rm+1 = V(Ak, a[Rm/X15..., Rmm/Xn]).
The first premise says that V([B/Xfc, a[R0/X1... Rn/Xn]) = 1 and the sec-
ond premise implies that
V([B/Xfc, a[Rm/X1... Rm/Xn]) = 1 only if
V([B/Xfc, a[Rm+1/X1... Rm+ /Xn]) = 1.
We conclude that Tm V([B/X]φ, a[Rmm/X1... Rm1 /Xn]) = 1 and use Lemma 7
to derive that V([B/Xfc, a[Rm/X1... Rm/Xn]) = 1. From this the Theorem
follows with Lemma 8. □
23