i need q2 and q4

A very similar example to q4 is attached

i am attaching notes as well which can help both in q2 and q4

Attachments: Introduction

The aim of this course is to give the student a working knowledge in logic and its

applications in Computer Science. Rather than trying to cover logic in its full breadth,

which, given the diversity and complexity of the subject, would be an impossible task

for a one-semester course, we will focus on the most fundamental concepts which

every computer scientists should be familiar with, be it as a practitioner in industry

or as a researcher at university. Although the selection of topics reflects to some

extent my personal view and taste of logic, I will aim at a balanced presentation that

also takes into account aspects of logic are not so close to my own research interests.

Throughout the course I will emphasize that logic is something one does: one models

a computing system, specifies a data type or a program, checks or proves that a

system satisfies a certain property. We will do a lot of exercises where these logical

activities will be trained, mostly on the blackboard or with pencil and paper, and

occasionally using the computer. The aim is to provide the student with active logic

skills to solve computing problems.

1

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 2

Besides its practical applications we will also look into the historical development

of logic. What were the main philosophical and mathematical questions that led to

modern logic as we know it today? We will see that these questions and their answers

did shape not only logic, but also large parts of Computer Science.

The main prerequisites for this course are curiosity and a good appetite for solving

problems. No prior knowledge of logic is required. However, I take it for granted

that the student is able to digest formal definitions of syntactic entities such as terms

or formulas. For a Computer Science student, who is familiar with formal syntactic

objects such as computer programs, this will not be a problem at all.

“Logic for Computer Science” is a stand-alone course, but it is also intended to support

other Computer Science modules offered, in particular the modules on Embedded

Systems, High Integrity Systems, Software Testing, Big Data and Machine Learning,

and Modeling and Verification Techniques. Our course does not follow a particular

textbook, but it will use material from several books and lectures on logic. Some of

the main sources are:

[1] D van Dalen, Logic and Structure, 3rd edition, Springer, 1994.

[2] J H Gallier, Logic for Computer Science, John Wiley & Sons, 1987.

[3] Handbook of Logic in Computer Science, Vol. 1-6, S Abramsky, D M

Gabbay, T S E Maibaum, eds, OUP, 1994.

[4] J R Shoenfield, Mathematical Logic, Addison-Wesley, 1967.

[5] D B Plummer, J Barwise, J Etchemendy, Tarski’s World, CSLI Lecture

Notes, 2008.

[6] U Schoening, Logic for Computer Science, Birkh¨auser, 1989.

[7] A S Troelstra, D van Dalen, Constructivism in Mathematics, Vol. I,

North-Holland, 1988.

[8] D Velleman, How to Prove It, 2nd edition, CUP, 1994.

[9] U B, Programming with Abstract Data Types, Lecture Notes, Swansea

University, 2009.

These are preliminary course notes which are being developed as the course progresses.

I will be grateful for reporting to me any errors or suggestions for improvements. For

students seriously interested in logic I recommend to study in addition the sources

listed below as well as further literature on logic which will be recommended during

the course.

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 3

2 Propositional Logic

Propositional Logic is the logic of atomic propositions that are combined by logical

connectives such as “and”, “or”, “not”, “implies”. Here is an example taken from [2]

Consider the following propositions

A “John is a teacher”,

B “John is rich”,

C “John is a rock singer”.

We call A, B, C, atomic propositions.

Now consider the following statements:

• John is a teacher.

• It is not the case that John is a teacher and John is rich.

• If John is a rock singer then John is rich.

We wish to show that the above assumptions, which we call (∗) imply

(∗∗) It is not the case that John is a rock singer.

Using the abbreviations and parentheses to disambiguate the statements (in particular

the second assumption!) this amounts to showing that the formal statement ((∗)

implies (∗∗)) holds, that is

(A and not(A and B) and (C implies B)) implies not(C)

holds.

Without worrying at the moment too much about what it precisely means for a

statement to “hold” we can give a proof that (∗) implies (∗∗) using common sense

reasoning:

To prove that (∗) implies (∗∗) we assume that the premises (∗), that is, A, not(A and

B), (C implies B) are all true.

We must show that the conclusion, not(C), is true, that is, C is false. In other words,

we must show that assuming C leads to a contradiction.

Hence, we assume C, aiming for a contradiction.

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 4

Since we assumed C and we assumed (C implies B) we know that B holds. Hence

in fact (A and B) holds since we assumed A. But this contradicts the assumption

not(A and B).

It is possible to make this kind of reasoning completely precise and formal. Moreover,

there are computer systems carrying out the reasoning automatically. We will explore

this possibility later in the course.

Yet, there is another, completely different method of finding out that the statement

((∗) implies (∗∗)) holds: Since we know nothing about the atomic propositions A,

B, C, other than that they are either true or false, we can simply try all possible

assignments of “true” or “false” to A, B, C and check that statement ((∗) implies

(∗∗)) is true in all cases. It is rather obvious that this method can be automatised as

well.

Note that the method of checking all assignments relies on the assumption that the

atomic propositions involved are completely independent of each other and that it

only matters whether they are true or false, but not what they actually “mean”. In

other words, in propositional logic atomic propositions are viewed as “black boxes”

whose internal structure is invisible.

To highlight this point consider the atomic propositions A := “It is raining” and B :=

“the street is wet”. Common sense tells us that the statement “A implies B” holds,

but there is no way finding this out using the assignment method. One can say that

the statement “A implies B” holds, however not for reasons of propositional logic,

but for reasons having to do with the meaning of A and B.

On the other hand our proof above was purely logical. I did not depend on the

meanings of the statements “John is a teacher”, “John is rich”, and “John is a rock

singer”.

2.1 The three elements of logic

Although our example of teacher John is very simple, it suffices to discern three

fundamental elements of logic:

Syntax The expressions

(+) (A and not(A and B) and (C implies B)) implies not(C) (that is “(∗) implies

(∗∗)”)

(++) not(A and B)

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 5

are examples of formulas, that is, a syntactic representations of a statements. In a

given logic it is precisely defined what expressions are wellformed, that is, syntactically

correct, formulas. Different logics may have different formulas. In Computer Science,

formulas are used to specify computer programs, processes, etc., that is, to describe

their properties.

Semantics Given a formula, the question arises what is its semantics, that is,

meaning, or, more specifically, what does it mean for a formula to be true? Looking

at the formula (++) we might say that we cannot determine its truth unless we know

whether A and B are true. This means that we can determine the truth of (++)

only with respect to a certain assignment of truth values. Such an assignment is a

special case of a structure, also called model, or world. In semantics one often studies

structures and the question whether a formula is true in a structure. However, looking

at formula (+) we might say that it is true irrespectively of the model. One also says

(+) is valid, or logically true.

Proof How can we find out whether a formula is true with respect to a certain

model or whether it is logically true? Are there mechanisable, or even automatisable

methods to prove that a formula is true? In Computer Science, a lot of research effort

is spent on developing systems that can automatically or semi-automatically prove

formulas or construct a model where a given formula is false. Many of these systems

are already in use to improve the quality and dependability of safety critical computer

applications.

All forms of logic are essentially concerned with the study of these three elements.

They will also be the guiding principles of this logic course.

2.2 Syntax of propositional logic

We assume we are given an infinite sequence P1, P2, . . . of atomic propositions.

2.2.1 Propositional formula

The set of propositional formulas is defined inductively as follows.

(i) Every atomic proposition is a propositional formula.

(ii) > and ⊥ are propositional formulas.

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 6

(iii) If A is a propositional formula, then ¬A is a propositional formula .

(iv) If A and B are propositional formulas, then (A ∧ B), (A ∨ B), and (A → B)

are propositional formulas.

Some comments regarding notation:

• Atomic propositions are also called propositional variables (because, as we will

see, their truth value may vary).

• The formulas > and ⊥ represent the truth values “true” and “false”. These are

also often denoted by the numbers 1 and 0.

• Atomic propositions as well as > and ⊥ are called basic formulas. All other

formulas are called composite formulas.

• The formula ¬A is called the negation of A, pronounced “not A”. Some textbooks

use the notation ∼ A instead.

• The formula (A ∧ B) is called conjunction of A and G, pronounced “A and B”.

• The formula (A ∨ B) is called disjunction of A and B, pronounced “A or B”.

• A formula of the form (A → B) is called implication, pronounced “A implies

B”. In many textbooks implication is written A ⊃ B.

• It is often convenient to introduce the abbreviation

(A ↔ B) := (A → B) ∧ (A → B)

A formula of the form (A ↔ B) is called equivalence, pronounced “A is equivalent

to B”. In many textbooks this is written A ≡ B.

• The symbols ¬, ∧, ∨,→ are called “propositional connectives” (or “logical connectives”).

Since in this and the following chapters we will only consider propositional formulas

and no other kind of formulas we will allow ourselves to say “formula” instead of

“propositional formula”.

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 7

Definition 2.2.1 maybe equivalently formulated as a context free grammar in BackusNaur

form:

< formula > ::= < atomic proposition >

| >

| ⊥

| ¬ < formula >

| (< formula > ∧ < formula >)

| (< formula > ∨ < formula >)

| (< formula > → < formula >)

2.2.2 Examples of formulas

Let A, B, C be atomic propositions.

(a) (A ∨ ¬A)

(b) (A ∧ B) ∨ C

(c) ((A ∨ B) → (A ∧ B))

(d) (((A ∨ B) → (A ∧ B)) → ⊥)

(e) ((A ∨ B) → ((A ∧ B) → ⊥))

These examples, in particular (d) and (e), demonstrate that a proliferation of parentheses

can make formulas hard to read. In order to improve readability we will make

use of the following conventions:

• Outermost parentheses are omitted. For example, we write ¬A ∧ B instead of

(¬A ∧ B).

• Implication is the least binding operator. For example, we write A∧B → B ∨A

for (A ∧ B) → (B ∨ A).

• Implication is assumed to associate to the right. This means, for example, that

we write A → B → C → D for A → (B → (C → D)).

• Conjunction and disjunction are assumed to associate to the left. For example,

we write A ∧ B ∧ C instead of (A ∧ B) ∧ C.

Warnings: We do not assume that ∧ binds stronger than ∨, and, for example, in

the formula (A → B) → C the parentheses may not be omitted. Furthermore, the

formulas ¬A ∧ B and ¬(A ∧ B) are not the same. In order to distinguish the latter

two formulas more clearly we may occasionally enclose a negation in (redundant)

parentheses, as, for example, in (¬A) ∧ B.

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 8

2.2.3 Exercise

(a) Write down the formulas of Example 2.2.2 omitting as many parentheses as

possible according to the conventions above.

(b) Add to the formula A ∧ B → A ∨ C → D all omitted parentheses.

(c) Is the expression A ∧ B ∨ C a correct denotation of a formula?

2.2.4 Exercise

Write down the formula of the initial exercise about John the teacher, with maximal

and with minimal parentheses.

2.3 Induction on formulas

The way formulas are defined in 2.2.1 is an example of an inductive definition. Instead

of going into the theory of this kind of definition I try to give the intuition. The clauses

(i) – (iv) are to be viewed as a generation process: All expression, and only those,

which can be generated by a finite number of applications of the clauses are formulas.

Associated with this inductive definition is a principle of proof by induction on formulas.

It says that in order to prove that a certain property P(A) holds for all formulas

A it is enough to prove

• Induction base: P(A) holds if A is a basic formula.

• Induction step: P holds for a composite formula provided P holds for its parts.

For example when proving P(A → B) one may assume (as induction hypothesis)

that P(A) and P(B) hold (similarly for the other logical connectives).

2.3.1 Example of a proof by induction on formulas

Lemma 1. Every formula has as many opening parentheses as closing parentheses

(assuming all parentheses are written).

Proof. By induction on formulas. We set

P(A) := A has as many opening parentheses as closing parentheses

Induction base: Clearly P holds for basic formulas, since these have no parentheses

at all.

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 9

Induction step: Consider a composite formula, for example, (A ∧ B). By induction

hypothesis A and B both satisfy P. Hence clearly (A ∧ B) satisfies P as well since

exactly on opening and one closing parentheses were added. For the other logical

connectives the argument is similar.

This completes the proof of the lemma.

Induction of formulas is very similar to the well-known induction on natural numbers

which is a proof principle saying that in order to prove a property P(n) for all natural

number n it suffices to prove

• the base case, P(0),

• and the step, P(n+ 1), under the assumption that P(n) (induction hypothesis)

holds.

The reason why induction on natural numbers is correct is the same as for formulas:

natural numbers are inductively defined by the clauses

(i) 0 is a natural number.

(ii) If n is a natural number, then n + 1 is a natural number.

2.4 Recursion on formulas

In addition to the fact that all formulas are generated by the clauses (i)-(iv) of Defi-

nition 2.2.1 it is true that this generation is non-ambiguous. That is, for each formula

there is only one way to generate it. In other words each string representing a formula

can be parsed in exactly one way. One says that formulas are freely generated by the

clauses (i)-(iv).

Associated with the free generation of formulas is a principle of definition by recursion

on formulas. This principle says that in order to define a function f on all formulas

it is enough to

• Base case: define f(A) for all basic formulas A,

• Recursive case: define f for a composite formula using the definition of for

its parts. For example when defining f(A → B) one may recursively call f(A)

and f(B).

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 10

2.4.1 Example of a function defined by recursion on formulas

We define the depth of a formula as follows

• depth(A) = 0 for every basic formula.

• depth(¬A) = depth(A) + 1.

• depth(A B) = max(depth(A), depth(B)) + 1 for ∈ {∧, ∨,→}.

We also let con(A) be the number of occurrences of logical connectives in the formula

A.

