Talk:Proof sketch for Gödel's first incompleteness theorem

Good start and to do list

This looks like a good start; I haven't read it in detail, but I see that certain things that need to be proved are currently just asserted, such as the definability of provability. There are a few things that could be done easily to improve the article. Feel free to strike out these as they are completed and add more items. CMummert · talk 14:28, 27 January 2007 (UTC)

• "wikify" the article: break it into sections (Godel numbering, derivation of the Bew(x) predicate, conclusion), and add wikilinks to help integrate it into the encyclopedia
• Give an outline of the proof at the top
• Use wiki formatting for math expressions, use display style for some formulas and numbers
• Add additional references to introductory books that explain the proof
• Add categories

You're absolutely correct, I hope to get some time to do all that soon... (just saw that now). a little help will be great. Dan Gluck 20:08, 5 April 2007 (UTC)

I feel that "definability of provability" is quite an important requirement to the proof, and probably technically a bit difficult to handle. This can't be addressed in just a few lines of text. I would appreciate a concrete example of how to write down a proof as a formula, using only the given symbols. See below for two questions that should be easy to answer from the article.

• Don't we need an extra symbol for each "deduction rule" relation?
• Any statement can be proven from itself or from any false statement. Think P(G(P)) -> P(G(P)) or S0 = 0 -> P(G(P))... so maybe we need a mechanism to exclude some "proofs" that are not "interesting"?

Illegal604 (talk) 15:06, 30 December 2009 (UTC)

(1) A proof of a statement S is of the form (P_1, P_2, ..., P_n), where P_n=S, each P_i is either an axiom or a statement provable from (some statements chosen from) P_1, P_2, ..., P_{i-1}. (For example, P_2, P_4 proves P_8, by deduction rule D_5.)

Since there is a finite number of statements preceding P_i, a finite number of axiom schemas, and a finite number of deduction rules, there is an effective procedure to decide whether each P_i is either an axiom or provable from P_1, P_2, ..., P_{i-1}.

Thus, a proof need not explicitly state the deduction rule invoked at each step.

However, for greater ease of understanding, introducing the deduction rules into the proof, and encoding them as numbers, is also acceptable, although not necessary.

(2) (S0=0, T) is not a proof of T, since "S0=0" is not an axiom of Peano arithmetic.

(3) (T,T) is not a proof of T, if T is not an axiom of Peano arithmetic.--Palaeovia^talk 16:17, 30 December 2009 (UTC)

Unclear on one part

Good summary and a very clear explanation for the most part, but I got lost here:

One may now define a set of numbers, which we will denote P, which consists of all numbers in AX (representing axioms) and all numbers which can be derived from them by applying the functions F1, F2,F3... a finite number of times. The set P represents the set of provable statements. That is, the members of P are the Gödel numbers of the provable statements. (Emphasis added)

What inputs are applied to the functions? The leading comments suggest the numbers in AX. —The preceding unsigned comment was added by 207.171.180.101 (talk) 21:06, 4 April 2007 (UTC).

As it stands, this article needs a lot of work, so you may want to consult a print reference for details. The idea is that the functions stand for inference rules, and P is the smallest set of Godel numbers containing the Godel numbers of the axioms and closed under the inference rules. CMummert · talk 21:47, 4 April 2007 (UTC)

Thanks. I've tried to clarify this point in the article, is it clearer now? Dan Gluck 20:06, 5 April 2007 (UTC)

Content issues

The list above was all formatting and style issues. Here are some content issues. They aren't really errors so much as terminology issues.

1. Para. 1: "First, every mathematical statement is written in a fully formal manner," This isn't quite right; arithmetic has a particular formal language and the proof is about particular well formed formulas of that language.
2. Paras. 5 and 6. Although it is possible to replace the deduction rules with partial functions, this just adds complexity to the situation. The deduction rules are more naturally viewed as relations of some sort than functions.
3. Para 7. This terminology is nonstandard.

I will be glad to make these changes myself, once the current discussion at WT:WPM finishes. The more I read this sketch the more I like it, modulo the terminology. CMummert · talk 20:12, 6 April 2007 (UTC)

Well, it seems that you have better qualifications than me to make these changes... Dan Gluck 20:36, 12 April 2007 (UTC)

GEB coding for reference

I offered to provide the coding used by Douglas Hofstadter in his monumental work "Godel, Escher, Bach". Here it is.

666 0 zero

123 S successor function

111 = equality relation

112 + addition operator:

236 . multiplication operator

362 (

323 )

212 <

213 >

312 [

313 ]

262 a variable name

163 ' prime (used to make more variables)

161 ^ logical and

616 v logical or

633 contains

223 ~ logical not

333 there exists

626 for all

636 : punctuation

611 . punctuation

Please correct the above if there are mistakes or omissions. Geometry guy 18:03, 9 April 2007 (UTC)

Is there no copyright issue? Dan Gluck 20:35, 12 April 2007 (UTC) OK, I just saw your answer on this elsewhere. I'll do the changes Dan Gluck 20:38, 12 April 2007 (UTC)

