2
$\begingroup$

I wish to check if my understanding of the limitations on mathematical logic due to Gödel's incompleteness theorem is correct. I was under the impression that it is possible to both avoid contradictions and prove every false statement false. For some statements it may not be possible to find an algorithm that can be used to prove them true. The word algorithm in this definition is where my question lies.

Is it possible to prove certain statements true by just chancing upon the proof?

Unless my definition or use of the term is wrong, doing so would not require an algorithm to arrive at that point.

I feel this question is relevant to a lot of people, because if true, it changes the perspective on incompleteness theorems from one of impossibility to unlikelihood of certain things been proved.

(I have also heard that some statements are simply not provable in a finite amount of time; but I was under the impression that there exist a few true statements that no algorithm can prove true given a number of axioms to start with).

|cite|improve this question
$\endgroup$
  • 1
    $\begingroup$ Note that 'algorithm' here includes any formal proof system. Whether the 'originator' is human-based or digital, the proof itself is a series of formal steps; a recipe, if you will, that starts with the axioms of your system and proceeds by a series of rules to the result. Those proofs - and not the process of finding them - are what cannot possibly cover all true statements of a (sufficiently rich and consistent) theory. $\endgroup$ – Steven Stadnicki Dec 31 '16 at 13:47
  • 1
    $\begingroup$ "check if my understanding of the limitations on mathematical logic due to Gödel's incompleteness theorem is correct"... No, it is not. $\endgroup$ – Mauro ALLEGRANZA Dec 31 '16 at 13:55
  • $\begingroup$ "For some statements it may not be possible to find an algorithm that can be used to prove them true. " In formalized arithmetic (like e.g. first-order Peano arithmetic) the sentence found by Godel are not provable with the "resources" of the formal system involved. Here the "algorithm" is the proof system : arithmetical axioms + logical rules of inference. $\endgroup$ – Mauro ALLEGRANZA Dec 31 '16 at 13:57
  • $\begingroup$ "chancing upon the proof?" What does it mean ? $\endgroup$ – Mauro ALLEGRANZA Dec 31 '16 at 13:57
  • $\begingroup$ So algorithm refers to the rules of a system without reference to the process of finding the result? $\endgroup$ – user400188 Dec 31 '16 at 13:58
2
$\begingroup$

There is nothing about not being able to find an algorithm to prove a statement in the conclusion of Godel's theorem. It is about the existence of proofs themselves within formal systems. Perhaps the confusion is from the fact that proofs in formal systems are very mechanical in nature; they are rigid applications of rules of inference to axioms and could in principle be listed off one by one by a computer.

What Godel's (first) incompleteness theorem says is, roughly, in any formal system of axioms and rules of inference (that is sufficiently rich that it supports basic arithmetic), there are well-defined statements for which there is no proof either way. The part in the theorem about algorithms isn't about the existence of an algorithm to prove a given result, but rather the existence of an algorithm that will list all the theorems off one by one, which is an important precondition for the theorem to hold.

If you have a statement that you want to prove, you could in principle wait for the algorithm to spit it out, but you could be waiting for an arbitrarily long time and you're out of luck if it isn't a theorem after all. To prove a theorem, you don't use this enumeration, you try to figure out the proof (chance upon it). This all doesn't have much to do with the conclusion of Godel's theorem, that there are statements that cannot be proven either way from the axioms, since the existence of the enumeration algorithm is a different issue than the existence of particular proofs and the provability of statements.

|cite|improve this answer
$\endgroup$
  • $\begingroup$ This answers my question pretty well. However I have to ask is it not possible that we can prove a statement that is unable to be proven true not false? This is where some of the confusion lies I think. Because it feels like there is a process that cant be done for proving something true but a process for proving it not false is possible. I would move this to chat because the comments are getting extended but I don't have enough rep. $\endgroup$ – user400188 Dec 31 '16 at 14:24
  • $\begingroup$ I commented below last post too, yeah it's getting long. I don't understand what you're getting at here. Let's start with the first thing 'is it not possible that we can prove a statement that is unable to be proven true not false?' If a statement is unable to be proven true, we can't prove it. Those are the same thing. Not false is the same as true. Can you think a little more about what you're asking and rephrase? $\endgroup$ – spaceisdarkgreen Dec 31 '16 at 14:37
  • $\begingroup$ I got schooled by Daniel below his answer. The upshot of my answer doesn't change but he shed some light on the confusion over the algorithm issue. I edited to my answer extensively to reflect that and to, let's say, increase its correctness. $\endgroup$ – spaceisdarkgreen Dec 31 '16 at 20:34
  • 2
    $\begingroup$ Your answer (as it is now) is correct as far as I can see, so well done! By the way, we say that the set of provable sentences is recursively enumerable since there is an algorithm that spits them out one by one, but note that no algorithm can enumerate them in order because if not we can enumerate the set of unprovable sentences as well, which is impossible if the formal system can interpret arithmetic. See my post at math.stackexchange.com/a/1895288/21820 for a definition of "interpret arithmetic" that should cover almost every possible useful formal system. $\endgroup$ – user21820 Jan 2 '17 at 8:47
  • $\begingroup$ @user21820 Thanks! $\endgroup$ – spaceisdarkgreen Jan 2 '17 at 20:07
