Here the constants + and × are of type e × e → e, but we use infix notation
and write x + y and x × y for +(hx, yi) and ×(hx, yi) respectively. As is
usual, we abbreviate ∃z. x + z = y as x ≤ y and we write S0 (0) for 0 and
Sn+1 (0) for S(Sn(0)), so that Sn(0) is be the object-level representation of
the number n.
We identify the variables x introduced in section 2 with the variables of
type e and variables X with the variables of type s × s → t. Note that the
first identification turns the set F defined in section 2 into a subset of the
set of first-order formulae of our logic.
The natural numbers shall in fact play a double role in our translation of
the programming language defined in section 2. Their first role is obvious:
they must interpret the elements of N . Their second role will be to act as
addresses of registers. In order to let them behave in this way, we let V be
some fixed non-logical constant of type e → (s → e). The intended interpre-
tation of, say, V (S17(0))(i) is the number which is stored in the register with
address 17 in state i. The formula V (S17(0))(i) = S23(0) thus expresses that
the value of register 17 in state i is 23. As a mnemonic to help distinguish
between these two roles of the natural numbers, we shall use the variable v
whenever we think of them as the addresses of registers but use x, y, z in all
other cases. Formally, however, there is no difference here.
Since we want objects of types s to really behave as states, and since we
want it to be the case that registers can be updated independently from each
other, we shall impose an axiom. If t is a term of type e and i and j are
variables of type s we may use i[t]j to abbreviate ∀v(v 6= t → V (v)(i) =
V (v)(j)). This expresses that states i and j differ at most in the register
with address t. Our axiom requires that there are enough states; so that
given any state, any register, and any number, we can update the register
and set its value to the given number without effecting the values of other
registers.1
UA ∀i ∀v ∀x ∃j. i[v]j ∧ V (v)(j) = x
1If we interpret registers as (logical) variables, states as (logical) assignments, and
V (v)(i) as the application of assignment i to variable v, the axiom formalises the usual
situation in logic that we have enough assigments to let variables take their values inde-
pendently from one another. In [23, 24] Van Benthem studies various weakenings of this
requirement, obtaining variants of predicate logic which are decidable and in which one
can have dependent variables. Weakening UA would not result in decidability of course,
but would also result in introducing similar dependencies among variables. This could be
useful for particular purposes. See also [17].
13