Propositional Logic

Steffen Hölldobler
International Center for Computational Logic
Technische Universität Dresden, Germany
and
North Caucasus Federal University, Russian Federation

I Syntax

I Semantics

I Equivalence and Normal Forms

I Proof Procedures

I Satisfiability Testing

I Properties

Steffen Hölldobler
Propositional Logic 1
Syntax – Formulas

I Definition 3.1 An alphabet Σ is a finite or countably infinite set.

The elements of this set are called symbols.
Without loss of generality (Wlog) we assume that Λ 6∈ Σ.

I Definition 3.2 Let Σ be an alphabet. The set of words (or strings) over Σ
is denoted by Σ∗ and is the smallest set satisfying the following conditions:
1 Λ ∈ Σ∗ .
2 If w ∈ Σ∗ and a ∈ Σ, then aw ∈ Σ∗ .
Λ is called empty word or empty string.

I Example Let Σ = {1, 2}. We can form the following words:

Λ, 1Λ, 2Λ, 11Λ, 12Λ, 21Λ, 22Λ, 111Λ, . . . .

Steffen Hölldobler
Propositional Logic 2
The Alphabet of Propositional Logic

I Definition 3.3 An alphabet of propositional logic consists of

. a (countably) infinite set R = {p1 , p2 , . . .} of propositional variables,

. the set {¬/1, ∧/2, ∨/2, → /2, ↔ /2} of connectives, and
. the set {(, )} of special characters.

I We will occasionally use other letters to denote variables.

I Indices are sometimes omitted; but sometimes R = N.

I Propositional variables are also called nullary relation symbols.

I Different alphabets of propositional logic differ in R.

Steffen Hölldobler
Propositional Logic 3
Propositional Formulas

I Definition 3.4
A (propositional) atomic formula, briefly called atom, is a propositional variable.

I Definition 3.5 Let R be a set of propositional variables. The set of

propositional formulas is the smallest set L(R) of strings over R, the
connectives and the special symbols with the following properties:
1 If F is an atomic formula, then F ∈ L(R).
2 If F ∈ L(R), then ¬F ∈ L(R).
3 If ◦ is a binary connective and F , G ∈ L(R), then (F ◦ G) ∈ L(R).

I Does such a smallest set exist?

. There are sets, which satisfy all properties.

. The intersection of such sets satisfies the properties too.
. The smallest set is the intersection of all sets satisfying the properties.

I Notation A (possibly indexed) denotes an atom,

F , G, H (possibly indexed) denote propositional formulas.

Steffen Hölldobler
Propositional Logic 4
Structural Induction

I How can we prove properties of sets of formulas?

I Theorem 3.6 (Principle of structural induction)

Every propositional formula has a property E,
if the following conditions are met:
1 Induction Base Every atom has property E.
2 Induction Steps
If F has property E, then ¬F has property E as well.
If ◦ is a binary connective, and F , G have property E,
then (F ◦ G) has property E as well.

I Proof Let E be the set of all formulas satisfying E.

. E ⊆ L(R).
. E satisfies the three conditions of Definition 3.5.
. Because L(R) is the smallest set satisfying these conditions,
L(R) ⊆ E must hold. qed

Steffen Hölldobler
Propositional Logic 5
Structural Recursion

I How can we define functions acting on formulas?

I Theorem 3.7 (Principle of structural recursion)

Let M be an arbitrary set and let the following functions be given:
. fooR : R → M,
. foo¬ : M → M,
. foo◦ : M × M → M for ◦ ∈ {∧, ∨, →, ↔}.
Then there is exactly one function foo : L(R) → M
satisfying the following conditions:

1 Recursion base foo(A) = fooR (A) for all A ∈ R.

2 Recursion steps
foo(¬G) = foo¬ (foo(G)) for all G ∈ L(R).
foo((G1 ◦ G2 )) = foo◦ (foo(G1 ), foo(G2 )) for all G1 , G2 ∈ L(R).

I Proof Exercise

Steffen Hölldobler
Propositional Logic 6
Structural Recursion – Example

I M = N.

I foo1R (A) = 0 for all A ∈ R.

I foo1¬ (X ) = X for all X ∈ M.

I foo1◦ (X , Y ) = X + Y + 1 for all ◦ ∈ {∧, ∨, →, ↔} and all X , Y ∈ M.

I We obtain:

 0 if F is an atom,
foo1 (F ) = foo1 (G) if F is of the form ¬G,
foo1 (G1 ) + foo1 (G2 ) + 1 if F is of the form (G1 ◦ G2 ).


I Often foo1R , foo1¬ and foo1◦ are not explicitely specified.

I foo is a function symbol of a meta language.

Steffen Hölldobler
Propositional Logic 7
Structural Recursion – Another Example

I The set of positions or occurrences in F



 ∅ if F is an atom,
{1π | π ∈ pos(G)} if F is of the form ¬G,

pos(F ) = {Λ} ∪
 {1π1 | π1 ∈ pos(G1 )} ∪ {2π2 | π2 ∈ pos(G2 )}

if F is of the form (G1 ◦ G2 )


Steffen Hölldobler
Propositional Logic 8
Subformulas

I Definition 3.8 Let F ∈ L(R) be a propositional formula. The set of subformulas

of F is the smallest set of formulas SF satisfying the following conditions:
1 F ∈ SF .
2 If ¬G ∈ SF , then G ∈ SF .
3 If (G1 ◦ G2 ) ∈ SF , then G1 , G2 ∈ SF .
The set RF of variables occurring in F is SF ∩ R.
G is called subformula of F , if it is in SF .

I Example Let F = ¬((p1 → p2 ) ∨ p1 ).

SF = {¬((p1 → p2 ) ∨ p1 ), ((p1 → p2 ) ∨ p1 ), (p1 → p2 ), p1 , p2 }.

RF = {p1 , p2 }

Steffen Hölldobler
Propositional Logic 9
Semantics

I What is the meaning of ¬((p1 → p2 ) ∨ p1 )?

I Here formulas may be true (>) or false (⊥) binary logic.

Steffen Hölldobler
Propositional Logic 10
The Structure of the Truth Values

