First let me explain what I mean by algorithmically derivable. An algorithm must be able to come up with the proof without prior knowledge of the proof, in the same way mathematicians and computer scientists are able to create new proofs without prior knowledge of the proofs.

Our proof deriver enumerates all possible axiomatic systems, and with each system enumerates all possible proofs. It checks each proof to see if it proves Goedel's 1st theorem. This algorithm will necessarily derive all finite proofs eventually.

Goedel's 1st theorem states no sufficiently powerful axiomatic system can be complete and consistent at the same time. The deriver is complete, since it will eventually be able to prove all true statements and disprove all false statements. This means the deriver is inconsistent, so it cannot know whether a set of axioms used to prove Goedel's 1st are consistent.

Therefore, an algorithmic deriver is unable to derive the proof for Goedel's 1st theorem.

Does this proof succeed in showing Goedel's 1st theorem is not algorithmically derivable?

  • $\begingroup$ Can you formulate a more specific question than "please review my thoughts"? $\endgroup$ – Raphael Sep 19 '17 at 17:38
  • 2
    $\begingroup$ There is the little detail of having arithmetic around. Your recollection of Gödel's first incompleteness theorem is wrong. $\endgroup$ – Andrej Bauer Sep 19 '17 at 21:34
  • 2
    $\begingroup$ Define "without prior knowledge of the proof". Hint: I don't think that can be defined in any precise or rigorous way. It's the kind of thing that sounds like it means something but is very difficult to formalize. $\endgroup$ – D.W. Sep 20 '17 at 1:04
  • $\begingroup$ @D.W. it may be difficult to define "prior knowledge" in an all encompassing way. Printing out the proof definitely counts. However, the enumeration algorithm I outline does not possess any prior knowledge. $\endgroup$ – yters Sep 20 '17 at 2:28
  • $\begingroup$ @D.W. Here is another way. If there are multiple sets of proofs from consistent axioms, and we must choose between them, and our target proof only occurs in some, then picking the right set counts as prior knowledge, especially if the right sets are vanishingly small portion of the population. From a Shannon information point of view, picking the right set is highly improbable, thus doing so consequently entails a large amount of information. $\endgroup$ – yters Sep 21 '17 at 4:45

The deriver is complete, since it will eventually be able to prove all true statements and disprove all false statements. This means the deriver is inconsistent, so it cannot know whether a set of axioms used to prove Goedel's 1st are consistent.

To start with, your deriver is actually not an axiomatic system to which Goedel's theorem would apply.

But assuming I understood your description correctly, it'll simply "prove" all sentences for two different reasons: 1) for each sentence there is a system where it's an axiom and so provable; 2) systems it enumerates will include inconsistent systems in which every sentence is provable. So the deriver is trivially inconsistent and tells you nothing about Goedel's theorem.

Now, instead of your deriver consider one which enumerates all proofs in $PA$ until it finds a proof of Goedel's first theorem and then stops. This seems to satisfy your requirements ("seems" because you don't define "prior knowledge").

  • 2
    $\begingroup$ @yters But Gödel's theorem, stated as a sentence of arithmetic, happens to be provable in $PA$ as well as true, which is why the deriver in the last paragraph works. $\endgroup$ – Alexey Romanov Sep 21 '17 at 6:44
  • 1
    $\begingroup$ "How then can $PA$ prove the sentence is true but unprovable within $PA$?" It can't! It just proves that the sentence is unprovable (and so is its negation). By Tarski's theorem (en.wikipedia.org/wiki/Tarski%27s_undefinability_theorem), we can't even define "a sentence of arithmetic is true" in $PA$, so it doesn't really make sense to talk about $PA$ proving that some sentence is true. $\endgroup$ – Alexey Romanov Sep 21 '17 at 8:45
  • 1
    $\begingroup$ But $PA$ can prove something like "a sentence of arithmetic is provable in $ZFC$ but not in $PA$". Since we believe $ZFC$ is valid, this implies such a sentence is true, but on metalanguage level, not inside $PA$. $\endgroup$ – Alexey Romanov Sep 21 '17 at 8:49
  • 1
    $\begingroup$ A good example is: $PA$ proves "$ZFC$ proves "$PA$ is consistent"", but it doesn't prove "$PA$ is consistent". $\endgroup$ – Alexey Romanov Sep 21 '17 at 11:25
  • 1
    $\begingroup$ @yters Another possible point of confusion is that some proofs of Gödel's theorem use the notion of truth (like Boolos' one). But there are other proofs which don't and it's those proofs which can be formalized in $PA$. $\endgroup$ – Alexey Romanov Sep 21 '17 at 21:02

