Program Semantics and Classical Logic



Lemma 16 (Soundness of the ρ rule)

V((hXi ^ Piii(P))*,a) = V(([hXi ^ Piii(Pk)/Xk],nP)*,a)

Proof. Directly from Lemma 8 and Proposition 10.   

Proposition 17 (Soundness of C) P1 'C P2 V(Pι,a) V(P2,α)

Proof. The proof proceeds by induction on the length of the derivation of P2
from P1 .   

We now come to a series of five lemmas which are of a more technical nature.
They are needed for the proof of Theorem 23 below. Let us begin with three
simple lemmas of a proof-theoretical nature. Lemma 18 says that a program
P can only derive a sequence P
1 ; P2 if P can be split into two parts which
derive P
1 and P2 respectively; lemma 20 establishes a useful substitution
property and uses lemma 19 for its proof.

Lemma 18 P 'C P1; P2 iff there are P10 and P22 such that P = P10; P22, P11 'C
Pi and P22 'C P2.

Proof. A straightforward induction on length of derivation.

Lemma 19 Let i and` range over {1, . . . , n} and let k range over {1, . . . , m},
then

1. [Pk/Xk]k (Q1 Q2) follows from [Pk/Xk]k Q1 and from [Pk/Xk]k Q2 by
the
rule;

2. [Pk/Xk]k hY ^ Qiii(Q) follows from [Pk/Xk]k [hY ^ Qfii(Qf)/Y']' Q
by the ρ rule.

Proof. The first statement is trivial, so we prove the second. Let Z1, . . . , Zm
be the first variables in some given ordering which do not occur in any of
the P
k, in (Yi ^ Qiii(Q), or in any of the Xk. For any P, abbreviate
[
Pk/Yk]k [Z'/Y']' P as P0. We have

[Pk/Xk]k [hYi ^ Qfii(Qf)/Y']' Q =

[Pk/Xk]k [hYi ^ Qiii(Q')/Z']` [Z'/Y']' Q = by Lemma 1

[[Pk/Xk]k Y ^ Qiii(Q')/Z']' Q0 = by Definition 3
[
hzi ^ Qiii(Q')/Z']' Q0

This means that [Pk/Xk]k (Yi ^ Qiii(Q), which by definition is (Zi ^
Qiii(Q0), follows from [Pk/Xk]k [hYi ^ Qfii(Q'i/Yf]' Q by the P rule.

27



More intriguing information

1. Optimal Vehicle Size, Haulage Length, and the Structure of Transport Costs
2. The name is absent
3. The Veblen-Gerschenkron Effect of FDI in Mezzogiorno and East Germany
4. The name is absent
5. Improving the Impact of Market Reform on Agricultural Productivity in Africa: How Institutional Design Makes a Difference
6. Fiscal Rules, Fiscal Institutions, and Fiscal Performance
7. The name is absent
8. Pupils’ attitudes towards art teaching in primary school: an evaluation tool
9. The name is absent
10. The name is absent