I A structure consists of a set of individuals and a set of functions defined on it.

I The set of truth values W is the set {>, ⊥}.
I Unary functions of type W → W:

. Negation ¬∗ : ¬∗ (>) = ⊥ and ¬∗ (⊥) = >.

. Identity.
. Projections onto ⊥ and >.
I Some binary functions of type W × W → W:

. Conjunction ∧∗ /2.
. Disjunction ∨∗ /2.
. Implication →∗ /2.
. NAND ↑ ∗ /2.
. NOR ↓∗ /2.
. Equivalence ↔∗ /2.

Steffen Hölldobler
Propositional Logic 11
The Functions over the Set of Truth Values

∧∗ ∨∗ →∗ ←∗ ↑ ∗ ↓∗ 6→∗ 6←∗
> > > > > > ⊥ ⊥ ⊥ ⊥
> ⊥ ⊥ > ⊥ > > ⊥ > ⊥
⊥ > ⊥ > > ⊥ > ⊥ ⊥ >
⊥ ⊥ ⊥ ⊥ > > > > ⊥ ⊥
Q∗ `∗
↔∗ 6↔∗ .∗ 6.∗ &∗ 6&∗
> > > ⊥ > ⊥ > ⊥ > ⊥
> ⊥ ⊥ > > ⊥ > ⊥ ⊥ >
⊥ > ⊥ > > ⊥ ⊥ > > ⊥
⊥ ⊥ > ⊥ > ⊥ ⊥ > ⊥ >

I Here negation, conjunction, disjunction, implication, equivalence.

Steffen Hölldobler
Propositional Logic 12
Interpretations

I Definition 3.9 A (propositional) interpretation I = (W, ·I ) consists of the set W

and a mapping ·I : L(R) → W which meets the following conditions:
 ∗
¬ [G]I if F is of the form ¬G,
[F ]I =
([G1 ]I ◦∗ [G2 ]I ) if F is of the form (G1 ◦ G2 ).

I An interpretation I = (W, ·I ) is uniquely defined

by specifying how ·I acts on propositional variables.

I Recall that A denotes an atom.

I We will sometimes identify an interpretation I = (W, ·I ) with {A | [A]I = >}.

I We often write F I instead of [F ]I .

I I (possibly indexed) denotes an interpretation.

Steffen Hölldobler
Propositional Logic 13
Satisfiability of Formulas

I Definition 3.12 Let F ∈ L(R).

. F is called satisfiable
if there is an interpretation I = (W, ·I ) with F I = >.
. F is called valid (or F is a tautology)
if for all interpretations I = (W, ·I ) we have: F I = >.
. F is called falsifiable
if there is an interpretation I = (W, ·I ) with F I = ⊥.
. F is called unsatisfiable
if for all interpretations I = (W, ·I ) we have: F I = ⊥.

Steffen Hölldobler
Propositional Logic 14
Truth Tables

I How can we compute the value of a formula F

under all possible interpretations?

I Computing a truth table:

1 Let m = |SF | be the number of subformulas of F .

2 Let n = |RF |
3 Form a table with 2n rows and m columns,
where the first n columns are marked by
the n propositional variables occurring in F ,
the last column is marked by F , and
the remaining columns are marked by the other subformulas of F .
4 Fill in the first n columns with > und ⊥ as follows:
In the first column fill in alternating downwards >⊥>⊥ . . .,
in the second column >>⊥⊥ . . .,
in the third column >>>>⊥⊥⊥⊥ . . ., etc.
5 Calculate the values in the remaining columns using
the known functions on the set of truth values.

Steffen Hölldobler
Propositional Logic 15
Working with Truth Tables

I Let F be a formula and T (F ) a corresponding truth table. Then:

. F is satisfiable iff T (F ) contains a row with > in the last column.

. F is valid iff all rows in T (F ) have > in the last column.
. F is falsifiable iff T (F ) contains a row with ⊥ in the final column.
. F is unsatisfiable iff all rows T (F ) have ⊥ in the final column.

Steffen Hölldobler
Propositional Logic 16
Models

I Definition 3.13 An interpretation I = (W, ·I ) is called model for a

propositional formula F , in symbols I |= F , if F I = >.

I Abbreviations

. If I is not a model for the formula F , i. e. if F I = ⊥, then we write I 6|= F .

. If F is valid, then we write |= F .

Steffen Hölldobler
Propositional Logic 17
Validity and Unsatisfiability

I Theorem 3.14 A propositional formula F is valid (|= F ) iff ¬F is unsatisfiable.

I Proof |= F iff all interpretations are models for F

iff no interpretation is a model for ¬F
iff ¬F is unsatisfiable. qed

Steffen Hölldobler
Propositional Logic 18
Satisfiability of a Set of Formulas

I Definition 3.15 Let G be a set of formulas.

. An interpretation I is called model for G, in symbols I |= G,

if I is model for all F ∈ G.
. G is satisfiable, if there is a model for G.
. G is unsatisfiable, if there is no model for G.
. G is falsifiable, if there is an interpretation which is no model for G.
. G is valid, if all interpretations are models for G.

Steffen Hölldobler
Propositional Logic 19
Logical Consequences

I Definition 3.16 A formula F is a logical consequence of a set of propositional

formulas G, in symbols G |= F , iff for every interpretation I we have:
if I |= G, then I |= F as well.

I Theorem 3.17 Let F , F1 , . . . , Fn be propositional formulas.

{F1 , . . . , Fn } |= F holds iff |= ((. . . (F1 ∧ F2 ) ∧ . . . ∧ Fn ) → F ) holds.

I Proof Exercise

Steffen Hölldobler
Propositional Logic 20
Equivalence and Normal Forms

I Semantic Equivalence

I Negation Normal Form

I Clausal Form

Steffen Hölldobler
Propositional Logic 21
Semantic Equivalence

I Definition 3.18 Two propositional formulas F and G are semantically

equivalent, in symbols F ≡ G, if for all interpretations I we have:
I |= F iff I |= G.

I Observe ≡ is an equivalence relation:

. ≡ is reflexive: F ≡ F .
. ≡ is symmetric: If F ≡ G, then G ≡ F .
. ≡ is transitive: If F ≡ G and G ≡ H, then F ≡ H.
This follows immediately from Definition 3.18 Exercise

Steffen Hölldobler
Propositional Logic 22
Well-Known Semantic Equivalences

I Theorem 3.19 The following equivalences hold:

(F ∧ F ) ≡ F
(F ∨ F ) ≡ F idempotency
(F ∧ G) ≡ (G ∧ F )
(F ∨ G) ≡ (G ∨ F ) commutativity
((F ∧ G) ∧ H) ≡ (F ∧ (G ∧ H))
((F ∨ G) ∨ H) ≡ (F ∨ (G ∨ H)) associativity
((F ∧ G) ∨ F ) ≡ F
((F ∨ G) ∧ F ) ≡ F absorption
(F ∧ (G ∨ H)) ≡ ((F ∧ G) ∨ (F ∧ H))
(F ∨ (G ∧ H)) ≡ ((F ∨ G) ∧ (F ∨ H)) distributivity

Steffen Hölldobler
Propositional Logic 23
Theorem 3.19 (continued)

I The following equivalences hold:

¬¬F ≡ F double negation

¬(F ∧ G) ≡ (¬F ∨ ¬G)
¬(F ∨ G) ≡ (¬F ∧ ¬G) de Morgan
(F ∨ G) ≡ F , if F is valid
(F ∧ G) ≡ G, if F is valid tautology
(F ∨ G) ≡ G, if F is unsatisfiable
(F ∧ G) ≡ F , if F is unsatisfiable unsatisfiability
(F ↔ G) ≡ ((F ∧ G) ∨ (¬G ∧ ¬F )) equivalence
(F → G) ≡ (¬F ∨ G) implication

I Proof Exercise

Steffen Hölldobler
Propositional Logic 24
Positions

I Recall


 ∅ if F is an atom,
{1π | π ∈ pos(G)} if F is of form ¬G,

pos(F ) = {Λ} ∪

 {1π1 | π1 ∈ pos(G1 )} ∪ {2π2 | π2 ∈ pos(G2 )}
if F is of the form (G1 ◦ G2 ).


I Definition 3.20
Let F be a formula. The set of positions in F , in symbols PF , is pos(F ).

I Positions are words over {1, 2}.

Steffen Hölldobler
Propositional Logic 25
Subformulas and Replacements

I Definition 3.21 The subformula of F at position π ∈ PF ,

in symbols F dπe, is defined by:
1 F dΛe = F .
2 F d1πe = Gdπe, if F is of the form ¬G.
3 F diπe = Gi dπe, if F is of the form (G1 ◦ G2 ) and i ∈ {1, 2}.

I Definition 3.22 The replacement of the subformula of F at position π ∈ PF

by H, in symbols F dπ 7→ He, is defined by:
1 F dΛ 7→ He = H,
2 F d1π 7→ He = ¬(Gdπ 7→ He), if F is of the form ¬G.
3 F d1π 7→ He = (G1 dπ 7→ He ◦ G2 ), if F is of the form (G1 ◦ G2 ).
4 F d2π 7→ He = (G1 ◦ G2 dπ 7→ He), if F is of the form (G1 ◦ G2 ).

Steffen Hölldobler
Propositional Logic 26
The Replacement Theorem

I Theorem 3.23 Let F , G, H ∈ L(R), π ∈ PF , F dπe = G and G ≡ H.

Then, F ≡ F dπ →
7 He.

I Proof Structural induction on π

I Induction basis Let π = Λ

√
. F = F dΛe = G ≡ H = F dΛ 7→ He

I Induction hypothesis (IH) The theorem holds for π 0

Steffen Hölldobler
Propositional Logic 27
Proof Replacement Theorem (Continuation)

I Induction step Let π = iπ 0 . We distinguish two cases:

. i =1 π = 1π 0 ∈ PF , hence F must be of the form ¬F 0 or (G1 ◦ G2 )

II ¬F 0 F d1π 0 7→ He = (¬F 0 )d1π 0 7→ He = ¬(F 0 dπ 0 7→ He)
II From IH we conclude: F 0 ≡ F 0 dπ 0 7→ He
II Hence, for all interpretations I we find:

[F ]I = [¬F 0 ]I Assumption
= ¬∗ [F 0 ]I Def I
= ¬∗ [F 0 dπ 0 7→ He]I IH and Def ≡
= [¬(F 0 dπ 0 7→ He)]I Def I
= [(¬F 0 )d1π 0 7→ He]I Def replacement
= [F d1π 0 7→ He]I Assumption
√
II Hence, F ≡ F d1π 0 7→ He
II (G1 ◦ G2 ) analogously

. i =2 analogously qed

Steffen Hölldobler
Propositional Logic 28
Agreement

I If π 6∈ PF then F dπ 7→ He = F .

I Let F dπe = G.
If it is obvious from the context which subformula G is to be replaced,
then we write F dG 7→ He instead of F dπ 7→ He.

I Theorem 3.23 allows to replace all occurrences of the connectives ↔ and →.

. Wlog we consider only formulas over R ∪ {¬, ∧, ∨, (, )}.

Steffen Hölldobler
Propositional Logic 29
Negation Normal Form

I Definition 3.24 A propositional formula F is in negation normal form if all

negation signs ¬ occurring in F appear directly in front of propositional
variables.

I Proposition 3.25 There is an algorithm which transforms any formula into a

semantically equivalent formula in negation normal form.

I Algorithm Given F . While F is not in negation normal form do:

. Select a subformula of F having the form ¬G with G 6∈ R

. If ¬G = ¬¬H, then replace ¬G by H
. If ¬G = ¬(G1 ∧ G2 ), then replace ¬G by (¬G1 ∨ ¬G2 )
. If ¬G = ¬(G1 ∨ G2 ), then replace ¬G by (¬G1 ∧ ¬G2 )

Steffen Hölldobler
Propositional Logic 30
The Rules of the Algorithm

I The rules will be abbreviated by:

¬¬H ¬(G1 ∧ G2 ) ¬(G1 ∨ G2 )

H (¬G1 ∨ ¬G2 ) (¬G1 ∧ ¬G2 )

I The algorithm is (don’t care) non-deterministic!

I Example

¬(r ∨ ¬(¬p ∧ q)) ≡ (¬r ∧ ¬¬(¬p ∧ q)) de Morgan

≡ (¬r ∧ (¬p ∧ q)) double negation

Steffen Hölldobler
Propositional Logic 31
3.3.3 Clause Form
I Definition 3.26
A literal is a propositional variable, or a negated propositional variable.
A propositional variable is also called positive literal,
whereas a negated propositional variable is called negative literal.
I Notation
. L (possible indexed) denotes a literal.
. Generalized disjunction

[F1 , . . . , Fn ] = (. . . ((F1 ∨ F2 ) ∨ F3 ) ∨ . . . ∨ Fn )

. Generalized conjunction

hF1 , . . . , Fn i = (. . . ((F1 ∧ F2 ) ∧ F3 ) ∧ . . . ∧ Fn )

. Observe [F ] = F and hF i = F . Hence, [F ] ≡ F and hF i ≡ F .

. Empty generalized disjunction: [ ] with [ ]I = ⊥ for all I.
. Empty generalized conjunction: hi with hiI = > for all I.
. Observe (G ∨ [ ]) ≡ G and (G ∧ hi) ≡ G.

Steffen Hölldobler
Propositional Logic 32
Clauses

I Definition 3.27

. A clause is a generalized disjunction [L1 , . . . , Ln ], n ≥ 0,

where every Li , 1 ≤ i ≤ n, is a literal.
. A dual clause is a generalized conjunction hL1 , . . . , Ln i, n ≥ 0,
where every Li , 1 ≤ i ≤ n, is a literal.
. A formula is in conjunctive normal form, or clause form, iff it is of the form
hC1 , . . . , Cm i, m ≥ 0, and if every Cj , 1 ≤ j ≤ m, is a clause.
. A formula is in disjunctive normal form, or dual clause form, iff it is of the
form [C1 , . . . , Cm ], m ≥ 0, and if every Cj , 1 ≤ j ≤ m, is a dual clause.

I Notation C (possibly indexed) denotes a clause.

Steffen Hölldobler
Propositional Logic 33
An Observation

I Let F be a formula in clause form. The following holds:

. F is unsatisfiable if a clause occurring in F is unsatisfiable.

. A clause is unsatisfiable iff it is of the form [ ].

Steffen Hölldobler
Propositional Logic 34
Transformation into Clause Form

I Theorem 3.28

1 There is an algorithm which transforms any formula into a semantically

equivalent formula in clause form.
2 There is an algorithm which transforms any formula into a semantically
equivalent formula in dual clause form.

I Proof of 1

. We have to specify the algorithm.

. We have to show that the algorithm is correct or sound,
i.e., if it outputs G given F ,
then G must be in clause form and F ≡ G must hold.
. We have to show that the algorithm terminates,
i.e., it stops in finite time given F .

Steffen Hölldobler
Propositional Logic 35
An Algorithm for the Transformation into Clause Form

I Input: A propositional formula F .

Output: A formula, which is in conjunctive normal form and is equivalent to F .
G := h[F ]i. (G is a conjunction of disjunctions.)
While G is not in conjunctive normal form do:
Select a non-clausal element H from G.
Select a non-literal element K from H.
Apply the rule among the following ones which is applicable.

¬¬D (D1 ∧ D2 ) ¬(D1 ∧ D2 ) (D1 ∨ D2 ) ¬(D1 ∨ D2 )

D D1 | D2 ¬D1 , ¬D2 D1 , D2 ¬D1 | ¬D2

I A rule DD0 is applicable to K if K is of the form D.

If applied, then K is replaced by D 0 .
I A rule D D|D is applicable to K if K is of the form D.
1 2
If applied, H is replaced by two disjunctions:
The first one is obtained from H by replacing the occurrence of D by D1 .
The second one is obtained from H by replacing the occurrence of D by D2 .

Steffen Hölldobler
Propositional Logic 36
A Lemma

I Lemma 3.29 If a propositional formula G is a conjunction of disjunctions and

G 0 is obtained from G by applying one of the rules of the algorithm,
then G 0 is a conjunction of disjunctions and G ≡ G 0 .

I Proof Exercise

Steffen Hölldobler
Propositional Logic 37
Induction Principle for While-Loops
I A loop invariant for a while-loop W is a statement E having the following
property: If E holds, then E still holds after one execution of the body of W .

I Theorem 3.30 (Induction Principle for While-Loops)

If a statement E holds before entering a loop W , and is a loop invariant for W ,
then E holds after termination of W as well (if W terminates).

I Proof

. Suppose E is true on the first entry into the loop.

. Suppose E is not true after termination of W .
. There exists an iteration after which E becomes false.
. Let n be the first such iteration.
. Thus, after the ith iteration E is true for i ∈ [1, n).
. In particular, after the n − 1st iteration E is true.
. After the n − 1st iteration the guard of the loop W must be true
as otherwise termination would occur.
. Because E is a loop invariant, E must hold after the nth iteration
Contradiction qed

Steffen Hölldobler
Propositional Logic 38
Soundness of the Algorithm

I Let F be the given propositional formula and let E be the statement:

G ist a conjunction of disjunctions and F ≡ G holds.

. Initially G is defined to be h[F ]i.

. Because F ≡ h[F ]i holds, E holds before entering the while-loop.
. From Lemma 3.29 we learn that E is a loop invariant for the while-loop.
. Hence, by Theorem 3.30 E holds when the loop has terminated.
. The loop terminates only when G is in conjunctive normal form.
. Thus, the algorithm is sound!

Steffen Hölldobler
Propositional Logic 39
Termination of the Algorithm

I When does a non-deterministic algorithm terminate?

. Weak Termination
There is at least one way to execute the algorithm such that it terminates.
. Strong Termination The algorithm terminates independently of
which choice we make in the non-deterministic situations.

I Definition 3.31 The function rnk, called rank of a propositional formula, is

defined over L(R) as follows:


 0 if H is a literal,



 rnk(F ) + 1 if H is of the form ¬¬F ,
rnk(F ) + rnk(G) + 1 if H is of the form

rnk(H) =

 (F ∧ G) or (F ∨ G),
rnk(¬F ) + rnk(¬G) + 1 if H is of the form




¬(F ∧ G) or ¬(F ∨ G).


Steffen Hölldobler
Propositional Logic 40
Multisets

I A multiset is comparable to a set,

but the individual elements may occur multiple times in it.

I Here multisets of natural numbers.

˙ 1, 2, 2, 2, 3}.
. {1, ˙
. M1  M2 holds iff M2 is obtained from M1 by deleting a number n from M1
and replacing it by finitely many numbers which are all less than n.
˙ 1, 2, 2, 2, 3}˙  {1,
. {1, ˙ 1, 1, 1, 2, 2, 2, 2}.
˙
.  is not transitive and, hence, is not an ordering relation.
. Observation there cannot be infinitely long sequences (Mi | i ≥ 0) of finite
multisets of natural numbers such that M0  M1  . . ..
Proof see Dershowitz, Manna: Proving Termination with Multiset Orderings,
CACM 22, 465-475 (1979).

Steffen Hölldobler
Propositional Logic 41
Proof of Termination

I Let G = h[H11 , . . . , H1,n1 ], . . . , [Hm1 , . . . , Hmnm ]i. We define:

n1 nm
X X
f(G) = {˙ rnk(H1j ), . . . , rnk(Hmj )}˙
j=1 j=1

I Observation With every execution of the while-loop, the associated multisets

become smaller with respect to /2 (Proof Exercise) Termination. qed

I Example
h[¬(p ∨ (¬(p ∧ q) ∧ ¬r))]i ˙ }˙
{5
h[¬p], [¬(¬(p ∧ q) ∧ ¬r)]i ˙ 4}˙
{0,
h[¬p], [¬¬(p ∧ q), ¬¬r ]i ˙ 3}˙
{0,
h[¬p], [(p ∧ q), ¬¬r]i ˙ 2}˙
{0,
h[¬p], [(p ∧ q), r]i ˙ 1}˙
{0,
h[¬p], [p, r], [q, r ]i ˙{0, 0, 0}˙

˙ . . . , 0}˙ and
I Observation If G is in clause form, then f(G) = {0,
the number of clauses occurring in G is equal to
the number of occurrences of 0 in f(G).

Steffen Hölldobler
Propositional Logic 42
Proof Methods

I {F1 , . . . , Fn } |= F
iff (hF1 , . . . , Fn i → F ) is valid
iff ¬(hF1 , . . . , Fn i → F ) is unsatisfiable
iff hF1 , . . . , Fn , ¬F i is unsatisfiable.

I Until now truth tabling

I Resolution

I Semantic tableaus

I Calculus of natural deduction

I Other proof systems and calculi

(sequent calculus, connection method, Hilbert systems,
Davis-Putnam-Logemann-Loveland procedure)

Steffen Hölldobler
Propositional Logic 43
Resolution

I Resolution is a method to show unsatisfiability of formulas.

I Here Wlog we assume that formulas are in clause form.

I A formula in clause form is unsatisfiable if

. it contains the empty clause, or

. it can be transformed into a semantically equivalent formula which contains
the empty clause.

I Resolution is search for the empty clause using an appropriate inference rule.

Steffen Hölldobler
Propositional Logic 44
Example

I Some Facts

K1 If it is hot and humid, then it will rain.

K2 If it is humid, then it is hot.
K3 It is humid now.

I Question

K4 Will it rain?

I Introducing propositional variables

p it is hot
q it is humid
r it will rain

I Formalization

F1 ((p ∧ q) → r )
F2 (q → p)
F3 q
F4 r

Steffen Hölldobler
Propositional Logic 45
Example (continued)

{((p ∧ q) → r ), (q → p), q} |= r
iff
(h((p ∧ q) → r), (q → p), qi → r ) is valid
iff
¬(h((p ∧ q) → r), (q → p), qi → r) is unsatisfiable
iff
h((p ∧ q) → r ), (q → p), q, ¬r i is unsatisfiable
iff
h[¬p, ¬q, r], [¬q, p], [q], [¬r]i is unsatisfiable

Steffen Hölldobler
Propositional Logic 46
How to Show Unsatisfiability?

I Recall
h[¬p, ¬q, r], [¬q, p], [q], [¬r ]i

I Observation
{[¬p, ¬q, r], [q]} |= [¬p, r ]

I Hence

h[¬p, ¬q, r ], [¬q, p], [q], [¬r]i ≡ h[¬p, ¬q, r], [¬q, p], [q], [¬r], [¬p, r]i

Steffen Hölldobler
Propositional Logic 47
Resolution Rule

I Definition 3.32 Let C1 be a clause where the atom A occurs,

and C2 a clause where the negated atom ¬A occurs.
Let C be the result of performing the following steps:
1 Remove all occurrences of A from C1 .
2 Remove all occurrences of ¬A from C2 .
3 Combine the clauses obtained in this way disjunctively.
C was generated applying the (propositional) resolution rule to C1 and C2 ,
where A is the literal that was resolved upon.
We also call C the resolvent of C1 and C2 wrt A.

I C may be the resolvent of C1 and C1 .

Steffen Hölldobler
Propositional Logic 48
Derivations and Refutations

I Definition 3.33 Let F = hC1 , . . . , Cn i be a formula in clause form.

1 The sequence (Ci | 1 ≤ i ≤ n) is a resolution derivation for F .

2 If (Ci | 1 ≤ i ≤ m) is a resolution derivation for F , and Cm+1 is obtained by
applying the resolution rule to two elements from (Ci | 1 ≤ i ≤ m), then
(Ci | 1 ≤ i ≤ m + 1) is a resolution derivation for F .
3 A resolution derivation for F which contains the empty clause [ ] is called
resolution refutation for F .

I F may contain [ ].

I It suffices to consider refutations in which [ ] occurs once.

I We may assume that [ ] is the last clause in a refutation.

Steffen Hölldobler
Propositional Logic 49
Example (continued)

1 [¬p, ¬q, r ]
2 [¬q, p]
3 [q]
4 [¬r]
5 [¬q, ¬q, r] res(1, 2)
6 [r] res(3, 5)
7 [] res(4, 6)

Steffen Hölldobler
Propositional Logic 50
Resolution Proofs

I Definition 3.34 Let F be a propositional formula,

and G a formula in clause form equivalent to ¬F .
. A propositional resolution proof for F is a resolution refutation for G.
. F is called theorem of the resolution calculus,
if there is a resolution proof for F .
. We denote by `r F , that F has a resolution proof.

