LogicMaths/CompScience-2SmallQuestions

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(A B) 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.

Unlike most other websites we deliver what we promise;

  • Our Support Staff are online 24/7
  • Our Writers are available 24/7
  • Most Urgent order is delivered with 6 Hrs
  • 100% Original Assignment Plagiarism report can be sent to you upon request.

GET 15 % DISCOUNT TODAY use the discount code PAPER15 at the order form.

Type of paper Academic level Subject area
Number of pages Paper urgency Cost per page:
 Total: