Thales and Gödel's Legacy: What is Proof?

Thales’ Legacy: What Is A Proof?

Thales Of Miletus (600 BC) Insisted on Proofs! “first mathematician” Most of the starting theorems of geometry. SSS, SAS, ASA, angle sum equals 180, . . .

So 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? Intuitively, statements must take place in some language. Formally, statements will take place in a computable language.

Let S be a computable language. Then there is a Java program PS(x) that outputs "Yes" if , and outputs "No" otherwise. S implicitly defines the “syntactically valid” statements of a language.

We define our “language” to be a decidable set of strings S. Any is called a STATEMENT or a SYNTACTICALLY VALID string.

Before pinning down the notion of “logic”, let’s see some examples of languages in mathematics.

In fact, valid language syntax is typically defined inductively, so it is easy to make a recursive program to recognize the strings considered valid.

Example in Detail: Propositional Logic

Here is a typical example on defining a language. Firstly we begin with the set of valid symbols, in propositional logic:
Let be Propositional Variables.
Let T and F be propositional "truth" constants.
Let be a unary connective.
Let be binary connectives.
Let S be the set of syntactically valid statements in Propositional Logic (also called wff or well-formed-formulae in propositional logic). S can recursively be defined to contain the following statements:
All propositional variables and constants are valid formulae. (The base case)
If p is a valid formula, then, is a valid formula. (One recursive case)
If p and q are valid formulae, then so are and . (Another recursive case)

Cleary. one can easily define a function "validate(s)" in a primitive recursive (or superior) language that checks whether a statement , as follows:
if s is a propositional variable return true.
if s is a propositional constant return true.
if s is in the form , return true is validate(p) is true.
if s is in the form or , return true if validate(p) is true and validate (q) is true.
return false in all other cases.

Some smaller examples

First-order Logic

Let S be the set of all syntactically well formed statements in first-order logic. This is a revision of propositional logic to include the concept naming "terms", and "relations" that hold over the terms. Therefore, first order logic can easily be extended to a formal language, by describing the language in terms of "terms" in the language, and relations that hold over these terms. Therefore, for a term x and a relation P, the following are valid statements in first-order logic:

(functions over values are also terms)

Peano Arithmetic

Let S be the set of all syntactically well formed statements in Peano Arithmetic.


But not:

Peano Arithmetic can be described as an extension of first order logic that has the following additional syntactic elements:
A constant 0.
The successor function S(x) (used to represent other numbers).
Operators +, *
Equivalence relation =

Valid formulae would then look like:
, for any terms $e_1, e_2$.
, for a value V.

etc...

A Recursive Validation Program:
ValidPeano (s)
return True if any of the following:
S has form and ValidPeano (T)
S has form …..

Euclid's Elements

Let S be the set of all syntactically well formed statements Euclidean Geometry.

Logic

Now we have a way to precisely define what it means to set forth a syntactically valid set of statements in a “language”.

What is “logic” and what is “meaning”?

In fact, we will continue to ignore “meaning” and pin down our concepts in purely symbolic (syntactic) terms. One simple way to do this is the semi-Thue notation (known by some other names), named after the Norwegian mathematician Alex Thue
We have a computable set of “statements” S.
Fix any single computable logic relation: = True/False
If = True, we say that y is implied by x.

In fact, let’s expand the inputs space of our logic function to include a “start statement” A, an axiom i.e. a self evident truth, from which other results may follow.
= True will mean that our logic views A as an axiom.

A sequence of statements is a VALID PROOF of statement Q in iff
= True
And
= True, for some

The system described above is a pretty weak proof system, because there are systems of logic with inference rules that permit the inference of a statement from several others. However, the idea that is expressed here is that of a computable (in fact, primitive recursive) function that can act as a proof checker.

Let S be a set of statements. Let L be a logic function.
PROVABLES_L = All for which there is a valid proof of Q in logic L

Example: SILLY FOO FOO 1
S = All binary strings.
L = All pairs of the form:
PROVABLES_L is the set of all strings.

Example: SILLY FOO FOO 2
S = All binary strings.
L = and all pairs of the form:
PROVABLES_L is the set of all strings.

Example: SILLY FOO FOO 3
S = All binary strings.
L = and all pairs of the form
PROVABLES_L is the set of all strings with a zero parity.