I Requirements

. Soundness If `r F , then |= F .
. Completeness If |= F , then `r F .

I Observation

. Let F be a formula with n propositional variables.

. (F ∧ (p ∧ ¬p)) is unsatisfiable.
. The proof consists of a single resolution step!

Steffen Hölldobler
Propositional Logic 51
The Calculus of Natural Deduction

I Gentzen 1935: How to represent logical reasoning in mathematics?

. Calculus of natural deduction.

I Its set of propositional letters is Rn := R ∪ {[ ]}.

I [ ]I := ⊥ for all interpretions I.

I Its language is L(Rn ).

Steffen Hölldobler
Propositional Logic 52
An Introductory Example

I Suppose we want to show the validity of

((p ∨ (q ∧ r)) → ((p ∨ q) ∧ (p ∨ r))).

I A proof could look like the following:

Assume that (p ∨ (q ∧ r)) holds. We distinguish two cases:

(i) Assume that p holds.
Hence, (p ∨ q) must hold.
(ii) Assume that (q ∧ r) holds.
Hence, q and, consequently, (p ∨ q) must hold.
Thus, (p ∨ q) must hold in any case. (1)
Likewise, we conclude that (p ∨ r) must hold. (2)
From (1) and (2) we conclude that ((p ∨ q) ∧ (p ∨ r)) holds.
We can now cancel the assumption and, thus, obtain
a proof of ((p ∨ (q ∧ r)) → ((p ∨ q) ∧ (p ∨ r))).

