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 Ni be obtained by
replacing, for all k, each free xk in N with V(Sk(0))(i). Similarly, let Fi be
the result of replacing each free xk in F with V(Sk (0))(i) for all k. Then
1. =ax Nt (i) = Ni
2. =ax Ft(i) → Fi
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, (∀xkF)i is equivalent with (∀j (i[Sk(0)]j → [V(Sk(0))(j)/xk]F))i and
use the definition of i[Sk(0)]j to see that this formula is equivalent with
∀j(i[Sk(0)]j → Fj). Induction tells us that this formula in its turn is equiv-
alent with ∀j (i[S k (0)]j → Ft(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)
|
(xk := N)t |
= λr. r0[Sk(0)]r1 ∧ V(Sk(0))(r1) = Nt(r0) |
(11) |
|
(B?)t |
= λr. Bt(r0) ∧ r0 = r1 |
(12) |
|
Xt |
=X |
(13) |
|
(P1;P2)t |
= λr. ∃j. P1t(hr0, ji) ∧ P2t(hj, r1i) |
(14) |
|
(P1 ∪ P2)t |
= λr.P1t(r) ∨ P2t(r) |
(15) |
|
(hXi ^ Piin=ι(P))t |
= λr.∀X1...Xn(^n Xi=Pit→Pt(r)) |
(16) |
15