Logic in Computer Science
An Introductory Course for Master Students
Wang Ji
jiwang@nudt.edu.cn
Lecture 2
Propositional Calculus
Logic in Computer Science { p.1/39
Syntax
Formation Rules for P
The The Axiomatic Structure of P
Theorems and Derived Rules
Logic in Computer Science { p.2/39
Primitive Symbols
The primitive symbols of P are the following:
Improper symbols: (; ); ;_
Proper symbols: denumerably many
propositional variable, p;q;r;p
1
;q
1
;r
1
;
:The set of Primitive Symbols
Logic in Computer Science { p.3/39
Well-Formed Formulas
The set of w s is the intersection of all sets S of
formulas such that:
1. p 2 S for each propositional variable p
2. For each formula A, if A 2 S, then ( A) 2 S
3. For all formulas A and B, if A 2 S and B 2 S,
then (A _ B) 2 S
A w is a member of the set of w s.
Logic in Computer Science { p.4/39
Principle of Induction on W
Let < be a property of formulas, and let <(A) mean
that A has property <. Suppose
1. <(q) for each propositional variable q.
2. Whenever <(A), then <( A).
3. Whenever <(A) and <(B), then <((A _ B)).
Then every w has property <.
Logic in Computer Science { p.5/39
Abbreviations
(A ^ B) stands for ( A_ B)
(A B) stands for ( A _ B)
(A B) stands for ((A B) ^ (B A))
Logic in Computer Science { p.6/39
Substitution
A function :
!
is a substitution i
1. If x 2 , then (x) 6=
2. If x;y 2
, then (xy) = (x) (y)
If
1
and
2
are substitutions such that
1
(x) =
2
(x)
for every primitive symbol x, then
1
=
2
Logic in Computer Science { p.7/39
Substitution(Continued)
A substitution is nite i fx 2 j (x) 6= xg is
nite.
A substitution is a substitution for variables i
the only primitive symbols x such that (x) 6= x
are variables.
Let x
1
; ;x
n
be distinct primitive symbols and
let Y
1
; ;Y
n
be formulas. S
x
1
; ;x
n
Y
1
; ;Y
n
is a
substitution such that
(x) =
8
<
:
Y
i
if x = x
i
; 1 i n
x if x 62 fx
1
; ;x
n
g
Logic in Computer Science { p.8/39
The Axiomatic Structure of P
Axiom Schema 1 A _ A A
Axiom Schema 2 A (B _ A)
Axiom Schema 3 A B (C _A (B _C))
Modus Ponens (MP)
A; A B
B
Logic in Computer Science { p.9/39
The Axiomatic Structure of P
Axiom Schema 1 A _ A A
Axiom Schema 2 A (B _ A)
Axiom Schema 3 A B (C _A (B _C))
Modus Ponens (MP)
A; A B
B
Logic in Computer Science { p.9/39
The Axiomatic Structure of P
Axiom Schema 1 A _ A A
Axiom Schema 2 A (B _ A)
Axiom Schema 3 A B (C _A (B _C))
Modus Ponens (MP)
A; A B
B
Logic in Computer Science { p.9/39
The Axiomatic Structure of P
Axiom Schema 1 A _ A A
Axiom Schema 2 A (B _ A)
Axiom Schema 3 A B (C _A (B _C))
Modus Ponens (MP)
A; A B
B
Logic in Computer Science { p.9/39
The Axiomatic Structure of P
Axiom Schema 1 A _ A A
Axiom Schema 2 A (B _ A)
Axiom Schema 3 A B (C _A (B _C))
Modus Ponens (MP)
A; A B
B
Logic in Computer Science { p.9/39
What is a Proof
A proof of a w B from the set of hypotheses is a
nite sequence B
1
;B
2
; ;B
m
of w s such that
B
m
is B, and
for each j(1 j m) at least one the following
conditions is satis ed.
1. B
j
is an axiom;
2. B
j
2 ;
3. B
j
is inferred by MP from w s B
i
and B
k
,
where i < j and k < j.
Logic in Computer Science { p.10/39
‘
‘ B
There is a proof of B from .
‘ B
A proof of a w B is a proof of B from the
empty set of hypotheses. A theorem is a w
which has a proof.
Logic in Computer Science { p.11/39
Formal System
formal system =
+ Formation Rules
+ Axioms
+ Rules
Logic in Computer Science { p.12/39
2 and 2
+
2
If A 2 , then ‘ A.
2
+
If
1
‘ A and
1
2
, then
2
‘ A.
Logic in Computer Science { p.13/39
MP
If
1
‘ A and
2
‘ A B
and
1
and
2
,
then
‘ B
Logic in Computer Science { p.14/39
Rule of Substitution(Sub)
If ‘ A, and if p
1
; ;p
n
are distinct variables
which do not occur in any w in , then
‘ S
p
1
; ;p
n
B
1
; ;B
n
A
Proof Sketch. Let be the substitution S
p
1
; ;p
n
B
1
; ;B
n
. It
is easy to see that if C
1
; ;C
m
is a proof of A from
, then (C
1
); ; (C
m
) is a proof of (A) from .
Logic in Computer Science { p.15/39
Derived Rules
DR
1
If ‘ A B and ‘ C _ A then
‘ B _ C.
‘ A_ A
‘ A A
‘ A A
‘ A A
‘ A A
Logic in Computer Science { p.16/39
Derived Rules
Commut If ‘ A _ B then ‘ B _ A.
Trans If
1
‘ A B,
2
‘ B C,
1
and
2
, then ‘ A C.
DR
2
If
1
‘ A C,
2
‘ B C,
1
and
2
, then ‘ A _ B C.
DR
3
If
1
‘ A C,
2
‘ A C,
1
and
2
, then ‘ C.
DR
4
If ‘ A B, then ‘ A (C _ B) and
‘ A (B _ C)
Assoc ‘ (A _ B) _ C i ‘ A _ (B _ C)
DR
5
If
1
‘ A B,
2
‘ A (B C),
1
and
2
, then ‘ A C
Logic in Computer Science { p.17/39
Deduction Theorem
If ;A ‘ B then ‘ A B
Proof Sketch: Let C
1
; ;C
m
be a proof from B
from . We Prove
‘ A C
i
for all i(1 i m) by induction on i.
Logic in Computer Science { p.18/39
Theorems
‘ A ( B (A _ B))
‘ A ( A B)
Logic in Computer Science { p.19/39
Frequently Used Rules
(2
) If
1
;A ‘ B,
2
; A ‘ B,
1
and
2
, then ‘ B
(::
+
) If ‘ A, then ‘ A
(::
) If ‘ A, then ‘ A
(:
+
) If ;A ‘ B, ;A ‘ B, then ‘ A
(DR) If ‘ A, ‘ A, then ‘ B
Logic in Computer Science { p.20/39
Proof Systems
Hilbert-style proof system
Gentzen’s National Deduction Systems
The Sequent Calculus
Logic in Computer Science { p.21/39
A Hilbert-style proof system
Axiom K
A (B A)
Axiom S
(A (B C)) ((A B) (A C))
Axiom DN
A A
Modus Ponens
A B A
B
Logic in Computer Science { p.22/39
Gentzen’s National Deduction Systems
National Deduction is based upon three principles.
1. Proof takes place within a varying context of
assumptions.
2. Each logical connective is de ned independently
of the others.
3. Each connective is de ned by introduction and
elimination rules.
Logic in Computer Science { p.23/39
The sequent calculus
A sequent has the form
)
where and are nite set of formulas.
The sequent
A
1
;A
2
; ;A
m
) B
1
;B
2
; ;B
n
is true if
A
1
^ A
2
^ ^ A
m
B
1
_ B
2
_ _ B
n
:
Logic in Computer Science { p.24/39
Sequent Rules
basis sequent A; ) A;
Negation rules
) ;A
A; )
(:l)
A; )
) ; A
(:r)
Conjunction rules
A;B; )
A ^ B; )
(^l)
) ;A ) ;B
) ;A ^ B
(^r)
Logic in Computer Science { p.25/39
Sequent Rules
Disjunction rules
A; ) B; )
A _ B; )
(_l)
) ;A;B
) ;A _ B
(_r)
Implication rules
) ;A B; )
A B; )
(! l)
A; ) ;B
) ;A B
(! r)
Logic in Computer Science { p.26/39
Structural Rules
Weakening rules
)
A; )
(w : l)
)
) ;A
(w : r)
Exchange rules
Contract rules
A;A; )
A; )
(c : l)
) ;A;A
) ;A
(c : r)
Cut rule
) ;A A; )
)
(cut)
Logic in Computer Science { p.27/39
Semantics
Logic in Computer Science { p.28/39
Operations over Truth Values
Truth Values
T; F
Operations
:;_;^; ;
8
<
:
:T = F
:F = T
8
<
:
F _ F = F
F _ T = T _ F = T _ T = T
Logic in Computer Science { p.29/39
Assignment
An assignment of truth values to propositional
variables is a function from the set of variables to the
set of fT, Fg of truth values.
An assignment of w A
: V ar(A) ! fT; Fg
An assignment of
: V ar( ) ! fT; Fg
Logic in Computer Science { p.30/39
The Semantic Function V
V
: L(P) ! fT; Fg
The value V
(A) of a w A with respect to the
assignment is de ned as follows by induction on
the construction of A:
1. V
(p) = (p)
2. V
( B) = :V
(B)
3. V
(B _ C) = V
(B)_V
(C)
Logic in Computer Science { p.31/39
Related Concepts
1. A is true with respect to if V
(A) = T, and
false with respect to if V
(A) = F.
2. A is a tautology(j= A). A is a contradiction.
3. satis es A(j=
A).
4. satis es . Note that every assignment
satis es the empty set of w s.
5. is satis able. is unsatis able or
contradictory.
Logic in Computer Science { p.32/39
Unique Readability
To prove that we have used enough parentheses to
eliminate any ambiguity in analyzing w s.
1. Every w has the same number of left as right
parentheses.
2. Any proper initial segment of a w contains an
excess of left parentheses.
3. No proper initial segment of a w can itself be a
w .
Logic in Computer Science { p.33/39
Unique Readability Theorem
and _, when restricted to the set of w s,
have ranges which are disjoint from each other
and from the set of propositional variables, and
are one to one.
Logic in Computer Science { p.34/39
Validity and Soundness
A w of a logistic system is valid w.r.t an
interpretation i the value of that w is truth(under
that interpretation) for all assignments of values to
its (free) variables.
An interpretation of a logistic system is
emphasissound i , under that interpretation, the
axioms are all valid and the rules of inference
preserve validity.
Logic in Computer Science { p.35/39
Soundness Theorem
A w of P is a tautology if it is valid under the
interpretation which is implicit in the de nition of
the valuation function V
.
Every theorem of P is a tautology.
If ‘ A then j= A.
Logic in Computer Science { p.36/39
Consistency
A logistic system is absolutely consistent i there
is a w which is not a theorem.
A logistic system is consistent w.r.t negation i
there is no w A such that both A and A are
theorems.
is consistent i there is a w A such that
6‘ A.
Logic in Computer Science { p.37/39
Consistency
Let S be any logistic system in which
A ( A B)
is a theorem schema and in which MP is a primitive
or derived rule. Then S is absolutely consistent i S
is consistent w.r.t negation.
Logic in Computer Science { p.38/39
Consistency Theorem
P is absolutely consistent and consistent w.r.t
negation.
Lemma:
If is consistent and A 62 Th( ) then [f Ag is
consistent.
Logic in Computer Science { p.39/39