Transcript Logic

Brief Introduction to Logic
Outline
•
•
•
•
•
Historical View
Propositional Logic : Syntax
Propositional Logic : Semantics
Satisfiability
Natural Deduction : Proofs.
Historical view
• Philosophical Logic
– 500 BC to 19th Century
• Symbolic Logic
– Mid to late 19th Century
• Mathematical Logic
– Late 19th to mid 20th Century
• Logic in Computer Science
Philosophical Logic
• 500 B.C – 19th Century
• Logic dealt with arguments in the
natural language used by humans.
• Example
– All men are motal.
– Socrates is a man
– Therefore, Socrates is mortal.
Philosophical Logic
• Natural language is very ambiguous.
– Eric does not believe that Mary can pass any
test.
– I only borrowed your car.
– Tom hates Jim and he likes Mary.
• It led to many paradoxes.
– “This sentence is a lie.” (The Liar’s Paradox)
The Sophist’s Paradox
• A Sophist is sued for his tuition by
the school that educated him. He
argued that he must win, since, if he
loses, the school didn’t educated him
well enough, and doesn’t deserve the
money. The school argue that he
must loss, since, if he win, he was
educated well enough therefore
should pay for it.
Symbolic Logic
• Mid to late 19th Century.
• Attempted to formulate logic in terms
of a mathematical language
• Rules of inference were modeled
after various laws for manipulating
algebraic expressions.
Mathematical Logic
• Late 19th to mid 20th Century
• Frege proposed logic as a language for
mathematics in 1879.
• With the rigor of this new foundation,
Cantor was able to analyze the notion of
infinity in ways that were previously
impossible. (2N is strictly larger than N)
• Russell’s Paradox
T = { S | S ∉ S}
Logic in Computer Science
• In computer science, we design and
study systems through the use of
formal languages that can themselves
be interpreted by a formal system.
–
–
–
–
Boolean circuits
Programming languages
Design Validation and verification
AI, Security. Etc.
Logics in Computer Science
•
•
•
•
•
•
•
Propositional Logic
First Order Logic
Higher Order Logic
Theory of Construction
Real-time Logic, Temporal Logic
Process Algebras
Linear Logic
Syntax
•
•
•
•
The symbol of the language.
Propositional symbols: A, B, C,…
Prop: set of propositional symbols
Connectives:  (and),  (or),  (not),
 (implies),  (is equivalent to), 
(false).
• Parenthesis: (, ).
Formulas
• Backus-Naur Form
– Form := Prop | (Form) | (Form o Form).
• Context-Free Grammar
– Form  Prop,
– Form  ( Form),
– Form  (Form o Form)
Formulas (2)
• The set of formulas, Form, is defined
as the smallest set of expressions
such that:
1.Prop  Form
2.pForm
 (p)Form
3.p,q Form  (p o q)  Form
Formulas (3)
• Examples:
–
–
–
–
–
(A)
((A))
(A  (B  C))
(A (B C))
Correct expressions of
Logic
are
full
of
parenthesis.
Propositional
unnecessary
Formulas (4)
• Abbreviations. Let o=, , . We write
AoBoCo…
• in the place of
(A o (B o (C o …)))
• Thus, we write
A  B  C,
ABC, …
• in the place of
(A  (B  C)),
(A (B C))
Formulas (5)
• We omit parenthesis whenever we may
restore them through operator precedence:
•  binds more strictly than , , and , 
bind more strictly than , .
• Thus, we write:
A
A B
A B C for
for
((A)),
for
((A ) B)
((AB)  C), …
Semantics
• Def) A truth assignment, , is an
elements of 2Prop(I.e.,   2Prop).
• Two ways to think of truth assignment
– 1) X ⊆ Prop
– 2)  : Prop ↦ {0,1}
• Note : These notions are equivalence.
Philosopher’s view
•  |= p means
–  satisfies p or
–  is true of p or
– p holds at  or
–  is a model of p
Satisfaction Relation
• Def 1) |= ⊆ (2Prop x Form)
–
–
–
–
–
–






