Program Semantics and Classical Logic

over individual variables is translated in (10) by means of quantification over
states. The following two Lemmas are there to ensure that this is correct.

Lemma 3 Let φ be a formula in which j does not occur free, then

=AX ∀v∀i ((∀j (i[v]j → [V(v)(j)∕x]φ) ^ ∀xφ)

Proof. Immediate from AX1. □

Lemma 4 For any type s variable i and term N, let Nⁱ be obtained by
replacing, for all k, each free x_k in N with V(S^k(0))(i). Similarly, let Fⁱ be
the result of replacing each free x_k in F with V(S^k (0))(i) for all k. Then

1. =ax N^t (i) = Nⁱ

2. =ax Ft(i) → Fⁱ

Proof. The truth of the first statement is obvious and the second state-
ment is proved by an induction on the complexity of formulas in which
only the ∀xk F case is interesting. For the latter, consider that, by Lemma
3, (∀x_kF)ⁱ is equivalent with (∀j (i[S^k(0)]j → [V(S^k(0))(j)/x_k]F))ⁱ and
use the definition of i[S^k(0)]j to see that this formula is equivalent with
∀j(i[S^k(0)]j → F^j). Induction tells us that this formula in its turn is equiv-
alent with ∀j (i[S ^k (0)]j → F^t(j)), which needed to be proved. □

The previous Lemma in fact tells us that the translation given thus far pre-
serves entailment between formulas F if we take our axioms into account.
The following definition translates programs into type logic. The type of
target terms is s × s → t here: binary relations between states.

Definition 13 (Translation of Programs)

15

<<   12   13   14   15   16   17   18   >>

More intriguing information