Program Semantics and Classical Logic

Lemma 16 (Soundness of the ρ rule)

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

Proof. Directly from Lemma 8 and Proposition 10.   □

Proposition 17 (Soundness of C) P₁ 'C P₂ ⇒ V(Pι,a) ⊆ V(P₂,α)

Proof. The proof proceeds by induction on the length of the derivation of P₂
from P₁ .   □

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 P1 ; P2 if P can be split into two parts which
derive P₁ and P₂ respectively; lemma 20 establishes a useful substitution
property and uses lemma 19 for its proof.

Lemma 18 P 'C P₁; P₂ iff there are P₁⁰ and P22 such that P = P₁⁰; P22, P11 'C
Pi and P22 'C P₂.

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 (Y_i ^ Qiii(Q), or in any of the X_k. For any P, abbreviate
[Pk/Yk]k [Z'/Y']' P as P⁰. 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']' Q⁰ = by Definition 3
[hzi ^ Qiii(Q')/Z']' Q⁰

This means that [P_k/X_k]_k (Y_i ^ Qiii(Q), which by definition is (Z_i ^
Qiii(Q⁰), follows from [Pk/Xk]k [hYi ^ Qfii(Q'i/Yf]' Q by the P rule. □

27

<<   24   25   26   27   28   29   30   >>

More intriguing information