Program Semantics and Classical Logic

Note that the logical operators that were obtained in Definition 9 get their
standard meaning.

We can now define the notion of entailment.

Definition 11 Let Γ ∪ {φ} be a set of sentences. Γ (standardly) entails φ,
Γ =_s φ, iff, for each model M, and each assignment a for M, VM (φ, a) = 1,
if V^M (γ, a) = 1 for all γ ∈ Γ.

It will be useful to have a typographical convention which helps us distinguish
between variables of various types. The following table gives an overview of
the symbols we shall typically use for variables of a fixed type. For variables
whose type is not fixed, we shall continue to use ξ and ζ .

5 Nonlogical Axioms

There are two kinds of constraints we wish to impose on our models. First,
we want our domain D_s to behave as a set of states. Second, we want D_e to
behave as the natural numbers.

Starting with the second requirement, we impose the (second order) Peano
Axioms, which for the sake of completeness we shall list here. We refer to
the conjunction of these axioms as PA² .

-∃x. S(x) = 0

∀x ∀y. S(x) = S(y) → x = y

∀x. x + 0 = x

∀x ∀y. x + S(y) = S(x + y)

∀x. x × 0 = 0

∀x ∀y. x × S(y) = (x × y) + x

∀X ((X (0) ∧∀x(X(x) → X (S(x)))) →∀xX(x))

12

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