Transcript Full version

Giorgi Japaridze
Logic
Propositional Logic
Episode 4
• What logic is or should be
• Propositions
• Boolean operations
• The language of classical propositional logic
• Interpretation and truth
• Validity (tautologicity)
• Truth tables
• The NP-completeness of the nontautologicity problem
• Gentzen-style axiomatizations (sequent calculus systems)
0
4.1
What logic is or should be
Below are a few theses about what your lecturer believes logic is or
should be:
1. Logic is the most basic, general-purpose, universal-utility tool for reasoning and
acting rationally.
2. All intellectual activities (sciences, engineering, politics, everyday life) are or should
be based on logic, while logic, in turn, is self-sufficient and needs none of those.
3. Logic makes no ontological commitments, and is focused on form rather than
content. It is exactly this full abstraction from content that makes logic
general-purpose and universal-utility.
4. All other sciences can be seen as applications of logic to some particular domains. For
this very reason, such sciences are special- rater than general-purpose tools, applicable
only to limited parts of the world.
5. Logic is the same to (all other) intellectual activities as programming languages
are to (all other) application programs.
4.2
Propositions
There are only two propositions: ⊤ (true) and ⊥ (false).
Classical logic sees no difference between two true or two false
propositions, so we have
“2+2=4” = “snow is white” = ⊤
and
“2+2=5” = “snow is black” = ⊥.
If you find this strange or confusing, remember that, from the point
of view of set theory, we similarly have
{x | x>(x+1)} = {x | x is an elephant that can fly} = 
4.3
Boolean operations
Symbol




Name
Translation
Type
“Not”
“And”
“Or”
“If ... then”
Negation
Conjunction
Disjunction
Implication
{⊤, ⊥}  {⊤, ⊥}
{⊤, ⊥}{⊤, ⊥}  {⊤, ⊥}
{⊤, ⊥}{⊤, ⊥}  {⊤, ⊥}
{⊤, ⊥}{⊤, ⊥}  {⊤, ⊥}
Note that:
p = p
p p
p q
⊥
⊤
⊥
⊥
⊥
⊥
⊤
⊤
⊥
⊥
⊤
⊥
⊤
⊤
⊤
⊥
⊥
⊤
⊥
(pq) = pq
⊤
⊤
⊤
⊤
⊤
(pq) = pq
pq
pq pq
pq =  pq
4.4
The language of classical propositional logic
The language of classical propositional logic is built from:
1. Two logical atoms: ⊤ and ⊥.
2. Infinitely many nonlogical atoms: p, q, r, s, p1, p2, p3, ...
3. Propositional connectives: , , , .
4. Parentheses: (, ).
Formulas are defined inductively by:
1. Atoms (logical or nonlogical) are formulas.
2. If F is a formula, then so is (F).
3. If E and F are formulas, then so are (E)(F), (E)(F), (E)(F).
For readability, we will be typically omitting certain parentheses,
whenever this does not create ambiguity.  has the highest precedence,
so that, say, pq should be understood as (p)q rather than as
(pq). And  has the lowest precedence, so that, say, pqr
should be understood as (pq)r rather than as p(qr).
4.5
Interpretation and truth
An interpretation is a function * that assigns a particular proposition p*
(⊤ or ⊥) to each nonlogical atom p.
Synonyms of “interpretation” are model and truth assignment.
Every interpretation * extends from nonlogical atoms to all formulas by
stipulating that:
⊤* = ⊤
⊥* = ⊥
(F)* = (F*)
(EF)* = (E*)(F*)
(EF)* = (E*)(F*)
(EF)* = (E*)(F*)
We say that formula F is true under interpretation *, or simply that
F* is true, if F*= ⊤. Otherwise we say that it is false.
4.6
Validity; truth tables; NP-completeness of the nonvalidity problem
We say that a formula F is valid (or is a tautology) if F is true under every interpretation.
Examples of tautologies:
⊤;  ⊥; pp; p(qp); ⊥p.
How about this one? [(pq)r]  [(pq)(pr)] There is a brute force method,
called the truth table method, that allows us to get answers to such questions. It consists
of going through all possible interpretations to see if all of them make the formula true.
p q r [(pq)  r]  [ (p  q)  (p  r)]
⊥
⊥
⊥
⊥
⊤
⊤
⊤
⊤
⊤
⊥
⊥
⊤
⊥
⊤
⊤
⊤
⊤
⊤
⊥
⊤
⊥
⊥
⊤
⊤
⊤
⊤
⊤
⊥
⊤
⊤
⊥
⊤
⊤
⊤
⊤
⊤
⊤
⊥
⊥
⊥
⊤
⊤
⊥
⊤
⊥
⊤
⊥
⊤
⊥
⊤
⊤
⊥
⊤
⊤
⊤
⊤
⊥
⊤
⊥
⊤
⊤
⊥
⊥
⊤
⊤
⊤
⊤
⊤
⊤
⊤
⊤
⊤
What is the trouble with the
truth table method?
Inefficiency. The truth table
for a formula with a couple of
hundred atoms would have
more rows than the number of
particles in the Universe!
Deductive methods (the
following slides) are more
practical, even though,
generally, we have:
Theorem 4.1. The problem of telling whether a formula is tautological is
coNP-complete, meaning that no truly efficient algorithms are known for it.
4.7
Deductive systems
There are various deductive systems for classical propositional logic.
They can be divided into two major classes: Hilbert-style and Gentzen-style.
Hilbert-style systems are axiom-based while Gentzen-style systems are rule-based.
Gentzen-style systems have a number of advantages, including existence of
straightforward proof search algorithms.
In this course we will deal only with Gentzen-style systems. Another name for
such systems is sequent calculi.
From now on we will consider the version of the language of classical propositional
logic where formulas are not allowed to contain logical atoms or implication. This
does not mean diminishing the expressive power of the language, as ⊤ can be
considered an abbreviation of pp, ⊥ considered an abbreviation of pp, and
EF an abbreviation of EF.
Furthermore, officially  will only be allowed on atoms. When applied to
non-atomic formulas,  is considered an abbreviation defined by:
E = E
(EF) = EF
(EF) = EF
4.8
A sequent calculus system for classical propositional logic
A sequent is any finite sequence of formulas (in the sense of Slide 4.7). Here
are the rules of one of several equivalent sequent calculus systems for classical
propositional logic. Let us call it G1.
In the following rules, E,F stand for any formulas, and G,H stand for any sequents.
Above the horizontal line is (are) the premise(s), and below the line is the conclusion.
A proof in such a system is a tree of sequents, where each node is the conclusion
of some rule, and the children of the node are the premises of that rule. Such a tree
is a proof of the sequent at its root. A formula F is considered provable if the sequent
F is provable (of course, “provable” means “has a proof”).
Identity
[no premises]
E,E
Exchange
Weakening
G,E,F,H
G
I
-Introduction
G, E, F
G, EF
G,E,E
E
G,F,E,H

