Transcript Logic and Mathematics

Logic and Mathematics
The Art and Science of
Mathematics
The 4 Color Theorem
• In 1879, Kempe produced a famous proof of the
4 color theorem: any map of countries can be
colored in such a way that no 2 bordering
countries have the same color, using only 4
colors.
• In 1890, Heawood showed the proof not to be a
proof at all!
• When is a proof a proof, and when is it not a
proof?
• Logic to the rescue!
Logic
• Logic is the study of reasoning
• In particular, logic studies the conditions
under which we can say that a piece of
reasoning is valid, i.e. that something (the
conclusion) can be said to follow from
something else (the premises, givens,
assumptions).
Deduction and Induction
• If the conclusion has to be true assuming
the truth of the premises, we call the
reasoning deductive.
• If the conclusion is merely more likely to
be true than false given the truth of the
premises, we call the reasoning inductive.
• Logic studies both deduction and
induction, but does tend to focus on
deduction, especially formal logic.
Normative and Descriptive
Theories of Reasoning
• Psychology of reasoning is a scientific study of
how humans reason:
– What do humans infer from what?
– What is the mechanism behind human reasoning?
• As such, psychologists come up with descriptive
theories of reasoning: hypotheses as to how
humans reason based on empirical studies.
• Logicians, however, try to come up with
normative theories of reasoning:
– What actually follows from what?
• Question: But if not empirical, what is the basis
for such theories? (Human!) reason alone?
Implication and Truth
• Logic tells us about implication, not truth.
• Example: “All flurps are toogle, but not all flems
are toogle, so not all flems are flurps” is perfectly
logical, but tells us nothing about what-is-thecase.
• One exception: Implication itself can be seen as
a kind of (necessary) truth. So, logic can tells us
that certain statements of the form “If
<premises> then <conclusion>” are necessarily
true (i.e. true in all possible worlds), and hence
true in our world as well.
Logic and Science
• Of course, if I do know that my premises are
true, then if the reasoning is (deductively) valid I
know the conclusion to be true as well.
• But that’s just science: science combines
observation (facts) with logic (reasoning), to get
to truth (laws of physics, chemistry, etc).
• Of course, scientific reasoning is inherently
inductive: a finite set of data is always
compatible with multiple theories. Hence:
scientific theories can change over time.
Logic and Mathematics
• Most of what I just said for logic is true for
mathematics as well!
– Scientists use mathematics to help figure out
(calculate, compute, etc) what-is-the-case but
mathematics alone does not tell us what-is-the-case
– Like logic, mathematical theorems are proven from a
set of definitions or axioms: if those axioms or
definitions don’t apply to our world, then the theorem
doesn’t say anything about our world either.
– The only thing we can claim to be certain of is a
statement of the form “If <bunch of
definitions/axioms> then <some claim>”.
– So, theorems like “There is no greatest prime
number” are really expressions of “If we define
‘number’ to be ..., and ‘prime’ as … and ‘greater than’
as …, then there is no greatest prime number.”
Further Similarities Between
Logic and Mathematics
• Both logic and mathematics have been around
for thousands of years
• Both logic and mathematics study abstractions
that can be applied to any subject matter
• Formal logic is probably best seen as a branch
of mathematics
• Mathematics can be applied to formal logic
(mathematical logic)
• Formal logic can be applied to mathematics
(theorem proving)
Formal Logic
• We can determine that “All flurps are toogle, but
not all flems are toogle, so not all flems are
flurps” is a valid inference because of the
abstract form of the reasoning: “All P’s are Q’s,
but not all R’s are Q’s, so not all R’s are P’s”.
• Formal logic is just that: studying the validity of
reasoning by looking at its abstract form:
– Just as in mathematics:
• 1) expressions of abstract symbols are assigned the objects
of study, and
• 2) by manipulating these expressions of abstract symbols,
we can figure something out about these objects.
Little History of Formal Logic
• Formal logic goes back at least to Aristotle, probably
earlier
• In Medieval Times work was being done on categorical
syllogisms like the one on previous page (that one would
be classified as AOO-2)
• ‘Modern’ formal logic was developed in mid 19th century
by people like Georges Boole and Augustus DeMorgan.
They developed the system of propositional or truthfunctional logic.
• The much more powerful system of first-order logic (or
predicate logic or quantificational logic) was completed
by the turn of the 20th century.
• Many other systems of logic have been developed since;
just as with mathematics, different systems have
different applications.
Truth-Functional Logic
• Applies to reasoning dealing with
compound sentences built from truthfunctional operators like ‘and’, ‘or’, ‘not’,
and ‘if … then’.
• An operator is truth-functional in that the
truth-value of a sentence like “P and Q” is
a function of the truth-values of the
sentences P and Q.
Truth-Tables
P P
T F
F T
P
T
T
F
F
Q PQ
T
T
F
F
T
F
F
F
P
T
T
F
F
Q PQ
T
T
F
T
T
T
F
F
De Morgan’s Laws
P
T
T
F
F
Q
T
F
T
F
(P 
F
T
T
T
↑
T
F
F
F
Q)
P  Q
F
F
T
T
F
T
T
T
↑
F
T
F
T
(P 
F
F
F
T
↑
Q)
T
T
T
F
P  Q
F
F
T
T
F
F
F
T
↑
F
T
F
T
Modus Ponens
PQ
P
Q
P
T
T
F
F
Q PQ
T
T
F
F
T
T
F
T
P
T
T
F
F
Q
T
F
T
F
←
Ladies and Tigers
• The prisoner is told that if there is a lady in
room I, then its sign is true, but if there is a
tiger in the room, then its sign is false. For
room II, it is exactly the opposite.
• Sign I says: ‘Both rooms contain ladies’
• Sign II says: ‘Both rooms contain ladies’
• Question: Which room should the prisoner
pick?
Truth-Table Solution
L1
T
T
F
F
L2 L1  L2
T
T
F
F
T
F
F
F
L1  (L1  L2)
T
F
T
T
L2  (L1  L2)
F
F
T
←
F
Boolean Algebra Solution
L2  (L1  L2)  (Equivalence)
(L2  (L1  L2)  (L2 → (L1  L2)  (Transposition)
(L2 → (L1  L2)  ((L1 L2) → L2)  (Implication)
(L2 → (L1  L2)  ((L1  L2)  L2)  (Double Neg.)
(L2 → (L1  L2)  ((L1  L2)  L2)  (Subsumption)
(L2 → (L1  L2)  L2  (Implication)
(L2  (L1  L2))  L2  (De Morgan)
(L2  (L1  L2))  L2  (Commutation)
(L2  (L2  L1))  L2  (Association)
((L2  L2)  L1)  L2  (Idempotence)
(L2  L1)  L2  (Distribution)
(L2  L2)  (L1  L2)  (Contradiction)
  (L1  L2)  (Contradiction)
L1  L2
Formal Proof Solution
1.
L1  (L1  L2)
Assumption
2.
L2  (L1  L2)
Assumption
3.
L2
4.
5.
6.
Assumption
(L1  L2)
Assumption
L2
 Elim 2, 4

 Intro 3, 5
7.
(L1  L2)
 Intro 4-6
8.
L1  L2
 Elim 7
9.
L2
 Elim 8
10.

11.
1. L2
12. L2
 Intro 3, 9
 Intro 3-10
 Elim 11
The Dreadsbury Mansion Problem
• Someone who lived at the Dreadsbury Mansion
killed Aunt Agatha. Agatha, the butler, and
Charlie were the only ones living at the
Dreadsbury Mansion. A killer always hates its
victim but is never richer than its victim.
Whomever aunt Agatha hated, Charlie did not
hate. Agatha hated everybody but the butler. The
butler hated everybody not richer than aunt
Agatha, as well as everyone that aunt Agatha
hated. No one who lived at the mansion hated
everybody who was living at the mansion.
Finally, aunt Agatha was not the butler. Who
killed aunt Agatha?
Automated Theorem Proving
• Formal proofs seem perfect for automation:
proofs require tediously many applications of
precisely defined rules: just something a
computer would be good at!
• Problem: the rules of logic are like the rules of
chess: they tell you what you can do, but not
what you must do.
• In Automated Theorem Proving (a branch of
Artificial Intelligence) researchers try and come
up with algorithms to create formal proofs (to be
exact: they come up with algorithms to check
whether some inference is valid or not).
Axiomatization
• In fact, why not do this: Express basic axioms
and definitions about various branches of
mathematics in logic, and simply run an ATP to
automatically prove all theorems about any
branch of mathematics!
• This ambitious project was called the Hilbert
Program, after the mathematician David Hilbert
who proposed it at the turn of the 20th century.
The MetaMath Project
• Check it out!
• www.metamath.org
Godel’s Incompleteness Result
• Unfortunately (or fortunately?), the Hilbert
Program failed, and necessarily so.
• In 1931 Kurt Godel proved that the idea couldn’t
work for simple arithmetic, let alone all of
mathematics.
• Godel showed that for any finite set of axioms
for arithmetic (just dealing with addition and
multiplication for natural numbers) there is an
arithmetical truth that cannot be derived from
those axioms.
Arithmetic is Undecidable
• In fact, based on computability theory
(starting with Turing in 1936) we have
excellent reasons to believe that arithmetic
is undecidable, i.e. that there is no
systematic procedure (computer program)
that can decide for any first-order logic
arithmetical statement whether it is true or
false!
So what does this mean?
• Well, if one believes that human mathematicians
are able to figure out (in principle of course!) all
arithmetical truths, then it is false that human
information processing can be captured by a
computer program. In short, AI is a pipe dream!
• On the other hand, if you do believe that human
thought can be captured by some kind of
computer program (as many cognitive scientists
believe), then it seems that there will be truths
(in simple arithmetic!) that we won’t be able to
figure out.
How good are
Automated Theorem Provers?
• Frankly, they stink!
• In 1956, the Logic Theorist was able to prove theorem
2.16 of Russell and Whitehead’s book Principia
Mathematica: (P → Q) → (Q → P) given basic
axioms about propositional logic
• 50 years later, the best ATP’s around still can’t prove that
P() = {} given basic set theory axioms
• Some researchers see this as evidence that human
thought cannot be captured through computation, but
others say it’s too early to tell.
• For practical matters though, the best approach would
be to combine human intellect with computational effort:
Assisted Theorem Proving: the human lays out the ‘proof
plan’, and the ATP will fill in the details.
The 4 Color Theorem
• In fact, this is exactly how the 4 color theorem was finally proven in
1976: Appel and Haken used a computer running for 1200 hours to
finally settle this conjecture.
• Or did they?
• At first, the proof was regarded with much skepticism, as it wasn’t
verifiable by hand in any reasonable manner.
• In fact, the proof is of course only reliable as far as the computer
program was reliable, i.e. did what it was supposed to do. So, you’d
need to prove that the computer program was reliable.
• Also, the program didn’t produce anything that we would recognize
as a formal proof.
• In 2004, Werner and Gonthier produced a proof using Coq, an
Automated Theorem Prover, finally producing a ‘proof-like’ object for
the 4 color theorem.
• So, assuming Coq has been verified for working as it should be,
that’s it then, right?
Are my Logic Rules Logical?
• Well, one tiny problem.
• Suppose I am a real stickler, and
challenge the validity of the logical
inference rules as defined.
• In other words, in order for me to accept a
formal logic proof of some theorem, I need
to be able to accept the validity of the
inference rules used in that proof.
Modus Bogus and
Hokus Ponens
PQ
Q
P
Modus Bogus
P
Hokus Ponens
Clearly, Modus Bogus and Hokus Ponens are not acceptable!
But what about Modus Ponens?
• Earlier I demonstrated the validity of Modus
Ponens using a truth table.
• However, I thus reasoned as follows: If the truthtable of some argument reveals that there is no
row where the premises of that argument are
true, while its conclusion is false, then that
argument is valid. The truth-table for Modus
Ponens shows that there is no row where its
premises are true and the conclusion is false.
Hence, Modus Ponens is valid.
• But what logic did I just use? Modus Ponens!
• Hmm…
Interested in Logic?
• PHIL 2140 – Introduction to Logic (I think a must
for all Math majors)
• PHIL 4XXX – Intermediate Logic (applying logic
to mathematics)
• PHIL 4420 – Computability and Logic (applying
mathematics to logic, including a proof of
Godel’s incompleteness theorem)
• Also: PHIL/PSYC 2xxx – Methods of Reasoning
(more informal logic and psychology of
reasoning; good course to improve your
everyday life reasoning skills!)