Lemma 2. con(A) < 2
depth(A)
.
Proof. By induction on formulas.
Induction base: If A is a basic formula, then con(A) = 0 < 1 = 20 = 2depth(A)
.
Induction step: We have to consider composite formulas.
¬A: By induction hypothesis (i.h.) we have con(A) < 2
depth(A)
. Therefore
con(¬A) = con(A) + 1
i.h.
< 2
depth(A) + 1
≤ 2 ∗ 2
depth(A)
= 2depth(A)+1
= 2depth(¬A)
A B where ∈ {∧, ∨,→}: By induction hypothesis we have con(A) < 2
depth(A) and
con(B) < 2
depth(B)
.
con(A B) = con(A) + con(B) + 1
< con(A) + 1 + con(B) + 1
i.h.
≤ 2
depth(A) + 2depth(B)
≤ 2 ∗ 2
max(depth(A),depth(B))
= 2depth(AB)
This completes the proof.
Natural numbers are also freely generated, namely from 0 and the successor operation.
Consequently, there is a corresponding recursion principle which is called primitive
recursion: in order to define a function f on natural numbers it is enough to define
October 13, 2015 CSC375/CSCM75 Logic for Computer Science 11
• f(0) and
• f(n + 1) with a possible recursive call to f(n).
Induction and recursion principles such as induction on formulas and natural numbers,
recursion on formulas and primitive recursion occur very often in computer science
and are of fundamental importance. It is therefore essential to be familiar with them
and to be able to apply them. In fact, we will frequently use them in this course.
These principles are instances of two general principles which are valid for all freely
generated structures: Structural Induction and Structural recursion (see, for example
the preliminary chapter of [2]).
Recursion on formulas vs. general recursion In most programming languages
general recursion is allowed. This means that when defining a function f, a value
f(x) may be defined making recursive calls to f(y) where y is arbitrary.
Clearly, general recursion captures recursion on formulas, primitive recursion and, in
general, structural recursion. So why bother with restricted forms of recursion?
The reason is that recursion on formulas (and more generally structural recursion)
guarantees that the recursively defined function will terminate for all inputs, while
with general recursion this is of course not the case. Moreover, it can be decided
easily whether a given recursive definition is structural recursive or not, while the
question whether or not a general recursive program terminates is undecidable, due
to the undecidability of the Halting Problem.
2.4.2 Exercise
Prove depth(A) ≤ con(A).
2.4.3 Exercise
Give a definition of con(A) by recursion on formulas.
2.4.4 Exercise
Compute depth(A) and con(A) for the following formulas A:
(a) (A ∧ B) ∨ (A ∧ ¬B))
(b) ((A → B) → A) → A
October 13, 2015 CSC375/CSCM75 Logic for Computer Science 12
2.4.5 Exercise
Let atom(A) be the number of occurrences of atomic formulas of A. Give a definition
of atom(A) by recursion on formulas.
2.4.6 Exercise
Prove atom(A) ≤ 2 · con(A) + 1.
2.4.7 Exercise
Define a Haskell data type of propositional formulas.
2.4.8 Exercise
Implement the functions depth(A), con(A) and atom(A) in Haskell.
2.5 Semantics of propositional logic
The semantics (= meaning) of a formula A is a truth value: either 0 (for “false”) or
1 (for “true”). The truth values 0 and 1 are also called boolean values. Of course,
the meaning of A depends on the meaning of the atomic propositions occurring in
A. Once the meaning of these atomic propositions is fixed, the meaning of A can be
computed according to the following truth tables of the propositional connectives.
>

1

⊥

0

x ¬x

0 1

1 0

x y x ∧ y

0 0 0

0 1 0

1 0 0

1 1 1

x y x ∨ y

0 0 0

0 1 1

1 0 1

1 1 1

x y x → y

0 0 1

0 1 1

1 0 0

1 1 1

These tables are to be understood as shorthand notations for the definitions of Boolean

functions associated with the propositional connectives:

H¬ : {0, 1} → {0, 1}, H∧, H∨, H→ : {0, 1}

2 → {0, 1}

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 13

For example,

H→(0, 0) = 1

H→(0, 1) = 1

H→(1, 0) = 0

H→(1, 1) = 1

In the following we fix a finite set of atomic propositions

A := {P1, . . . , Pn}

and consider only formulas containing atomic propositions from A.

2.5.1 Definition (Assignment)

An assignment is a mapping α : A → {0, 1}. Hence, α assigns to each atomic

proposition Pi ∈ A a truth value α(Pi) ∈ {0, 1}. An assignment α can also be viewed

as an array of boolean values (b1, . . . , bn) where α(Pi) = bi

for i ∈ {1, . . . , n}.

2.5.2 Definition (truth value of a formula)

We define the truth value of A under an assignment α

[[A]]α ∈ {0, 1}

by recursion on formulas:

[[Pi

]]α = α(Pi)

[[>]]α = 1

[[⊥]]α = 0

[[¬A]]α = H¬([[A]]α)

[[A G]]α = H([[A]]α, [[G]]α) for ∈ {∧, ∨,→}

2.5.3 Definition (substitution)

Let A, B be formulas and P an atomic proposition. By A[P := B] we denote the

formula obtained by substituting (that is, replacing) in A every occurrence of A by

B.

For example, if A = P → P and B = C ∧ P, then A[P := B] = C ∧ P → C ∧ P.

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 14

2.5.4 Exercise

Define A[P := B] by recursion on the formula A.

Solution.

P[P := B] = B

Q[P := B] = Q if Q is an atomic proposition different from P

>[P := B] = >

⊥[P := B] = ⊥

(¬A)[P := B] = ¬(A[P := B])

(A A

0

)[P := B] = A[P := B] A

0

[P := B] for ∈ {∧, ∨, →}

2.5.5 Substitution Theorem

Let A, B be formulas and P an atomic proposition. For every assignment α we have

[[A[P := B]]]α = [[A]]α

0

where α

0

is the assignment that is identical to α except that α

0

(P) := [[B]]α.

Proof. By induction on formulas. We refer to the recursive definition of substitution

given in the solution to Exercise 2.5.4.

[[P[P := B]]]α = [[B]]α = α

0

(P) = [[P]]α

0

If A is an atomic proposition different from P, then

[[A[P := B]]]α = [[A]]α = α(A) = α

0

(A) = [[A]]α

0

[[¬A[P := B]]]α = [[¬A[P := B]]]α by definition of substitution

= H¬([[A[P := B]]]α) by definition of the value of a formula

= H¬([[A]]α

0

) by induction hypothesis

= [[¬A]]α

0

by definition of the truth value of a formula

The proof for the remaining cases (conjunction, disjunction, . . . ) is similar.

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 15

Remark. The assignment α

0

in the Substitution Theorem is often denoted by α[P :=

b] where b := [[B]]α ∈ {0, 1}. In general the “updated” assignment α[P := b] is defined

as

α[P := b](P) := b

α[P := b](Q) := α(Q) if Q is an atomic proposition different from P

Remark. The Substitution Theorem says that the value of a formula which contains

a formula B as a subformula only depends on the value of B but not on its syntactic

form. The principle expressed by this theorem is called

Referential Transparency

Referential Transparency also holds for arithmetic expressions, derivations, types,

and many other types of syntax with a well defined semantics.

Referential Transparency is essential for any kind of reasoning about syntax and

semantics because it allows to reason in a modular way. For example, in a formula

A we may replace a subformula B by an equivalent formula B0 without changing the

meaning of A (this is shown in the Equivalence Theorem 2.6.8 below; what it means

for two formulas to be equivalent is defined in 2.6.4).

Referential Transparency does hold for functional programs, but generally not for

programs written in an imperative language such as C or Java. The reason is that

the Substitution Theorem may fail if the substituted program performs side effects.

Therefore, reasoning about imperative programs is more difficult than reasoning about

functional programs.

2.6 Logic gates and equivalence

In Sect. 2.5 we defined the meaning of the propositional connectives as certain boolean

functions H¬ : {0, 1} → {0, 1}, H∧, H∨, H→ : {0, 1}

2 → {0, 1}. Now we study boolean

functions in general.

2.6.1 Definition (logic gate, boolean function)

A logic gate or called boolean function or switch) of n arguments is a function

f : {0, 1}

n → {0, 1}

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 16

2.6.2 Exercise

Obviously, there exist only finitely many logic gates of n arguments. How many?

2.6.3 Definition (logic gate defined by a formula)

Since an assignment α can be viewed as an array of boolean values

α = (α(P0), . . . , α(Pn−1)) ∈ {0, 1}

n

the value of a formula A can also be viewed as a boolean function or logic gate

HA : {0, 1}

n → {0, 1}, HA(α) := [[A]]α

2.6.4 Definition (equivalence)

Usually, one is only interested in the logic gate a formula defines. Therefore, two

formulas A, B are called equivalent, in symbols, A ≡ B if they define the same logic

gate, that is, [[A]]α = [[B]]α for all assignments α.

2.6.5 Exercise

Let A, B be atomic formulas. Which of the following formulas are equivalent?

(a) A → ¬B

(b) ¬(B ∧ A)

(c) ¬B → A

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 17

Here is a list of important equivalences:

A ∧ B ≡ B ∧ A

(A ∧ B) ∧ C ≡ A ∧ (B ∧ C)

A ∨ B ≡ B ∨ A

(A ∨ B) ∨ C ≡ A ∨ (B ∨ C)

A ∧ (B ∨ C) ≡ (A ∧ B) ∨ (A ∧ C)

A ∨ (B ∧ C) ≡ (A ∨ B) ∧ (A ∨ C)

¬(A ∧ B) ≡ ¬A ∨ ¬B

¬(A ∨ B) ≡ ¬A ∧ ¬B

¬(A → B) ≡ A ∧ ¬B

¬¬A ≡ A

¬A ≡ A → ⊥

A → B ≡ ¬A ∨ B

A ∧ ¬A ≡ ⊥

A ∨ ¬A ≡ >

(A ∧ B) → C ≡ A → (B → C)

(A ∨ B) → C ≡ (A → C) ∧ (B → C)

(¬A) → B ≡ (¬B) → A

2.6.6 Exercise

Verify that the equivalences above do indeed hold by checking in each case that the

formula on left hand side and the formula on the right hand side have the same truth

value for all assignments.

2.6.7 Exercise

For each of the following formulas find an equivalent one which is shorter:

(a) A ∧ >

(b) A ∧ ⊥

(c) A ∨ >

(d) A ∨ ⊥

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 18

(e) A → A

(f) A → >

(g) > → A

(h) ⊥ → A

(i) ¬A → B

(j) A ∨ ¬A

(k) A ∧ ¬A

(l) ((A → B) → A) → A

2.6.8 Equivalence Theorem

Let A, A0

, B, B0 be formulas and P an atomic proposition.

If A ≡ A0 and B ≡ B0

, then A[P := B] ≡ A0

[P := B0

].

Proof. This is an easy consequence of the Substitution Theorem (detailed proof left

as an exercise for the lecture).

Remark. Since there are only finitely many logic gates of n arguments, but infinitely

many formulas with n atomic propositions, each logic gate can be defined by many

(in fact infinitely many) formulas. Finding for a given logic gate a shortest formula

defining it is an important and computationally difficult problem. We will later look

at some of the most important approaches to this problem.

2.7 Satisfiability and logical validity

2.7.1 Definition (satisfaction, model, tautology)

If [[A]]α = 1 we say α satisfies A, or α is a model of A, in symbols

α |= A

A formula A is called satisfiable if it has a model, otherwise it is unsatisfiable.

The satisfiability problem is the problem of deciding whether a formula is satisfiable.

A formula A is called a tautology or logically valid if it is satisfied by all assignments,

that is, [[A]]α = 1 for all assignments α.

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 19

Remarks.

• Speaking in terms of logic gates, for a formula A to be logically valid means

that the logic gate HA it defines is constant 1. This is also the same as saying

that A ≡ >.

• Similarly, for A to be a unsatisfiable means that the logic gate HA is constant

0 or that A ≡ ⊥.

• In particular, all tautologies are equivalent and all unsatisfiable formulas are

equivalent.

• Formulas A that are neither tautologies nor unsatisfiable (which is the case for

most formulas) define a logic gate HA which is not constant, that is, there are

assignments α, α0

such that [[A]]α = 1 and [[A]]α

0 = 0.

2.7.2 Exercise

Let A, B be atomic formulas. Which of the following formulas are satisfiable, unsatisfiable,

tautologies?

(a) A ∨ ¬A

(b) A ∧ ¬A

(c) B → ¬A

2.7.3 Exercise

Is the formula of the “John the teacher” example a tautology?

2.7.4 Theorem

A formula A is a tautology if and only if ¬A is unsatisfiable.

Proof. The proof has two parts.

1. Assume A is a tautology. We show that ¬A is unsatisfiable. Let α be an assignment.

We must show that α is not a model of ¬A, that is, [[¬A]]α = 0:

[[¬A]]α = H¬([[A]]α) by definition of the value of a negated formula

= H¬(1) because A is a tautology

= 0

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 20

2. Assume ¬A is unsatisfiable. We show that A is a tautology. Let α be an assignment.

We must show that α is a model of A, that is, [[A]]α = 1.

Since H¬(H¬(b)) = b for all b ∈ {0, 1} we have

[[A]]α = H¬(H¬([[A]]α))

= H¬([[¬A]]α) by definition of the value of a negated formula

= H¬(0) because ¬A is unsatisfiable

= 1

2.7.5 Theorem (closure of tautologies under arbitrary substitution)

Let A and B be formulas and P an atomic proposition.

If A is a tautology, then A[P := B] is a tautology.

Proof. This is another easy consequence of the Substitution Theorem. The proof is

left as an exercise for the student.

2.7.6 Exercise

(a) Does the converse of Theorem 2.7.5 hold? That is, is the following true?

If A[P := B] is a tautology, then A is a tautology.

(b) Does Theorem 2.7.5 still hold if “is a tautology” is replaced by “is satisfiable”?

(c) Does Theorem 2.7.5 still hold if “is a tautology” is replaced by “is unsatisfiable”?

Justify your answers.

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 21

3 Normal forms

In this chapter we introduce special classes of “normal forms” of formulas which

are built from restricted sets of logical connectives. Some of these classes are still

rich enough to define all logic gates, some are not. We will also look at compact

representations of logic gates that are frequently used in practical applications.

3.1 Conjunctive Normal Form (CNF)

3.1.1 Definition (literal)

A literal is an atomic proposition or the negation of an atomic proposition. Hence a

literal is of the form A (positive literal) or of the form ¬A (negative literal) where A

is an atomic proposition. We denote literals by L, L1, . . ..

3.1.2 Definition (literal, conjunctive normal form)

A formula is in conjunctive normal form, abbreviated CNF it is of the form

C1 ∧ . . . ∧ Cn

where each Ci

is a disjunction of literals. The formulas Ci are also called (disjunctive)

clauses.

3.1.3 Exercise (pigeon hole principle)

We assume that A1, A2, B1, B2, C1, C2 are atomic propositions. The following is an

example of a formula in CNF:

(A1 ∨ A2) ∧ (B1 ∨ B2) ∧ (C1 ∨ C2) ∧

(¬A1 ∨ ¬B1) ∧ (¬A1 ∨ ¬C1) ∧ (¬B1 ∨ ¬C1) ∧