Contraction
W
C
G,E
G,E
-Introduction
G, E
H, F
G, H, EF

4.9
An example of a proof in sequent calculus
Example. Find a proof of (pq)(r s)  (pr)(qs).
First, we rewrite the formula as [(pq)(r s)][(pr)(qs)].
Next, we construct a proof of it in the bottom-up fashion as follows:
r, r
p, p
p, p, r
p, pr
I
W

q, q
q, q, s
q, qs
p, q, (pr)(qs)
(pr)(qs), p, q
(pr)(qs), pq
I
W


r, r, p
r, p, r
r, pr
I
s, s
W
s, s, q
E
s, q, s

s, qs
r, s, (pr)(qs)
E (twice)

(pr)(qs), r, s
(pr)(qs), rs
(pr)(qs), (pr)(qs), (pq)(r s)
E (twice)
(pq)(r s), (pr)(qs), (pr)(qs)
C
(pq)(r s), (pr)(qs)
[(pq)(r s)][(pr)(qs)]

I
W
E


E (twice)


4.10
Soundness and completeness
Theorem 4.2. For any formula F, we have:
1. (Soundness) If F is provable in G1, then F is a tautology.
2. (Completeness) If F is a tautology, then F is provable in G1.
Soundness:
Completeness:
“Good”
formulas
Provable
formulas
Provable
formulas
“Good”
formulas
In our present case, “good” = “tautological”.
4.11
A sequent calculus system without structural rules
• The Identity rule of G1 can be called an axiom, as it takes no premises.
• The rules -Introduction and -Introduction are called logical rules as they “explain”
the logical meanings of connectives.
• The remaining rules of Exchange, Weakening and Contraction are called structural
rules, as they only restructure sequents and otherwise are not related to any logical
connectives.
Below comes a simpler system --- let us call it G2 --- that has no structural rules
at all. A significant change, however, is that in G2 sequents are seen as sets rather
than sequences of formulas. G2 only has the following three rules, where E,F are
any formulas and G is any “sequent”, i.e. any set of formulas.
Axiom
-Introduction
[no premises]
G, E, F
A
G,E,E
G, EF

-Introduction
G, E
G, F

G, EF
In view of Theorems 4.2 and 4.4, system G2 is equivalent, in its deductive power, to
our old friend G1.
4.12
Another example
Example. Find a proof of [(pq)(r s)][(pr)(qs)] in G2.
We use a standard proof search method, which can be applied to any formula.
The method is to start with the target formula, and keep applying, in the bottom-up
sense, the two logical rules (in whatever order you like) as long as there are
conjunctions or disjunctions in the sequent:
p, q, p, r
p, q, pr
A

p, q, q, s
p, q, qs
p, q, (pr)(qs)
pq, (pr)(qs)
A


r, s, p, r
r, s, pr

A

r, s, q, s
r, s, qs
r, s, (pr)(qs)
rs, (pr)(qs)
(pq)(r s), (pr)(qs)
[(pq)(r s)][(pr)(qs)]
A





You will end up with a tree where all leaves are sequents containing only atoms
and negated atoms. Such a tree is a G2-proof if (and only if) every leaf contains
some atom together with the negation of the same atom.
One can show (see next slide) that the target formula is provable iff this method
generates a proof tree.
4.13
Soundness and completeness proof
We extend the concepts of truth and validity (tautologicity) from formulas to sequents
by understanding each sequent F1,...,Fn as the formula F1...Fn.
Lemma 4.3.
(a) Every sequent which is (the conclusion of) an axiom of G2 is valid.
(b) The two logical rules of G2 preserve validity in both top-down and
bottom-up directions. That is, the premise(s) is (are) valid iff so is the conclusion.
Proof: Obvious. 
Theorem 4.4. (Soundness and completeness of G2:)
A sequent is provable in G2 iff it is valid (tautological).
Proof. The Soundness of G2 is an immediate consequence of Lemma 4.3: Axioms
are valid and the rules preserve validity, so every sequent in a proof tree will be valid.
As for completeness, assume a given formula is valid. Apply to it the method
of Slide 4.12. In view of Lemma 4.3, all sequents in the tree generated by this
method will be valid. This includes the leaves of the tree. But leaves only contain
sequents where every formula is an atom or a negated atom. Obviously such a
sequent is valid iff it is an axiom. Thus, the tree will be a proof tree. 