Example: SILLY FOO FOO 4
S = All binary strings.
L = and all pairs of the form
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. (hopefully) PROVABLES_L is the set of all formulas that are tautologies in propositional logic.

Truth

We know what valid syntax is, what logic, proof, and theorems are …. Where does “truth” and “meaning” come in it?

Let S be any computable language. Let TRUTHS be any fixed function from S to {T, F}. We will say that we have a “truth concept” associated with the strings in S.

The world of mathematics has certain established truth concepts associated with logical statements.

Let A(x1, x2, .., xn) be a syntactically valid Boolean proposition. TRUTHprop logic (A) is T iff any setting of the variables evaluates to true. A would be called a tautology.

GENERAL PICTURE: A decidable set of statements S. A (possibly incomputable) Truth concept TRUTH_S: S à {True, False}

We work in logics that we think are related to our truth concepts….. A (possibly incomputable) Truth concept TRUTH_S: S à {True, False}

Soundness, Completeness and Consistency of a Logic

A logic is sound if any statement that it proves is true. A logic is complete if every statement that is true of what it models can be proven by the logic. Some systems, like Propositional Logic and First order logic are sound and complete. Some systems, such as peano arithmetic, are sound, but not-complete. A logic is said to be consistent if the logic never proves a statement as well as its negation. These concepts can be represented syntactically as:
SOUNDNESS: PROVABLES_L ½ TRUTHS
COMPLETE: TRUTHS ½ PROVABLES_L

L is SOUND for TRUTHS if L(D, A) = true ) TRUTH(A)= True L(B,C)=true and TRUTH(B)=True ) TRUTH(C)=True

If L is sound for TRUTHS Then L proves C ) TRUTHS(C) = yes L is sound for TRUTHS means that L can’t prove anything false for the truth concept TRUTH.

Boolean algebra is SOUND for the truth concept of propositional tautology. High school algebra is SOUND for the truth concept of algebraic equivalence.

SILLY FOO FOO 3 is SOUND for the truth concept of an even number of ones.

Euclidean Geometry is SOUND for the truth concept of facts about points and lines in the Euclidean plane. It is also known to be complete.

When we say that a system of logic is incomplete, it means there exists a statement representable in that language, which cannot be proven true, and whose negation can also not be proven true. Some examples follow

Peano Arithmetic is SOUND for the truth concept of (first order) number facts about Natural numbers.

SILLY FOO FOO 3 is sound and complete for the truth concept of strings having an even number of 1s.

What is a proof? A language. A truth concept. A logic that is sound (maybe even complete) for the truth concept.

An ENUMERABLE list of PROVABLE THEOREMS in the logic.

A set S is Recursively Enumerable if its elements can be printed out by a computer program. In other words: There is a program LISTS that outputs a list of strings separated by spaces, and such that an element is on the list if and only if it is in S.

SUPER IMPORTANT Let F be any logic. We can write a program to enumerate the provable theorems of F.

Listing THEOREMSF k;=0; For sum = 0 to forever do {Let PROOF loop through all strings of length k do {Let STATEMENT loop through strings of length <k do If proofcheck(STATEMENT, PROOF) = valid, output STATEMENT k++ } }

Whatever the details of our proof system, an inherent property of any proof system is that its theorems are recursively enumerable

(FIX ME!) Self Referential Proofs

Theorem: God is not omnipotent. Proof: Let S be the statement “God can’t make a rock so heavy that he can’t lift it.”. If S is true, then there is something God can’t do, and is hence not omnipotent. If S is false, then God can’t lift the rock

Alan Turing (1912-1954) THEOREM: There is no program to solve the halting problem (Alan Turing 1937) Suppose a program HALT, solving the halting problem, existed: HALT(P)= yes, if P(P) halts HALT(P)= no, if P(P) does not halt We will call HALT as a subroutine in a new program called CONFUSE.

CONFUSE(P): If HALT(P) then loop_for_ever Else return (i.e., halt)

---

Does CONFUSE(CONFUSE) halt? YES implies HALT(CONFUSE) = yes thus, CONFUSE(CONFUSE) will not halt NO implies HALT(CONFUSE) = no thus, CONFUSE(CONFUSE) halts

K = { P | P(P) halts } K is an undecidable set. There is no procedure running on an ideal machine to give yes/no answers for all questions of the form “x 2 K?”

