Transcript PPT

Logic in Computer Science Overview
박성우
Sep 1, 2011
POSTECH
Introduction to Logic
[ inspired by The Universal Computer, Martin Davis]
Logic
• Study of propositions and their use in argumentation
(Encyclopædia Britannica)
– Propositions
(A Æ B) ¾ (B Æ A)
AÇ:A
– Argumentation
(A Æ B) ¾ (B Æ A) is true or false?
(A Æ B) ¾ (B Æ A) is provable or not provable?
• Use of a system of symbols for reasoning or deduction
3
Aristotle [384 BC - 322 BC]
• Syllogisms
– inferences from premises to a conclusion
– sentences
• All X are Y.
No X are Y.
• Some X are Y.
Some X are not Y.
– valid:
All X are Y
All Y are Z
-------------All X are Z
All students are humans
All humans are animals
-------------------------------------All students are animals
4
Gottfried Leibniz [1646 - 1716]
• Inventor of differential and integral calculus
– mathematics reduces to manipulating symbols
• Dream: Calculus ratiocinator
– bring human reasoning under mathematical laws
– use symbols
5
George Boole [1815 - 1864]
• Turns logic into (Boolean) algebra
•
•
•
•
•
•
•
•
L = Joe left his checkbook at the supermarket
F = Joe's checkbook was found at the supermarket
W = Joe wrote a check at the restaurant last night
P = After writing the check last night,
Joe put his checkbook in his jacket pocket
H = Joe hasn't used his checkbook since last night
S = Joe's checkbook is still in his jacket pocket
Premises:
- If L, then F.
- W and P.
- H.
Conclusions:
- Not L.
- Not F.
- If W and P and H, then S.
- S.
6
Gottlob Frege [1848 - 1925]
• Breakthrough: first-order logic
– formal syntax
– universal (for all) and existential (some) quantifiers
A ::= P(x) | A ¾ A | A Æ A | A Ç A | :A | 8x.A | 9x.A
• ... shown to be self-contradictory by Russell
7
Bertrand Russell [1872 - 1970]
• Coauthored Principia Mathematica
• Russell's paradox
– shows that the set theory by Georg Cantor is
inconsistent
"a set containing all sets that are not members
of themselves"
• Proposes type theory
8
Further Story
• Georg Cantor [1845 - 1918]
– set theory, diagonal argument
• David Hilbert [1862 - 1943]
– Hilbert's program
• Kurt Gödel [1906 - 1978]
– incompleteness theorem, undecidability
• Alan Turing [1912 - 1954]
– Turing machine, algorithmic unsolvability
• John von Neumann [1903 - 1957]
– von Neumann architecture
9
Outline
• Methodology
– Model theory (모델이론)
– Proof theory (증명이론)
• Philosophy
– Classical logic
– Constructive logic
10
Model Theory vs. Proof Theory
Model theory
• Model
¼ assignment of
truth values
Proof theory
• Inference rules
– use premises
to obtain the conclusion
• Semantic consequence
A1, ¢¢¢, An ² C
• Syntactic entailment
A1, ¢¢¢, An ` C
11
Disjunction & Implication
12
) Truth of A is not affected by truth of B.
13
Inference Rules in Proof Theory
• With premises
• Axioms
14
Three Types of Systems
1. Hilbert-type system (Axiomatic system)
2. Natural deduction system
3. Sequent calculus
15
1. Hilbert-type System
• Consists of axioms and Modus Ponens
• Axioms
I :A¾A
K : A ¾ (B ¾ A)
S : (A ¾ (B ¾ C)) ¾ ((A ¾ B) ¾ (A ¾ C))
• Inference rule
16
2. Natural Deduction System
• Introduced by Gentzen, 1934
• For each connective Æ, Ç, ¾, ...
– introduction rule(s)
– elimination rule(s)
17
Implication
18
Outline
• Methodology
– Model theory
– Proof theory
• Philosophy
– Classical logic (고전 논리)
– Constructive logic (건설적 논리, 직관 논리)
(¼ intuitionistic logic)
19
Tautology
Intuitive interpretation of
) Truth of A is not affected by truth of B.
20
Tautology
But what is an intuitive interpretation of
21
Classical Logic
• Concerned with:
– "whether a given proposition is true or not."
• Logic from God's point of view
– Every proposition is either true or false.
• Tautologies in classical logic
¼ Logic for mathematics
22
Constructive Logic
• Concerned with:
– "how a given proposition becomes true."
• Logic from a human's point of view
– we know only what we can prove.
• Not true in constructive logic (for all A and B)
¼ Logic for computer science
23
Example
• Theorem:
There are two irrational numbers a and b
such that ab is rational.
• Proof in classical logic:
– Let c = p2p2
If c is rational, we take a = b = p2.
If c is not rational, we take a = c and b = p2.
• Proof in constructive logic:
– a lot more involved, but presents a procedure for
computing a and b.
24
This course is about
Constructive Proof Theory.
Natural deduction
Curry-Howard isomorphism
First-order logic
Sequent calculus
Classical logic
Automated theorem proving
Welcome to
the world of logic!