Class 36: Proofs about Unprovability David Evans University

Class 36: Proofs about Unprovability David Evans University

Class 36: Proofs about Unprovability David Evans University of Virginia cs1120 Story So Far Much of the course so far: Getting comfortable with recursive definitions

Learning to write programs that do (almost) anything (PS1-4) Learning more expressive ways of programming (PS5-7) Starting today and much of the rest of the course: Getting un-comfortable with recursive definitions Understanding why there are some things no program can do! Monday

Computer Science (Imperative Knowledge) Are there (well-defined) problems that cannot be solved by any procedure? Today Computer Science/Mathematics Mathematics (Declarative Knowledge)

Are there true conjectures that cannot be the shown using any proof? Mechanical Reasoning Aristotle (~350BC): Organon Codify logical deduction with rules of inference (syllogisms) Every A is a P X is an A X is a P

Every human is mortal. Gdel is human. Gdel is mortal. Premises Conclusion More Mechanical Reasoning Euclid (~300BC): Elements We can reduce geometry to a few axioms and

derive the rest by following rules Newton (1687): Philosophi Naturalis Principia Mathematica We can reduce the motion of objects (including planets) to following axioms (laws) mechanically Mechanical Reasoning 1800s mathematicians work on codifying laws of reasoning

George Boole (1815-1864) Laws of Thought Augustus De Morgan (1806-1871) De Morgans laws proof by induction Bertrand Russell (1872-1970) 1910-1913: Principia

Mathematica (with Alfred Whitehead) 1918: Imprisoned for pacifism 1950: Nobel Prize in Literature 1955: Russell-Einstein Manifesto 1967: War Crimes in Vietnam Note: this is the same Russell who wrote In Praise of Idleness! When Einstein said, Great spirits have

always encountered violent opposition from mediocre minds. he was talking about Bertrand Russell. All true statements about numbers

Perfect Axiomatic System Derives all true statements, and no false statements starting from a finite number of axioms and following mechanical inference rules. Incomplete Axiomatic System incomplete

Derives some, but not all true statements, and no false statements starting from a finite number of axioms and following mechanical inference rules. Inconsistent Axiomatic System

Derives all true statements, and some false statements starting from a finite number of axioms and following mechanical inference rules. some false statements Principia Mathematica

Whitehead and Russell (1910 1913) Three Volumes, 2000 pages Attempted to axiomatize mathematical reasoning Define mathematical entities (like numbers) using logic Derive mathematical truths by following mechanical rules of inference Claimed to be complete and consistent All true theorems could be derived No falsehoods could be derived

Russells Paradox Some sets are not members of themselves e.g., set of all Jeffersonians Some sets are members of themselves e.g., set of all things that are non-Jeffersonian S = the set of all sets that are not members of themselves

Is S a member of itself? Russells Paradox S = set of all sets that are not members of themselves Is S a member of itself? If S is an element of S, then S is a member of itself and should not be in S. If S is not an element of S, then S is not a member

of itself, and should be in S. Ban Self-Reference? Principia Mathematica attempted to resolve this paragraph by banning self-reference Every set has a type The lowest type of set can contain only objects, not sets The next type of set can contain objects and sets of objects, but not sets of sets

Russells Resolution (?) Set ::= Setn Set0 ::= { x | x is an Object } Setn ::= { x | x is an Object or a Setn - 1 } S: Setn it is a Setnofso,itself? it cant be a member of a Setn Is SNo, a member

Epimenides Paradox Epidenides (a Cretan): All Cretans are liars. Equivalently: This statement is false. Russells types can help with the set paradox, but not with these. Gdels Solution

All consistent axiomatic formulations of number theory include undecidable propositions. undecidable cannot be proven either true or false inside the system. Kurt Gdel Born 1906 in Brno (now Czech Republic, then Austria-Hungary)

1931: publishes ber formal unentscheidbare Stze der Principia Mathematica und verwandter Systeme (On Formally Undecidable Propositions of Principia Mathematica and Related Systems) 1939: flees Vienna

Institute for Advanced Study, Princeton Died in 1978 convinced everything was poisoned and refused to eat Gdels Theorem In the Principia Mathematica system, there are statements that cannot be

proven either true or false. Gdels Theorem In any interesting rigid system, there are statements that cannot be proven either true or false. Gdels Theorem All logical systems of any complexity are incomplete: there are statements

that are true that cannot be proven within the system. Proof General Idea Theorem: In the Principia Mathematica system, there are statements that cannot be proven either true or false. Proof: Find such a statement

Gdels Statement G: This statement does not have any proof in the system of Principia Mathematica. G is unprovable, but true! Gdels Proof Idea G: This statement does not have any proof in the system of PM.

If G is provable, PM would be inconsistent. If G is unprovable, PM would be incomplete. Thus, PM cannot be complete and consistent! Gdels Statement G: This statement does not have any proof in the system of PM. Possibilities: 1. G is true G has no proof System is incomplete

2. G is false G has a proof System is inconsistent incomplete Pick one: Derives some, but not all true statements, and no false