4
$\begingroup$

Suppose I write down a system of axioms, like so:

  1. $\forall x. \forall y. (x y) z = x (y z)$
  2. $\exists e. \forall x. e x = x e = e$
  3. $\forall x. \exists y. x y = y x = e$

This system of axioms is incomplete, because for instance it does not allow us to determine whether the following statement is true or false:

  1. $\forall x. \forall y. x y = y x$.

Why? Well, if you consider axioms (1) - (3), there is more than one mathematical object satisfying them. One object which satisfies them is the multiplicative group $\mathbb{R}^\times$ of real numbers. Another is the group $\operatorname{GL}_2(\mathbb{R})$ of $2 \times 2$ real matrices. In $\mathbb{R}^\times$ axiom (4) is true; in $\operatorname{GL}_2(\mathbb{R})$ it is false.

Moreover, any time a system of axioms is incomplete it is for precisely this reason: it describes more than one mathematical object and those objects have different properties.

Now if we're trying to describe $\mathbb{R}^\times$ with our axioms and we want to rule out $\operatorname{GL}_2(\mathbb{R})$, we could add (4) to our list of axioms. But they'd still be incomplete. (Exercise: check this!)

Now, maybe if you have a particular mathematical object in mind you can just keep adding true statements about it and at some point your axioms will completely describe it (up to elementary equivalence). At that point your axioms will be complete, since they can determine if any first-order statement about the object is true or false.

But there's no guarantee you'd ever finish. To draw an analogy, consider an arbitrary real number, say

$r = 2,345,098.231456981324509813245098123409123409123049\ldots$

If there's no useful "pattern" to the number, it's possible that we can't describe it in a finite amount of space. To make this precise, we say that a number $r$ is computable if there exists a Turing machine that, given a positive integer $n$ as input, prints out the first $n$ decimal digits of $r$. Since there are countably many Turing machines and uncountably many real numbers, almost all real numbers are uncomputable.

It's often the case that a mathematical object requires infinitely many axioms to completely describe it (up to elementary equivalence). (It's always possible, because you could simply take your list of axioms to be every single true statement about the object.) However, such a list might be more akin to

$\pi = 3.14159265358\ldots$

-- that is, computable -- or it may be more akin to the uncomputable number $r$ above.

What Godel's incompleteness theorem says is that if you're trying to describe the natural numbers, every complete set of axioms describing them is uncomputable.

|cite|improve this answer
$\endgroup$
  • $\begingroup$ Your answer seems to imply that there is a system of axioms that describes the natural numbers in which every statement is decidable... precisely what the theorem forbids. The axioms being uncomputable in some sense does not get around the that. Just cause you keep adding more and more axioms doesn't mean the resulting system ever becomes complete (in the sense that every statement is decidable), even if you think it's complete in the sense that it uniquely specifies the concept you're trying to describe (unlike geometry w/o parallel postulate or your 1.,2.,.3 example) $\endgroup$ – spaceisdarkgreen Dec 31 '16 at 17:13
  • 2
    $\begingroup$ @spaceisdarkgreen "Your answer seems to imply that there is a system of axioms that describes the natural numbers in which every statement is decidable" There is indeed such a system of axioms. There are many such. One example: take your axioms to be the set of all true statements about the natural numbers. This does not contradict Godel's incompleteness theorem, because Godel's incompleteness theorem merely says that none of the complete sets of axioms for the naturals are recursively enumerable. $\endgroup$ – Daniel McLaury Dec 31 '16 at 19:47
  • $\begingroup$ @spaceisdarkgreen: I'm not sure precisely how to interpret the rest of your comment, but completeness is indeed equivalent to having exactly one model up to elementary equivalence. $\endgroup$ – Daniel McLaury Dec 31 '16 at 19:56
  • $\begingroup$ Ok, I get it now, you're right! Thanks, and sorry for the unwarranted criticism. $\endgroup$ – spaceisdarkgreen Dec 31 '16 at 20:55

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.