Steffen Hölldobler
Propositional Logic 53
Inference Rules – Examples

I Elimination of the implication

G (G → F )
(→ E)
F

I Introduction of the implication

bGc
..
.
F
(→ I)
(G → F )

I Schemas which need to be instantiated, e.g.,

(p ∧ q) ((p ∧ q) → (q ∧ p))
(→ E)
(q ∧ p)

Steffen Hölldobler
Propositional Logic 54
Natural Deduction - Inference Rules
I Negation

b¬F c bF c
[] .. .. F ¬F
(f ) . . (¬E)
G [] [] []
(raa) (¬I)
F ¬F

I Conjunction

F G (F ∧ G) (F ∧ G)
(∧I) (∧E) (∧E)
(F ∧ G) F G

I Disjunction

bF c bGc
F G . .
.. ..
(∨I) (∨I)
(F ∨ G) (F ∨ G) (F ∨ G) H H
(∨E)
H

Steffen Hölldobler
Propositional Logic 55
Natural Deduction – Inference Rules (Continued)

I Implication

bGc b¬F c
.. .. G (G → F )
. . (→ E)
F ¬G F
(→ I) (→ I)
(G → F ) (G → F )

I Equivalence

bGc bF c
.. .. G (G ↔ F ) F (G ↔ F )
. . (↔ E) (↔ E)
F G F G
(↔ I)
(G ↔ F )

