Thales and G del s Legacy Proofs and Their Limitations 15 251 Lecture 27 April 14 2009 Great Theoretical Ideas in Computer Science The Halting Problem K P P P halts Is there a program HALT such that A Quick Recap of the Previous Lecture HALT P HALT P yes if P K no if P K I e HALT decides whether or not any given program is in K Alan Turing 1912 1954 Theorem 1937 There is no program to solve the halting problem Computability Theory Old Vocabulary We call a set of strings S decidable or recursive if there is a program P such that P x yes if x S P x no if x S Hence the halting set K is undecidable No program can decide membership in K 1 Computability Theory New Vocabulary We call a set of strings S enumerable or recursively enumerable r e if there is a program P such that Is the halting set K enumerable 1 P prints an infinite list of strings 2 Any element on the list should be in S 3 Each element in S appears after a finite amount of time Enumerating K Enumerate K for n 0 to forever for W all strings of length n do if W W halts in n steps then output W K is not decidable but it is enumerable Let K Java P P P does not halt Is K enumerable No If both K and K are enumerable then K is decidable why And on to newer topics What s a proof The more things change the more they remain the same 2 Thales Of Miletus 600 BC Insisted on Proofs first mathematician Most of the starting theorems of geometry SSS SAS ASA angle sum equals 180 Axioms In traditional logic an axiom is a proposition that is not proved but is considered to be self evident Its truth is taken for granted It serves as a starting point for inferring other truths Peano s Axioms for Arithmetic The Peano axioms formally define the properties of the natural numbers 1 For every natural number n n n Peano Arithmetic contd 5 0 is a natural number 6 For every natural number n its successor S n is a natural number 2 For all natural numbers if n m then m n 7 For every natural number n S n 0 3 For all naturals if k m and m n then k n 4 If n is a natural number and n m then m is also a natural number What is a proof Intuitively a proof is a sequence of statements each of which follows logically from some of the previous steps What are statements What does it mean for one to follow logically from another 8 For all natural numbers m and n if S m S n then m n What are statements What does it mean for one to follow logically from another Intuitively statements are strings in some language Formally statements are strings of a decidable language S over That is S is a subset of and there is a Java program PS x that outputs Yes if x is in S and outputs No otherwise 3 This decidable set S is the set of syntactically valid strings or statements of a language Example Let S be the set of all syntactically well formed statements in propositional logic X X X Y Y X Y not well formed E g syntax for Statements in Propositional Logic Variable X Y X1 X2 X3 Literal Variable Variable Statement Literal Statement Statement Statement Statement Statement E g recursive program to decide S ValidProp S return True if any of the following S has the form S1 and ValidProp S1 S has the form S1 S2 and ValidProp S1 AND ValidProp S2 S has the form Intuitively a proof is a sequence of statements each of which follows logically from some of the previous steps Statements some set S of strings whose membership is decidable But what does it mean to follow logically What is logic Define a function LogicS Given a decidable set of statements S fix a computable logic function LogicS S S Yes No If Logic x y Yes we say that the statement y is implied by statement x We also have a start statement not in S where LogicS x Yes will mean that our logic views the statement x as an axiom A valid proof in logic LogicS A sequence s1 s2 sn of statements is a valid proof of statement Q in LogicS iff LogicS s1 True s1 must be an axiom of our language For all 1 i n 1 LogicS sj sj 1 True each statement implied by the previous one And finally sn Q the final statement is what we wanted to prove 4 Provable Statements a k a Theorems Let S be a decidable set of statements Let L be a computable logic function Define ProvableS L All statements Q in S for which there is a valid proof of Q in logic L Example SILLY2 S All strings over 0 1 L 0 1 and all pairs of the form s s0 or s s1 ProvableS L is the set of all strings Example SILLY4 S All strings over 0 1 L 0 11 and all pairs of the form s s0 or st s1t1 ProvableS L is the set of all strings with an even number of 1s Example SILLY1 S All strings over 0 1 L All pairs of the form s s S ProvableS L is the set of all strings Example SILLY3 S All strings over 0 1 L 0 11 and all pairs of the form s s0 or s s11 ProvableS L is the set of all strings where all the 1s occur in pairs More Practical Example Propositional Logic S All well formed formulas in the notation of Propositional Logic L Two formulas are one step apart if one can be made from the other from a finite list of forms see next page for a partial list 5 More Practical Example Propositional Logic S All well formed formulas in the notation of Propositional Logic L Two formulas are one step apart if one can be made from the other from a finite list of forms see previous page for a partial list hopefully ProvableS L is the set of all formulas that are tautologies in propositional logic Super important fact about theorems Let S be a decidable set of statements Let L be a computable logic function Define ProvableS L All statements Q in S for which there is a valid proof of Q in logic L We can write a program to enumerate the provable theorems of L I e ProvableS L is enumerable Example Euclid and ELEMENTS We could write a program ELEMENTS to check STATEMENT PROOF pairs to determine if PROOF is a sequence where each step is either one logical inference or one application of the axioms of Euclidian geometry THEOREMSELEMENTS is the enumerable set of all statements provable from the axioms of …
View Full Document
Unlocking...