(¬A2 ∨ ¬B2) ∧ (¬A2 ∨ ¬C2) ∧ (¬B2 ∨ ¬C2)

Is this formula satisfiable?

Hint: Think of of Ai as expressing that pigeon A sits in hole i, similarly for Bi

, Ci

.

Then the formula expresses that each of the three pigeons A, B, C sits in one of the

two holes, but no two pigeons sit in the same hole.

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 22

A formula is said to be in n-CNF, where n is a natural number, if it is in CNF and

every clause contains at most n literals. For example the pigeon hole formula above is

in 2-CNF. In general, the pigeon hole formula for n pigeons and m holes is in m-CNF.

Stephen Cook proved in 1971 1

that the satisfiability problem for formulas in 3-CNF

is NP-complete. This problem is also known as 3-SAT. On the other hand, the 2-

SAT problem, that is, the satisfiability problem for formulas in 2-CNF, is solvable in

polynomial time (for those interested in complexity theory: it is NL-complete, that

is, complete for all non-deterministic log-space problems).

3.2 Horn Formulas

Another important class of formulas are Horn Formulas. These are formulas in CNF

where each clause is a Horn clause, that is, a clause containing at most one positive

literal. Hence, a Horn Clause has the form

¬A1 ∨ . . . ∨ ¬An ∨ B or ¬A1 ∨ . . . ∨ ¬An

Horn Clauses can be written equivalently using conjunction and implication:

A1 ∧ . . . ∧ An → B or A1 ∧ . . . ∧ An → ⊥

Many problems can naturally expressed by Horn Formulas, for example, in logic

programming and in expert systems. The satisfiability problem for Horn Formulas

can be solved in polynomial time, in fact it is P-complete.

3.3 Disjunctive Normal Form (DNF)

3.3.1 Definition (disjunctive normal form

A disjunctive normal form, abbreviated DNF, is a formula of the form

D1 ∨ . . . ∨ Dn

where each Di

is a conjunction of literals. The formulas Di are also called conjunctive

clauses.

Formulas in DNF are less frequently used. However, they have the interesting property

that the satisfiability problem for them is trivial.

1Stephen A. Cook, The Complexity of Theorem-Proving Procedures, Proc. 3rd ACM Symp. Theory

of Computing, May 1971

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 23

3.3.2 Exercise (satisfiability for DNF)

Prove that satisfiability for DNF formulas is solvable in linear time.

It easy to see that CNF and DNF are complete classes of formulas, that is, they can

define every logic gate.

3.3.3 Theorem (completeness of CNF and DNF)

For every logic gate there exists a formula in CNF and also a formula in DNF defining

it.

Proof. We prove the theorem for DNF (for CNF the argument is similar and left as

an exercise).

g : {0, 1}

n → {0, 1} be a logic gate. We are looking for a formula F in DNF that

defines g, that is [[F]]α = g(α) for all assignments α. Recall that we identify the set

of assignments with the set {0, 1}

n of n-tuples of Boolean values by identifying an

assignment α with the tuple (α(P1), . . . , α(Pn)) ∈ {0, 1}

n

.

Recall that there exist 2n assignments. Let α1, . . . , αk a listing of those assignments

for which g returns 1. That is, g(α1) = . . . = g(αk) = 1, and g(α) = 0 for all other

assignments α.

We encode each αi by a conjunctive clause Di as follows:

Di

:= Li,1 ∧ . . . ∧ Li,n

where Li,j := Pj

if αi(Pj ) = 1 and Li,j := ¬Pj

if αi(Pj ) = 0.

For example, if αi = (0, 1, 0), then Di = ¬P1 ∧ P2 ∧ ¬P3.

Clearly, we have for any assignment α and any j ∈ {1, . . . , n}

[[Li,j ]]α = 1 ⇔ α(Pj ) = αi(Pj )

Therefore,

[[Di

]]α = 1 ⇔ for all j ∈ {1, . . . , n} [[Li,j ]]α = 1

⇔ for all j ∈ {1, . . . , n} α(Pj ) = αi(Pj )

⇔ α = αi

which means that Di does indeed properly encode αi

.

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 24

Now we define the formula we are looking for by

F := D1 ∨ . . . ∨ Dk

Clearly, F is in DNF. We show that F defines the logic gate g. Let α be an assignment.

We have to show [[F]]α = g(α), that is, [[F]]α = 1 ⇔ g(α) = 1.

[[F]]α = 1 ⇔ for some i ∈ {1, . . . , k} [[Di

]]α = 1

⇔ for some i ∈ {1, . . . , k} α = αi

⇔ g(α) = 1

3.3.4 Example

Consider the logic gate g of three variables defined by the truth table

x y z g(x, y, z)

0 0 0 0

0 0 1 1

0 1 0 0

0 1 1 0

1 0 0 1

1 0 1 0

1 1 0 0

1 1 1 0

There are two assignments where g returns 1: α1 := (0, 0, 1) and α2 := (1, 0, 0).

Hence D1 = ¬P1 ∧ ¬P2 ∧ P3 and D2 = P1 ∧ ¬P2 ∧ ¬P3, and the formula F in DNF

which defines g is

(¬P1 ∧ ¬P2 ∧ P3) ∨ (P1 ∧ ¬P2 ∧ ¬P3)

In general, we call a class of formulas complete if every logic gate can be defined by

a formula in the class. Theorem 3.3.3 shows that DNF and CNF are complete.

We call a set of logical connectives complete if the class of all formulas defined from

them is complete. In this definition we regard the logical constants ⊥ and > as

connectives.

For example, since DNF is complete, and formulas in DNF only use the connectives

∧, ∨, ¬, it follows, that the set {∧, ∨, ¬} is complete.

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 25

3.3.5 Theorem (Complete sets of connectives)

Each of the following sets of connectives is complete:

(a) {∧, ¬}

(b) {∨, ¬}

(c) {→, ⊥}

Proof. (a) Since {∧, ∨, ¬} is complete it suffices to show that ∨ can be defined by ∧

and ¬.

Recall that ¬¬A ≡ A and ¬(A ∨ B) ≡ ¬A ∧ ¬B. It follows

A ∨ B ≡ ¬¬(A ∨ B) ≡ ¬(¬A ∧ ¬B)

The proof of part (b) is similar and left as an exercise.

To prove (c), it suffices, by (b), to show that ¬ and ∨ can be defined by → and ⊥.

We have ¬A ≡ A → ⊥. Furthermore, since A → B ≡ ¬A ∨ B,

A ∨ B ≡ ¬¬A ∨ B ≡ ¬A → B

3.3.6 Exercise (Incomplete sets of connectives)

Show that none of the following sets of connectives is complete:

(a) {∧, ∨}

(b) {∧,→}

(c) {∧, ⊥}

Hint: For (a) and (b) show that the logic gate which is constant 0 is not definable.

For (c) show that every formula F definable by ∧ and ⊥ defines a monotone logic

gate, that is, if α ≤ α

0

, then [[F]]α ≤ [[F]]α

0 where the order on assignments is defined

pointwise. Use induction on formulas.

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 26

3.3.7 Exercise (Incompleteness of Horn Formulas)

Show that the class of Horn Formulas is not complete.

Hint: Show that if F is a Horn Formula and α1 and α2 are models of F (that is,

[[F]]α1 = [[F]]α1 = 1), then the assignment α, defined by α(A) := H∧(α1(A), α2(A)),

is also a model of F. Conclude from this that the logic gate H∨ cannot be defined by

a Horn Formula.

Remark. The hint above implies in particular that if a Horn Formula is satisfiable,

then it has a smallest model. This fact is fundamental for Logic Programming since

it implies that the standard proof strategy applied in Prolog is complete in the sense

that it can derive any facts that are a logical consequence of the given logic program.

The notions of “logical consequence” and “proof” will be explained in detail later.

Since, as we have seen in Exercise 3.3.2, the satisfiability problem for DNF is solvable

in linear time, it seems that the satisfiability problem for CNF can be efficiently

solved by translating CNF into DNF. That this translation is possible, follows from

the completeness of DNF. However, the obvious translation derived below, which is

derived from the de Morgan Law

(A ∨ B) ∧ (C ∨ D) ≡ (A ∧ C) ∨ (A ∧ D) ∨ (B ∧ C) ∨ (B ∧ D)

leads to an exponential blow up. Hence, in terms of the satisfiability problem for CNF

nothing is gained.

3.3.8 Definition (Translation of CNF into DNF)

Let F = C1 ∧ . . . ∧ Cn a formula in CNF, that is, each Ci

is a disjunctive clause. To

simplify matters we assume that all Ci contain the same number m of literals (this

can always be achieved by repeating literals). Hence

Ci = Li,1 ∨ . . . ∨ Li,m

Then the following formula G in DNF is equivalent to F:

G := _

α:{1,…,n}→{1,…,m}

(L1,α(1) ∧ . . . ∧ Ln,α(n))

Since there are mn

functions α : {1, . . . , n} → {1, . . . , m}, we clearly have

size(G) = O

2

size(F)

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 27

3.4 Binary Decision Diagrams

A decision tree where each internal nodes contains a question and the children of a

node are the answers to the question.

A fragment of a decision tree (courtesy Univ. T¨ubingen)

Decision trees can be represented as special formulas using a ternary logical connective

A → (B, C), to be read as “if A then B else C”. It can easily be defined using

implication, conjunction and negation:

A → (B, C) := (A → B) ∧ (¬A → C)

The decision tree shown in the image above can now be written as

picClear → (sound → (. . . , checkMB),screenBlank → (sound → (checkPC, . . .), . . .))

The truth table of the if-then-else connective · → (·, ·) is as follows

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 28

x y z x → (y, z)

0 0 0 0

0 0 1 1

0 1 0 0

0 1 1 1

1 0 0 0

1 0 1 0

1 1 0 1

1 1 1 1

3.4.1 Exercise

Define A → (B, C) as a formula in

(a) CNF

(b) DNF

3.4.2 Definition

The set of formulas in if-then-else normal form (INF) is inductively defined as follows:

(i) ⊥ and > are in INF.

(ii) if A is an atomic proposition and F, G are in INF, then A → (F, G) is in INF.

For example, if A, B are atomic proposition, then the formula

F := A → (B → (>, ⊥), B → (⊥, ⊥))

is in INF.

3.4.3 Exercise

(a) Draw the tree for the formula F above.

(b) Find a formula in INF that is equivalent to F but shorter.

(c) Find a formula that is equivalent to F but uses only one basic logical connective

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 29

Obviously, every logic gate can be defined by a decision tree and hence by a formula

in INF. The decision tree is not uniquely determined: it depends on the order of the

variables.

Decision trees given by formulas in INF may contain redundancies:

(1) Repeated variables (atomic propositions) in one branch: these can be eliminated

by replacing the subtree beginning at the lower occurrence by its left respectively

right subtree if that lower occurrence is in the left respectively subtree of the

upper occurrence of that variable.

(2) A node with two identical subtrees: Replace the node by that subtree.

(3) Identical subtrees that don’t have a common parent node: these can be avoided

by passing from a tree structure to graph structure, more precisely a directed

acyclic graph (DAG).

After carrying out these simplifications one arrives at a binary decision diagram

(BDD). If in addition one requires that on all paths in the dag the variables appear

in a fixed order one has a reduced ordered BDD (ROBDD). However, in the

literature ROBDDs are often referred to simply as BDDs.

3.4.4 Example

Consider the following decision tree:

A

0

✠

❅ 1

❅

❅❘

B

0 ✁

✁

✁☛

❆ 1

❆

❆❯

B

0 ✁

✁

✁☛

❆ 1

❆

❆❯

C

0 ✄

✄

✄✎

❈ 1

❈

❈❲

C

0 ✄

✄

✄✎

❈ 1

❈

❈❲

C

0 ✄

✄

✄✎

❈ 1

❈

❈❲

C

0 ✄

✄

✄✎

❈ 1

❈

❈❲

1 1 1 0 1 0 0 0

Simplification (1) does not apply since not variable occurs twice on the same path.

The leftmost subtree beginning with C has only 1s at its leaves. Hence, applying

simplification (2), it may be replaced by the leaf 0. Similarly, the rightmost subtree

beginning with C has only 0s at its leaves. Therefore we replace it by the leaf 1.

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 30

Carrying out these simplifications we obtain:

A

0

✠

❅ 1

❅

❅❘

B

0 ✁

✁

✁☛

❆ 1

❆

❆❯

B

0 ✁

✁

✁☛

❆ 1

❆

❆❯

1 C

0 ✄

✄

✄✎

❈ 1

❈

❈❲

C

0 ✄

✄

✄✎

❈ 1

❈

❈❲

0

1 0 1 0

Since the two remaining subtrees starting with C are identical we my identify them:

A

0

✠

❅ 1

❅

❅❘

B

0 ✁

✁

✁☛

❅ 1

❅

❅❘

B

0

✠

❆ 1

❆

❆❯

1 C

0 ✄

✄

✄✎

❈ 1

❈

❈❲

0

1 0

Finally, we identify all leaves with the same result:

A

0

✠

❅ 1

❅

❅❘

B

0

✄

✄

✄

✄

✄

✄✎

❅ 1

❅

❅❘

B

0

✠

1

❈

❈

❈

❈

❈

❈❲

C 0✏✏

✏✮✏✏

PP1PPPq

1 0

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 31

Most applications of BDDs rely on the fact that every logic gate is implemented by

exactly one ROBDD when the order of variables is fixed:

3.4.5 Canonicity Theorem for BDDs

For every logic gate g of n variables and every order of the n input variables there

exists exactly one reduced ordered BDD defining g.

3.4.6 Choosing the variable ordering

The ordering of variables in a BDD is crucial. There are logic gates whose sizes

of ROBDDs vary between linear and exponential, depending on the chosen order of

variables. For example, the ROBDD of the DNF

(A1 ∧ A2) ∨ (A3 ∧ A4) ∨ . . . ∨ (A2n−1 ∧ A2n)

has 2n + 2 nodes when the variable order A1, A2, A3, . . . , A2n−1, A2n is chosen. However,

for the order A1, A3, . . . , A2n−1, A2, A4, . . . , A2n the ROBDD has 2n+1 nodes.

Finding the optimal variable ordering is a hard problem. More precisely, this problem

is NP-hard (Sieling, 2002). Deciding whether a given order is optimal is NP-complete

(Bollig/Wegener, 1996).

3.4.7 Applications of BDDs

BDDs are heavily used in CAD software, equivalence and correctness testing of digital

circuits, synthesizing circuits and formal verification, in particular model checking.

BDDs where systematically studied first by Randal E. Bryant (Graph-based algorithms

for Boolean function manipulation. IEEE Transactions on Computers 8(C-

35), 1986).

There are several BDD packages that are able to efficiently construct and manipulate

BDDs, for example BuDDy (Kopenhagen), CUDD (Boulder).

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 32

3.4.8 Exercises

(a) Draw the truth table of the logic gate defined by the BDD (or decision tree) of

Example 3.4.4.

(b) Find a DNF defining the logic gate in (a).

(c) Find a CNF defining the logic gate in (a).

(d) Construct the decision tree for the logic gate in (a) with respect to the variable

ordering C, A, B.

(e) Transform the decision tree in (d) into an ROBDD.

(f) Construct ROBDDs for the formula

(A1 ∧ A2) ∨ (A3 ∧ A4) ∨ ∨(A3 ∧ A4)

with respect to the following variable orderings (see the discussion in Section

3.4.6):

(i) A1, A2, A3, A4, A5, A6

(ii) A1, A3, A5, A2, A4, A6

(g) Show that a program that transforms a CNF into the corresponding ROBDD

(with respect ot some given variable ordering) can be used to solve the satisfi-

ability problem for CNFs.

(h) What can you deduce from (g) regarding the computational complexity of computing

a reduced ordered BDD from a CNF (without using other complexity

results about ROBDDs)?

(i) Give the ROBDD for the formula given in Exercise 3.1.3 expressing the pigeon

hole principle for three pigeons and two holes.

(j) Write down a formula that expresses the pigeon hole principle for two pigeons

and two holes.

(k) Is the formula in (j) a Horn formula?

(l) Draw the truth table for the logic gate defined by the formula in (j).

(m) Give the ROBDD for the logic gate you found in (l).

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 33

4 The Compactness Theorem

The Compactness Theorem is a fundamental result in logic which has many applications,

for example in mathematics and automated theorem proving and satisfiability

testing. The theorem refers to the notion of satisfiability of a (typically infinite) set

of formulas. We first define this notion and related notions.

Since we consider infinite sets of formulas we also need to consider infinite assignments

which assign to infinitely many atomic propositions P1, P2, . . . truth values in {0, 1}.

Hence an assignment can either be

finite (as before), that is α = (α(P1), α(P2), . . . , α(Pn)) ∈ {0, 1}

n

,

or infinite, that is α = (α(P1), α(P2), . . .) ∈ {0, 1}

N.

4.0.9 Definition (Model, Satisfiability, for a set of formulas)

Let Γ be a set of formulas.

An assignment α is a model of Γ if [[F]]α = 1 for all formulas F ∈ Γ. One also says α

satisfies Γ and writes

α |= Γ

Γ is satisfiable if it has a model.

If a set of formulas has no model, then it is called unsatisfiable.

Warning: it is not true that a set of formulas Γ is satisfiable if and only if all formulas

in Γ are satisfiable! Give a counterexample.

4.0.10 Definition (Logical consequence)

A formula G is a logical consequence of a set of formulas Γ if every model of Γ is a

model of G, that is, for all assignments α, if α |= Γ, then [[G]]α. One also says Γ

logically implies G and writes

Γ |= G

Remarks.

1. A formula G is a tautology if and only ∅ |= G. Instead of ∅ |= G one also writes

just |= G.

2. For finite sets of formulas the new notions can be explained in terms of notions

introduced earlier:

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 34

{F1, . . . , Fn} is satisfiable if and only F1 ∧ . . . ∧ Fn is satisfiable,

{F1, . . . , Fn} |= G if and only F1 ∧ . . . ∧ Fn → G is a tautology.

4.0.11 Exercise

Let Γ be a set of formulas and G a formula. Show:

(a) Γ |= G if and only if Γ ∪ {¬G} is unsatisfiable.

(b) If Γ |= G and Γ is satisfiable, then G is satisfiable.

Solution.

(a) For the implication from left to right assume Γ |= G. We show that Γ ∪ {¬G} is

unsatisfiable. Let α be an assignment. We have to show α 6|= Γ ∪ {¬G}.

Case 1: α 6|= Γ. Then α 6|= Γ ∪ {¬G}.

Case 2: α |= Γ. Since we assumed that Γ |= G, it follows that α |= G, that is

[[G]]α = 1. Hence [[¬G]]α = 0, that is, α 6|= ¬G. Therefore α 6|= Γ ∪ {¬G}.

For the opposite implication we assume that Γ ∪ {¬G} is unsatisfiable. We show

Γ |= G. Assume α |= Γ. We have to show α |= G. Assume not, that is [[G]]α = 0.

Then [[¬G]]α = 1, that is α |= ¬G. Hence α |= Γ∪{¬G} contradicting the assumption

that Γ ∪ {¬G} is unsatisfiable.

(b) Assume that Γ |= G and Γ is satisfiable. We show that G is satisfiable. Since Γ

is satisfiable, there exists an assignment α such that α |= Γ. Since we assumed that

Γ |= G, it follows that α |= G. Hence G is satisfiable.

4.0.12 Exercises (Schoening, Ex. 7)

Give an example of a set Γ of 3 formulas such that Γ is unsatisfiable, but every

2-element subset of it is satisfiable.

Solution. Consider the 3 formulas A, B and ¬A ∨ ¬B where A and B are atomic.

It is easy to check that these have the desired property.

The essence of the proof of the Compactness Theorem is a theorem about binary

trees called K¨onig’s Lemma.

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 35

4.0.13 Definition (Binary Tree)

Let β ∈ {0, 1}

n and β

0 ∈ {0, 1}

m be finite assignments. We say β

0

is a restriction of

β, or β is an extension of β

0

, written β

0 ⊆ β, if m ≤ n and β

0

(Pi) = β(Pi) for all

i ∈ {1, . . . , m}.

A binary tree is a set T of finite assignments which is closed under restriction, that

is if β ∈ T and β

0 ⊆ α, then β

0 ∈ T. The elements of T are also called the nodes of

T. The length of a node is also called its depth.

An infinite path in a binary tree T is an infinite assignment α = (α(P1), α(P2), . . .)

such that for all n ∈ N the finite assignment α(n) := (α(P1), . . . , α(Pn)) is in T.

4.0.14 Theorem (K¨onig’s Lemma)

Every infinite binary tree has an infinite path.

Proof. Let T be an infinite binary tree.

We define an infinite assignment α = (α(P1), α(P2), . . .) as follows:

We set α(P1) := 0 if for infinitely many β ∈ T we have β(P1) = 0 (that is, the left

subtree of T is infinite), otherwise we set α(P1) := 1 (in that case the right subtree

of T is infinite, because T is infinite).

In any case there are infinitely many assignments β ∈ T with β(P1) = α(P1).

With a similar argument we define α(P2) ∈ {0, 1} such that there are infinitely many

assignments β ∈ T with β(P1) = α(P1) and β(P2) = α(P2).

Repeating this procedure over and over again we obtain an infinite assignment α =

(α(P1), α(P2), . . .) such that for each n there are infinitely many β ∈ T with β(Pi) =

α(Pi) for all i ∈ {1, . . . , n}. Since T is closed under restrictions it follows in particular

that α(n) ∈ T for all n ∈ N, that is, α is an infinite path in T. This completes the

proof.

Remarks.

1. The construction of the infinite path α is not effective since it is impossible to

decide effectively which subtree of an infinite binary tree is infinite. In fact, there

exists a computable infinite tree, the so-called Kleene tree, which has no infinite

computable path (it has, of course an infinite path, according to K¨onig’s Lemma, but

this path is not computable).

2. K¨onig’s Lemma holds more generally for finitely branching trees (instead of just

binary trees), that is, trees where every node has only finitely many children. K¨onig’s

Lemma fails for infinitely branching trees, even if we strengthen the hypothesis of T

being infinite to T being infinitely deep, that is, having arbitrarily deep nodes.

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 36

4.0.15 Theorem (Compactness Theorem)

Let Γ be a set of formulas such that every finite subset of Γ is satisfiable. Then Γ is

satisfiable.

Proof. If there are only finitely many atomic formulas occurring in Γ, then the

number of logic gates defined by some formula in Γ is finite. Therefore, we can select

finitely many formulas F1, . . . , Fn such that any such logic gate is defined by some

Fi

. Hence every F ∈ Γ is equivalent to some Fi

. By assumption, the set {F1, . . . , Fn}

has a model α which necessarily is then a model of Γ.

Hence, we consider now the interesting case that Γ is infinite, and there are infinitely

many atomic propositions occurring in Γ, say

P1, P2, . . .

For every natural number n we let Γn be the set of those formulas in Γ which contain

at most the atomic propositions P1, . . . , Pn.

By the argument above, each Γn is satisfiable (since there are only finitely many

atomic formulas occurring in Γn).

We set

Tn := {β ∈ {0, 1}

n

| β |= Γn}

Hence, Γn is the set of those finite assignments β that assign values to P1, . . . , Pn and

satisfy Γn.

Since Γn is satisfiable, Tn is non-empty for each n.

Let T be the union of all the Tn. Clearly, T is a tree, since if β = (b1, . . . , bn) ∈ Tn

and β

0 ⊆ β, say β

0 = (b1, . . . , bk) with k ≤ n, then β

0 ∈ Tk.

Since all the Tn are nonempty, T is infinite. By K¨onig’s Lemma, T has an infinite

path

α = (a1, a2, . . .)

This means that α(P1) = a1, α(P2) = a2, and so on, and α(n) = (a1, . . . , an) ∈ Tn.

Hence α(n) |= Γn and consequently α |= Γn for all n. Therefore, α |= Γ. This

completes the proof.

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 37

4.0.16 Corollary

(a) If a set of formulas is unsatisfiable, then it has a finite unsatisfiable subset.

(b) If Γ |= G, then Γ0 |= G for some finite subset Γ0 of Γ.

Proof.

(a) This is the contrapositive of the Compactness Theorem.

(b) Assume Γ |= G. By Exercise , Γ ∪ {¬G} is unsatisfiable. By part (a) above,

there exists a finite unsatisfiable subset Γ1 of Γ ∪ {¬G}. Set Γ0 := Γ1 ∩ Γ. Clearly,

Γ0 is finite. Furthermore, Γ1 ⊆ Γ0 ∪ {¬G}. Hence Γ0 ∪ {¬G} is unsatisfiable. By

Exercise it follows that Γ0 |= G.

4.0.17 Definition (Axiom system)

Let Γ be a set of formulas. A set of formulas Γ0 is an axiom system for Γ if Γ and Γ0

have the same models, that is for every assignment α,

α |= Γ if and only if α |= Γ0

A set of formulas is called finitely axiomatisable if it has a finite axiom system.

4.0.18 Exercise

Show that Γ0 is an axiom system for Γ if and only if (i) Γ |= G for every G ∈ Γ0 and

(ii) Γ0 |= F for every F ∈ Γ.

4.0.19 Exercise

Let Γ = {F1, F2, . . .} be an infinite set of formulas such that |= Fn+1 → Fn, but

6|= Fn → Fn+1 for all n ∈ N. Show that Γ is not finitely axiomatisable.

4.0.20 Example (Four Colour Theorem)

As an application of the Compactness Theorem we show that the Four Colour Theorem

for infinite maps or graphs can be derived from its finite version.

The (finite) Four Colour Theorem states that each finite map can be coloured by 4

colours such that neighbouring countries have different colours. The theorem was

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 38

proven in 1975 by Appel and Haken with the help of a computer. Since the proof

was too complex to be checked by a human, some doubts remained about its validity.

In 1997, Robertson, Sanders, Seymour, and Thomas gave a simpler proof which still

required help by a computer, and in 2005 the whole proof was formalized by Gonthier

in the interactive proof system Coq. Now the proof is widely accepted. The Four

Colour Theorem is the first theorem for which no proof without computer assistance

is known.

The finite Four Colour Theorem can be restated in terms of undirected planar graphs

(a graph is planar if it can be drawn in the plane without crossing edges): each finite

planar graph has a colouring of the nodes (or vertices) using not more than four

colours such that nodes connected by an edge have different colours.

The infinite Four Colour Theorem is the same statement, but for infinite planar

graphs.

To show that the infinite Four Colour Theorem holds, we express the statement by a

set of propositional formulas.

Let G be an infinite planar graph.

For every n ∈ N (representing a node) and every c ∈ {1, 2, 3, 4} representing the

4 colours) we introduce an atomic proposition Pn,c with the intended meaning that