Steffen Hölldobler
Propositional Logic 56
Derivation Trees

I Derivations are finite trees, where

. nodes are labeled by formulas,

. arcs are labeled by inference rules,
. leaf nodes may be marked by b c and an index j ∈ N,
. arcs may be marked by an index j ∈ N,
and which are constructed as defined below.

I If a leaf node is labeled by F and marked by b c and j,

then this is denoted by bF cj ; F is said to be marked by b c and j.

I Formulas labeling leaf nodes are called hypotheses or assumptions.

. If a leaf node is labeled by bF cj ,

then this occurrence of F is said to be cancelled;
otherwise it is said to be uncancelled.

I If a derivation tree 5 contains an uncancelled occurrence of a hypothesis F ,

then F is said to be an uncancelled hypothesis of 5.

Steffen Hölldobler
Propositional Logic 57
Derivation Trees – Notation

I A derivation tree whose root is labeled by F is denoted by 5F .

I A derivation tree whose root is labeled by F and which contains an uncancelled

hypothesis G is denoted by 5G
F.

I Let j be an index.
j
5bGc denotes the tree obtained from 5G by marking
F F
at least one of the uncancelled occurrences of the hypothesis G by b cj .

Steffen Hölldobler
Propositional Logic 58
Derivation Trees – Formal Definition (1)

