Great Theoretical Ideas In Computer Science John Lafferty Lecture 27 CS 15 251 November 30 2006 Fall 2006 Carnegie Mellon University Thales and G del s Legacy Proofs and Their Limitations A Quick Recap of the Previous Lecture The Halting Problem K P P P halts Is there a program HALT such that HALT P HALT P yes if P K no if P K 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 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 Computability Theory New Vocabulary We call a set S enumerable or recursively enumerable r e if there is a program P such that P prints an infinite list of strings Any element on the list should be in S Each element in S appears after a finite amount of time Is the halting set K enumerable 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 If both K and K are enumerable then K is decidable why And on to newer topics The more things change the more they remain the same Thales Of Miletus 600 BC Insisted on Proofs first mathematician Most of the starting theorems of geometry SSS SAS ASA angle sum equals 180 What is a proof anyways 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 Intuitively statements must be stated in some language Formally statements are substrings of a decidable language Let S be a decidable language 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 This decidable set S is the set of syntactically valid strings or statements of a language Before pinning down the notion of logic let s see examples of statements and languages in mathematics Example Let S be the set of all syntactically well formed statements in propositional logic X X X Y Y But not X Y Typically valid language syntax is defined inductively This makes it easy to write a recursive program to recognize the strings in the language Syntax for Statements in Propositional Logic Variable X Y X1 X2 X3 Literal Variable Variable Statement Literal Statement Statement Statement Statement Statement 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 Example Let S be the set of all syntactically well formed statements in first order logic 8x P x 8x9y8z f x y z g x y z Example Let S be the set of all syntactically well formed statements in Euclidean Geometry OK we can now precisely define a syntactically valid set of statements in a language But what is logic and what is meaning For the time being let us ignore the meaning of meaning and pin down our concepts in purely symbolic syntactic terms Define a function LogicS Given a decidable set of statements S fix any single 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 i e s1 is an axiom of our language For all 1 j n 1 LogicS sj sj 1 True i e each statement implies the next one and finally sn Q i e the final statement is indeed Q Notice that our notion of valid proof is purely symbolic In fact we can make a proof checking machine to read a purported proof and give a Valid Invalid answer Provable Statements a k a Theorems Let S be a set of statements Let L be a logic function Define ProvableS L All statements Q in S for which there is a valid proof of Q in logic L Example SILLY1 S All strings L All pairs of the form s s2S ProvableS L is the set of all strings Example SILLY2 S All strings L 0 1 and all pairs of the form s s0 or s s1 ProvableS L is the set of all strings Example SILLY3 S All strings L 0 11 and all pairs of the form s s0 or st s1t1 ProvableS L is the set of all strings with zero parity Example SILLY4 S All strings L 0 1 and all pairs of the form s s0 or st s1t1 ProvableS L is the set of all strings Example Propositional Logic S All well formed formulas in the notation of Boolean algebra 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 Example Propositional Logic S All well formed formulas in the notation of Boolean algebra L Two formulas are one step apart if one can be made from the other from a finite list of forms hopefully ProvableS L is the set of all formulas that are tautologies in propositional logic Super Important Fact Let S be any decidable set of statements Let L be any computable logic We can write a program to enumerate the provable theorems of L I e ProvableS L is enumerable Enumerating the set ProvableS L for k 0 to forever do let PROOF loop through all strings of length k let STMT loop through all strings of length k if proofcheckS L STMT PROOF Valid output STMT this is a theorem No matter the details of the system an inherent property of any proof system is that its theorems are recursively 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 set of all statements provable from the axioms of Euclidean geometry Example Set Theory and ZFC We could write a program ZFC 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 Zermelo Frankel Set Theory as well as the axiom of choice THEOREMSZFC is the set of all statements …
View Full Document
Unlocking...