Slide 1MenuGödel’s ProofWhat does it mean for an axiomatic system to be complete and consistent?Slide 5Why is an Inconsistent Axiomatic System less useful than an Incomplete Axiomatic System?Inconsistent Axiomatic SystemProofProof Checking ProblemFinite-Length Proof Finding ProblemProof Finding ProblemComputabilityAlgorithmsSlide 14Are there any undecidable problems?Any others?Undecidable ProblemsAlan Turing (1912-1954)Halting ProblemExamplesHalting ExamplesCan we define halts? ?find-proofAnother Informal ProofReducing Undecidable ProblemsChargeDavid Evanshttp://www.cs.virginia.edu/evansCS150: Computer ScienceUniversity of VirginiaComputer ScienceClass 24: ComputabilityHalting Problems Hockey Team Logo2CS150 Fall 2005: Lecture 24: ComputabilityMenu•Review: –Gödel’s Theorem–Proof in Axiomatic Systems•Computability:Are there some problems that it is impossible to write a program to solve?3CS150 Fall 2005: Lecture 24: ComputabilityGödel’s ProofG: This statement of number theory does not have any proof in the system of PM.If G were provable, then PM would be inconsistent.If G is unprovable, then PM would be incomplete.PM cannot be complete and consistent!4CS150 Fall 2005: Lecture 24: 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.5CS150 Fall 2005: Lecture 24: ComputabilityWhat does it mean for an axiomatic system to be complete and consistent?It means the axiomatic system is weak.Its is so weak, it cannot express “This statement has no proof.”6CS150 Fall 2005: Lecture 24: ComputabilityWhy is an Inconsistent Axiomatic System less useful than an Incomplete Axiomatic System?7CS150 Fall 2005: Lecture 24: ComputabilityInconsistent Axiomatic SystemDerives all true statements, and some false statements starting from a finite number of axioms and following mechanical inference rules.some false statements Once you can prove one false statement,everything can be proven! false  anything8CS150 Fall 2005: Lecture 24: ComputabilityProof•A proof of S in an axiomatic system is a sequence of strings, T0, T1, …, Tn where:–The first string is the axioms–For all i from 1 to n, Tn is the result of applying one of the inference rules to Tn-1–Tn is S•How much work is it to check a proof?9CS150 Fall 2005: Lecture 24: ComputabilityProof Checking Problem•Input: an axiomatic system (a set of axioms and inference rules), a statement S, and a proof P containing n steps of S•Output: true if P is a valid proof of Sfalse otherwise How much work is a proof-checking procedure?We can write a proof-checking procedure that is  (n)10CS150 Fall 2005: Lecture 24: ComputabilityFinite-Length Proof Finding Problem•Input: an axiomatic system (a set of axioms and inference rules), a statement S, n (the maximum number of proof steps) •Output: A valid proof of S with no more then n steps if there is one. If there is no proof of S with <= n steps, unprovable.How much work?At worst, we can try all possible proofs: r inference rules, 0 - n steps ~ rn possible proofsChecking each proof is  (n)So, there is a procedure that is  (nrn) but, it might not be the best one.11CS150 Fall 2005: Lecture 24: ComputabilityProof Finding Problem•Input: an axiomatic system, a statement S•Output: If S is true, output a valid proof. If S is not true, output false.How much work?It is impossible! “It might take infinite work.”Gödel’s theorem says it cannot be done.12CS150 Fall 2005: Lecture 24: ComputabilityComputability13CS150 Fall 2005: Lecture 24: ComputabilityAlgorithms•What’s an algorithm?A procedure that always terminates.•What’s a procedure?A precise (mechanizable) description of a process.14CS150 Fall 2005: Lecture 24: ComputabilityComputability•Is there an algorithm that solves a problem?•Decidable (computable) problems:–There is an algorithm that solves the problem.–Make a photomosaic, sorting, drug discovery, winning chess (it doesn’t mean we know the algorithm, but there is one)•Undecidable problems:–There is no algorithm that solves the problem.There might be a procedure, but it doesn’t always terminate.15CS150 Fall 2005: Lecture 24: ComputabilityAre there any undecidable problems?The Proof-Finding Problem:•Input: an axiomatic system, a statement S•Output: If S is true, output a valid proof. If S is not true, output false.16CS150 Fall 2005: Lecture 24: ComputabilityAny others?How would you prove a problem is undecidable?Hint: how did we prove 3-SAT was NP-Complete (once we knew Smiley Puzzle was?17CS150 Fall 2005: Lecture 24: ComputabilityUndecidable Problems•We can prove a problem is undecidable by showing it is at least as hard as the proof-finding problem•Here’s a famous one:Halting ProblemInput: a procedure P (described by a Scheme program) and its input IOutput: true if executing P on I halts (finishes execution), false otherwise.18CS150 Fall 2005: Lecture 24: ComputabilityAlan Turing (1912-1954)•Codebreaker at Bletchley Park–Broke Enigma Cipher–Perhaps more important than Lorenz•Published On Computable Numbers … (1936)–Introduced the Halting Problem –Formal model of computation (now known as “Turing Machine”)•After the war: convicted of homosexuality (then a crime in Britain), committed suicide eating cyanide apple5 years after Gödel’s proof!19CS150 Fall 2005: Lecture 24: ComputabilityHalting ProblemDefine a procedure halts? that takes a procedure and an input evaluates to #t if the procedure would terminate on that input, and to #f if would not terminate.(define (halts? procedure input) … )20CS150 Fall 2005: Lecture 24: ComputabilityExamples> (halts? ‘(lambda (x) (+ x x)) 3)#t> (halts? ‘(lambda (x) (define (f x) (f x)) (f x)) 27)#f21CS150 Fall 2005: Lecture 24: ComputabilityHalting Examples> (halts? `(lambda (x) (define (fact n) (if (= n 1) 1 (* n (fact (- n 1))))) (fact x)) 7)#t> (halts? `(lambda (x) (define (fact n) (if (= n 1) 1 (* n (fact (- n 1))))) (fact x)) 0)#f22CS150 Fall 2005: Lecture 24: ComputabilityCan we define halts? ?•We could try for a really long time, get something to work for simple examples, but could we solve the problem – make it work for all possible inputs?•Could we compute find-proof if we had halts?23CS150 Fall 2005: Lecture 24: Computabilityfind-proof(define (find-proof S