Self-Reference Puzzle Write a program that prints itself out as output. No calls to the operating system, or to memory external to the program. Auto_Cannibal_Maker Write a program AutoCannibalMaker that takes the text of a program EAT as input and outputs a program called SELFEAT. When SELFEAT is executed it should output EAT(SELFEAT). For any (input taking) program: EAT AutoCannibalMaker (EAT) = SELFEAT SELFEAT is a program taking no input. When executed SELFEAT should output EAT(SELFeat) Suppose Halt with no input was programmable in JAVA. Contradiction! Hence EAT does not have a corresponding JAVA program.

Theorems of F Define the set of provable theorems of F to be the set: THEOREMSF = { STATEMENT 2 S* | 9 PROOF 2 S*, proofcheckF(STATEMENT, PROOF) = valid }

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 statement provable from the axioms of Euclidean geometry.

Example: Set Theory and SFC. 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 Zermilo Frankel Set Theory, as well as, the axiom of choice. THEOREMSZFC is the set of all statement provable from the axioms of set theory.

Example: Peano and PA. We could write a program PA 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 Peano Arithmetic THEOREMSPA is the set of all statement provable from the axioms of Peano Arithmetic

Listing THEOREMSF k;=0; For sum = 0 to forever do {Let PROOF loop through all strings of length k do {Let STATEMENT loop through strings of length <k do If proofcheck(STATEMENT, PROOF) = valid, output STATEMENT k++ } }

Whatever the details of our proof system, an inherent property of any proof system is that its theorems are recursively enumerable

Language and Meaning By a language, we mean any syntactically defined subset of S* By truth value, we mean a SEMANTIC function that takes expressions in the language to TRUE or FALSE.

Truths of Natural Arithmetic ARITHMETIC _TRUTH = All TRUE expressions of the language of arithmetic (logical symbols and quantification over Naturals).

Truths of Euclidean Geometry EUCLID _TRUTH = All TRUE expressions of the language of Euclidean geometry.

Truths of JAVA program behavior. JAVA _TRUTH = All TRUE expressions of the form program P on input X will output Y, or program P will/won’t halt.

TRUTH versus PROVABILITY Let L be a language L, with a well defined truth function. If proof system F proves only true statements in the language, we say that F is SOUND. If F proves all statements in language, we say that F is COMPLETE.

Happy News: THEOREMSELEMENTS = EUCLID_TRUTH The ELEMENTS are SOUND and COMPLETE for geometry.

THEOREMSPA is a proper subset of ARITHMETIC_TRUTH PA is SOUND. PA is not COMPLETE.

FOUNDATIONAL CRISIS: It is impossible to have a proof system F such that THEOREMSF = ARITHMETIC_TRUTH F is SOUND will imply F is INCOMPLETE for arithmetic.

JAVA_TRUTH is not R.E. Assume a program LIST enumerates JAVA_TRUTH. We can now make a program Halt(P) Run list until one of the two statements appears: “P(P) halts”, or “P(P) does not halt”. Output the appropriate answer. Contradiction of undecidability of K.

JAVA_TRUTH has no proof system.. There is no proof system for JAVATRUTH. Let F be any proof system. There must be a program LIST to enumerate THROEMSF. THEOREMF is R,E. JAVA_TRUTH is not R.E. So THEOREMSF ¹ JAVA_TRUTH

Whatever the details of our proof system, an inherent property of any proof system is that its theorems are recursively enumerable

JAVA_TRUTH is not recursively enumerable. Hence, JAVA_TRUTH has no sound and complete proof system. ARITHEMTIC_TRUTH is not recursively enumerable. Hence, ARITHMETIC_TRUTH has no sound and complete proof system!!!!

Hilbert’s Question [1900] Is there a foundation for mathematics that would, in principle, allow us to decide the truth of any mathematical proposition? Such a foundation would have to give us a clear procedure (algorithm) for making the decision.

Foundation F Let F be any foundation for mathematics: • F is a proof system that only proves true things [Soundness] • The set of valid proofs is computable. [There is a program to check any candidate proof in this system]

Incompleteness

When we say that a system of logic is incomplete, it means there exists a statement representable in that language, which cannot be proven true, and whose negation can also not be proven true. Some examples follow

