Thales’ and Gödel’s Legacy: Proofs and Their LimitationsCarnegie Mellon UniversityNovember 30, 2006Lecture 27CS 15-251 Fall 2006John Lafferty Great Theoretical Ideas In Computer ScienceA Quick Recap of the Previous LectureThe Halting ProblemK = {P | P(P) halts }Is there a program HALT such that:HALT(P) = yes, if P∈KHALT(P) = no, if P∉KHALT 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 S⊆Σ*decidable or recursive if there is a program P such that:P(x) = yes, if x∈SP(x) = no, if x∉SHence, the halting set K is undecidableComputability Theory:New VocabularyWe 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 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?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) ⇒ YBut not: ∨X¬YTypically, 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 LogicVariable → X, Y, X1, X2, X3, …Literal → Variable | ¬VariableStatement →Literal¬(Statement)Statement ∧ StatementStatement ∨ StatementRecursive 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 …..}Example:Let S be the set of all syntactically well formed statements in first-order logic.∀ x P(x)∀ x∃y∀z 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 LogicSGiven a decidable set of statements S, fix any single 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 LogicSA sequence s1, s2, …, snof statements is a valid proof of statement Q in LogicSiff• LogicS(∆, s1) = True(i.e., s1is 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 whichthere is a valid proof of Q in logic L.Example SILLY1S = All strings.L = All pairs of the form: <∆, s> s∈SProvableS,Lis the set of all strings.Example: SILLY2S = All strings.L = <∆, 0> , <∆, 1>, andall pairs of the form: <s,s0> or <s, s1>ProvableS,Lis the set of all strings.Example: SILLY3S = All strings.L = <∆, 0> , <∆, 11>, andall pairs of the form: <s,s0> or <st, s1t1>ProvableS,Lis the set of all strings with zero parity.Example: SILLY4S = All strings.L = <∆, 0> , <∆, 1>, andall pairs of the form: <s,s0> or <st, s1t1>ProvableS,Lis the set of all strings.Example: Propositional LogicS = All well-formed formulas in the notation ofBoolean algebra.L = Two formulas are one step apart if one can bemade from the other from a finite list of forms.(see next page for a partial list.)Example: Propositional LogicS = All well-formed formulas in the notation ofBoolean algebra.L = Two formulas are one step apart if one can bemade from the other from a finite list of forms.(hopefully) ProvableS,Lis the set of all formulas that are tautologies in propositional logic.Super Important FactLet 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,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}}}}No matter the details of the system, an inherent property of anyproof system is that its theorems are recursively enumerableExample: 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.THEOREMSELEMENTSis 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
View Full Document
Unlocking...