2007-4-18

I started working on the article this afternoon. Terms like "statement" and "statement form" ought to be replaced with the standard terminology - "sentences" or "well formed formulas". I tried to integrate the coding by Hofstadter from higher on this page, although I'm not sure about the variable x. I will keep working on other sections. My goal is to smooth out some of the rough edges and make the article more WP-like. CMummert · talk 19:39, 18 April 2007 (UTC)

2007-4-26

The new section on Godel numbers isn't right (because it is copied from the WP article on Godel numbers that also isn't right). It makes no sense to say that a Godel nubering function is computable. Moreover, the numbering must have important properties, so not just any assignment will do. I'll edit both of this article and the Godel number article later this evening. CMummert · talk 22:34, 26 April 2007 (UTC)

Great! I think Formal system should be referenced and quoted in the "Hypothesis" section.

Using the word "hypothesis" in this context seems unconventional. I am unsure what it refers to. Isn't the purpose of the section to define the formal system, and the formal theory? Palaeovia 00:53, 27 April 2007 (UTC)

As it is the article is very vague about exactly what theory is being considered. The article assumes that the language is that of Peano arithmetic, but doesn't go into detail about the inference rules, etc. If you would rather specialize the article to just consider Peano arithmetic, I wouldn't object. Linking to formal systems would be a good idea.

When I edited the article earlier, I tried to find a compromise by adding back some of the deleted material by hand without completely undoing everything you had done. CMummert · talk 01:16, 27 April 2007 (UTC)

Some questions

Hi all, this wiki entry is a great work~!I understand most of the points but not all, please help me.

1) In the 3rd paragraph of "Self-referential formula" 3rd paragraph,

Note that for every specific number n and formula F(y), q(n,G(F)) is a straightforward (though complicated) arithmetical relation between two numbers n and G(F), building on the relation PF defined earlier. Further, q(n,G(F)) is provable if the finite list of formulas encoded by n is not a proof of F(G(F)), and \lnot q(n,G(F)) is provable if the finite list of formulas encoded by n is a proof of F(G(F)). Given any numbers n and G(F), either q(n,G(F)) or \lnotq(n,G(F)) (but not both) is provable

Why "if n = G( proof of F(G(F)) ), then q(n,G(F)) is not provable", is it related to the property of PF?

2) The 9 th paragraph of "Self-referential formula" states that "P(G(P)) is not provable." while the 10 th paragraph state that P(G(P)) is provable ("for all natural numbers n, q(n,G(P)) is provable."), can someone explain if there is any contradiction?

Thz a lot~!

--Hokit 17:02, 28 June 2007 (UTC)

• 1) We defined (in the first paragraph) q(n, G(F)) as follows:

For every number n and every formula F(y), where y is a free variable, we define q(n,G(F)), a relation between two numbers n and G(F), such that it corresponds to the statement "n is not the Gödel number of a proof of F(G(F))".

In our formal system of arithmetic, either q(n,G(F)) or $\lnot$ q(n,G(F)) (but not both) is provable. (The preceding statement requires a lengthy proof that relies on the properties of Godel numbering, and of proofs in the formal system. This lengthy proof is omitted here.)

The answer to your question should be contained in the facts just stated.

• 2)There is no contradiction. Consider an example. Let P(x) be "400+x=3020", where x is a free variable. Let G(P)=21300, the Godel number of P(x). P(G(P)) is "400+21300=3020".

"P(G(P)) is not provable" says that "400+21300=3020" is not provable.

"For all natural numbers n, q(n,G(P)) is provable." says: q(1, 21300), q(2, 21300), q(3, 21300), ... , are all provable. (This is so because none of the numbers 1,2,3, ... , is the Godel number of a proof of the formula P(G(P)) ("400+21300=3020").) However, this does not imply that the formula "$\forall$n, q(n,21300)" is provable.

Does this clarify matters?--Palaeovia^talk 00:21, 29 June 2007 (UTC)

Thanks a lot Palaeovia~! But I still have a questions :

• How PF contributes to the proof in the part "Self-referential formula"? I only see it appears in the 3rd paragraph of the part "Self-referential formula" once and it seems that no proof is built on PF. --Hokit 09:19, 29 June 2007 (UTC)

You're welcome. PF(x,y) is a building block of q(x,y), as follows.

Consider a formula (in our formal system of arithmetic) P, with Godel number G(P). Let n be a natural number. There exists a formula PF(n, G(P)) such that either this formula, or its negation $\lnot$ PF(n, G(P)), but not both (assuming the consistency of the formal system), is provable. PF(n, G(P)) is provable if and only if n is the Godel number of (encodes) a proof of formula P. So, if $\lnot$ PF(n, G(P)) is provable, n does not encode a proof of P.

Now consider formula Q(x) with free variable x, with Godel number G(Q). There is a function f that maps G(Q) to G(Q(G(Q))). For example, let Q(x) be "400+x=3020". Let G(Q)=21300. Then, Q(G(Q)) is "400+21300=3020". Let the Godel number of this new formula G(Q(G(Q)))=619483. Then, f maps 21300 to f(21300)=619483.