CONFUSEF(P)
Loop though all sequences of symbols S
If S is a valid F-proof of “P halts”,
then LOOP_FOR_EVER
If S is a valid F-proof of “P never halts”, then HALT

GODELF= AUTO_CANNIBAL_MAKER(CONFUSEF)
Thus, when we run GODELF it will do the same thing as CONFUSEF(GODELF)

Can F prove GODELF halts?
Yes -> CONFUSEF(GODELF) does not halt: Contradiction
Can F prove GODELF does not halt?
Yes -> CONFUSEF(GODELF) halts: Contradiction

F can’t prove or disprove that GODELF halts.
GODELF = CONFUSEF(GODELF)
Loop though all sequences of symbols S
If S is a valid F-proof of “GODELF halts”,
then LOOP_FOR_EVER
If S is a valid F-proof of “GODELF never halts”, then HALT
Thus CONFUSEF(GODELF) = GODELF will not halt. Thus, we have just proved what F can’t. F can’t prove something that we know is true. It is not a complete foundation for mathematics.

CONCLUSION
No fixed set of assumptions F can provide a complete foundation for mathematical proof. In particular, it can’t prove the true statement that GODELF does not halt.

Gödel/Turing: Any statement S of the form “Program P halts on input x” can be easily translated to an equivalent statement S’ in the language of Peano Arithmetic. I.e, S is true if and only if S’ is true.
Hence: No mathematical domain that contains (or implicitly expresses) Peano Arithmetic can have a complete foundation.

Gödel's Incompleteness Theorems

In 1931, Gödel stunned the world by proving that for any consistent axioms F there is a true statement of first order number theory that is not provable or disprovable by F. I.e., a true statement that can be made using 0, 1, plus, times, for every, there exists, AND, OR, NOT, parentheses, and variables that refer to natural numbers.

So what is mathematics? We can still have rigorous, precise axioms that we agree to use in our reasoning (like the Peano Axioms, or axioms for Set Theory). We just can’t hope for them to be complete. Most working mathematicians never hit these points of uncertainty in their work, but it does happen!

ENDNOTE
You might think that Gödel’s theorem proves that we are mathematically capable in ways that computers are not. This would show that the Church-Turing Thesis is wrong. Gödel’s theorem proves no such thing!

GENERAL PICTURE: A *decidable* set of “SYNRACTICALLY VALID STATEMENTS S. A *possibly incomputable* subset of S called TRUTHS I.e. TRUE STATEMENTS OF S A computable LOGICS function LogicS (x,y) = y does/doesn’t follow from x. PROVABLES,L = All Q2S for which there is a valid proof of Q in logic L

PROOF IN LOGICS. If LOGIC_S(x,y) = y follows x in one step. Then we say that statement x implies statement y.

We add a “start statement” D to the input set of our LOGIC function. LogicS (D,S) = Yes will mean that our logic views S as an axiom. A sequence of statements s1, s2, …, sn is a VALID PROOF of statement Q in LOGICS iff LOGIC(D, s1) = True And for n+1> i>1 LOGIC (si-1,si) = True s_n = Q

Let S be a set of statements. Let L be a logic function. PROVABLES,L = All Q2S for which there is a valid proof of Q in logic L

A logic is “sound” for a truth concept if everything it proves is true according to the truth concept. LOGICS is SOUND for TRUTHS if LOGIC(D, A) = true ) A 2 TRUTHS LOGIC(B,C)=true and B 2 TRUTHS ) TRUTH(C)=True

If LOGICS is sound for TRUTHS Then LOGICS proves C ) C2 TRUTHS

If a LOGICS is sound for TRUTHS it means that L can’t prove anything not in TRUTHS.

Boolean algebra is SOUND for the truth concept of propositional tautology. High school algebra is SOUND for the truth concept of algebraic equivalence. SILLY FOO FOO 3 is SOUND for the truth concept of an even number of ones. Euclidean Geometry is SOUND for the truth concept of facts about points and lines in the Euclidean plane. Peano Arithmetic is SOUND for the truth concept of (first order) number facts about Natural numbers. A logic may be SOUND but it still might not be complete. A logic is “COMPLETE” if it can prove every statement that is True in the truth concept. SOUND: PROVABLES,L ½ TRUTHS COMPLETE: TRUTHS ½ PROVABLES,L Ex: Axioms of Euclidean Geometry are known to be sound and complete for the truths of line and point in the plane. SILLY FOO FOO 3 is sound and complete for the truth concept of strings having an even number of 1s.