statements starting from a finite number of axioms and following mechanical inference rules. Incomplete Axiomatic System some false statements

Derives all true statements, and some false statements starting from a finite number of axioms and following mechanical inference rules. Inconsistent Axiomatic

System Inconsistent Axiomatic System Derives all true statements, and some false statements starting from a finite number of axioms and following mechanical inference rules.

Once you can prove one false statement, everything can be proven! false anything some false statements Finishing The Proof Turn G into a statement in the Principia Mathematica system Is PM powerful enough to express G:

This statement does not have any proof in the PM system. ? How to express does not have any proof in the system of PM What does have a proof of S in PM mean? There is a sequence of steps that follow the inference rules that starts with the initial axioms

and ends with S What does it mean to not have any proof of S in PM? There is no sequence of steps that follow the inference rules that starts with the initial axioms and ends with S Can PM express unprovability? There is no sequence of steps that follows the

inference rules that starts with the initial axioms and ends with S Sequence of steps: T0, T1, T2, ..., TN T0 must be the axioms TN must include S Every step must follow from the previous using an inference rule Can we express

This statement? Yes! If you dont believe me (and you shouldnt) read the TNT Chapter in Gdel, Escher, Bach We can write every statement as a number, so we can turn This statement does not have any proof in the system into a number which can be written in PM.

Gdels Proof G: This statement does not have any proof in the system of PM. If G is provable, PM would be inconsistent. If G is unprovable, PM would be incomplete. PM can express G. Thus, PM cannot be complete and consistent! Generalization

All logical systems of any complexity are incomplete: there are statements that are true that cannot be proven within the system. Practical Implications Mathematicians will never be completely replaced by computers There are mathematical truths that cannot be

determined mechanically We can write a program that automatically proves only true theorems about number theory, but if it cannot prove something we do not know whether or not it is a true theorem. What does it mean for an axiomatic system to be complete and consistent? Derives all true statements, and no false

statements starting from a finite number of axioms and following mechanical inference rules. What does it mean for an axiomatic system to be complete and consistent? It means the axiomatic system is weak. Indeed, it is so weak, it cannot express:

This statement has no proof. Charge Monday How to prove a problem has no solving procedure Wednesday, Friday: enjoy your Thanksgiving! Exam 2 is due Monday

Recently Viewed Presentations

  • NSF CARGO: Multi-scale Topological Analysis of Deforming ...

    NSF CARGO: Multi-scale Topological Analysis of Deforming ...

    This optimization has linear cost. Let's look at Blist in the context of Boolean representations studied for logic synthesis. Most relevant are the RFGs. They are produced by building a tree through repeated Shannon's expansion, and then by recursively identifying...
  • Matter and Energy - Chemistry Geek

    Matter and Energy - Chemistry Geek

    Matter Flowchart. MATTER. Can it be physically separated? Homogeneous Mixture (solution) Heterogeneous Mixture. Compound. MIXTURE. PURE SUBSTANCE. yes. no. Can it be chemically decomposed? no. yes. Is the composition uniform? no. yes. Colloids. Suspensions. Element
  • Co-Teaching as Best Practice in Student Teaching

    Co-Teaching as Best Practice in Student Teaching

    JSU Co-Teaching Project and Timeline for 2012-2013. Initial training for JSU Faculty, LEA Administrators, Cooperating Teachers. Placement and training of initial group of selected JSU students. Initial implementation in Fall Practicum into Spring Internship. Embed co-teaching in all College of...
  • The MiTek Posi-Stud The MiTek Posi-Stud  Thermal Performance

    The MiTek Posi-Stud The MiTek Posi-Stud Thermal Performance

    The MiTek Posi X-Rafter. The Posi-Joist cassette floor provides the opportunity to guarantee a . totally accurate platform . for the spandrel panels. The MiTek Posi X-Rafter. The MiTek Posi X-Rafter. The . Posi X-Rafter system uses flat top spandrel...
  • Making the Least Dangerous Assumption - ESC3

    Making the Least Dangerous Assumption - ESC3

    This inherent prejudice against people with disabilities means that some differences will be defined as deficiencies and looked down upon by all of those "higher up" on the social ladder. What makes this even worse is that most people do...
  • Expressive AI

    Expressive AI

    Andrew Stern InteractiveStory.net ... (e.g. Vivienne virtual girlfriend) New genres: e.g. interactive drama The technologies of NLP Natural language understanding (NLU) - given natural language input, extract meaning Involves syntax, semantics, pragmatics May include added step of speech ...
  • European Contact - Mr. Soulis

    European Contact - Mr. Soulis

    habituating so . closely in the residential schools, and . that they . die at a much higher rate than in their villages. But . this alone . does . not justify a change . in the policy . of...
  • Anneleen Coen - Welkom

    Anneleen Coen - Welkom

    Anneleen Coen Een kleine voorstelling Een woordje over mezelf Ik ben Anneleen Coen, geboren op 26 december 1987. Ik woon samen met mijn vriend in Schoten. Momenteel studeer ik voor GOB aan Plantijn Hogeschool Antwerpen en voor Sociaal Werk via...