1.1 Declarative sentences 3
this text we will be content with sentences as soon as they can, in principle,
attain some truth value regardless of whether this truth value reflects the
actual state of affairs suggested by the sentence in question. Sentence (4)
seems a bit silly, although we could say that if Martians exist and eat pizza,
then all of them will either like pepperoni on it or not. (We have to introduce
predicate logic in Chapter 2 to see that this sentence is also declarative if no
Martians exist; it is then true.) Again, for the purposes of this text sentence
(4) will do. Et alors, qu’est-ce qu’on pense des phrases (5) et (6)? Sentences
(5) and (6) are fine if you happen to read French and German a bit. Thus,
declarative statements can be made in any natural, or artificial, language.
The kind of sentences we won’t consider here are non-declarative ones,
like
r
Could you please pass me the salt?
r
Ready, steady, go!
r
May fortune come your way.
Primarily, we are interested in precise declarative sentences, or statements
about the behaviour of computer systems, or programs. Not only do we
want to specify such statements but we also want to check whether a given
program, or system, fulfils a specification at hand. Thus, we need to develop
acalculus of reasoning which allows us to draw conclusions from given as-
sumptions, like initialised variables, which are reliable in the sense that they
preserve truth: if all our assumptions are true, then our conclusion ought to
be true as well. A much more difficult question is whether, given any true
property of a computer program, we can find an argument in our calculus
that has this property as its conclusion. The declarative sentence (3) above
might illuminate the problematic aspect of such questions in the context of
number theory.
The logics we intend to design are symbolic in nature. We translate a cer-
tain sufficiently large subset of all English declarative sentences into strings
of symbols. This gives us a compressed but still complete encoding of declar-
ative sentences and allows us to concentrate on the mere mechanics of our
argumentation. This is important since specifications of systems or software
are sequences of such declarative sentences. It further opens up the possibil-
ity of automatic manipulation of such specifications, a job that computers
just love to do
1
.Our strategy is to consider certain declarative sentences as
1
There is a certain, slightly bitter, circularity in such endeavours: in proving that a certain
computer program P satisfies a given property, we might let some other computer program Q try
to find a proof that P satisfies the property; but who guarantees us that Q satisfies the property
of producing only correct proofs? We seem to run into an infinite regress.