GENRALLY SPEAKING A LOGIC WILL NOT BE ABLE TO KEEP UP WITH TRUTH! THE PROVABLE CONSEQUENCES OF ANY LOGIC ARE RECURSIVELY ENUMERABLE. THE SET OF TRUE STATEMENTS ABOUT HALT/NON-HALTING PROGRAMS IS NOT.

We have seen that the set of programs which do not halt on themselves – IS NOT RECURSIVELY ENUMERABLE.

Given any LOGIC, we can enumerate all of its provable consequences.

Listing PROVABLELOGIC k;=0; For sum = 0 to forever do {Let PROOF loop through all strings of length k do {Let STATEMENT loop through strings of length <k do If proofcheck(STATEMENT, PROOF) = valid, output STATEMENT k++ } }

Let S be a language and TRUTHS be a truth concept. We say that “TRUTHS EXPRESSES THE HALTING PROBLEM” iff there exists a computable function r such that r(x) 2 TRUTHS exactly when x2 K.

Let S be a language, L be a logic, and TRUTHS be a truth concept that expresses the halting problem. THEOREM: If L is sound for TRUTHS, then L is INCOMPLETE for TRUTHS.

L proves r(x) ß> x(x) doesn’t halt. Thus, we can run x(x) and list theorems of L – one of them will tell us if x(x) halts.

FACT: Truth’s of first order number theory (for every natural, for all naturals, plus, times, propositional logic) express the halting problem.

INCOMPLETNESS: No LOGIC for number theory can be sound and complete.

Hilbert’s Question [1900] Is there a foundation for mathematics that would, in principle, allow us to decide the truth of any mathematical proposition? Such a foundation would have to give us a clear procedure (algorithm) for making the decision.

Gödel's First Incompleteness Theorem

In 1931, Gödel stunned the world by proving that for any consistent axioms F there is a true statement of first order number theory that is not provable or disprovable by F. I.e., a true statement that can be made using 0, 1, plus, times, for every, there exists, AND, OR, NOT, parentheses, and variables that refer to natural numbers. Commit to any sound LOGIC F for first order number theory. Construct a true statement GODELF that is not provable in your logic F.

YOU WILL EVEN BE ABLE TO FOLLOW THE CONTRUCTION AND ADMIT THAT GODELF is a true statement that is missing from the consequences of F.

CONFUSEF(P) Loop though all sequences of symbols S If S is a valid F-proof of “P halts”, then LOOP_FOR_EVER If S is a valid F-proof of “P never halts”, then HALT

GODELF GODELF= AUTO_CANNIBAL_MAKER(CONFUSEF) Thus, when we run GODELF it will do the same thing as: CONFUSEF(GODELF)

Can F prove GODELF halts? Yes -> CONFUSEF(GODELF) does not halt Contradiction Can F prove GODELF does not halt? Yes -> CONFUSEF(GODELF) halts Contradiction

F can’t prove or disprove that GODELF halts.

GODELF = CONFUSEF(GODELF) Loop though all sequences of symbols S If S is a valid F-proof of “GODELF halts”, then LOOP_FOR_EVER If S is a valid F-proof of “GODELF never halts”, then HALT

Thus CONFUSEF(GODELF) = GODELF will not halt. Thus, we have just proved what F can’t. F can’t prove something that we know is true. It is not a complete foundation for mathematics.

In any logic that can express statements about programs and their halting behavior – can also express a Gödel sentence G that asserts its own improvability!

Gödel's Second Incompleteness Theorem

This theorem proves an even stronger result, that no theory that extends a language of arithmetic (i.e. a system describing natural numbers) can prove its own consistency. The consequence of the theorem is that one needs another language to prove the consistency of any language of arithmetic.

Epilogue

So what is mathematics? THE DEFINING INGREDIENT OF MATHEMATICS IS HAVING A SOUND LOGIC – consistent for some notion of truth.

For the purpose of checking syntactic validity, this description is sufficient. If one would like to write a computer program to Godel's 1931 paper is a good resource, which, among other things, describes Godel's scheme of encoding proofs as natural numbers using the chinese remainder theorem into natural numbers, and checking if a proof is valid.