I Definition 3.38 The set of derivation trees in the calculus of natural deduction
is the smallest set X with the following properties

1 Each tree consisting of a single node labeled by some F ∈ L(Rn )

is in X .
2 If 5H ∈ X and1
H1
r
H2
is the instance of a rule r ∈ {(f ), (∧E), (∨I)}, then

5H
1
r
H2

is in X.

Steffen Hölldobler
Propositional Logic 59
Derivation Trees – Formal Definition (2)

H
3 If 5H1 ∈ X , j is a new index, and
2

bH1 c
..
.
H2
r
H3
is an instance of a rule r ∈ {(raa), (¬I), (→ I)}, then
j
5bH1 c
H2
rj
H3
is a derivation tree in X .

Steffen Hölldobler
Propositional Logic 60
Derivation Trees – Formal Definition (3)

4 If 5H1 , 5H2 ∈ X and

H1 H2
r
H3
is an instance of a rule r ∈ {(¬E), (∧I), (→ E), (↔ E)}, then

5H 5H
1 2
r
H3

is a derivation tree in X .

Steffen Hölldobler
Propositional Logic 61
Derivation Trees – Formal Definition (4)

5 If 5(F ∨G) , 5FH , 5G

H ∈ X and j is a new index, then

j j
5 5bF c 5bGc
(F ∨G) H H
(∨E)j
H
is a derivation tree in X.

6 If 5G
F,
5F ∈ X and j is a new index, then
G

