115-251Great Theoretical Ideas in Computer ScienceThales’ and Gödel’s Legacy: Proofs and Their LimitationsLecture 27 (April 14, 2009)A Quick Recap of the Previous LectureThe Halting ProblemK = {P | P(P) halts }Is there a program HALT such that:• HALT(P)= yes, if P∈K• HALT(P)= 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 problemComputability Theory:Old VocabularyWe call a set of strings S⊆Σ*decidable or recursive if there is a program P such thatP(x) = yes, if x∈SP(x) = no, if x∉SHence, the halting set K is undecidableNo program can decide membership in K2Computability Theory:New VocabularyWe call a set of strings S⊆Σ*enumerableor recursively enumerable (r.e.)if there is a program P such that: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. Is the halting set K enumerable?Enumerating KEnumerate-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**(The more things change, the more they remain the same…)What’s a proof?3Thales Of Miletus (600 BC)Insisted on Proofs!“first mathematician”Most of the starting theorems of geometry. SSS, SAS, ASA, angle sum equals 180, . . .AxiomsIn 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 ArithmeticThe Peano axioms formally define the properties of the natural numbers4. If n is a natural number and n = m, then m is also a natural number. 1. For every natural number n, n = n 2. For all natural numbers, if n = m, then m = n. 3. For all naturals if k = m and m = n then k = n. 5. 0 is a natural number. 8. For all natural numbers m and n, if S(m) = S(n), then m = n. 6. For every natural number n, its “successor” S(n) is a natural number. 7. For every natural number n, S(n) ≠ 0.Peano Arithmetic (contd.)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?What are “statements”? What does it mean for one to follow “logically” from another?Formally, statements are strings of a decidable language S over Σ. Intuitively, statements are strings in some language. 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.4This 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 LogicVariable → X, Y, X1, X2, X3, …Literal → Variable | ¬VariableStatement →Literal¬(Statement)Statement ∧ StatementStatement ∨ StatementE.g. recursive program to decide SValidProp(S) {return True if any of the following:S has the form ¬(S1) and ValidProp(S1)S has the form (S1∧ S2) andValidProp(S1) AND ValidProp(S2)S has the form …..}“Statements”: some set S of strings whose membership is decidable.But what does it mean to follow “logically”? What is “logic”? Intuitively, a proof is a sequence of “statements”, each of which follows “logically” from some of the previous steps. Define a function LogicSGiven a decidable set of statements S, fix a computable “logic function”:LogicS: (S ∪ ∆) × S → Yes/NoIf Logic(x, y) = Yes, we say that thestatement 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• LogicS(∆, s1) = True(s1must 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.)A sequence s1, s2, …, snof statements is a valid proof of statement Q in LogicSiff5Provable 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 whichthere is a valid proof of Q in logic L.Example: SILLY1S = All strings over {0,1}.L = All pairs of the form: <∆, s>, s∈SProvableS,Lis the set of all strings.Example: SILLY2S = All strings over {0,1}.L = <∆, 0> , <∆, 1>, andall pairs of the form: <s,s0> or <s, s1>ProvableS,Lis the set of all strings.Example: SILLY3S = All strings over {0,1}.L = <∆, 0> , <∆, 11>, andall pairs of the form: <s,s0> or <s, s11>ProvableS,Lis the set of all strings where all the 1s occur in pairs.Example: SILLY4S = All strings over {0,1}.L = <∆, 0> , <∆, 11>, andall pairs of the form: <s,s0> or <st, s1t1>ProvableS,Lis the set of all strings with an even number of 1sMore Practical Example: Propositional LogicS = All well-formed formulas in the notation ofPropositional 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.)6More Practical Example: Propositional LogicS = All well-formed formulas in the notation ofPropositional 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,Lis the set of all formulas that are tautologies in propositional logic.Super-important fact about theoremsLet S be a decidable set of statements. Let L be a computable logic function.Define ProvableS,L= All statements Q in S for whichthere is a valid proof of Q in logic L.We can write a program to enumerate the provable theorems of L.I.e., ProvableS,Lis enumerable.Enumerating the Set ProvableS,Lfor 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}}}}Example: Euclid and ELEMENTSWe could write a program
View Full Document
Unlocking...