Your reasoning is incorrect.

It is true that your hypothetical "proof deriver" cannot derive all true statements. No proof derivation system can, and indeed, it is not even possible to express the set of true statements in arithmetic, which is a consequence of Tarski's theorem on truth, itself a consequence of Gödel's theorem.

However, your algorithm does enumerate all provable statements, including the incompleteness theorem itself.

In fact, here's a much simpler algorithm:

  1. Print a formal proof of the incompleteness theorem.
  2. Halt.

So you need a much subtler argument to prove that computers can't do what humans can do in terms of proofs. Certainly you would need a better notion of what "prior knowledge" of a proof means. Indeed, many people today believe that there are no tasks which are fundamentally impossible for computers but possible for humans, and I know of no unassailable argument for that position.

  • $\begingroup$ Yes, the point is it proves all provable statements, and also disproves all provable statements, so it is inconsistent. But, that is the only way to guarantee it will print Goedel's proof. Otherwise, it must start with prior knowledge, as your algorithm does. But, Goedel did not start with prior knowledge of his proof. He had to derive it through careful thought. $\endgroup$ – yters Sep 19 '17 at 21:41
  • $\begingroup$ @yters well if you enumerate all possible systems, then yes, you'll hit a few inconsistent ones by accident. In fact, Peano Arithmetic itself might be inconsistent! Neither humans nor computers can tell if a system (containing "enough arithmetic) is consistent, only if they are inconsistent (because they have found an inconsistency). Again, nothing the humans do is theoretically impossible for computers. $\endgroup$ – cody Sep 19 '17 at 22:03
  • 1
    $\begingroup$ In fact you can imagine a program that enumerates all systems and all proofs in those systems, and then throws out all theorems from inconsistent systems as soon as it finds an inconsistency. One could argue that humans are running exactly that algorithm when they do mathematics... $\endgroup$ – cody Sep 19 '17 at 22:04
  • $\begingroup$ If we assume mathematicians are reliably finding consistent axioms and proofs, then my argument shows algorithms cannot do the same. On the other hand, if we assume algorithms can do everything humans can do, then we must also conclude we have no idea if our mathematical knowledge is consistent, it is a complete guess that it is. $\endgroup$ – yters Sep 19 '17 at 22:47

Our proof deriver enumerates all possible axiomatic systems

But the set of possible axiomatic systems also include the inconsistent systems. On the other hand, the consistent axiomatic systems are not computationally enumerable, hence you cannot enumerate them.

But cody's point is probably even more relevant, since the algorithm can just write down an existing proof. That existing proof will be relative to some formal system like Coq's calculus of construction, but that should be OK.

  • $\begingroup$ All axiomatic systems are just finite strings of symbols, so they can be enumerated, along with invalid systems. That's my point. $\endgroup$ – yters Sep 19 '17 at 21:39
  • $\begingroup$ @yters The upvoted comment by cody about throwing "out all theorems from inconsistent systems as soon as it finds an inconsistency" seems more to the point to me. Or at least I get the point cody is making here, while I still don't understand your point. Maybe you should explicitly state your point and explain why you think it is important. $\endgroup$ – Thomas Klimpel Sep 20 '17 at 0:26
  • $\begingroup$ If you throw out all inconsistent theorems, then you still will not know if the remaining theorems are consistent. So the boat you are in is no different than my boat. We are in the same boat, my friend. $\endgroup$ – yters Sep 21 '17 at 4:24
  • 1
    $\begingroup$ @yters And that is a valid point. So you have two different problems here: (1) you need to understand yourself what you try to explain, and (2) you need to find a way to explicitly state your points and explain them. For the topic above, both points are challenging. I am not even sure whether Goedel's 1st theorem does go slightly beyond the axiomatic method: "but the conclusions of strict containment (or inequality) go beyond the axiomatic method" or not (after reading cody's answer). $\endgroup$ – Thomas Klimpel Sep 21 '17 at 8:50
  • $\begingroup$ That's a good point, it seems G1 must somehow go beyond axiomatic systems to apply to all sufficiently powerful axiomatic systems. $\endgroup$ – yters Sep 21 '17 at 16:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.