Gödel's Incompleteness Theorems (2015)
plato.stanford.edu
plato.stanford.edu
One of the professors also had a very old newspaper clipping taped up (it was brown then and that was quite a while ago), about several mathematicians committing suicide in the wake of those proofs. I've looked for corroboration of this and have never found it. A bit difficult to comprehend from a modern perspective, but more plausible with an appreciation of the 19th Century faith in rationalism / logical positivism that Godel helped overturn.
Not many people are aware that Godel spent much of his life secretly working on a modern update of an ontological argument for God's existence, and didn't reveal this until late in life -- https://en.wikipedia.org/wiki/G%C3%B6del%27s_ontological_pro...
The main problem with ontological arguments (and why, even as a Christian, I don't like them) is because they seem to embed the conclusion in their first premise. E.g.: the possibility of a maximally great being seems to definitionally imply its necessity. Why? Because such a being B must have some properties P = { ? ? ? ... }. We may not be sure what's inside P, but we know, with absolute certainty, that existence is in there.
Kant would disagree. He thinks that existence is not a property. This is a rare case when I think he's right.
But that is also true of the informal rhetorical arguments that are more common in (christian) apologetics.
The gift of formal proofs is that they make explicit and unavoidable this embedding of conclusion in premise, which is fundamental to all (epistemologically rational) apologetics
It might be true of all ontological arguments, but certainly not all apologetic arguments.
One of my favourite tongue-in-cheeek replies I read to these ontological arguments: Ah, but surely there is no greater being than one who could create the universe despite not existing!
https://github.com/FormalTheology/GoedelGod
Now we just wait for someone to code a proof of Erdos' Supreme Fascist..
I'm curious where you studied; I also took a semester course on "logic and computability" where the main text we read was 'Godel, Escher, Bach'
We briefly talked about Godel's proofs, but they are nontrivial. Henkin's proof of completeness is hard enough[1]. I don't mean to sound dismissive, but a class where Godel, Escher, Bach is the text does not seem very rigorous. Logic is very tricky stuff. And once you get into infinities, it's not even intuitive.
[1] https://www.cs.nmsu.edu/historical-projects/Projects/complet...
To answer your question, I went to one of the so-called "elite" American colleges that still has a primarily classical/analytic philosophy program (as opposed to what is known as a "Continental" program). Would rather not say which one, but I was able to take some great logic courses through the philo department.
We used Godel's work directly, and if memory serves also some Goldfarb.
https://www.amazon.com/Computability-Logic-George-S-Boolos/d...
Let's say your beliefs about the integers can be summarized by some formal theory T. ("Every number has a successor", and so on, until your intuition runs out of things to say.) Now Godel jumps out of the bushes and says aha, your T doesn't include Con(T), so you aren't the math genius that you thought you were!
But let's stop for a moment and consider what it would take for T to include Con(T). First of all, compared to other sentences about integers that you believe, Con(T) is an absolutely huge sentence. It must contain an arithmetization of all of T (encoding the axioms, inference rules, etc. into integer arithmetic).
Second of all, if Con(T) is included in T while speaking about T, it might need to include an arithmetization of Con(T) itself! That uses a diagonal construction ("quine" in computer science terms), making the sentence even bigger. Now you're looking at some kind of hundred-kilobyte Diophantine equation, with no intuitive reason to believe it at all.
And third of all, it's easy to see that an inconsistent theory T would easily prove Con(T) (because it proves any sentence), so having Con(T) inside T doesn't even give you any positive evidence for trusting T. In fact, we're lucky to live in a world where Godel's theorems are true, and having Con(T) inside T is negative evidence instead of none at all!
Also, the comment about size and diagonalization is interesting. The Gödel sentence from the first incompleteness theorem is made by diagonalizing, while the sentence from the second incompleteness theorem is just "Con(T)", so the sentence from the 2nd theorem is shorter and more natural if written out in full---making it even more disappointing that it's not provable. Indeed, if we put in more work we should be able to prove a more interesting theorem, but I never really thought about it before.
"We outline our construction of a single equation involving only addition, multiplication, and exponentiation of non-negative integer constants and variables with the following remarkable property. One of the variables is considered to be a parameter. Take the parameter to be 0, 1, 2, ... obtaining an infinite series of equations from the original one. Consider the question of whether each of the derived equations has finitely or infinitely many non-negative integer solutions. The original equation is constructed in such a manner that the answers to these questions about the derived equations are independent mathematical facts that cannot be compressed into any finite set of axioms."
So there are finite (though several hundred pages long) equations for which the finiteness of the solution set is independent of every finite axiomatization of arithmetic. So suddenly, even though the formula is enormous, the type of sentence is perfectly normal. Does f(x) have finitely many solutions, where f(x) is built from addition, multiplication and exponentiation.
Much more so than Gödel’s incompleteness this deeply violates my intuition about what type of statements should be decidable.
And yes, I worded that ambiguously. Let me rephrase, to see if I got it correct: Pick any finite axiomatization. Then there is a concrete f(x) that we can write down in about 200 pages, for which finiteness of the solution set is not decidable.
The fact that there are diphantine equations for which finiteness is undecidable is really surprising to start with to me.
~(Ex)Proof(x, ~0=0)
I.e., "There doesn't exist a proof of ~0=0."
Of course, representing the word "proof" using PA isn't trivial, and expanding that bulks things up a bit. But the sentence that's really long is the Godel sentence. "(G) There is no proof of G."
[1] http://mathoverflow.net/questions/66776/alternative-arithmet...
https://en.wikipedia.org/wiki/Logicomix
get it at your library now.
http://www.worldcat.org/title/logicomix/oclc/708346776&refer...
This doesn't have anything to do with anything, just a thing that happened
1. p and not p (given).
2. p (from 1).
3. not p (from 1).
4. p or q (from 2 (disjunction introduction)).
5. q (from 3 and 4).
So obviously this would upset quite a few things around :) that said, the interesting stuff is with Graham Priest's (et al.) paraconsistent logic systems wherein your system can tolerate a contradiction without exploding in whole. And (so the story goes) those systems may offer an actual insight into handling incompleteness (while still being usable). If anyone has looked into this more, would be interesting to hear about it!
I would therefore say that mathematics is a human invention and build on top of logic, it seems in no way universal. All the things we discover in mathematics are nothing but consequences of the axioms, the definitions, and the logic used to prove things. If there is something universal, at least so it seems to me, than it would have to be logic.
This assumption wasn't always accepted by mathematicians.
— John Barrow
I would have a look at e.g. Bob Harper's homotopy type theory lectures. In the 2nd lecture on Judgements, he goes through it at about 50 minutes in.
http://www.cs.cmu.edu/~rwh/courses/hott/
And Andrej Bauer's paper/lecture on "5 stages of accepting constructive mathematics"
It is especially good at ensuring the reader doesn't come away infected with the pseudo-profound BS that plagues many discussions of the Gödel's Theorems.
For important, wiki-friendly topics like this one, HN is frustratingly not great for building a readily checkable/cumulative knowledge base, rather than encouraging a forgetful herd discussion that goes around in circles. It is as I say frustrating for anyone who wants long-term knowledge rather than flimsy "news".
1.https://smile.amazon.com/Incompleteness-Proof-Paradox-G%C3%B...
http://rationalwiki.org/wiki/G%C3%B6del's_incompleteness_the...
But how this can be extended to the whole universe of all possible formal systems? Who guarantee that there will be no some new system with quantum-oracle-operator, which will not be affected by incompleteness theorem, and can self-proof self-consistency?
Even well known m-recursive functions (which are essentially Turing machines) are wider class than primitive recursive functions used in the proof..
Effectively, syntactic completeness in logic is equivalent to the Halting Problem in computing, via bijective proofs.
Now you add new tool: existence predicate, and you got first order logic, which allows you to prove Godel's incompleteness Theorem.
What is the guarantee exactly that more advanced systems can't exist? Say system with new 'quantum hack' operator. You can't prove formula from Godel's proof? 'Quantum hack' under some conditions covers missing gap in proof path by building continuum truth table and give you tool to check if formula from Godel's proof actually provable, or it is false.
Again, this applies to any given formal system. Goedel's Incompleteness Theorem is parametric over formal systems, with first-order Peano Arithmetic being one of the weakest, most standardized systems in which it applies. The real condition for the Theorem is, "Any formal system sufficient to describe Turing machines."
>Say system with new 'quantum hack' operator.
That operator is called a Turing Oracle, and it's physically impossible. Possessing a Turing Oracle is equivalent to reversing the Second Law of Thermodynamics and refuting Heisenberg's Uncertainty Principle. It's physically wrong.
It is parametric over formal systems described in Principia Mathematics. That's it. It doesn't take into account other possible types of formal systems. At least I didn't notice this when reading actual proof.
> That operator is called a Turing Oracle
I think it may be very different thing. I just gave you a quick example. That operator can be something very different. You can set measure on space of proofs, and derive concept of asymptotic proof, and say if proof is asymptotic, then it is proof. There can be many variations around possible formal systems.
> and it's physically impossible
This is very strange argument. Turing machine contains infinite amount of memory, and likely is physically impossible.
If you have those two things, Godel's technique works. The details vary greatly based on the formal logic in use, but part of the process is encoding the formalism in Peano arithmetic.
So no, adding more things doesn't break it, because the construction takes those additional things into account.
Unless you want your logic to be infinite, of course. In that case, the method would break down. But it has to be infinite in the sense of having no finite representation, rather than the much weaker sense of having some infinite representation.
> Unless you want your logic to be infinite, of course. In that case, the method would break down.
Godel numbering is infinite, because it is just natural numbers. Nothing prevents you to build the same proof for infinite number of axioms, rules, functions, variables..
That's kind of a non-sequitor. Second-order logic, the logic required to express Peano arithmetic, consists of a finite number of axioms and inference rules. The number of statements that can be generated with those rules is irrelevant. The logic is finite.
Godel numbering requires assigning a number to each logical axiom and inference rule. The mechanism of Godel's numbering implies that every derivation has a unique number as well, but that number is derived, not assigned. The difference is important. It means that the information required to construct the system is finite. If the supply of axioms and inference rules was infinite, with no finite alternate encoding, it would mean Godel numbering would fail because the process of assigning numbers to each axiom and rule would never complete.
But that's all a bit of an aside. To get back to your original question...
Godel's proof provides a mechanism to construct a statement that refers to itself in any logic that can express Peano arithmetic. Once you can make a statement refer to itself, the game is over. You've lost.
But Godel's approach is even more clever. Not only can a statement refer to itself, it can refer to proofs in its own formal system.
So it constructs "This statement has no proof within the formal system it's expressed in."
That's far more subtle of a statement than you give it credit for. It makes no claim about other formal systems. But once you start addressing it from a different formal system (or an informal metalogic) the statement no longer refers to the logic system in which you are examining it.
So sure, you can say that Godel statement G0 constructed in formal system L0 is provable (or disprovable!) in formal system L1. But that doesn't prove anything about the completeness or consistency of L1, because G0 is a statement about L0. And if L1 happens to be strong enough to encode Peano arithmetic, you can construct a statement a Godel statement G1 which refers to logic L1.
This is always applicable. Whatever your G0 and L1 are, G0 says nothing about L1, but the existence of L1 is irrelevant to the statement G0, and very probably also allows the existence of G1. (I've spent lots of time discussing when it doesn't, and won't belabor the point further.)
I strongly disagree with that. There is no evidence of that.
> And if L1 happens to be strong enough to encode Peano arithmetic, you can construct a statement a Godel statement G1 which refers to logic L1.
As I said before, Godel proved that your G1 is unprovable in specific framework of Principia Mathematics, which is first/second/higher theory/logic (consist on quantors, functions, predicate, variables, rules).
I don't see evidence that there can be no other framework even with Peano arithmetic inside which can't deliver consistent theory. You started speculating about framework with infinite set of axiom, and I disagreed with that, but there can be other type of infinite framework, say when you allow proofs of infinite length, then Godel numbering may be impossible, and it can be example of such framework.
This piece about what the theorem means for developing "deep AI" and the human mind, was a fascinating eye opener for me, about the far stretching implications of the theorem.
"The Lucas-Penrose Argument about Gödel's Theorem" - http://www.iep.utm.edu/lp-argue/
(though maybe in a completely irrelevant sense of truth).
Wow, is that what people actually think a "computational theory of mind" is? Look, just because every program can be trivially rewritten as some kind of formal proof system, doesn't mean that any given program meaningfully has the semantics of a formal proof system, let alone the mind.
So therefore, the universe is either full of magic (in a system with inconsistency, anything can happen), or mystery (there are true things that we can never prove).
My belief is that the quest to find a unified physics that describes everything is provably impossible due to Godel's theorem.
And on the rare occasions when I look for evidence of God, the fact that one of the things we can know for sure - is that we can't know everything - provides about as much comfort as I need.
1. That the universe _is_ a formal system, rather than being describable in the language of some formal system. It's not evident what the universe being a formal system even means, or how it squares with basic intuition regarding e.g. the fact that physical systems have state.
2. That, dropping the physical system <=> formal system equivalence and given some real system R consisting of some fundamental entities whose behaviors can be described in full in the language of some formal system S, (borrowing a useful construct from Lucas' anti-mechanism argument, even though I don't buy that argument) no machine can be constructed in R which computes theorems of some formal system S' in which all true statements of S are provable, meaning that no state of the system R can be said to contain a description of S', and that S' is therefore not describable by any arrangement of the entities in R (assuming some reasonable predicate over states of R that is true for a state when some arrangement of a subset of the entities in that state describes S'). Intuitively, this doesn't seem to hold up: by analogy, I can describe a universal Turing machine with a computer equipped with only finite memory. You could then attempt to go down the road of claiming that, even if a description of S' is possible in R, that a mind within R would not be capable of formulating that description, but then you're heaping on an even larger tangle of assumptions, unknowns, and things you have to define if you're going to argue the case rigorously.
The point being that confidence about _any_ hypothesis about the nature of reality made on the basis of Gödel's incompleteness theorems is not epistemologically warranted.
How would that happen? Physics is an empirical science, all we have to do is to look at what actually happens and write it down. Even if we fail to find good mathematical expression to describe what we see, we can always just create charts and tables describing what happens. There is nothing that prevents us from fully describing physics.
Unifying physics then just means finding one mathematical model that is able to describe all the aspects we discovered in different limits. I can not see how Gödel's incompleteness theorem would have any bearing on this. We just have to find a set of equations that reproduce our observations given the experimental setup. This does not involve any proofs, it's just the question whether a set of equations accurately describes the universe.
I can really only think of one way in which describing the universe with mathematics must fail and that is if there is no mathematical description of the universe. Otherwise we could always guess a set of equations and then verify that it works in all experiments we ever performed. You can of course never be sure that you did not simply miss one experiment that causes your theory to fail, but that is in the nature of physics. This also seems pretty unlikely, I fail to imagine anything that could escape all attempts of mathematical describing it in principle.
To be precise: it tells us that it's not generally possible to build a complete consistent model, but it may still be possible in specific cases, like our universe. My hunch is that such a model does exist, that we will find it, and further, that it will actually be rather elegant. We'll never be able to prove we've found it though, because we only have partial information— if we were running on a virtual machine, is the host system running Linux or BSD?