node n has colour c.

We write down formulas that express that G has a 4-colouring.

1. Pn,1 ∨ Pn,2 ∨ Pn,3 ∨ Pn,4 for every n ∈ N (every node has a colour)

2. ¬(Pn,c ∧ Pn,d) for every n ∈ N and all c, d ∈ {1, 2, 3, 4}, c 6= d (a node can have

only one colour).

3. ¬(Pn,c ∧Pm,c) for all n, m ∈ N that are connected by an edge and c ∈ {1, 2, 3, 4}

(neighbouring nodes have different colours).

Let Γ be the set of all these formulas. Clearly Γ is satisfiable if and only if the graph

G admits a 4-colouring (and any satisfying assignment will define such a colouring).

By the Compactness Theorem it suffices to show that every finite subset of Γ is

satisfiable. Let Γ0 be such a finite subset. Let G0 the subgraph of G that is formed

by those nodes that are mentioned in Γ0. G0 is finite since Γ0 is finite. By the finite

Four Colour Theorem, G0 admits a 4-colouring which defines a satisfying assignment

for Γ0. Hence Γ0 is satisfiable.

This completes the proof.

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 39

5 Natural Deduction Proofs

We now study a system of simple proof rules for deriving tautologies, that is, logically

valid formulas. The famous Completeness Theorem, by the Austrian logician Kurt

G¨odel, states that this system of rules suffices to derive in fact all tautologies. G¨odel

proved this theorem for an extension of propositional logic, called first-order predicate

logic, which we will study later.

K G¨odel (1906-1978)

The proof calculus of Natural Deduction was first introduced by Gentzen and further

developed by Prawitz.

Compared with other proof calculi, e.g. Sequent Calculi, or Hilbert Calculi, Natural

Deduction has the advantage of being

• close to the natural way of human reasoning, and thus easy to learn;

• closely related to functional programming, and thus is particularly well suited

for program synthesis from proofs, which we will study later in the course.

