Program Semantics and Classical Logic



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 C
t 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(VnXi = 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



More intriguing information

1. Examining Variations of Prominent Features in Genre Classification
2. Segmentación en la era de la globalización: ¿Cómo encontrar un segmento nuevo de mercado?
3. The name is absent
4. The name is absent
5. Foreign direct investment in the Indian telecommunications sector
6. Business Cycle Dynamics of a New Keynesian Overlapping Generations Model with Progressive Income Taxation
7. Conservation Payments, Liquidity Constraints and Off-Farm Labor: Impact of the Grain for Green Program on Rural Households in China
8. Innovation Policy and the Economy, Volume 11
9. Nonparametric cointegration analysis
10. Investment and Interest Rate Policy in the Open Economy
11. The name is absent
12. The name is absent
13. Education Research Gender, Education and Development - A Partially Annotated and Selective Bibliography
14. Monetary Policy News and Exchange Rate Responses: Do Only Surprises Matter?
15. Gianluigi Zenti, President, Academia Barilla SpA - The Changing Consumer: Demanding but Predictable
16. Gerontocracy in Motion? – European Cross-Country Evidence on the Labor Market Consequences of Population Ageing
17. Consciousness, cognition, and the hierarchy of context: extending the global neuronal workspace model
18. Does South Africa Have the Potential and Capacity to Grow at 7 Per Cent?: A Labour Market Perspective
19. The name is absent
20. Dendritic Inhibition Enhances Neural Coding Properties