Thales’ and Gödel’s Legacy: Proofs and Their LimitationsA Quick Recap of the Previous LectureThe Halting Problem K = {P | P(P) halts }Alan Turing (1912-1954)Computability Theory: Old VocabularyComputability Theory: New VocabularySlide 7Enumerating KSlide 9And on to newer topics*Thales Of Miletus (600 BC) Insisted on Proofs!Slide 12Slide 13Slide 14Slide 15Slide 16Slide 17Slide 18Slide 19Syntax for Statements in Propositional LogicRecursive Program to decide SSlide 22Slide 23Slide 24Slide 25Define a function LogicSA valid proof in logic LogicSSlide 28Provable Statements (a.k.a. Theorems)Example SILLY1Example: SILLY2Example: SILLY3Example: SILLY4Example: Propositional LogicSlide 35Slide 36Super Important FactEnumerating the set ProvableS,LSlide 39Example: Euclid and ELEMENTS.Example: Set Theory and SFC.Example: Peano and PA.Slide 43Slide 44Truths of Natural ArithmeticTruths of Euclidean GeometryTruths of JAVA program behavior.Slide 48Slide 49Slide 50Slide 51Slide 52Slide 53Slide 54Slide 55Slide 56Slide 57Slide 58Slide 59How about other logics? Which natural logics are sound and complete?Truth versus ProvabilitySlide 62Slide 63Slide 64Here’s what we haveJAVA_Truth is not enumerableJAVA_Truth has no proof systemSlide 68Slide 69Hilbert’s Second Question [1900]Foundation FGödel’s Incompleteness TheoremIncompletenessCONFUSEF(P)Slide 75Slide 76GODELFSlide 78To summarizeCONCLUSIONSo what is mathematics?EndnoteSlide 83Thales’ and Gödel’s Legacy: Proofs and Their LimitationsGreat Theoretical Ideas In Computer ScienceAnupam GuptaCS 15-251 Fall 2005Lecture 27 Dec 1, 2005 Carnegie Mellon UniversityA Quick Recap of the Previous LectureThe Halting ProblemK = {P | P(P) halts }Is there a program HALT such that:HALT(P) = yes, if PKHALT(P) = no, if PKHALT 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 xSP(x) = no, if xSHence, 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(XY) YBut not: XYTypically, 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.8 x P(x)8 x9y8z 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 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 LogicSA sequence s1, s2, …, sn of statements is a valid proof of statement Q in LogicS if• 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 SILLY1S = All strings.L = All pairs of the form: <, s> s2SProvableS,L is the set of all strings.Example: SILLY2S = 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: SILLY3S = 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: SILLY4S = All strings.L = <, 0> , <, 1>, and all pairs of the form: <s,s0> or <st, s1t1>ProvableS,L is the set of all
View Full Document
Unlocking...