A Computability Proof of Gödel’s First Incompleteness Theorem(medium.com)
medium.com
A Computability Proof of Gödel’s First Incompleteness Theorem
https://medium.com/cantors-paradise/a-computability-proof-of-g%C3%B6dels-first-incompleteness-theorem-2d685899117c
43 comments
While I applaud the effort to recast Godel's proof in computational terms, I think this author makes a horrible mess of it. The core idea is extremely simple, particularly in today's world: strings of symbols can be re-cast as numbers (and vice-versa), and rules for manipulating those symbols can therefore be re-cast as arithmetic. The mapping between strings of symbols and numbers is called an encoding. Godel's original encoding relied on exponentiation of prime numbers, and that produced one particular set of mathematical operations that mapped onto the formal rules of Peano arithmetic. Nowadays we can simply encode symbols as ascii or unicode with the obvious translation into numbers and arithmetic, and that produces a different set of mathematical operations that map onto the formal rules of Peano arithmetic. All the rest, all the heavy lifting, is just cranking out the tedious details of what those mathematical operations actually are, but none of that is necessary in order to understand the core idea of the proof.
That's the core idea of the proof inasmuch as parsing is the core idea of writing a compiler. Once you get that part out of the way, the incompleteness theorem is a clever diagonalization argument (and is a consequence of the Lawvere fixed point theorem).
The way it all sort of works is:
1. A mathematical theory is called consistent if there is some model of it, a self-consistent set M of all mathematical objects for that theory. For example, a model of the natural numbers would be {0,1,2,...}, but there are other models too.
2. By some parsing method, we can encode every "first-order definable" (akin to "computable") statement and function as an element of M itself. Let (M -> M) denote the set of definable functions; by picking out an element nil from M, we can think of such a function as being a boolean-valued function, where like Lisp we say nil is the unique false value, everything else is truthy.
3. Since everything is encodable, there is a function print : (M -> M) -> M and a left inverse read : M -> (M -> M). (I imagine parse errors just return the constant-nil function.)
4. We can define lots of useful functions, like not, where not(nil) = 1 and not(x) = nil for all x != nil, where 1 is anything that's not nil. Another is iff(x,y) = (not(x) == not(y)), that is, whether both inputs are truthy in the same way.
5. An interesting function you can define is provable : (M -> M) -> M, which takes a function f and returns whether or not M contains a proof that f is non-nil for all inputs. This takes a bit of implementation, but it's not too hard.
6. Now to set up diagonalization. Define f : M -> M by
The way this is summarized is: either the theory is inconsistent (there is no model) or it is incomplete (the provable function can't prove all true things).
The way this ends up working in the mathematical landscape is that, if there is any model at all, there is more than one. (Something is provable if and only if it is true in all models -- Godel.)
The way it all sort of works is:
1. A mathematical theory is called consistent if there is some model of it, a self-consistent set M of all mathematical objects for that theory. For example, a model of the natural numbers would be {0,1,2,...}, but there are other models too.
2. By some parsing method, we can encode every "first-order definable" (akin to "computable") statement and function as an element of M itself. Let (M -> M) denote the set of definable functions; by picking out an element nil from M, we can think of such a function as being a boolean-valued function, where like Lisp we say nil is the unique false value, everything else is truthy.
3. Since everything is encodable, there is a function print : (M -> M) -> M and a left inverse read : M -> (M -> M). (I imagine parse errors just return the constant-nil function.)
4. We can define lots of useful functions, like not, where not(nil) = 1 and not(x) = nil for all x != nil, where 1 is anything that's not nil. Another is iff(x,y) = (not(x) == not(y)), that is, whether both inputs are truthy in the same way.
5. An interesting function you can define is provable : (M -> M) -> M, which takes a function f and returns whether or not M contains a proof that f is non-nil for all inputs. This takes a bit of implementation, but it's not too hard.
6. Now to set up diagonalization. Define f : M -> M by
f(x) = print(lambda _ -> not(provable(read(x)))
iff (forall z -> read(x)(z))).
g(nil) = not(provable(g)) iff (forall z -> g(z)).
The way this is summarized is: either the theory is inconsistent (there is no model) or it is incomplete (the provable function can't prove all true things).
The way this ends up working in the mathematical landscape is that, if there is any model at all, there is more than one. (Something is provable if and only if it is true in all models -- Godel.)
> this diagonalization argument is the core idea
No, not really. I mean yes, it is, if you're a mathematician. But no, it's not, if you're someone who needs to have binary encoding explained to them, which the original article attempts to do. (And if you're a mathematician you don't need Godel's theorem explained to you at all.)
Here's how I would go on with the exposition:
A formal proof is a sequence of strings, each of which can be derived from the set of strings that precede it in the sequence according to a set of rules. There is a particular set of rules called Peano arithmetic (because they were invented by a guy named Peano) that are so far mankind's best attempt at encoding the fundamental properties of the natural numbers. Ideally, a string in a formal proof under the Peano rules should correspond to a true statement about numbers, and conversely, every true statement about numbers should have a corresponding proof. But it turns out that both of these cannot be simultaneously true. In particular, we can prove that if all strings in proofs correspond to true statements about numbers, then there must be true statements about numbers that cannot appear in proofs.
Godel's original proof involved constructing a number N whose corresponding string essentially means "The string corresponding to N has no proof." Describing how N is constructed is tricky, but since we know about the halting problem we can prove this result in a much more straightforward way: suppose that we could prove any true statement about numbers. Consider an arbitrary program P. That program can be encoded as a number N. So the statement "The program corresponding to the number N halts" is a claim about numbers. It is either true or false. If it is true, then by our assumption we can prove it, and if it is false then its negation is true and we can prove that. So now all we have to do to solve the halting problem is to systematically search through the space of all possible proofs until we find a proof either of "the program corresponding to the number N halts" or its negation, at which point we will know whether or not P halts, and so we have solved the halting problem. But we already know that we can't solve the halting problem, so our assumption that all true statements about numbers can be proven must be false.
No, not really. I mean yes, it is, if you're a mathematician. But no, it's not, if you're someone who needs to have binary encoding explained to them, which the original article attempts to do. (And if you're a mathematician you don't need Godel's theorem explained to you at all.)
Here's how I would go on with the exposition:
A formal proof is a sequence of strings, each of which can be derived from the set of strings that precede it in the sequence according to a set of rules. There is a particular set of rules called Peano arithmetic (because they were invented by a guy named Peano) that are so far mankind's best attempt at encoding the fundamental properties of the natural numbers. Ideally, a string in a formal proof under the Peano rules should correspond to a true statement about numbers, and conversely, every true statement about numbers should have a corresponding proof. But it turns out that both of these cannot be simultaneously true. In particular, we can prove that if all strings in proofs correspond to true statements about numbers, then there must be true statements about numbers that cannot appear in proofs.
Godel's original proof involved constructing a number N whose corresponding string essentially means "The string corresponding to N has no proof." Describing how N is constructed is tricky, but since we know about the halting problem we can prove this result in a much more straightforward way: suppose that we could prove any true statement about numbers. Consider an arbitrary program P. That program can be encoded as a number N. So the statement "The program corresponding to the number N halts" is a claim about numbers. It is either true or false. If it is true, then by our assumption we can prove it, and if it is false then its negation is true and we can prove that. So now all we have to do to solve the halting problem is to systematically search through the space of all possible proofs until we find a proof either of "the program corresponding to the number N halts" or its negation, at which point we will know whether or not P halts, and so we have solved the halting problem. But we already know that we can't solve the halting problem, so our assumption that all true statements about numbers can be proven must be false.
I find computer scientists have a stronger grasp on encodings than mathematicians, who tend to get bogged down in these details due to lack of familiarity. With what I wrote up, the point I failed to make is that it comes down to some cleverness in how you mess around with read, eval(=provable), and print. That is, follow the Lisp way and think in s-expressions.
I was responding specifically to
> All the rest, all the heavy lifting, is just cranking out the tedious details of what those mathematical operations actually are, but none of that is necessary in order to understand the core idea of the proof.
The thing I'm taking issue with is calling parsing the core idea, with the rest "just"[1] being tedious details, where, as someone who has done some PL implementations, the parsing seems to me to be the tedious part. It's an important idea that's essential to the proof, but, again, that's like saying parsing is the core problem in writing a compiler (or that writing read is the core problem in implementing a Lisp interpreter). This is not exactly evidence of any kind, but notice your whole final paragraph is a diagonalization argument, and it is longer than the first paragraph of your exposition, which quickly explains how strings can represent logical statements and proofs.
Maybe this is a synthesis: the core idea is that you can write an interpreter that takes an encoding of a logical statement and returns whether or not it is provable. Since the interpreter is itself a logical statement, you can apply a diagonalization argument to produce a true statement that refutes its own provability. (When I say the core idea is the diagonalization, I mean both the interpreter and the fixed point finding. When you say the core idea is encoding, I suspect you might mean more the interpreter than how your comment reads to me.)
By the way, with the halting problem argument, it seems like if you're very careful you can write out an explicit Godel sentence, like what the Lawvere fixed point theorem would provide. I'm sort of curious what it would look like, rather than your recipe for how to construct it. (I also wonder what the shortest Godel sentence is. But only as much as I wonder what the shortest quines are.)
> "The string corresponding to N has no proof"
Small correction: it's that "N being true is equivalent to N having no proof." If N is false, then it is provable (bad), so if things are consistent it must be true, hence unprovable. It's interesting that N is a true statement.
[1] I have a banned words list in my office; one entry is "just" because of just what it lets you sweep under the rug.
I was responding specifically to
> All the rest, all the heavy lifting, is just cranking out the tedious details of what those mathematical operations actually are, but none of that is necessary in order to understand the core idea of the proof.
The thing I'm taking issue with is calling parsing the core idea, with the rest "just"[1] being tedious details, where, as someone who has done some PL implementations, the parsing seems to me to be the tedious part. It's an important idea that's essential to the proof, but, again, that's like saying parsing is the core problem in writing a compiler (or that writing read is the core problem in implementing a Lisp interpreter). This is not exactly evidence of any kind, but notice your whole final paragraph is a diagonalization argument, and it is longer than the first paragraph of your exposition, which quickly explains how strings can represent logical statements and proofs.
Maybe this is a synthesis: the core idea is that you can write an interpreter that takes an encoding of a logical statement and returns whether or not it is provable. Since the interpreter is itself a logical statement, you can apply a diagonalization argument to produce a true statement that refutes its own provability. (When I say the core idea is the diagonalization, I mean both the interpreter and the fixed point finding. When you say the core idea is encoding, I suspect you might mean more the interpreter than how your comment reads to me.)
By the way, with the halting problem argument, it seems like if you're very careful you can write out an explicit Godel sentence, like what the Lawvere fixed point theorem would provide. I'm sort of curious what it would look like, rather than your recipe for how to construct it. (I also wonder what the shortest Godel sentence is. But only as much as I wonder what the shortest quines are.)
> "The string corresponding to N has no proof"
Small correction: it's that "N being true is equivalent to N having no proof." If N is false, then it is provable (bad), so if things are consistent it must be true, hence unprovable. It's interesting that N is a true statement.
[1] I have a banned words list in my office; one entry is "just" because of just what it lets you sweep under the rug.
Assume the layman has been informed that first-order mathematical theories that admit of quantifier elimination (Presburger arithmetic, Euclidean geometry, real closed fields, abelian groups, random graphs, etc.) are complete and decidable.
From the layman's perspective the question then is: WHY is Peano Arithmetic incomplete? What does it add to the mix that makes it categorically different from those other axiom systems?
ENCODING power is the answer; that is, the expressive capacities of PA versus these other systems. In particular, PA is expressive enough to encode itself via Gödel numbering -- and hence construct "the Gödel sentence". Once you have the Gödel sentence, the consequences re: diagonalization/self-reference/Lawvere (depending on your background) are readily understood.
So to my mind, the layman would be more puzzled by the differing expressive powers of formal languages, and why exactly they lead to differences in provability. E.g., is the defineability of exponentiation a prerequisite to linguistic self-encoding? What's the relationship between quantifier elimination and self-reference? To what extent does a robust concept of 'infinity' play a role. Etc., etc.
From the layman's perspective the question then is: WHY is Peano Arithmetic incomplete? What does it add to the mix that makes it categorically different from those other axiom systems?
ENCODING power is the answer; that is, the expressive capacities of PA versus these other systems. In particular, PA is expressive enough to encode itself via Gödel numbering -- and hence construct "the Gödel sentence". Once you have the Gödel sentence, the consequences re: diagonalization/self-reference/Lawvere (depending on your background) are readily understood.
So to my mind, the layman would be more puzzled by the differing expressive powers of formal languages, and why exactly they lead to differences in provability. E.g., is the defineability of exponentiation a prerequisite to linguistic self-encoding? What's the relationship between quantifier elimination and self-reference? To what extent does a robust concept of 'infinity' play a role. Etc., etc.
A similar question is why are some Turing machines universal and some aren't? Or, more generally, why can you prove some Turing machines halt on all inputs and for some you cannot?
I think what you mean by "encoding" is what I mean by "being able to write an interpreter." It's not hard to encode mathematical statements as real numbers in the axioms of a real closed field, which someone outside the theory is easily able to decode. However, the fact the theory is complete implies there is no way to write an interpreter within the theory.
There are other kinds of interpreters you might be interested in. For example, one that determines absolute truth of a statement, that is, the truth of the statement in the "Platonic universe," whether or not it is provable. You can still apply the usual kind of argument, if such an interpreter existed, to generate a sentence that is true iff it is false.
I imagine a heuristic sort of issue is that to write such an interpreter you need to be able to encode environments (like in a Scheme interpreter), but the set of possible environments is too big in a Russell's paradox sort of way. In model theory, they call such a function, when restricted to a particular model, a truth term.
> expressive enough to encode itself via Gödel numbering -- and hence construct "the Gödel sentence". Once you have the Gödel sentence, the consequences re: diagonalization [...] are readily understood
I don't really understand you here: a diagonalization/Lawvere-like argument is how the Gödel sentence is constructed in the first place.
I think what you mean by "encoding" is what I mean by "being able to write an interpreter." It's not hard to encode mathematical statements as real numbers in the axioms of a real closed field, which someone outside the theory is easily able to decode. However, the fact the theory is complete implies there is no way to write an interpreter within the theory.
There are other kinds of interpreters you might be interested in. For example, one that determines absolute truth of a statement, that is, the truth of the statement in the "Platonic universe," whether or not it is provable. You can still apply the usual kind of argument, if such an interpreter existed, to generate a sentence that is true iff it is false.
I imagine a heuristic sort of issue is that to write such an interpreter you need to be able to encode environments (like in a Scheme interpreter), but the set of possible environments is too big in a Russell's paradox sort of way. In model theory, they call such a function, when restricted to a particular model, a truth term.
> expressive enough to encode itself via Gödel numbering -- and hence construct "the Gödel sentence". Once you have the Gödel sentence, the consequences re: diagonalization [...] are readily understood
I don't really understand you here: a diagonalization/Lawvere-like argument is how the Gödel sentence is constructed in the first place.
Encoding is an answer; Goedel's work uses self-encoding to establishes the existence of statements that cannot be derived from existing axioms, but do not conflict with them. That doesn't seem to rule out the possibility of some "organic" way of obtaining such axioms.
That is one of the most insightful and thought-provoking comments I have ever seen anywhere on any topic. Welcome to HN, charlie298436! I hope we see more of you.
Gödel’s Proof, by Nagel & Newman gives a good explanation for the semi-layman or undergrad coming across this for the first time.
Before picking up this book as an undergrad in pure maths, I still had romantic ideas about a separate platonic universe and the divine authority of mathematics to explain all human thought.
This book, along with studying the various geometries, each with a different choice of axioms not necessarily based in ‘reality’, destroyed the majority of that romance.
Before picking up this book as an undergrad in pure maths, I still had romantic ideas about a separate platonic universe and the divine authority of mathematics to explain all human thought.
This book, along with studying the various geometries, each with a different choice of axioms not necessarily based in ‘reality’, destroyed the majority of that romance.
Godel was himself a Platonist and didn't view incompleteness as a refutation of Platonism, rather as a restriction on the avenues of human access to mathematical truth.
I don't view it is a refutation either. I meant that the proof destroyed the greater feeling of romance I had towards mathematics.
Reading it now and enjoying it a lot. It's destroying one romance in favor of another!
Exactly! The beauty of life is in its flaws and limitations. Perfection is boring. Gödel opened the door to a multiverse of mathematics, all flawed in some way, yet not unworthy of study.
Mathematicians of the past sought perfection for the glory of God. Now we have the opportunity to give credit where it’s due: to our fellow human beings, many of whom devoted their lives to the craft of mathematics.
Mathematicians of the past sought perfection for the glory of God. Now we have the opportunity to give credit where it’s due: to our fellow human beings, many of whom devoted their lives to the craft of mathematics.
Gödel's work actually echoes Christianity quite deeply. A key theme of Christianity is that humans are incapable of being good (much less of achieving perfection) on their own strength--no more than Hilbert could axiomatize all of mathematics with a consistent, computable set of axioms.
"Do not be overly righteous, and do not make yourself too wise." (Ecclesiastes 7:16)
"There is no distinction, for all have sinned and fall short of the glory of God, and are justified freely by His grace through the redemption that is in Christ Jesus." (Romans 3:22-23)
"Do not be overly righteous, and do not make yourself too wise." (Ecclesiastes 7:16)
"There is no distinction, for all have sinned and fall short of the glory of God, and are justified freely by His grace through the redemption that is in Christ Jesus." (Romans 3:22-23)
It would be interesting to see an analysis where the most fundamental results in mathematics are looked at under the light of their discoverers' ideological beliefs and psychologies.
I wonder whether Gödel would have pursued the Proof if he did not believe in an omnipotent god.
I wonder whether Gödel would have pursued the Proof if he did not believe in an omnipotent god.
To echo this, Godel was influenced by Cantor and Leibniz, both definitive Christian theists. Godel himself was also a theist.
Cantor believed that he had been chosen as a messenger by God to be the recipient of what was to become set theory.
Cantor believed that he had been chosen as a messenger by God to be the recipient of what was to become set theory.
[deleted]
[deleted]
For me the easiest way to prove Gödel first's with perfect rigor, without bothering with numberings (but using computational undecidability) is here http://users.utu.fi/jkari/automata/fullnotes.pdf (Section 4.10)
You can access directly the relevant section[1] using the `#page=` directive. See here[2] for a full list of parameters you can use.
[1] http://users.utu.fi/jkari/automata/fullnotes.pdf#page=134
[2] https://www.adobe.com/content/dam/acom/en/devnet/acrobat/pdf...
[1] http://users.utu.fi/jkari/automata/fullnotes.pdf#page=134
[2] https://www.adobe.com/content/dam/acom/en/devnet/acrobat/pdf...
My favourite proof of the (Second) Incompleteness Theorem is the semantic proof due to Jech/Woodin: https://andrescaicedo.files.wordpress.com/2010/11/2ndincompl...
It is easiest to think about in terms of set theory, but it is possible to formalize it in a fragment of second-order arithmetic that is conservative over PA (and this conservativity is provable in PA itself). The beauty of this proof is that it first establishes semantic incompleteness without formalizing a proof system; the connection to syntactic incompleteness only uses the Completeness Theorem, which is of independent interest.
It is easiest to think about in terms of set theory, but it is possible to formalize it in a fragment of second-order arithmetic that is conservative over PA (and this conservativity is provable in PA itself). The beauty of this proof is that it first establishes semantic incompleteness without formalizing a proof system; the connection to syntactic incompleteness only uses the Completeness Theorem, which is of independent interest.
Is this a correct (over)simplification of the theory: there’s not enough information in a system that on its own can describe it’s correctness?
I know this is a very naive and maybe incorrect interpretation of it, but I think this theorem is so important in so many ways, it should be used more in layman’s discussions, even though I understand that it’s easy to misuse it etc.
The result in the Medium article applies only to a theory whose theorems are computationally enumerable. In computer science, we need theories that axiomatize subject matter such as natural numbers and computation up to a unique isomorphism so that the objects being axiomatized are characterized precisely. Such theories have induction axioms with uncountable instances. Consequently, the theories have uncountable axiom instances and their theorems cannot possibly be computationally enumerated although each proof can be computationally checked for correctness.
Therefore, a more general proof is needed to prove incompleteness. Such a proof can be found here:
https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3459566
Therefore, a more general proof is needed to prove incompleteness. Such a proof can be found here:
https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3459566
“semi” rigurously is what spooked me. The thing with Gödel’s proof is that it is very hard to do rigurously...
I went through it the first time by reading over Computability & Logic (5th edition) [1]. I'd love to go over it again, and would recommend it to anyone interested who has a few weekends to invest.
[1] https://www.goodreads.com/book/show/1556746.Computability_an...
[1] https://www.goodreads.com/book/show/1556746.Computability_an...
It's not that hard. There are several computer-checked proofs of it.
It's hard to explain, because the idea of encoding statements about a system in terms of the system itself is weird if you haven't seen it before.
It's hard to explain, because the idea of encoding statements about a system in terms of the system itself is weird if you haven't seen it before.
There are a lot of details that are needed in the proof. You need to define a first order logic and prove arithmetic theorems on top of PA to even start a rigorous proof.
That said it can be fully covered in a single semester of undergraduate study, so its not that hard. There are many theorems that couldn't be fully proved in a semester.
That said it can be fully covered in a single semester of undergraduate study, so its not that hard. There are many theorems that couldn't be fully proved in a semester.
There are many true theorems that couldn’t be fully proved ;)
Prove it!
Ok:
"this sentence is unprovably true".
Or Pinocchio saying:
“My nose will get longer”
“My nose will get longer”
There's another paper called "Incompleteness Ex Machina" with several proofs of both the first and second incompleteness theorems.
https://arxiv.org/abs/1909.04569
https://arxiv.org/abs/1909.04569
The article claims, "Given that some sets of strings are decidable, it stands to reason that other sets of strings are not. "
How can a string not be decidable?! Just search for the string in the set. It is either there, or not there.
What an I missing?
How can a string not be decidable?! Just search for the string in the set. It is either there, or not there.
What an I missing?
You can have a infinite set of finite strings, for example {“1”, “11”, “111”, “1111”, “11111”, “111111”, “1111111”, “11111111”, ...}
Is having an infinite amount of strings the only reason for the claim?
Infinity breaks a lot of things. Infinity isn't even real. So I'm not sure this counts. It seems like the article would have mentioned infinity if that were the reason for the claim. It seems like Enumeration fails for an infinite set too.
Infinity breaks a lot of things. Infinity isn't even real. So I'm not sure this counts. It seems like the article would have mentioned infinity if that were the reason for the claim. It seems like Enumeration fails for an infinite set too.
Infinity is the only reason: all finite sets of strings are decidable, simply because you can just keep a list and see if a string is in there. Important to mention that there are decidable infinite sets of strings. For instance, deciding whether a string contains only ones is easy, even though there are infinitely many such strings and you couldn’t write all of them down.
A lot of these ideas don’t require any actual “realized” infinity, however. For instance, there are infinitely many natural numbers, but natural numbers themselves are still finite. You can write a program that prints every number at some time in the nearby future (ignoring physical constraints), even though there is no point in time where it will have printed all numbers.
If you want to take away infinity, you have to draw an arbitrary upper bound somewhere, since unbounded things are infinite. Drawing that line is fairly arbitrary since there is no reason why things should no longer work if you add just one more.
A lot of these ideas don’t require any actual “realized” infinity, however. For instance, there are infinitely many natural numbers, but natural numbers themselves are still finite. You can write a program that prints every number at some time in the nearby future (ignoring physical constraints), even though there is no point in time where it will have printed all numbers.
If you want to take away infinity, you have to draw an arbitrary upper bound somewhere, since unbounded things are infinite. Drawing that line is fairly arbitrary since there is no reason why things should no longer work if you add just one more.
Did Godel say infinity is the reason too?
Thanks for the response, I don't remember reading about infinity being the reason.
Off topic: Still, you'd run out of matter in the universe (that you could use for ink), before you wrote down a finite amount of numbers while ever reaching a percentage of infinity. That's how unreal infinity is in my mind.
I know the concept of infinity is useful in math, and in this incompleteness theorem, it seems like infinity is the very reason not all truths are provable. But I thought Godel's incompleteness theorem would apply to physical reality, but since infinity doesn't exist in physical reality, I'm not sure the incompleteness theorem would apply to physical reality. Hmmm
Also, didn't Godel show his theorem to be informally true by stating, "This sentence is inprovably true."? There was no infinity invoked in that sentence.
Off topic: Still, you'd run out of matter in the universe (that you could use for ink), before you wrote down a finite amount of numbers while ever reaching a percentage of infinity. That's how unreal infinity is in my mind.
I know the concept of infinity is useful in math, and in this incompleteness theorem, it seems like infinity is the very reason not all truths are provable. But I thought Godel's incompleteness theorem would apply to physical reality, but since infinity doesn't exist in physical reality, I'm not sure the incompleteness theorem would apply to physical reality. Hmmm
Also, didn't Godel show his theorem to be informally true by stating, "This sentence is inprovably true."? There was no infinity invoked in that sentence.
Diagonalization arguments (which are used in Gödel's theorem) do require some infinity.
If there were only a finite number of such "True, but unprovable using your current proof rules" sentences, then you could simply add those sentences to your list of proof rules and there would be nothing "True, but unprovable" anymore. For Gödel's theorem to work, you need at least an infinite supply of those kinds of sentences.
Also here there's no need to actually write down all of them exhaustively. It's just important to be able to find "yet another one" whenever you would like to, which requires an inexhaustible supply.
If there were only a finite number of such "True, but unprovable using your current proof rules" sentences, then you could simply add those sentences to your list of proof rules and there would be nothing "True, but unprovable" anymore. For Gödel's theorem to work, you need at least an infinite supply of those kinds of sentences.
Also here there's no need to actually write down all of them exhaustively. It's just important to be able to find "yet another one" whenever you would like to, which requires an inexhaustible supply.
"which requires an inexhaustible supply. "
But this is how you can stress the theorem. I know it will take a long time, so consider a universe where only 1000 bits of matter actually exist, then try to use the theorem and you won't have enough ink to even hold the theorem, and sets in memory. It's the same for our universe, just with more bits.
"you could simply add those sentences to your list of proof rules " Thanks, for responding. Do you mean axioms? I don't understand why that would be a solution. I'll have to read Godel again.
But this is how you can stress the theorem. I know it will take a long time, so consider a universe where only 1000 bits of matter actually exist, then try to use the theorem and you won't have enough ink to even hold the theorem, and sets in memory. It's the same for our universe, just with more bits.
"you could simply add those sentences to your list of proof rules " Thanks, for responding. Do you mean axioms? I don't understand why that would be a solution. I'll have to read Godel again.
Yes, strictly speaking that's true, but then if the universe were slightly bigger, or you used a different encoding, you'd get different results. It feels kind of arbitrary to stop thinking about what would happen if the universe contained just one more bit.
Philosophically, I think it's also more interesting that Gödel's theorem would continue to produce such sentences, regardless of how large our universe happens to be. You could never have a universe that is so big that it could contain all Gödel sentences, even if our universe were bigger. This is a much more fundamental limitation.
Gödel's theorem gives you a sentence S where you can prove neither S nor its negation from the current axioms P. Of course, if you then add S (or its negation) as an axiom, then you CAN prove it. But then Gödel's theorem will just give you another sentence S', ad infinitum. You can never win this game.
Philosophically, I think it's also more interesting that Gödel's theorem would continue to produce such sentences, regardless of how large our universe happens to be. You could never have a universe that is so big that it could contain all Gödel sentences, even if our universe were bigger. This is a much more fundamental limitation.
Gödel's theorem gives you a sentence S where you can prove neither S nor its negation from the current axioms P. Of course, if you then add S (or its negation) as an axiom, then you CAN prove it. But then Gödel's theorem will just give you another sentence S', ad infinitum. You can never win this game.