UVA CS 150 - Gödel and Computability

Unformatted text preview:

1David Evanshttp://www.cs.virginia.edu/evansCS150: Computer ScienceUniversity of VirginiaComputer ScienceLecture 25: Lecture 25: GGöödel and del and ComputabilityComputabilityHalting ProblemsHockey Team2Lecture 25: Gödel and ComputabilityMenu• Review and finish Gödel’s Proof from Monday• Discuss Quiz• Computability3Lecture 25: Gödel and ComputabilityProof – General Idea• Theorem: In any interesting axiomatic system, there are statements that cannot be proven either true or false.• Proof: Find such a statement4Lecture 25: Gödel and ComputabilityGödel’s StatementG: This statement does not have any proof in the system.Possibilities:1. Gis true ⇒Ghas no proof System is incomplete2. Gis false ⇒Ghas a proof System is inconsistent5Lecture 25: Gödel and ComputabilityFinishing The Proof• Turn Ginto a statement in the Principia Mathematica system• Is PMpowerful enough to express “This statement does not have any proof in the PMsystem.”?6Lecture 25: Gödel and ComputabilityHow to express “does not have any proof in the system of PM”• What does “have a proof of Sin 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 Sin PM”?– There is no sequence of steps that follow the inference rules that starts with the initial axioms and ends with S27Lecture 25: Gödel and ComputabilityCan 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, ..., TNT0must be the axiomsTNmust include SEvery step must follow from the previous using an inference rule8Lecture 25: Gödel and ComputabilityCan we express “This statement”?• Yes!– That’s the point of the TNT Chapter in GEB• We can write turn every statement into a number, so we can turn “This statement does not have any proof in the system” into a number9Lecture 25: Gödel and ComputabilityGödel’s ProofG: This statement does not have any proof in the system of PM.If Gis provable, PM would be inconsistent.If Gis unprovable, PM would be incomplete.PM can express G.Thus, PM cannot be complete and consistent!10Lecture 25: Gödel and ComputabilityGeneralizationAll logical systems of any complexity are incomplete: there are statements that are truethat cannot be proven within the system.11Lecture 25: Gödel and ComputabilityPractical Implications• Mathematicians will neverbe completely replaced by computers– There are mathematical truths that cannot be determined mechanically– We can build a computer that will prove only true theorems about number theory, but if it cannot prove something we do not know that that is not a true theorem.12Lecture 25: Gödel and ComputabilityWhat 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.313Lecture 25: Gödel and ComputabilityWhat does it mean for an axiomatic system to be complete and consistent?It means the axiomatic system is weak.Indeed, it is soweak, it cannot express: “This statement has no proof.”14Lecture 25: Gödel and ComputabilityIncompleteAxiomatic SystemDerives some, but not all true statements, and no false statements starting from a finite number of axioms and following mechanical inference rules.incompleteInconsistentAxiomatic SystemDerives all true statements, and some false statements starting from a finite number of axioms and following mechanical inference rules.some falsestatementsPick one:15Lecture 25: Gödel and ComputabilityInconsistentAxiomatic SystemDerives all true statements, and some false statements starting from a finite number of axioms and following mechanical inference rules.some false statementsOnce you can prove one false statement,everything can be proven! false ⇒ anything16Lecture 25: Gödel and ComputabilityQuiz Answers1. b, e (read Tyson’s essay)2. SS0 = “successor of the successor of 0” = 23. MU is not a theorem (read Chapter IX)Results on these questions were quite poor!Only 6 people got >= 4 points on quizDoing these reading may not have a great direct impact on your grade, but they are very interesting and worthwhile.If that isn’t enough motivation, we’ll have another quiz some day next week (on the same material).17Lecture 25: Gödel and ComputabilitySurprise Quiz?Can this be a true statement:Q: You will have a surprise quiz some day next week.If the quiz is Friday, it is not a surprise. Q is false.Since the quiz can’t be Friday, if the quiz is not on Monday,it isn’t a surprise if it is on Wednesday. Q is false.Since the quiz can’t be Wednesday, if is not a surprise quizif it is on Monday. Q is false.Your quiz score is (max last-quiz next-quiz)18Lecture 25: Gödel and ComputabilityQuestion 5: Computer ScientistsFirst Compiler, COBOL5Grace HopperAwesome PS9 project9YourselfPancake sorting10Bill GatesTeaches this class13David EvansFirst programmer14Ada ByronComputability (rest of today), cryptography (exam 1, ps4), models of computing (later)16Alan TuringOthers receiving votes: Bach, Euclid, Godel, Escher, Doug Hofstadter, Aaron Bloomfield, BjarneStroustrup, Charles Babbage, John Backus (2), Linus Torvalds, Steve Jobs, Steve Wozniak, Alonzo Church, Emil Post, Frances Allen, Gordon Moore, Herman Hollerith, James Cohoon, John Lach, John McCarthy, John von Neumann, Kaspersky, Kinga Dobolyi, Neil de Grasse Tyson, Noam Chomsky, Paul Reynolds, Peter Naur, Richard Stallman, Sid Mayer, Will Wright419Lecture 25: Gödel and ComputabilityJohn Backus (1924-2007)• Chemistry major at UVA (entered 1943), flunked out first year• Joined IBM as programmer in 1950• Developed Fortran, first commercially successful programming language and compiler• Invented BNF (replacement grammars)I flunked out every year. I never studied. I hated studying. I was just goofing around. It had the delightful consequence that every year I went to summer school in New Hampshire where I spent the summer sailing and having a nice time.20Lecture 25: Gödel and ComputabilityJohn Backus on Simplicity“Because it takes pages and pages of gobbledygook to describe how a programming language works, it’s hard to prove that a given program actually does what it’s supposed to. Therefore, programmers must learn not only this


View Full Document

UVA CS 150 - Gödel and Computability

Documents in this Course
Objects

Objects

6 pages

Load more
Download Gödel and Computability
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Gödel and Computability and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Gödel and Computability 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?