j j
5bGc 5bF c
F G
(↔ I)j
(G ↔ F )

is a derivation tree in X .

Steffen Hölldobler
Propositional Logic 62
Derivations and Proofs

I Definition 3.39 Let 5F be a derivation tree and {F1 , . . . , Fm } the set of

uncancelled hypothesis occurring in 5F .
Then, 5F is said to be a derivation of F from {F1 , . . . , Fm },
and we denote this by {F1 , . . . , Fm } `n F .

I Definition 3.40 A proof of a propositional formula F

in the calculus of natural deduction is a derivation of F from the empty set.
Instead of ∅ `n F we write `n F ,
if there exists a proof of F in the calculus of natural deduction.

I A simple example A proof of (p → p)

bpc1
(→ I)1
(p → p)

Steffen Hölldobler
Propositional Logic 63
The Introductory Example Revisited

2 3
b(q ∧ r )c b(q ∧ r )c
(∧E) (∧E)
2 3
bpc q bpc r
(∨I) (∨I) (∨I) (∨I)
1 1
b(p ∨ (q ∧ r ))c (p ∨ q) (p ∨ q) b(p ∨ (q ∧ r ))c (p ∨ r ) (p ∨ r )
(∨E)2 (∨E)3
(p ∨ q) (p ∨ r )
(∧I)
((p ∨ q) ∧ (p ∨ r ))
(→ I)1
((p ∨ (q ∧ r)) → ((p ∨ q) ∧ (p ∨ r )))

I Please compare this to the informal proof given at the beginning.

Steffen Hölldobler
Propositional Logic 64
Lemmas (1)

I Certain derivation trees may occur over and over again,

e.g., {¬¬F } `n F or
¬¬F b¬F c1
(¬E)
[]
(raa)1
F

I Idea Generate such derivation tree once and for all,

specify corresponding inference rules called lemmas,
and apply the lemmas in addition to the usual inference rules.

I In the example we obtain

¬¬F
(l1)
F

Steffen Hölldobler
Propositional Logic 65
Lemmas (2)

I The lemma

¬(F ∧ G) F
(l2)
¬G

I and its derivation tree

F bGc1
(∧I)
¬(F ∧ G) (F ∧ G)
(¬E)
[]
(¬I)1
¬G

Steffen Hölldobler
Propositional Logic 66
Lemmas (3)

I The lemma

¬(F ∧ G) G
(l3)
¬F

I and its derivation tree

bF c1 G
(∧I)
¬(F ∧ G) (F ∧ G)
(¬E)
[]
(¬I)1
¬F

Steffen Hölldobler
Propositional Logic 67
Lemmas (4)

I The lemma

¬(F ∨ G)
(l4)
(¬F ∧ ¬G)

I and its derivation tree

bF c1 bGc2
(∨I) (∨I)
¬(F ∨ G) (F ∨ G) ¬(F ∨ G) (F ∨ G)
(¬E) (¬E)
[] []
(¬I)1 (¬I)2
¬F ¬G
(∧I)
(¬F ∧ ¬G)

Steffen Hölldobler
Propositional Logic 68
Another Example Demonstrating the Use of Lemmas

I A proof of (p ∨ ¬p)

b¬(p ∨ ¬p)c1
(l4)
(¬p ∧ ¬¬p) b¬(p ∨ ¬p)c1
(∧E) (l4)
¬¬p (¬p ∧ ¬¬p)
(l1) (∧E)
p ¬p
(¬E)
[]
(raa)1
(p ∨ ¬p)

Steffen Hölldobler
Propositional Logic 69
Some Remarks on Natural Deduction

I Lemmas shorten proofs, but enlarge the search space

I The calculus of natural deduction is sound and complete

(see e.g. van Dalen: Logic and Structure. Springer 1997)

I Human readable proofs versus machine generated proofs

I Sequent calculus

I Proof theory

Steffen Hölldobler
Propositional Logic 70
3.6 Properties

I Compactness Theorem

I Soundness and Completeness Theorems

Steffen Hölldobler
Propositional Logic 71
3.6.1 Compactness Theorem – Introduction

I How can we decide whether a possibly infinite set of formulas is satisfiable?

I Idea We test all finite subsets.

I Remember ≡ is an equivalence relation on L(R).

I Let L(R, n) ⊆ L(R) be the set of formulas in which only the variables
p1 , . . . , pn occur.

I There are 2n different interpretations for L(R, n).

I How many different equivalence classes are defined by ≡ on L(R, n)?

Steffen Hölldobler
Propositional Logic 72
Compactness Theorem

I Theorem 3.45 (Compactness Theorem)

A set G of propositional formulas is satisfiable
iff every finite subset H ⊆ G is satisfiable.

I Proof Let G be a (possibly infinite) set of formulas. We have to show:

(i) If G is satisfiable, so is each finite H ⊆ G.

(ii) If each H ⊆ G is satisfiable, so is G.

. (i) follows immediately from the definition of satisfiability for sets.

. To show (ii) we have to prove the existence of a model for G starting from the
models for each finite H ⊆ G.

Steffen Hölldobler
Propositional Logic 73
Proof of Part (ii) of the Compactness Theorem

I Suppose, each finite H ⊆ G is satisfiable.

I Let Gn = G ∩ L(R, n).

n
I There are at most k ≤ 22 different equivalence classes on Gn defined by ≡.

I Let G1 , . . . , Gk be representatives of these equivalence classes.

I Hence, for each G ∈ Gn there is an i, 1 ≤ i ≤ k , with G ≡ Gi .

I Hence, each model for {G1 , . . . , Gk } is also a model for Gn .

I Because {G1 , . . . , Gk } is a finite subset of G, it has a model.

I Let In be this model.

I Because G1 ⊆ G2 ⊆ . . . ⊆ Gn , In is also a model for all Gj , 1 ≤ j ≤ n.

Steffen Hölldobler
Propositional Logic 74
Proof of Part (ii) of the Compactness Theorem (continued)
I We construct a model I for G as follows:

Set I := ∅, K0 := N and n = 1.
Do the following:
If there are infinitely many j ∈ Kn−1 with [pn ]Ij = > , then set
I := I ∪ {pn } and Kn := Kn−1 \ {j | [pn ]Ij = ⊥}, (>)
else set
Kn := Kn−1 \ {j | [pn ]Ij = >}. (⊥)
Set n := n + 1.
Goto “Do the following”.

I I is an interpretation.

I By induction the following proposition E(n) can be proven:

Kn contains infinitely many elements and

for all m ∈ Kn we find: [pi ]Im = [pi ]I for all 1 ≤ i ≤ n.

Proof Exercise

Steffen Hölldobler
Propositional Logic 75
Proof of Part (ii) of the Compactness Theorem (continued)
I To show I is a model for G.

I Let F be an arbitrary but fixed element of G.

I There are at most finitely many propositional variables occurring in F .

I Let pn be the variable with the highest index.

I Then, F ∈ Gn ⊆ Gn+1 ⊆ . . .
and each interpretation In , In+1 , . . . is a model for F .

I Because of E(n) we find:

. Kn contains infinitely many elements.

. For all m ∈ Kn we find: [pi ]Im = [pi ]I for all 1 ≤ i ≤ n.

I Select m ∈ Kn with m > n.

I Because Im is a model for F and F contains only the variables p1 , . . . , pn ,

I must be a model for F as well.

I Because F is an arbitrary element from G, I must also be a model for G. qed

Steffen Hölldobler
Propositional Logic 76
Implications of the Compactness Theorem

I The proof is not constructive.

I We may negate both sides of the compactness theorem.

I Corollary 3.46 A set of propositional formulas is unsatisfiable

iff one of its finite subsets is unsatisfiable.

I Procedure to prove unsatisfiability of G:

. We generate all finite subsets of G in a systematic way

and test them for unsatisfiability.

Steffen Hölldobler
Propositional Logic 77
Soundness and Completeness Theorems
I Lemma 3.47 (Propositional Resolution Lemma) Let F = hC1 , . . . , Cn i be a
propositional formula in clause form with the clauses Ci , 1 ≤ i ≤ n, and let C
be a resolvent of two clauses from F . Then F ≡ (F ∧ C) holds.
I Proof To show I |= (F ∧ C) iff I |= F
⇒ immediate
⇐ Suppose I |= F . Let C be the resolvent of Ci and Cj wrt A, 1 ≤ i, j ≤ n
. Let Ci0 = Ci “without” A and Cj0 = Cj “without” ¬A
. Then C = (Ci0 ∨ Cj0 )
. Case 1 I |= A
Then I 6|= ¬A
Because I |= Cj we conclude I |= Cj0
Hence I |= C
. Case 2
I 6|= A
Because I |= Ci we find I |= Ci0
Hence I |= C qed

Steffen Hölldobler
Propositional Logic 78
An Implication of the Resolution Lemma

I Corollary 3.48 Let F = hC1 , . . . , Cn i be a propositional logic formula

in clause form with clauses Ci , 1 ≤ i ≤ n, and
let D1 , . . . , Dm be the computed resolvents in a resolution derivation from F .
Then, F ≡ hF , D1 , . . . , Dm i.

I Proof Induction over m Exercise

Steffen Hölldobler
Propositional Logic 79
Resolution Method

I Theorem 3.49 (Soundness and Completeness of the Prop. Resolution Method)

Let F be a propositional formula. |= F iff `r F .

I Proof Soundness To show If `r F then |= F

. Suppose `r F
. By Theorem 3.28 there is a formula G in clause form with G ≡ ¬F
. By Definition 3.34 we find a resolution refutation for G
i.e. by Definition 3.33 a resolution derivation with [ ] as last element
. Let D1 , . . . , Dm , [ ] be all resolvents computed in that refutation
. By Corollary 3.48 we find G ≡ hG, D1 , . . . , Dm , [ ]i
. Because [ ] is unsatisfiable we conclude by Theorem 3.19 that G ≡ [ ]
i.e. G ist unsatisfiable
. Because G ≡ ¬F and Theorem 3.14 we find |= F

Steffen Hölldobler
Propositional Logic 80
Completeness of the Resolution Method

I Proof Completeness To show If |= F , then `r F

. Suppose |= F
. By Theorem 3.28 we find a formula G in clause form with G ≡ ¬F
. By Theorem 3.14 we find that G is unsatisfiable
. To show there is a resolution refutation for G
. The proof is by induction on the number n of propositional variables
occurring in G

I n =0 Then G = h[ ], . . . , [ ]i and we are done

I n ⇒n+1 Assume that the proposition holds for n, i.e.

if G is unsatisfiable and in G occur only the variables p1 , . . . , pn
then there is a resolution refutation for G

. Wlog we may assume that p1 , . . . , pn are the n variables occurring in G

Exercise

Steffen Hölldobler
Propositional Logic 81
Completeness of the Resolution Method (continued)

I Let G 0 be a formula in clause form in which the variables p1 , . . . , pn+1 occur

0 be the formula obtained from G 0 by
. Let G>
II deleting each clause, in which pn+1 occurs, and
II deleting each occurrence of ¬pn+1
0 be the formula obtained from G 0 by
. Let G⊥
II deleting each clause, in which ¬pn+1 occurs, and
II deleting each occurrence of pn+1

. We find G>0 and G 0 are unsatisfiable if G 0 is unsatisfiable

⊥
Exercise

Steffen Hölldobler
Propositional Logic 82
Completeness of the Resolution Method (continued)

0 and G 0 .
I Applying the induction assumption we find refutations for G⊥ >
0
I resolvents G> resolvents G 0

Case 1 resolution refutation for G 0

Case 2 resolution derivation with [¬pn+1 , . . . ¬pn+1 ] as last entry
0
I resolvents G⊥ resolvents G 0

Case 1 resolution refutation for G 0

Case 2 resolution derivation with [pn+1 , . . . , pn+1 ] as last entry

I If case 2 was selected twice, then compute the resolvent of

[pn+1 , . . . , pn+1 ] and [¬pn+1 , . . . , ¬pn+1 ]
resolution refutation for G 0

I An application of the induction principle yields the desired result qed

Steffen Hölldobler
Propositional Logic 83