Program Semantics and Classical Logic

projection, but that the sixth clause explicitly requires the logical operator
= to be in the language. Having = is enough to get the usual other logical
operators, as some crucial ones can be defined as follows (see [9]) and the
others can be obtained as in Definition 2.

Definition 9 (Abbreviations)

is short for (λξα. φ) = (λξ_α. ξ = ξ)

is short for ∀ξ_t . ξ_t

is short for ((true, false) = hφ,ψ}') = false

In order to interpret the language of Definition 8, we need to have interpreta-
tions of its constants and variables. An interpretation function I for a frame
{Dα }α is a function with the set of all constants as its domain such that
I(cα) ∈ Dα for all cα . Similarly, an assignment a for {Dα }α is a function
taking variables as its arguments such that a(ξα ) ∈ Dα for all ξα . We write
α[d₁∕ξ₁,..., d_n/ξ_n] for the assignment α⁰ such that α⁰(ξi) = di if 1 ≤ i ≤ n
and a⁰(ξ) = a(ξ) if ξ ∈/ {ξ₁ , . . . , ξ_n}. A (standard) model is a pair hF, Ii of
a frame F and an interpretation function I for F. The following definition
provides the logic with a semantics. (We use fst and snd as functions that
will pick out the first and second element of an ordered pair respectively.)

Definition 10 (Tarski Definition) The value V^M (A, a) of a term A on
a standard model M = hF, Ii under an assignment a for F is defined as
follows (we suppress superscripts M to improve readability).

1. V(c, a) = I (c), if c is a constant;

V(ξ, a) = a(ξ), if ξ is a variable;

2. V (A(B), a) = V(A, a)(V(B, a)), i.e. V(A, a) applied to V(B, a);

3. V (λξα . Aβ, a) = the G ∈ Dα→β such that, for each d ∈ Dα ,
G(d) = V (A,a[d∕ξ]);

4. V(hA,Bi,a)=hV(A,a),V(B,a)i;

5. V((A)0, a) = fst(V (A, a)); V ((A)1 , a) = snd(V (A, a));

6. V(A = B, a) = 1 iff V(A, a) = V(B, a).

11

<<   <   8   9   10   11   12   13   14   >   >>