We shall refer to UA as to the Update Axiom . The axiom is related to the
‘Update Postulate’ of [10] and to the ‘Having Enough States’ axiom of [5].
We write Γ =AX φ if Γ, UA, PA2 =s φ.
This ends the list of axioms we wish to impose. To see that they are
consistent, it suffices to construct a model in which De consists of the set N
of natural numbers, where Ds is the set of all functions f : N → N, and
where I(V ) is the function such that I(V )(n)(f) = f(n) for all n ∈ De and
all f ∈ Ds . We can obtain a model with denumerable basic domains if we
let Ds be the set of all functions f : N → N such that f (n) 6= 0 for finitely
many n and define De and I(V ) as before.
6 The Translation
We are now in the position to define the promised translation of our pro-
gramming language into the second-order part of classical type logic. We
shall give it in three installments, translating terms and formulas first and
programs and correctness formulas afterwards. We assume that V ARe is
enumerated by the natural numbers. In the following definition arithmetical
terms N translate as terms of type s → e and formulas F translate as terms
of type s → t.
Definition 12 (Translation of Terms and Formulas)
|
0t |
= λi.0 |
(1) |
|
(S (Num)}) |
= λi.S(Numt(i)) |
(2) |
|
t |
= λi.V(Sk(0))(i) |
(3) |
|
(N1 + N2)t |
= λi.N1t(i) + N2t(i) |
(4) |
|
(N1 × N2)t |
= λi.N1t(i) × N2t(i) |
(5) |
|
falset |
= λi.false |
(6) |
|
(N1 = N2)t |
= λi.N1t(i) = N2t(i) |
(7) |
|
(N1 ≤ N2)t |
= λi.N1t(i) ≤ N2t(i) |
(8) |
|
(F1 → F2)t |
= λi.F1t(i) → F2t(i) |
(9) |
|
(∀xkF)t |
= λi.∀j(i[Sk(0)]j→Ft(j)) |
(10) |
Most clauses in this definition are self-explanatory; but note that in (3)
variables x are translated as the values of registers and that quantification
14