In the following, A, B, C stand for arbitrary propositional formulas unless stated

otherwise. In order to simplify things we view from now on a negation, ¬A, as an

abbreviation for the implication A → ⊥. This is justified since the two formulas are

equivalent.

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 40

5.0.21 Definition (Sequent)

A sequent is a syntactic object

A1, . . . , Ak ` B

where A1, . . . , Ak, B are formulas. The idea of a sequent is to express that the assumptions

A1, . . . , Ak logically imply the conclusion B, that is, {A1, . . . , Ak} |= B

holds. A1, . . . , Ak are called the assumptions (or antecedent) and B the consequence

or succedent of the sequent. In the antecedent A1, . . . , Ak we ignore the order and

multiplicities of formulas, that is, we consider the antecedent as a set of formulas.

Hence, a more accurate notation for a sequent would be {A1, . . . , Ak} ` B, but it is

common to omit the curly braces. We often denote the antecedent of a sequent by

the letter Γ. Furthermore, we write Γ, A as a shorthand for Γ ∪ {A}.

5.0.22 Definition (Derivation)

A derivation (or formal proof ) is a finite tree (drawn correctly, that is, leaves on

top and root at the bottom), where each node is labelled by a sequent and a rule

according to figure 1 on page 41.

There is an Assumption rule, and for each logical connective there are two kinds of

rules:

Introduction rules, describing how to obtain a formula built from that connective;

Elimination rules, describing how to use a formula built from that connective.

The sequent at the root of a derivation is called the end sequent. The assumption

rule could be equivalently written

Γ ` A, provided A ∈ Γ

The assumptions of the end sequent of a derivation are called the free assumptions

of a derivation.

5.0.23 Definition (Classical provability)

A sequent Γ ` A is called derivable if there is a derivation with end sequent Γ ` A.

We also say that A is derivable from the assumptions Γ.

In the special case when Γ is empty, we say that A is derivable.

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 41

Assumption rule use

Γ, A ` A

Introduction rules Elimination rules

∧

Γ ` A Γ ` B

∧

+

Γ ` A ∧ B

Γ ` A ∧ B ∧

−

l

Γ ` A

Γ ` A ∧ B ∧

−

r

Γ ` B

→

Γ, A ` B

→+

Γ ` A → B

Γ ` A → B Γ ` A

→−

Γ ` B

∨

Γ ` A ∨

+

l

Γ ` A ∨ B

Γ ` B ∨

+

r

Γ ` A ∨ B

Γ ` A ∨ B Γ ` A → C Γ ` B → C ∨

−

Γ ` C

⊥

Γ ` ⊥ efq

Γ ` A

Γ ` ¬¬A raa

Γ ` A

Figure 1: The rules of natural deduction for propositional logic (sequent notation)

5.0.24 Examples

1. We begin with a derivation involving the conjunction introduction rule, ∧

+, and

the conjunction elimination rules, ∧

−

l

and ∧

−

r

.

use A ∧ B ` A ∧ B ∧

−

r

A ∧ B ` B

use A ∧ B ` A ∧ B ∧

−

l

A ∧ B ` A

∧

+

A ∧ B ` B ∧ A

2. If we add to the derivation in Example 1 an application of the implication introduction

rule, →+, we obtain a proof of A ∧ B → B ∧ A without assumptions:

use A ∧ B ` A ∧ B ∧

−

r

A ∧ B ` B

use A ∧ B ` A ∧ B ∧

−

l

A ∧ B ` A

∧

+

A ∧ B ` B ∧ A

→+

` A ∧ B → B ∧ A

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 42

3. In the following derivation of the formula A → (B → A) we use the rule →+ twice.

use A, B ` A

→+

A ` B → A

→+

` A → (B → A)

4. Next let us derive (A → (B → C)) → (A ∧ B → C). Here we use for the first time

the implication elimination rule, →−, also called modus ponens. The easiest way to

find the derivations is to construct it “bottom up”.

use A ∧ B → C, A, B ` A ∧ B → C

use A ∧ B → C, A, B ` A

use A ∧ B → C, A, B ` B

∧

+

A ∧ B → C, A, B ` A ∧ B

→−

A ∧ B → C, A, B ` C

→+

A ∧ B → C, A ` B → C

→+

A ∧ B → C ` A → (B → C)

→+

` (A ∧ B → C) → (A → (B → C))

At the latest at this point we notice that even fairly simple derivations as the one

above are very tedious to write down and difficult to read because so many formulas

are repeated over and over again in the assumptions of sequents.

The following observation leads to a much more concise notation for derivations that

largely avoids repetitions of formulas: The assumptions of a sequent in a derivation

consist of formulas that

are free assumptions, that is, occur in the antecedent of the end sequent of the

derivation, or

are “introduced” by the rule →+.

Furthermore, the only rule where an assumption is “used” is the assumption rule.

Hence, the assumptions may be notationally omitted provided

the free assumptions are listed with labels, and

the introduction of an assumption via →+ is indicated by a label.

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 43

When an assumption is used in an assumption rule one refers to the corresponding

label.

Following this idea, the previous derivation now reads:

u : A ∧ B → C

v : A w : B

∧

+

A ∧ B

→−

C

→+w B → C

→+v

A → (B → C)

→+u

(A ∧ B → C) → (A → (B → C))

Note that the (invisible) assumptions at each point of the derivation consists of the

formulas X for which there is a rule of the form

Y

→+z X → Y

below that point. Consequently, assumptions are allowed exactly if they are of the

form z : X for such z and X. In this example there were no free assumptions.

To display the derivation 1, we list the only free assumption

u : A ∧ B

and the derivation is

u : A ∧ B ∧

−

r

B

u : A ∧ B ∧

−

l

A

∧

+

B ∧ A

5.0.25 Exercise

Write the derivations 2 and 3 above using the new shorthand notation.

The derivation rules themselves can be rewritten in the new style as well, as shown

in figure 2 on page 44.

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 44

Assumption rule (*) u : A

Introduction rules Elimination rules

∧

A B

∧

+

A ∧ B

A ∧ B ∧

−

l

A

A ∧ B ∧

−

r

B

→ B

→+u A → B

A → B A

→−

B

∨

A ∨

+

l

A ∨ B

B ∨

+

r

A ∨ B

A ∨ B A → C B → C ∨

−

C

⊥

⊥ efq

A

¬¬A raa A

Figure 2: The rules of natural deduction for propositional logic (short notation)

The correctness condition (*) for an instance u : A of the assumption rule is that

u : A is among the listed free assumptions, or

below the occurrence of that assumption rule there is a rule of the form

B

→+u A → B

In the following, when writing down concrete derivations, we will always work with

the shorthand notation.

5. In order to familiarise ourselves with the disjunction introduction rules, ∨

+

l

, ∨

+

r

,

and the disjunction elimination rule, ∨

−, we derive B ∨ A from the assumption

u : A ∨ B

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 45

u : A ∨ B

v : A ∨

+

r

B ∨ A

→+v A → B ∨ A

w : B ∨

+

l

B ∨ A

→+w B → B ∨ A

∨

−

B ∨ A

6. As a slightly more complicated example we derive (one half of) one of de-Morgan’s

laws, A ∧ (B ∨ C) → (A ∧ B) ∨ (A ∧ C).

u : A ∧ (B ∨ C)

∧

−

r

B ∨ C

u : A ∧ (B ∨ C)

∧

−

l

A v : B

∧

+

A ∧ B ∨

+

l

(A ∧ B) ∨ (A ∧ C)

→+v

B → (A ∧ B) ∨ (A ∧ C)

u : A ∧ (B ∨ C)

∧

−

l

A w : C

∧

+

A ∧ C ∨

+

r

(A ∧ B) ∨ (A ∧ C)

→+w

C → (A ∧ B) ∨ (A ∧ C)

∨

−

(A ∧ B) ∨ (A ∧ C)

→+u

A ∧ (B ∨ C) → (A ∧ B) ∨ (A ∧ C)

7. Finally, we turn our attention to the rules concerning absurdity, ⊥, namely exfalso-quodlibet,

efq, and reductio-ad-absurdum, raa. Recall that ¬A is shorthand for

A → ⊥, and therefore ¬¬A stands for (A → ⊥) → ⊥. We derive Peirce’s law

(A → B) → A ` A:

u : ¬A

(A → B) → A

u : ¬A v : A

→−

⊥ efq

B

→+v A → B

→−

A

→−

⊥

→+u

¬¬A raa A

8. The rule ex-falso-quodlibet is weaker than reductio-ad-absurdum in the sense that

the former can be obtained from the latter: From the assumption ⊥ we can derive any

formula A without using ex-falso-quodlibet (but using reductio-ad-absurdum instead):

⊥

→+u

(A → ⊥) → ⊥

raa A

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 46

5.0.26 Definition

Let Γ be a (possibly infinite) set of formulas and A a formula.

Γ `c A : ⇔ Γ0 ` A is derivable for some finite subset Γ0 of Γ.

(A is derivable from Γ in classical logic)

Γ `i A : ⇔ Γ `c A with a derivation not using the rule reductio-adabsurdum.

(A is derivable from Γ in intuitionistic logic)

Γ `m A : ⇔ Γ `c A with a derivation using neither the rule reductio-adabsurdum

nor the rule ex-falso-quodlibet.

(A is derivable from Γ in minimal logic)

5.1 Soundness and completeness

The soundness and completeness theorems below state that the logical inference rules

introduced above precisely capture the notion of logical consequence.

5.1.1 Soundness Theorem

If Γ `c A then Γ |= A.

Proof. The theorem follows immediately from the following statement which can be

easily shown by induction on derivations:

For every set of formulas Γ and every formula A,

if Γ `c A then α |= A for all models α of Γ

.

Whilst the soundness theorem is not very surprising, because it just states that the

inference rules are correct, the following completeness theorem proved by G¨odel,

states that the logical inference rules above in fact capture all possible ways of correct

reasoning.

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 47

5.1.2 Completeness Theorem

If Γ |= A then Γ `c A.

In words: If A is a logical consequence of Γ (i.e. A is true in all models of Γ), then

this can be formally derived by the inference rules of natural deduction.

It is important that the Completeness Theorem holds for other logics as well. In

particular it holds for first-order predicate logic which we will study later.

For propositional logic, the Completeness Theorem is an easy consequence of the

Compactness Theorem:

5.1.3 Exercise

Sketch a proof of the Completeness Theorem for Propositional Logic using the Compactness

Theorem and the fact that every formula is provably equivalent to a formula

in CNF.

Solution.

Assume Γ |= A. By the Compactness Theorem, there are finitely many formulas

B1, . . . , Bn ∈ Γ such that {B1, . . . , Bn} |= A. Hence B1 ∧. . .∧Bn → A is a tautology.

It suffices to show that B1 ∧ . . . ∧ Bn → A is derivable in classical logic, that is

`c B1 ∧ . . . ∧ Bn → A. Because then {B1, . . . , Bn} ` A is derivable and consequently

Γ `c A.

Therefore, in order to complete the proof of the Completeness Theorem, it suffices

to show that all propositional tautologies are derivable in classical logic. This can

be done as follows: Any formula F can be transformed into an equivalent formula in

Conjunctive Normal Form, that is,

F ≡ C1 ∧ . . . ∧ Cn

where each Ci

is a disjunctive clause. Moreover the equivalence can be formally

proven, that is,

`c F ↔ C1 ∧ . . . ∧ Cn

To construct the derivation one uses formal proofs of the de-Morgan laws and laws

expressing implication in terms of disjunction and negation. This is a bit tedious,

but easy.

Now, F is a tautology if and only if every Ci

is a tautology. Hence, we further

reduced the problem to showing that all disjunctive clauses which are tautologies are

derivable.

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 48

So, take any disjunctive clause

C = L1 ∨ . . . ∨ Lk

Clearly, C is a tautology if and only if it contains two complementary literals, say

Li = A and Lj = ¬A where A is an atomic proposition. But A ∨ ¬A is derivable in

classical logic. Hence C is derivable.

The following consequences of the Completeness Theorem refer to the notion of consistency.

5.1.4 Definition (Formal consistency)

A (possibly infinite) set of formulas Γ is called formally consistent if Γ 6`c ⊥, that

is there is no (classical) derivation of ⊥ from assumptions in Γ.

In other words: A set of formulas is consistent if and only if no contradiction can be

derived from it.

5.1.5 Lemma

A set of formulas Γ is satisfiable if and only if Γ 6|= ⊥.

Proof. “⇒”: Assume that Γ is satisfiable. This means that there exists an assignment

α such that α |= Γ. Clearly α 6|= ⊥ (since [[⊥]]α = 0). Therefore, Γ 6|= ⊥.

“⇒”: Assume Γ 6|= ⊥. This means it is not true that for all assignments α such that

α |= Γ it follows that α |= ⊥. Therefore, there exists an assignment α such that

α |= Γ, but α 6|= ⊥. In particular, there exists an assignment such that α |= Γ, which

means that Γ is satisfiable.

5.1.6 Satisfiability Theorem

A set of formulas is formally consistent if and only it is satisfiable.

Proof. Let Γ be a set of formulas. Using Lemma 5.1.5 above we can rephrase the

statement we have to prove equivalently as

Γ 6`c ⊥ if and only if Γ 6|= ⊥

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 49

or, equivalently, negating both sides, as

Γ `c ⊥ if and only if Γ |= ⊥.

But this is the Soundness and and Completeness Theorem (8.2.1, 8.2.2) for A := ⊥.

Remark. If Γ is satisfiable (that is Γ 6|= ⊥) one often also says that Γ is semantically

consistent. Hence the Satisfiability Theorem can also be phrased as follows:

A set of formulas is formally consistent if and only if it is semantically consistent.

Since formal consistency and semantic consistency coincides one often omits the predicate

“formal” and “semantic” and just speaks of “consistency”.

5.1.7 Exercise

Prove the Compactness Theorem from the Soundness and Completeness Theorem.

Solution. Let Γ be a set of formulas such that every finite subset of Γ is satisfiable.

By Lemma 5.1.5, this means that for every finite subset Γ0 of Γ we have Γ0 6|= ⊥.

By the Soundness Theorem 8.2.1, it follows that for every finite subset Γ0 of Γ we

have Γ0 6`c ⊥. Therefore Γ 6`c ⊥, since if we had a derivation of ⊥ from Γ, this

derivation would be finite and would hence use only finitely many formulas in Γ as

assumptions which would mean that Γ0 `c ⊥ for some finite subset Γ0 of Γ. From the