Define q(x,y) to be $\lnot$PF(x,f(y)).

Let n be a number. As just seen, PF(n, 619483) is provable if and only if n encodes a proof of "400+21300=3020". q(n, 21300) = $\lnot$PF(n, f(21300))=$\lnot$PF(n, 619483) is provable if and only if n does not encode a proof of "400+21300=3020".--Palaeovia^talk 11:17, 29 June 2007 (UTC)

Thx for the explaination~!--Hokit 00:52, 2 July 2007 (UTC)

Proof Of Godel's Theorem

My often stated opinion, although not on this talk page so I repeat it, is that there is a problem with this type of discussion. It follows Godel's original work too closely. The arithmetization of syntax and the construction of a proposition which asserts its own unprovability are complicated, because they avoid using the idea of a computer program. Since all modern readers know what a computer program is, a proof today should be completely trivial. I have tried to include such a discussion in the past, but I have been censured for it. I include it here, for the benefit of new editors.

The theorems talk about a formal system S, which is sufficiently strong. The precise assumptions on S are as follows:

1. S is capable of stating any theorem about the memory state of a computer program. Each clock cycle of a computer takes a certain memory state M to M'=f(M), where the memory contents M can be viewed as a big integer and f is a simple computable function which does one processor step. The theorems that S should be able to state are of the form "for all N, f iterated N times on M does not have the k-th bit zero" (The equivalent condition in Godel is that S can state an arbitrary first-order theorem of Peano Arithmetic).

2. S will prove that the value of f(f(f(...f(M))))=M' where M is any initial memory state and M' is the state after a finite number N of steps. (The equivalent condition in Godel is that S will determine the value of any primitive recursive function). For the corollary, it is also necessary to assume that S can prove property 2 is true of itself, S needs to prove that S proves these theorems for all N and some special M. In arithmetic this holds when S has at least enough mathematical induction to prove theorems with one (forall X) in front.

3. S is consistent, meaning it never proves a statement and its negation.

Theorem 1: There are true theorems about the asymptotic behavior of computer programs that S cannot prove.

Proof: construct the computer program DEDUCE to print its own code into a variable R, then deduce all consequences of S looking for the theorem R does not halt. If it finds this theorem it halts.

If S proves that DEDUCE does not halt, DEDUCE halts. By assumption, S eventually proves all theorems about the finite time behavior of computer programs, so S would also eventually prove that DEDUCE halts, so S would be inconsistent.

So DEDUCE does not halt and S does not prove it.

Corollary: S cannot prove its own consistency.

Proof: If S proves that DEDUCE does not halt, the previous argument shows that S is inconsistent. So if S proves itself consistent, and if the previous argument can be formalized in S, then S also proves that DEDUCE does not halt, which is impossible.

Theorem 2: S is incomplete, meaning there is a statement that it cannot prove or disprove.

Proof: construct program ROSSER to print its own code into a variable R, then deduce all consequences of S looking for either the theorem 1. R does not print anything out or 2. R prints something out. If it finds 1, ROSSER prints "Hello" and halts . If it finds 2, ROSSER halts without printing out anything.

Now S cannot prove either that ROSSER prints something out nor the negation ROSSER does not print anything out.Likebox (talk) 01:01, 10 January 2008 (UTC)

I disagree with this post for several reasons

1- The goal of this page is not to provide content for a course on logic. I consider that it has rather a historical importance, as it allows to understand the original proof of Gödel. The proof you propose, though maybe clearer, is not the proof that was shown in 1930 by Gödel in front of a few of the most important mathematicians of this century.

2- A precise verification of the equivalence between your statement and that of Gödel requires some time. The pedagogical simplification is only effective once we are really convinced it is the same theorem.

3- The formulation you prodive does not underline the universality of Gödel's result. Computers only exist in our era, while Gödel's theorem is a statement about the first-order logic which has been an implicit framework for mathematics during centuries. For a universal theorem, the universal formulation is preferable. — Preceding unsigned comment added by 92.129.159.234 (talk) 11:11, 26 October 2019 (UTC)

Missing symbols?

It seems to me that a minimal suitable formal arithmetic should include additional symbols, such as either a "member of" and "s" for a set, or alternatively a "F" for a formula. Otherwise, it's hard to see how for example the fact that a formula is well-formed can be expressed within the arithmetics, or how the Goedel number of a number can be constructed. For example, it seems like for these tasks, the operation 10^n for every n must be defined (if the Goedel numbers are concatenated in their decimal representation, as in the article), and I can't see how this can be done without additional symbols.

If additional symbols are indeed necessary, this should be noted somewhere. If not, can someone please explain how to construct the above examples without aditional symbols? (with the "member of" and "s" for a set it is clear to me how this can be done, assuming that the deduction rules and some deduction symbols are also incorporated).

Dan Gluck (talk) 21:37, 2 February 2010 (UTC)

No, it's OK. I sorted that out. I will write here an example if anyone else encounters the same difficulty. Dan Gluck (talk) 19:45, 3 February 2010 (UTC)