|=
|=
|=
|=
|=
|=
A if  (A) =1 (or, A  )
p if it is not the case  |= p.
pq if  |= p and  |= q
p  q if  |= p or  |= q
p  q if  |= p implies  |= q
p  q if  |= p iff  |= q
Satisfaction Relation
• {A,B} |= A  B
– Iff {A,B} |= A and {A,B} |= B
– Iff A  {A,B} and B  {A,B}
Electrical Engineer’s view
• A mapping of voltages on a wire  :
Prop  {0,1}
– : {0,1}  {0,1}
• (0) = 1 and (1) = 0
– : {0,1}2  {0,1}
• (0,0)= (0,1)= (1,0)=0 and (1,1)=1
–  : {0,1}2  {0,1}
• (1,1)= (0,1)= (1,0)=1 and (0,0)=0
Semantics
• Def 2)
– A() = (A)
– (p)() = (p())
– (p o q)() = o(p(), q())
• Lemma) Let p  Form and   2Prop,
then  |= p iff p() = 1.
Software Engineer’s view
• Intuition : a formula specifies a set of truth
assignments.
Prop
2
• Def 3) Function Models : From  2
–
–
–
–
–
models(A) = { |(A) = 1}, A  Prop
models(p) = 2Prop – models(p)
models(pq) = models(p)  models(q)
models(pq) = models(p)  models(q)
models(pq) = (2Prop – models(p))  models(q)
Theorem
• Let p  Form and   2Prop, then the
following statements are all true:
– 1.  |= p
– 2. p() = 1
– 3.   models(p)
Relevance Lemma
• Let’s use AP(p) to denote the set of
all propositional symbols occurred in
p. Let 1, 2  2Prop, pForm.
• Lemma) if 1|AP(p) = 2|AP(p) , then
1|= p iff 2 |= p
Corollary) | = p iff |AP(p) |= p
Algorithmic Perspective
• Truth Evaluation Problem
– Given pForm and   2AP(p),
does  |= p ? Does p() = 1 ?
• Eval(p, ):
– If p  A, return (A).
– If p  (q), return (Eval(q, ))
– If p  (q o r), return o(Eval(p), Eval(q))
• Eval uses polynomial time and space.
Extension of |=
• Let T  2Prop,   Form
• Def) T |= p if T  models(p)
– i.e., |=  22
Prop
X Form
• Def) T |=  if T  models()
– models() = p models(p)
Prop
2
– I.e., |=  2
X 2Form
Extension of |=
• |=  2Form x 2Form
• Def) 1 |= 2
iff models(1)  models(2)
Iff for all   2Prop
if  |= 1 then  |= 2
Semantic Classification
• A formula p is called valid if models(p)
= 2Prop. We denote validity of the
formula p by |=p
• A formula p is called satisfiable if
models(p) ≠ .
• A formula is not satisfiable is called
unsatisfiable or contradiction.
Semantic Classification(II)
• Lemma
– A formula p is valid iff p is unsatifiable
– p is satisfiable iff p is not valid
• Lemma
– p |= q iff |= (p  q)
Satisfiability Problem
• Given a p, is p satisfiable?
• SAT(p)
B:=0
for all   2AP(p)
B = B  Eval(p,)
end
return B
• NP-Complete
Proofs
• Formal Proofs. We introduce a notion
of formal proof of a formula p:
Natural Deduction.
• A formal proof of p is a tree whose
root is labeled p and whose children
are assumptions p1, p2, p3, … of the
rule r we used to conclude p.
Proofs
• Natural Deduction: Rules. For each logical
symbol o=, , , , and each formula p
with outermost connective o, we give:
• A set of Introduction rules for o,
describing under which conditions p is
true;
• A set of Elimination rules for o,
describing what we may infer from the
truth of p.
Proofs
• Natural Deduction: notations for proofs.
• Let p be any formula, and  be a set of
formulas. We use the notation

…
p
• abbreviated by |- p, for:
• “there is a proof of p whose assumptions are
included in ”.
Proofs
• Natural Deduction: assumptions of a proof
p1
p2
p3
…
r -------------------------------p
• are inductively defined as:
• all assumptions of proofs of p1, p2, p3, …,
minus all assumptions we “crossed”.
Proofs
• Identity Principle: The simplest proof is:
p
----p
• having 1 assumption, p, and conclusion
the same p.
• We may express it by: |-p, for all p
• We call this proof “The Identity Principle”
(from p we derive p).
Proofs
• Rules for 
• Introduction rules: none ( is always
false).
• Elimination rules: from the truth of  (a
contradiction) we derive everything:

---p
If |- , then |-p, for all p
Proofs
• Rules for 
• Introduction rules:
p
q
-------pq
• If |- p and |- q then |- p  q
Proofs
• Elimination rules:
pq
-------p
pq
------q
• If |- p  q, then |- p and |- q
Proofs
• Rules for 
Introduction rule:
[p]
…
q
-------pq
• If ,p |- q, then |-pq
• We may drop any number of assumptions equal
to p from the proof of q.
Proofs
• Elimination rule:
pq
p
---------------q
• If |-pq and |-p, then  |- q.
Proofs
• The only axiom not associated to a connective,
nor justified by some Introduction rule, is Double
Negation:
[p]
….

--p
• If , p|- , then |-p
• We may drop any number of assumptions equal
to p from the proof of q.
Soundness
|- p then
|= p
Completeness
|= p then |- p