Completeness Theorem 8.2.2 it follows that Γ 6|= ⊥ which, by Lemma 5.1.5, means

that Γ is satisfiable.

5.1.8 Exercises

Derive the following formulas

1. Minimal logic

(a) (A → ¬B) → (B → ¬A)

(b) (A → (B → C)) → ((A → B) → (A → C))

(c) A → ¬¬A

(d) ¬(A ∧ ¬A)

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 50

(e) (A ∧ (B ∨ C)) ↔ ((A ∧ B) ∨ (A ∧ C))

(f) (A ∨ B) → ¬(¬A ∧ ¬B)

(g) ¬(A ↔ ¬A)

(f) A → ¬(A∧B) → (C → B) → ¬C (essentially the “John the teacher” example)

2. Intuitionistic logic

(a) (A ∧ ¬A) → C

(b) (¬A ∨ B) → (A → B)

(c) (¬¬A → A) ↔ ((¬A → A) → A)

(d) (A ∨ B) → (¬A → B)

3. Classical logic

(a) ¬¬A → A

(b) (¬A → A) → A

(c) A ∨ ¬A

(d) ¬(¬A ∧ ¬B) → (A ∨ B)

(e) ¬(¬A ∨ ¬B) → (A ∧ B)

(f) ¬(A → B) → A ∧ ¬B

Sample Solution: We give a derivation for 3 (f):

u : (A → B) → ⊥

v : A → ⊥ w : A

→−

⊥ efq

B

→+ w : A A → B

→−

⊥

→+ v : A → ⊥ (A → ⊥) → ⊥

raa A

u : (A → B) → ⊥

x : B →+ y : A

A → B

→−

⊥

→+ x : B B → ⊥ ∧

+

A ∧ (B → ⊥) →+ u : (A → B) → ⊥

((A → B) → ⊥) → (A ∧ (B → ⊥))

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 51

6 Resolution

This chapter follows closely the text book [6].

Resolution is a proof method used in logic programming and automatic theorem

proving. A resolution proof shows that a given formula in CNF is unsatisfiable.

Resolution is defined for formulas in CNF only, and it has only one proof rule.

Recall that a literal is an atomic proposition, or the negation of an atomic proposition.

For any literal L we define the dual literal L as

L :=

¬A if L = A (an atomic proposition)

A if L VA

By a clause we mean in the following always a disjunctive clause, that is, a disjunction

of literals. It is convenient to view a clause simply as a (finite) set of literals (connected

implicitly by ∨).

We consider a formula in conjunctive normal form (CNF) as a (finite) set of clauses

(connected implicitly by ∧). Hence, in the following “set of clauses” and “CNF

formula” means the same.

6.0.9 Example

An example of a CNF formula written in set notation is

F := {{A, E, ¬B}, {¬A, B, C}, {¬A, ¬D, ¬E}, {A, D}}

where A, B, C, D, E are atomic formulas. This means

F = (A ∨ E ∨ ¬B) ∧ (¬A ∨ B ∨ C) ∧ (¬A ∨ ¬D ∨ ¬E) ∧ (A ∨ D)

The set notation implies that one ignores the order of literals and clauses as well as

any duplications of literals or clauses. For example, the CNF formula

{{A, B}, {A, ¬B, A}, {¬B, ¬B, A}}

is the same as

{{¬B, A}, {B, A}}

6.0.10 Definition (Resolvent)

Let C1 and C2 be (disjunctive) clauses. A clause R is called a resolvent of C1 and C2

if there is a literal L ∈ C1 such that L ∈ C2 and

R = (C1 \ {L}) ∪ (C2 \ {L})

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 52

6.0.11 Exercise

Compute all resolvents that can be generated from clauses in the CNF formula F of

Example 6.0.9.

A clause is called a unit clause if it contains exactly one literal. If we resolve two

unit clauses, say {A} and {¬A}, we obtain the empty clause as resolvent which

corresponds to an empty disjunction. Since the empty disjunction is, by convention,

defined as the false proposition, we denote it by ⊥.

Since the empty clause is unsatisfiable, any CNF formula containing the empty clause

is unsatisfiable.

6.0.12 Resolution Lemma

Let F be a CNF formula. Let R be a resolvent of two clauses in C1 and C2 in F.

Then F and F ∪ {R} are equivalent.

Proof. One can either prove this by showing directly that F and F ∪ {R} have the

same value for all assignments, or give a formal proof that F implies R. For the latter

it suffices to show that, for arbitrary formulas C, D, A we have that C ∨A and D∨¬A

together imply C ∨ D. This holds even in intuitionistic logic:

C ∨ A, D ∨ ¬A `i C ∨ D

We leave this as an exercise.

6.0.13 Definition

For a set F of clauses we define

Res(F) = F ∪ {R | R is a resolvent of two clauses in F}

Furthermore, we set

Res0

(F) = F

Resn+1(F) = Res(Resn

(F))

and, finally,

Res∗

(F) = [

n≥0

Resn

(F)

6.0.14 Exercise

For F = {{A, ¬B, C}, {B, C}, {¬A, C}, {B, ¬C}, {¬C}} determine Resn

(F) for n =

0, 1, 2, . . ..

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 53

6.0.15 Exercise

Prove that for every CNF formula F there is a k ≥ 0 such that

Resk

(F) = Resk+1(F) = . . . = Res∗

(F)

6.0.16 Resolution Theorem

A CNF formula is unsatisfiable if and only if Res∗

(F) contains the empty clause.

Proof. The proof has two parts.

First, we show correctness (or soundness): We assume that ⊥ ∈ Res∗

(F) and show

that F is unsatisfiable. Since ⊥ ∈ Res∗

(F), there exists some n such that ⊥ ∈

Resn

(F). Hence Resn

(F) is unsatisfiable. By the Resolution Lemma (6.0.12) we have

F ≡ Res1

(F) ≡ Res2

(F) ≡ . . . ≡ Resn

(F)

Hence F is unsatisfiable.

For completeness, one assumes that F is unsatisfiable and shows ⊥ ∈ Res∗

(F). The

proof is by induction on the number of different atomic propositions in F. Details of

the somewhat technical proof can be found in [6].

From the Resolution Theorem the following algorithm can be derived that decides

satisfiability for a given input formula in CNF

Input: a CNF formula F

repeat

G := F;

F := Res(F);

until F contains the empty clause, or F = G;

if F contains the empty clause then F is unsatisfiable,

otherwise F is satisfiable

In some cases this algorithm can come up with a decision quite fast, but there do exist

examples for unsatisfiable formulas where exponentially many resolvents have to be

generated before the until condition of the algorithm is satisfied (cf. A. Urquhart.

Hard examples for resolution. Journal of the Association of Computing Machinery

34(1987):209-219).

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 54

6.0.17 Definition (Resolution Derivation)

A resolution derivation or (proof ) of the empty clause from a clause set F is a sequence

C1, C2, . . . , Cm of different clauses such that

Cm is the empty clause, and for every i = 1, . . . , m, Ci either is a clause in F

or a resolvent of two clauses Ca, Cb with a, b ≤ i.

6.0.18 Theorem (Soundness and Completeness for Resolution Derivations)

A clause set F is unsatisfiable if and only if a resolution derivation of the empty clause

from F exists.

Proof. This is a direct consequence of the Resolution Theorem (6.0.16). One simply

keeps track of the clauses involved in generating the empty clause.

6.0.19 Example

Let F = {{A, B, ¬C}, {¬A}, {A, B, C}, {A, ¬B}}. We prove that F is unsatisfiable

by the following resolution derivation:

C1 = {A, B, ¬C} (clause in F)

C2 = {A, B, C} (clause in F)

C3 = {A, B} (resolvent of C1, C2)

C4 = {A, ¬B} (clause in F)

C5 = {A} (resolvent of C3, C4)

C6 = {¬A} (clause in F)

C7 = ⊥ (resolvent of C5, C6)

6.0.20 Example (Linear resolution for Horn Clauses)

Show that the following modification of the resolution calculus is sound and complete

for the class of Horn formulas:

Derive a resolvent from two clauses only if one of them is a unit clause and drop

the other clause.

Conclude that the satisfiability problem for Horn formulas is solvable in quadratic

time.

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 55

7 Predicate logic

In propositional logic we can only talk about the truth and falsity of propositions. If

we want to talk about objects and their relationships, or if we want to say “for all

objects” or “there exists an object” we need a more expressive logic called predicate

logic.

For example, the statement

“every positive number has a positive square root”

can be written in more detail (but still informally)

“for every number x, if 0 < x, then there exists y such that 0 < y and x = y ∗ y”
As a formula in predicate logic this reads
∀x (0 < x → ∃y (0 < y ∧ x = y ∗ y))
The subformulas 0 < x, 0 < y, and x = y ∗y are called atomic formulas. The infix notation
is syntactic sugar for <(0, x), <(0, y), and x = ∗(y, y). < is a predicate symbol
(denoting the less-than relation) and ∗ is a function symbol (denoting multiplication).
Before studying the precise syntax, semantics and proof calculus for predicate logic
we discuss, informally, some simple examples in order to familiarise ourselves with
the new concepts.
7.0.21 Exercise
Consider the following statements
A If the train is late and there is no taxi at the station, then I’m late for the meeting.
B the train is late
C I’m not late for the meeting.
D There is a taxi at the station.
Using the atomic formulas
LT The train is late.
T S(x) Taxi x is at the station
LM I’m late at the meeting
Formalise the statement A ∧ B ∧ C → D in predicate logic and prove it.
Discuss whether the use of predicate logic was necessary in this example.
October 13, 2015 CSC375/CSCM75 Logic for Computer Science 56
7.0.22 Exercise
Consider the following statements
A All people living in Snowdonia speak Welsh.
B John doesn’t speak Welsh.
C John doesn’t live in Snowdonia.
Using the atomic formulas
S(x) Person x lives in Snowdonia.
W(x) Person x speaks Welsh.
Formalise the statement A ∧ B → C in predicate logic and give an informal proof of
it.
Try to isolate a new proof rule that was necessary to complete the proof.
7.0.23 Exercise
Formalise the statement
Every female who has the same father as me, is a sister of mine.
in two different ways: (a) using a relation for father-ship, (b) using a function symbol
for denoting the father of a person.
7.0.24 Exercise
Formalise the following statements:
(a) An American astronaut is well trained.
(b) An American astronaut has landed on the moon.
7.1 Syntax of predicate logic
Predicate logic deals not only with propositions, but also with objects and relations
between objects. The syntactic entities to denote objects are called terms the syntactic
entities to denote relations are called predicates. Terms are built from variables
and function symbols. Each function symbol has an arity which specifies what sort of
arguments it accepts and what sort of results it produces. Similarly, each predicate
symbol has an arity which specifying what sort of arguments it accepts.
October 13, 2015 CSC375/CSCM75 Logic for Computer Science 57
7.1.1 Definition
A many-sorted signature (signature for short), is a triple Σ = (S, F,P) such
that the following conditions are satisfied.
• S is a nonempty set. The elements s ∈ S are called sorts.
• F is a set whose elements are called function symbols, and which are of the
form
f : s1 × . . . × sn → s,
where n ≥ 0 and s1, . . . , sn, s ∈ S.
s1 × . . . × sn → s is called arity of f, with argument sorts s1, . . . , sn and
target sort s.
Function symbols are also called operations or functions.
A function symbol of the form c : → s (i.e. n = 0) is called a constant of sort
s. For constants we often use the shorter notation c : s (i.e. we omit the arrow).
• P is a set whose elements are called predicate symbols, and which are of the
form
P : (s1 × . . . × sn),
where n ≥ 0 and s1, . . . , sn ∈ S.
(s1 × . . . × sn) is called arity of P, with argument sorts s1, . . . , sn.
Predicate symbols are also called predicates.
Note that atomic propositions can be viewed as predicate symbols of zero arguments.
In this sense, propositional logic can be viewed as a part of predicate
logic.
A sort s is to regarded as a name of a set, so it is similar to a type in programming. A
function symbol f : s1 × . . . × sn → s is a name for a function on the sets denoted by
the sorts s1, . . . , sn, s. This will be made more precise when we discuss the semantics
of predicate logic.
In logicians jargon a signature is also called a many-sorted first-order language and
by the “arity” of a function or predicate symbol one also means just the number of
arguments it takes. If the arity is 1, 2, or 3, one speaks of unary, binary, or ternary
function or predicate symbols.
October 13, 2015 CSC375/CSCM75 Logic for Computer Science 58
7.1.2 Example
Consider the signature Σ := (S, F,P), where
S = {nat}
F = {0: nat, +: nat × nat → nat}
P = {<: (nat × nat), ≤: (nat × nat)}
The function symbols of a signature Σ can be used to build formal expressions, called
terms, which denote elements of a given structure interpreting the signature Σ (the
notion of a structure will be made precise later).
7.1.3 Definition
Let Σ = (S, F,P) be a signature, and let X = (Xs)s∈S be a family of pairwise disjoint
sets. The elements of Xs are called variables of sort s. We define terms and their
sorts by the following rules.
(i) Every variable x ∈ Xs is a term of sort s.
(ii) Every constant c in Σ of sort s is a term of sort s.
(iii) If f : s1 × . . . × sn → s is a function symbol in Σ, and t1, . . . , tn are (previously
defined) terms of sorts s1, . . . , sn, respectively, then the formal expression
f(t1, . . . , tn)
is a term of sort s.
The set of all terms of sort s is denoted by T(Σ, X)s.
A term is closed if it doesn’t contain variables, i.e. is built without the use of rule
(i).
The set of all closed terms of sort s is denoted by T(Σ)s. Clearly T(Σ)s = T(Σ, ∅)s.
7.1.4 Example
For the signature Σ of example 7.3.3 and the set of variables X := {x, y} the following
are examples of terms in T(Σ, X):
x
October 13, 2015 CSC375/CSCM75 Logic for Computer Science 59
0
0 + y (which stands for +(0, y))
(0 + x) + y (which stands for +(+(0, x), y))
((0 + 0) + (x + x) (which stands for +(+(0, 0), +(x, x))
0 + (0 + (0 + 0)) (which stands for +(0, +(0, +(0, 0)))
The second and the last of these terms are closed.
In a similar way as terms are syntactic constructs denoting objects, formulas are
syntactic construct to denote propositions.
7.1.5 Definition
The set of formulas over a signature Σ = (S, F,P) and a set of variables X = (Xs)s∈S
is defined inductively by the following rules.
(i) > and ⊥ are formulas.

(ii) t1 = t2 is a formula, called equation, for each pair of terms t1, t2 ∈ T(Σ, X) of

the same sort.

(iii) If P : (s1 × . . . × sn) is a predicate symbol in P and t1, . . . , tn are terms of sorts

s1, . . . , sn, the P(t1, . . . , tn) is a formula.

(iv) If A and B are formulas then (A ∧ B), (A ∨ B) and (A → B) are formulas.

(v) If A is a formula then (∀x A) and (∃x A) are formulas for every variable x ∈ X,

called universal quantification (‘for all’) and existential quantification

(‘exists’), respectively.

Formulas over a signature Σ are also called Σ-formulas

A free occurrence of a variable x in a formula A is an occurrence of x in A which

is not in the scope of a quantifier ∀x or ∃x. We let FV(A) denote the set of free

variables of A, i.e. the set of variables with a free occurrence in A. A formula A is

closed if FV(A) = ∅.

We set

L(Σ, X) := {A | A is a Σ-formula , FV(A) ⊆ X}

and use the abbreviation

L(Σ) := L(Σ, ∅),

i.e. L(Σ) is the set of closed Σ-formulas.

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 60

7.1.6 Remarks and Notations

1. Formulas as defined above are usually called first-order formulas, since we

allow quantification over object variables only. If we would also quantify over

set variables we would obtain second-order formulas.

2. A formula is quantifier free, qf for short, if it doesn’t contain quantifiers.

3. A formula is universal if it is of the form ∀x1 . . . ∀xn A where A is quantifier

free.

4. The basic formulas are ⊥, equations t1 = t2 and formulas of the form P(t1, . . . , tn).

for the latter we often write more briefly P(~t).

7.1.7 Abbreviations

As in the case of propositional logic we omit brackets as long as this does not lead to

ambiguities. We let the quantifiers bind stronger than the logical connectives, hence

∀x A → B stands for (∀x A) → B. Furthermore, we use the following abbreviations:

Formula Abbreviation

A → ⊥ ¬A (negation)

∀x1∀x2 . . . ∀xn A ∀x1, x2, . . . , xnA

∃x1∃x2 . . . ∃xn A ∃x1, x2, . . . , xn A

∀x1, . . . , xnA, where {x1, . . . , xn} = FV(A) ∀ A (closure of A)

(A → B) ∧ (B → A) A ↔ B (equivalence)

7.1.8 Examples

A :≡ x = 0 → y + x = y

B :≡ ∃y (x = y → ∀z x = z)

C :≡ ∀x (0 ≤ x)

A is quantifier free. C is universal. A and C are universal. FV(A) = {x, y}, FV(B) =

{x}.

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 61

7.1.9 Definition (Substitution)

By A[x := t] we denote the result of substituting in the formula A every free occurrence

of the variable x by the term t, possibly renaming bound variables in A in order

to avoid variable clashes.

For example,

(∀x (0 < x → y < x + y) ∧ ∀y (¬y < 0))[y := x + 1]
= ∀z (0 < z → x + 1 < x + (x + 1)) ∧ ∀y (¬y < 0)
Note that we renamed the bound variable x by the fresh variable z. For z to be
“fresh” means that z occurs neither free in the formula nor does it occur in the term
t := x + 1. Note also that the occurrence of y in the subformula ¬y < 0 is not
substituted because it is bound by ∀y .
7.2 Formalising statements in predicate logic
In this section we look at further examples of informal statements and their formalisations
in predicate logic. Since we haven’t yet introduced the precise semantics
of predicate logic (this will be done in Sect. 7.3) we have to rely on an intuitive
understanding of the meaning of formulas.
7.2.1 Example (Students)
Formalise the following statements in predicate logic:
(a) All students submitted Coursework 1 or Coursework 2.
(b) All students who submitted Coursework 2 also submitted Coursework 1.
(c) Not all students attended all lectures.
(d) No student skipped all lectures.
(e) No two students attended exactly the same lectures.
Use the following signature, i.e. variables, constants function symbols and predicates,
in your formalisation:
October 13, 2015 CSC375/CSCM75 Logic for Computer Science 62
x, y students
l lectures
CW1(x) student x submitted Coursework 1
CW2(x) student x submitted Coursework 2
A(x, l) student x attended lecture l
Solution:
(a) ∀x (CW1(x) ∨ CW2(x))
(b) ∀x (CW2(x) → CW1(x))
The remaining questions are left as an exercise for the lecture.
(c)
(d)
(e)
7.2.2 Example (Maths)
Formalise the following statements in predicate logic:
(a) The equation x
2 + 1 = 0 has no solution.
(b) Exactly the non-negative numbers have a square root.
(c) √
2 is irrational.
(d) A square root of an integer is either an integer or irrational.
Use the following signature:
x, y, z real numbers
0, 1 constants 0 and 1
+, ∗ addition and multiplications (used infix)
Q(x) x is a rational number
Z(x) x is an integer
x ≤ y x is less or equal y (used infix)
You may use abbreviation, for example 2 := 1 + 1, x
2
:= x ∗ x, etc.
October 13, 2015 CSC375/CSCM75 Logic for Computer Science 63
Solution:
(a) ¬∃x(x
2 + 1 = 0)
(b) ∀x (∃y(y
2 = x) ↔ 0 ≤ x)
The remaining questions are left as an exercise for the lecture.
(c)
(d)
7.2.3 Example (Processes)
Consider a system of processes and two binary relations R and S on on processes.
If R(x, y) holds, we say x reduces y, or y is a reduct of x.
If S(x, y) holds, we say y simulates x.
The relation R is called
- deterministic if every process can be reduced in at most one way;
- confluent if whenever x reduces to y and z, then y and z have a common reduct;
- deadlock free if every process can be reduced;
- normalising if every process reduces to a process that cannot be reduced further.
The relation S is called a bisimulation for R if whenever y simulates x, then all
reducts of x are simulated by some reduct of y and all reducts of y simulate some
reduct of x.
(a) Formalise each of the properties of R described informally above.
(b) Formalise the property that S is a bisimulation for R.
Solution:
(a) - deterministic: ∀x ∀y ∀z (R(x, y) ∧ R(x, z) → y = z).
The remaining questions are left as an exercise for the lecture.
- confluent:
- deadlock free:
- normalising:
(b)
October 13, 2015 CSC375/CSCM75 Logic for Computer Science 64
7.3 Semantics of predicate logic
In order to determine the truth value of a formula F in propositional logic it was
sufficient to have an assignment α prescribing to every atomic proposition A a truth
value α(A) ∈ {0, 1}. For predicate logic we need in addition a universe, that is a set
of objects, and assignments must prescribe meanings to
constants as elements of the universe
function symbols as functions on the universe
predicate symbols as boolean valued functions on the universe
7.3.1 Definition (Structure)
A structure M = ((Ms)s∈S, α) for a signature Σ = (S, F,P) is given by the following:
• For each sort s in S a nonempty set Ms, called the carrier set of sort s.
• An assignment α that assigns
– to each constant c : s in F an element α(c) ∈ Ms,
– to each function symbol f : s1 × . . . × sn → s in F a function
α(f): Ms1 × . . . × Msn → Ms
– For each predicate symbol P : (s1×. . .×sn) in P a boolean valued function
(also called predicate or relation)
α(P): Ms1 × . . . × Msn → {0, 1}
7.3.2 Remarks
1. In the definition of a signature (7.1.1) the expression f : s1 ×. . .×sn → s is meant
symbolically, i.e. ‘×’ and ‘→’ are to be read as uninterpreted symbols. In the definition
of a structure (7.3.1), however, we used the familiar mathematical notation for settheoretic
functions to communicate by α(f): Ms1 × . . . × Msn → Ms a semantical
object, namely a function α(f) whose domain is the cartesian product of the sets Msi
and whose range is Ms.
2. It is common to call the elements α(c) constants. Hence the word ‘constant’ has a
double meaning. Conversely, the function symbols of a signature are often just called
’functions’. Whenever we use such slightly ambiguous names it will be clear from the
context what is meant.
October 13, 2015 CSC375/CSCM75 Logic for Computer Science 65
3. We will often identify the semantics of a predicate symbol, α(P): Ms1 × . . . ×
Msn → {0, 1}, with the set {~a | ~a ∈ Ms1 × . . . × Msn
, α(P)(~a) = 1} ⊆ Ms1 × . . . ×
Msn
.
4. By a Σ-structure we mean a structure for the signature Σ.
5. Signatures with more than one sort are sometimes called many-sorted signatures
and structures without predicate symbols are sometimes called algebras. This is the
case for example in the book
[10] J V Tucker, Theory of Programming Languages, Course Notes, UWS, 2005.
7.3.3 Example
Consider the signature Σ := (S, F,P), where
S = {nat}
F = {0: nat, +: nat × nat → nat
P = ≤: (nat × nat)}
We follow [10] and display signatures in a box:
Signature Σ
Sorts nat
Constants 0: nat
Functions +: nat × nat → nat
Predicates ≤: (nat × nat)
The Σ-structure M of natural numbers with 0, and addition and the predicate ≤ is
given by:
the carrier set N = {0, 1, 2, . . .}, that is,
Mnat = N;
the constants 0, that is,
α(0) = 0;
the operation of addition on N, that is,
α(+)(n, m) = n + m;
October 13, 2015 CSC375/CSCM75 Logic for Computer Science 66
the relation < ⊆ N × N, that is
α(≤) = {(n, m) ∈ N × N | n ≤ m} (that is, α(≤)(n, m) = 1 iff n ≤ m).
Again we use the more readable box notation [10]
Structure M
Carriers N
Constants 0
Functions +: N × N → N
Predicates ≤ ⊆ N × N
For the signature Σ we may also consider another structure, M0 = (M0
nat, α0
) with
carrier M0
nat = N+ := N \ {0} (= {1, 2, 3, 4, . . .}), the constant 1, multiplication
restricted to N+, and the divisibility relation · | ·. Hence we have
the carrier set N+ = {1, 2, . . .}, that is,
M0
nat = N+;
the constants 1, that is,
α
0
(0) = 1;
the operation of multiplication on N+, that is,
α
0
(∗)(n, m) = n ∗ m;
the relation · | · ⊆ N × N, that is
α
0
(≤) = {(n, m) ∈ N+ × N+ | n divides m}.
Written in box notation:
Structure M0
Carriers N+
Constants 1
Functions ∗: N+ × N+ → N+
Predicates ·|· ⊆ N+ × N+
October 13, 2015 CSC375/CSCM75 Logic for Computer Science 67
7.3.4 Remarks
1. The display of signatures and structures via boxes has to be handled with some
care. If, for example, in the box displaying the signature Σ in example 7.3.3 we would
have exchanged the order of the sorts nat and boole, we would have defined the same
signature. But then the box displaying the structure M would not be well-defined,
since then the sort boole would be associated with the set N and nat with B, and
consequently the arities of the operations of Σ would not fit with the operations of
the structure M.
Therefore: When displaying signatures and structures in boxes order matters.
7.3.5 Definition (Semantics of terms)
Let M = ((Ms)s∈S, α) be a structure for the signature Σ = (S, F,P), and let X =
(Xs)s∈S a set of variables.
A variable assignment η : X → M is a function assigning to every variable x ∈ Xs
an element η(x) ∈ Ms.
Given a variable assignment η : X → M we define for each term t ∈ T(Σ, X)s its
value
tM,η ∈ Ms
by the following rules.
(i) xM,η := η(x).
(ii) cM,η := α(c).
(iii) f(t1, . . . , tn)M,η := α(f)(t
M,η
1
, . . . , tM,η
n
).
For closed terms t, i.e. t ∈ T(Σ) (= T(Σ, ∅)) the variable assignment η and rule (i)
are obsolete and we write tM instead of tM,η
.
7.3.6 Exercise
Let Σ be the signature of example 7.3.3 and M the Σ-structure of the natural numbers
with zero, addition and the ‘less-or-equal’ relation. Write down Σ-formulas expressing
in M the following statements.
(a) x is an even number.
(b) x is greater than y.
October 13, 2015 CSC375/CSCM75 Logic for Computer Science 68
(c) x is the average of y and z.
In order to precisely declare the semantics of a formula we define what it means for
a formula to be true in a structure.
7.3.7 Definition (Semantics of formulas)
In order to define the semantics of formulas we need the semantics of the logical
connectives and quantifiers. The semantics of the logical connectives (∧, ∨, →) was
defined in Section 2.5 by the boolean functions
H∧, H∨, H→ : {0, 1}
2 → {0, 1}
It remains to define
H∃, H∀ : P({0, 1}) → {0, 1}
where P+({0, 1}) is the set of all non-empty subsets of {0,1}, i.e. P+({0, 1}) =
{{0}, {0, 1}, {1}}. We define for every X ∈ P({0, 1})
H∃(X) :=
1 if 1 ∈ X
0 otherwise
H∀(X) :=
1 if 0 6∈ X
0 otherwise
Hence,
H∃(X) = 1 iff there exists x ∈ X such that x = 1
H∀(X) = 1 iff for all x ∈ X, x = 1
As truth tables this reads
X H∃(X)
{0} 0
{0, 1} 1
{1} 1
X H∀(X)
{0} 0
{0, 1} 0
{1} 1
7.3.8 Definition (Semantics of formulas)
Let Σ = (S, F,P) be a signature, X = (Xs)s∈S a set of variables, M = ((Ms)s∈S, α)
a Σ-structure, η : X → M a variable assignment, and A ∈ L(Σ, X) a Σ-formula.
For every formula A of predicate logic we define the value
[[A]](M, η) ∈ {0, 1}
October 13, 2015 CSC375/CSCM75 Logic for Computer Science 69
[[>]](M, η) = 1

[[⊥]](M, η) = 0

[[t1 = t2]](M, η) =

1 if t

M,η

1 = t

M,η

2

0 otherwise

[[P(t1, . . . , tn)]](M, η) = α(P)(t

M,η

1

, . . . , tM,η

1

)

[[A B]](M, η) = H([[A]](M, η), [[B]](M, η)) for ∈ {∧, ∨, →}

[[∀x A]](M, η) = H∀({[[A]](M, η[x := a]) | a ∈ Ms})

[[∃x A]](M, η) = H∃({[[A]](M, η[x := a]) | a ∈ Ms})

where in the last two cases the variable x is assumed to be of sort s. We also define

M, η |= A :⇔ [[A]](M, η) = 1

which is to be read ‘A is true in M under η’, or ‘M, η is a model of A’.

The following Lemma is an immediate consequence of the definition above. In many

textbooks the clauses of the Lemma are used to define the semantics of formulas.

7.3.9 Lemma

(i) M, η 6|= ⊥, i.e. M, η |= ⊥ does not hold.

(ii) M, η |= t1 = t2 iff t

M,η

1 = t

M,η

2

.

(iii) M, η |= P(t1, . . . , tn) iff α(P)(t

M,η

1

, . . . , tM,η

n

) = 1.

(iv) M, η |= A ∧ B iff M, η |= A and M, η |= B.

M, η |= A ∨ B iff M, η |= A or M, η |= B.

M, η |= A → B iff M, η |= A implies M, η |= B (i.e. M, η 6|= A or

M, η |= B).

(v) M, η |= ∀x A iff M, η[x := a] |= A for all a ∈ Ms (provided x is of

sort s).

M, η |= ∃x A iff M, η[x := a] |= A for at least one a ∈ Ms (provided

x is of sort s).

For closed Σ-formulas A the variable assignment is obviously redundant and we write

M |= A

for M, η |= A. For a set Γ of closed Σ-formulas we say that the Σ-structure M is a

model of Γ, written

M |= Γ,

if M |= A for all A ∈ Γ.

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 70

7.4 Logical consequence, logical validity, satisfiability

We may now make precise what it means that a formula A is a logical consequence

of a set of formulas.

7.4.1 Definition (Logical consequence)

Let Γ be a set of closed formulas and A a closed formula. We say that A is a logical

consequence of Γ, or Γ logically implies M, written

Γ |= A,

if A is true in all models of Γ, that is,

M |= Γ implies M |= A, for all Σ-structures M

7.4.2 Definition (Logical validity)

A closed Σ-formula A is said to be (logically) valid, written

|= A,

if A is true in all Σ-structures, that is M |= A for all Σ-structures M. Valid formulas

is also called a tautologies.

Obviously, A is valid if and only if it is a logical consequence of the empty set of

formulas.

7.4.3 Definition (Satisfiability)

A set of closed Σ-formulas Γ is called satisfiable if it has a model, that is, there

exists a Σ-structure M in which all formulas of Γ are true (M |= Γ).

7.4.4 Exercise

Show that validity and satisfiability are related by the following equivalences:

A valid ⇔ {¬A} unsatisfiable (that is, not satisfiable)

A satisfiable ⇔ {¬A} not valid

October 13, 2015 CSC375/CSCM75 Logic for Computer Science 71

7.4.5 Theorem (A Church)

It is undecidable whether or not a closed formula is valid.

This theorem can be proven by reducing the halting problem to the validity problem

(i.e. coding Turing machines into logic).

Although, by Church’s Theorem, the validity problem is undecidable, there is an

effective procedure generating all valid formulas (technically: the set of valid formulas

is recursively enumerable). We will study such a generation process in the next

chapter.

7.4.6 Examples

Consider a signature with the sorts nat and boole and the operation <: nat × nat →
boole. Then the formula
∃x ∀y (x < y) → ∀y ∃x (x < y)
is a tautology. The formula
∀x, y (x < y → ∃z (x < z ∧ z < y))
is satisfiable, but not a tautology (why?). Set
Γ := {∀x ¬(x < x), ∀x.y.z (x < y ∧ y < z → x < z)}
Then the formula
A :≡ ∀x, y (x < y → ¬y < x)
is a logical consequence of Γ, that is, Γ |= A.
8 Natural deduction proofs for predicate logic and
G¨odel’s Completeness Theorem
In addition to the rules for propositional logic, the Natural Deduction calculus has
introduction and elimination rules for the quantifiers:
October 13, 2015 CSC375/CSCM75 Logic for Computer Science 72
Introduction rules Elimination rules
∀
Γ ` A(x)
∀
+
Γ ` ∀x A(x)
(*) Γ ` ∀x A(x)
∀
−
Γ ` A(t)
∃
Γ ` A(t)
∃
+
Γ ` ∃x A(x)
Γ ` ∃x A(x) Γ ` ∀x (A(x) → B)
∃
−
Γ ` B
(**)
Figure 3: The rules of natural deduction for quantifiers (sequent notation)
(*) The ∀
+ rule is subject to the so-called variable condition: x must not occur free
in Γ.
(**) The ∃
− rule is subject to the restriction that x must not be free in B.
The rules for quantifiers can also written in the short notation where the assumptions
Γ are implicit:
Introduction rules Elimination rules
∀
A(x)
∀
+
∀x A(x)
(*) ∀x A(x)
∀
−
A(t)
∃
A(t)
∃
+
∃x A(x)
∃x A(x) ∀x (A(x) → B)
∃
−
B
(**)
Figure 4: The rules of natural deduction for quantifiers (short notation)
The variable condition for ∀
+ now reads:
(*) x must not occur free in in any free assumption valid at that point.
8.0.7 Examples
1. In the following derivation of ∀y A(y + 1) from ∀x A(x) we use the for-all introduction
rule, ∀
+, and the for-all elimination rule, ∀
−:
October 13, 2015 CSC375/CSCM75 Logic for Computer Science 73
∀x A(x)
∀
−
A(x + 1)
∀
+
∀x A(x + 1)
In the application of ∀
+ the variable condition is satisfied, because x is not free in
∀x A(x).
2. Find out what’s wrong with the following ‘derivations’.
∀y(x < 1 + y)
∀
−
x < 1 + 0
∀
+
∀x(x < 1 + 0)
∀ x(∀y(x < y + 1) → x = 0)
∀
−
∀y(y < y + 1) → y = 0 ∀y(y < y + 1)
→−
y = 0
∀
+
∀y(y = 0)
3. The exists introduction rule, ∃
+, and the exists elimination rule, ∃
− are used in
the following derivation.
u : ∀x (x − 1) + 1 = x
∀
−
(x − 1) + 1 = x
∃
+
∃y(y + 1 = x)
∀
+
∀x ∃y(y + 1 = x)
→+u
∀x ((x − 1) + 1 = x) → ∀x ∃y(y + 1 = x)
4. Let us derive from the assumptions ∃x A(x) and ∀x(A(x) → B(f(x))) the formula
∃y B(y):
∃x A(x)
∀x(A(x) → B(f(x)))
∀
−
A(x) → B(f(x)) u : A(x)
→−
A(f(x))
∃
+
∃y B(y)
→+u
A(x) → ∃y B(y)
∀
+
∀x (A(x) → ∃y B(y))
∃
−
∃y B(y)
We see that in the application of ∀
+ the variable condition is satisfied, because x is
not free in ∃y B(y).
October 13, 2015 CSC375/CSCM75 Logic for Computer Science 74
8.1 Equality rules
So far we only considered the Natural Deduction rules for logic without equality. Here
are the rules for equality:
Reflexivity refl t = t
Symmetry s = t
sym
t = s
Transitivity r = s s = t
trans
r = t
Compatibility s1 = t1 . . . sn = tn comp
f(s1, . . . , sn) = f(t1, . . . , tn)
for every operation f of n arguments.
8.1.1 Example
Let us derive from the assumptions ∀x, y (x + y = y + x) and ∀x (x + 0 = x) the
formula ∀x, y ((0 + x) ∗ y = x ∗ y):
∀x ∀y (x + y = y + x)
∀
−
∀y (0 + y = y + 0)
∀
−
0 + x = x + 0
∀x (x + 0 = x)
∀
−
x + 0 = x
trans 0 + x = x
refl y = y
comp
(0 + x) ∗ y = x ∗ y
∀
+
∀y ((0 + x) ∗ y = x ∗ y)
∀
+
∀x ∀y ((0 + x) ∗ y = x ∗ y)
October 13, 2015 CSC375/CSCM75 Logic for Computer Science 75
8.1.2 Definition
The notions of minimal, intuitionistic and classical derivability for predicate logic
completely analogous to the propositional case (Definition 5.0.26), but for formulas
in predicate logic and for derivations composed from propositional rules and the new
rules for quantifiers and equality:
Let Γ be a (possibly infinite) set of formulas and A a formula, all in predicate logic.
Γ `c A : ⇔ Γ0 ` A is derivable for some finite subset Γ0 of Γ.
(A is derivable from Γ in classical logic)
Γ `i A : ⇔ Γ `c A with a derivation not using the rule reductio-adabsurdum.
(A is derivable from Γ in intuitionistic logic)
Γ `m A : ⇔ Γ `c A with a derivation using neither the rule reductio-adabsurdum
nor the rule ex-falso-quodlibet.
(A is derivable from Γ in minimal logic)
8.1.3 Lemma
Let t(x) be a term possibly containing the variable x, and let r, s be terms of the
same sort as x. Then
r = s `m t(r) = t(s)
Proof. Induction on t(x).
If t(x) is a constant or a variable different from x, then t(r) and t(r) are the same
term t. Hence the assertion is r = s `m t = t which is an instance of the reflexivity
rule.
If t(x) is the variable x then t(r) is r and t(s) is s, and the assertion becomes r =
s `m r = s which is an instance of the assumption rule.
Finally, consider t(x) of the form f(t1(x), . . . , tn(x)). By induction hypothesis we may
assume that we already have a derivation of r = s `m ti(r) = ti(s) for i = 1, . . . , n.
One application of the compatibility rule yields the required sequent.
October 13, 2015 CSC375/CSCM75 Logic for Computer Science 76
8.1.4 Lemma
Let A(x) be a formula possibly containing the variable x, and let r, s be terms of the
same sort as x. Then:
r = s `m A(r) ↔ A(s)
Proof. Induction on the formula A(x).
If A(x) is an equation, say, t1(x) = t2(x), then we have to derive
r = s `m t1(r) = t2(r) ↔ t1(s) = t2(s)
By Lemma 8.1.3 we have already derivations of
r = s `m t1(r) = t1(s) and r = s `m t2(r) = t2(s)
It is now easy to obtain the required derivation using the symmetry rule and the
transitivity rule. We leave this as an exercise to the reader.
If A(x) is a compound formula we can use the induction hypothesis in a straightforward
way.
8.2 Soundness and completeness
The soundness and completeness theorems for predicate logic are analogous to the
propositional case. However, now the notion of a model is much more complex. While
in the propositional case a model was just a vector of Booleans (assigning truth values
to atomic propositions), in the case of predicate logic a model is a first-order structure
which is a rather complex object.
8.2.1 Soundness Theorem for predicate logic
If Γ `c A then Γ |= A.
Proof. The proof is easy and similar to the propositional case, but taking into
account the additional rules for quantifiers .
8.2.2 Completeness Theorem for predicate logic (G¨odel)
If Γ |= A then Γ `c A.
October 13, 2015 CSC375/CSCM75 Logic for Computer Science 77
In words: If A is a logical consequence of Γ (i.e. A is true in all models of Γ), then
this can be formally derived by the inference rules of natural deduction for predicate
logic.
The proof of this theorem is completely different from the corresponding proof for
the propositional case and beyond the scope of this course. Detailed expositions can
be found in any textbook on Mathematical Logic.
The notion of formal consistency is analogous to the propositional case:.
8.2.3 Definition (Formal consistency for predicate logic)
A (possibly infinite) set of formulas Γ is called formally consistent if Γ 6`c ⊥, that
is there is no (classical) derivation of ⊥ from assumptions in Γ.
In other words: A set of formulas Γ is formally consistent if and only if no contradiction
can be derived from Γ.
8.2.4 Satisfiability Theorem for predicate logic
Every consistent set of formulas has a model.
Proof. As for the propositional case.
Another important consequence of G¨odel’s Completeness Theorem is the fact that all
logically valid formulas can be effectively enumerated.
8.2.5 Enumerability Theorem for predicate logic
The set of all logically valid formulas is recursively enumerable, that is, there is an
effective procedure producing all logically valid formulas.
Proof. By the Soundness and Completeness Theorem, the logically valid formulas
are exactly the provable ones. Hence, it suffices to systematically generate all proofs.
The next theorem shows that effective enumerability for logically valid formulas in
predicate logic is the best one can achieve.
October 13, 2015 CSC375/CSCM75 Logic for Computer Science 78
8.2.6 Theorem (A Church)
It is undecidable whether or not a closed formula of predicate logic is logically valid.
This theorem can be proven by reducing the halting problem to the validity problem
(i.e. coding Turing machines into logic).
Another proof is by showing that Post’s correspondence problem, which is known to
be undecidable, can be encoded by predicate logic.
Recall that for propositional logic the situation is different: logical validity for formulas
in propositional logic is decidable. More precisely, the set of logically valid
propositional formulas is co-NP complete, since its complement is the set of propositional
formulas A for which ¬A is satisfiable, which is NP complete.
9 Axioms and rules for natural numners and other
data types
For many common data types we can formulate axioms describing their characteristic
features. We will only treat the (unary) natural numbers. Similar axioms could be
stated for binary number, lists, finite trees etc., more generally for freely generated
data types.
9.0.7 Peano Axioms
The following axioms and rules where introduced (in a slightly different form) by
Peano to describe the structure of natural numbers with zero and the successor function
(we write t + 1 for the successor of t).
In the following the terms s, t and the variable x are supposed to be of sort nat.
October 13, 2015 CSC375/CSCM75 Logic for Computer Science 79
G Peano (1858 - 1932)
Peano 1 peano1
0 6= t + 1
Peano 2 peano2
s + 1 = t + 1 → s = t
Induction A(0) ∀x (A(x) → A(x + 1))
ind ∀x A(x)
9.0.8 Remark
In applications there will be further axioms describing additional operations on the
natural numbers. Examples are, the equations defining addition and multiplication
by primitive recursion:
x + 0 = x
x + (y + 1) = (x + y) + 1
x ∗ y = 0
x ∗ (y + 1) = x ∗ y + x
At least as famous as the Completeness Theorem for Predicate Logic is G¨odel’s Incompleteness
Theorem for the theory of natural numbers given by the Peano Axioms:
October 13, 2015 CSC375/CSCM75 Logic for Computer Science 80
9.0.9 Incompleteness Theorem (K G¨odel)
Every consistent and effectively presented system of axioms and rules extending the
Peano Axioms is incomplete, that is, there exists a formula A such that neither A
nor its negation ¬A is provable.
In particular, there exists a true statement about that natural numbers that is not
provable.
Similar Incompleteness Theorems hold for lists and trees and other data types that
can (in principle) be encoded by natural numbers.