Mixing
Is Gödel's incompleteness theorem provable without any model-theoretic notion?
$begingroup$
The entry on Gödel's incompletenss theorem in Wikipedia says:
Any effectively generated theory capable of expressing elementary arithmetic cannot be both consistent and complete. In particular, for any consistent, effectively generated formal theory that proves certain basic arithmetic truths, there is an arithmetical statement that is true,[1] but not provable in the theory (Kleene 1967, p. 250).
My understanding of Gödel's theorem derived from the proof sketch in the article above is that it is completely formal (axioms+logical axioms+inference rules) and does not rely on any model-theoretic notion where truth is established (a formal sentence being true iff every interpretation of it in every model is true).
But is this correct, that is are there proofs that use the apparatus of logic but do not not use any model theory at all? One piece of evidence that they must is that the quote above says that a statement is true but not proveable, and truth is a model-theoretic notion, unless of course there is a notion of truth different from model-theoretic truth?
EDIT
There is a very similar question here.
From the answer there one notices that 'true' is taken in the standard model of the integers. This is not the same as the model-theoretic notion of true taken above.
So, the question is refined to can we dispense with this restricted notion of truth and make the proof completely formal?
logic model-theory incompleteness
edited Apr 13 '17 at 12:21
Community♦
1
asked Jun 14 '13 at 21:16
Mozibur UllahMozibur Ullah
2,7291129
$endgroup$
add a comment |
$begingroup$
The entry on Gödel's incompletenss theorem in Wikipedia says:
Any effectively generated theory capable of expressing elementary arithmetic cannot be both consistent and complete. In particular, for any consistent, effectively generated formal theory that proves certain basic arithmetic truths, there is an arithmetical statement that is true,[1] but not provable in the theory (Kleene 1967, p. 250).
My understanding of Gödel's theorem derived from the proof sketch in the article above is that it is completely formal (axioms+logical axioms+inference rules) and does not rely on any model-theoretic notion where truth is established (a formal sentence being true iff every interpretation of it in every model is true).
But is this correct, that is are there proofs that use the apparatus of logic but do not not use any model theory at all? One piece of evidence that they must is that the quote above says that a statement is true but not proveable, and truth is a model-theoretic notion, unless of course there is a notion of truth different from model-theoretic truth?
EDIT
There is a very similar question here.
From the answer there one notices that 'true' is taken in the standard model of the integers. This is not the same as the model-theoretic notion of true taken above.
So, the question is refined to can we dispense with this restricted notion of truth and make the proof completely formal?
logic model-theory incompleteness
edited Apr 13 '17 at 12:21
Community♦
1
asked Jun 14 '13 at 21:16
Mozibur UllahMozibur Ullah
2,7291129
$endgroup$
$begingroup$
One just omits the "basic arithmetical truths" part, and shows that any consistent r.e. extension of say PA, (or something far weaker) is incomplete.
$endgroup$
– André Nicolas
Jun 14 '13 at 21:23
4
$begingroup$
After all one shows that there is some $Phi$ such that $Phi(lceil nrceil)$ is provable for all $n$, but $forall n:Phi(n)$ is not provable. This does not need models, only considering proofs syntactically.
$endgroup$
– Hagen von Eitzen
Jun 14 '13 at 21:28
$begingroup$
Aside: the informal usage of "true" squashes together a number of different concepts that one often doesn't care to distinguish. But in a context like this, doing that means we misunderstand all of the subtleties of the issue! In my opinion, the word "true" and its derivatives should be avoided entirely, except in the special case where the top element of a boolean algebra actually appears in a mathematical equation and needs to be named.
$endgroup$
– Hurkyl
Dec 20 '17 at 21:55
$begingroup$
For future readers, note that the mistake in this question is the failure to properly distinguish between the meta-system MS and the formal system being studied within MS. MS itself can be formalized, so the incompleteness theorems can be completely formalized. This has nothing to do with truth. At the same time, those theorems as stated and proven in MS of course talk about arithmetical truths, which are sentences that hold in some particular model of PA that MS proves or assumes to exist. But naturals cannot be absolutely pinned down.
$endgroup$
– user21820
Dec 12 '18 at 13:26
add a comment |
$begingroup$
The entry on Gödel's incompletenss theorem in Wikipedia says:
Any effectively generated theory capable of expressing elementary arithmetic cannot be both consistent and complete. In particular, for any consistent, effectively generated formal theory that proves certain basic arithmetic truths, there is an arithmetical statement that is true,[1] but not provable in the theory (Kleene 1967, p. 250).
My understanding of Gödel's theorem derived from the proof sketch in the article above is that it is completely formal (axioms+logical axioms+inference rules) and does not rely on any model-theoretic notion where truth is established (a formal sentence being true iff every interpretation of it in every model is true).
But is this correct, that is are there proofs that use the apparatus of logic but do not not use any model theory at all? One piece of evidence that they must is that the quote above says that a statement is true but not proveable, and truth is a model-theoretic notion, unless of course there is a notion of truth different from model-theoretic truth?
EDIT
There is a very similar question here.
From the answer there one notices that 'true' is taken in the standard model of the integers. This is not the same as the model-theoretic notion of true taken above.
So, the question is refined to can we dispense with this restricted notion of truth and make the proof completely formal?
logic model-theory incompleteness
edited Apr 13 '17 at 12:21
Community♦
1
asked Jun 14 '13 at 21:16
Mozibur UllahMozibur Ullah
2,7291129
$endgroup$
The entry on Gödel's incompletenss theorem in Wikipedia says:
Any effectively generated theory capable of expressing elementary arithmetic cannot be both consistent and complete. In particular, for any consistent, effectively generated formal theory that proves certain basic arithmetic truths, there is an arithmetical statement that is true,[1] but not provable in the theory (Kleene 1967, p. 250).
My understanding of Gödel's theorem derived from the proof sketch in the article above is that it is completely formal (axioms+logical axioms+inference rules) and does not rely on any model-theoretic notion where truth is established (a formal sentence being true iff every interpretation of it in every model is true).
But is this correct, that is are there proofs that use the apparatus of logic but do not not use any model theory at all? One piece of evidence that they must is that the quote above says that a statement is true but not proveable, and truth is a model-theoretic notion, unless of course there is a notion of truth different from model-theoretic truth?
EDIT
There is a very similar question here.
From the answer there one notices that 'true' is taken in the standard model of the integers. This is not the same as the model-theoretic notion of true taken above.
So, the question is refined to can we dispense with this restricted notion of truth and make the proof completely formal?
logic model-theory incompleteness
logic model-theory incompleteness
edited Apr 13 '17 at 12:21
Community♦
1
asked Jun 14 '13 at 21:16
Mozibur UllahMozibur Ullah
2,7291129
edited Apr 13 '17 at 12:21
Community♦
1
asked Jun 14 '13 at 21:16
Mozibur UllahMozibur Ullah
2,7291129
edited Apr 13 '17 at 12:21
Community♦
1
edited Apr 13 '17 at 12:21
Community♦
1
edited Apr 13 '17 at 12:21
Community♦
1
1
asked Jun 14 '13 at 21:16
Mozibur UllahMozibur Ullah
2,7291129
asked Jun 14 '13 at 21:16
Mozibur UllahMozibur Ullah
2,7291129
asked Jun 14 '13 at 21:16
Mozibur UllahMozibur Ullah
2,7291129
2,7291129
$begingroup$
One just omits the "basic arithmetical truths" part, and shows that any consistent r.e. extension of say PA, (or something far weaker) is incomplete.
$endgroup$
– André Nicolas
Jun 14 '13 at 21:23
4
$begingroup$
After all one shows that there is some $Phi$ such that $Phi(lceil nrceil)$ is provable for all $n$, but $forall n:Phi(n)$ is not provable. This does not need models, only considering proofs syntactically.
$endgroup$
– Hagen von Eitzen
Jun 14 '13 at 21:28
$begingroup$
Aside: the informal usage of "true" squashes together a number of different concepts that one often doesn't care to distinguish. But in a context like this, doing that means we misunderstand all of the subtleties of the issue! In my opinion, the word "true" and its derivatives should be avoided entirely, except in the special case where the top element of a boolean algebra actually appears in a mathematical equation and needs to be named.
$endgroup$
– Hurkyl
Dec 20 '17 at 21:55
$begingroup$
For future readers, note that the mistake in this question is the failure to properly distinguish between the meta-system MS and the formal system being studied within MS. MS itself can be formalized, so the incompleteness theorems can be completely formalized. This has nothing to do with truth. At the same time, those theorems as stated and proven in MS of course talk about arithmetical truths, which are sentences that hold in some particular model of PA that MS proves or assumes to exist. But naturals cannot be absolutely pinned down.
$endgroup$
– user21820
Dec 12 '18 at 13:26
add a comment |
$begingroup$
One just omits the "basic arithmetical truths" part, and shows that any consistent r.e. extension of say PA, (or something far weaker) is incomplete.
$endgroup$
– André Nicolas
Jun 14 '13 at 21:23
4
$begingroup$
After all one shows that there is some $Phi$ such that $Phi(lceil nrceil)$ is provable for all $n$, but $forall n:Phi(n)$ is not provable. This does not need models, only considering proofs syntactically.
$endgroup$
– Hagen von Eitzen
Jun 14 '13 at 21:28
$begingroup$
Aside: the informal usage of "true" squashes together a number of different concepts that one often doesn't care to distinguish. But in a context like this, doing that means we misunderstand all of the subtleties of the issue! In my opinion, the word "true" and its derivatives should be avoided entirely, except in the special case where the top element of a boolean algebra actually appears in a mathematical equation and needs to be named.
$endgroup$
– Hurkyl
Dec 20 '17 at 21:55
$begingroup$
For future readers, note that the mistake in this question is the failure to properly distinguish between the meta-system MS and the formal system being studied within MS. MS itself can be formalized, so the incompleteness theorems can be completely formalized. This has nothing to do with truth. At the same time, those theorems as stated and proven in MS of course talk about arithmetical truths, which are sentences that hold in some particular model of PA that MS proves or assumes to exist. But naturals cannot be absolutely pinned down.
$endgroup$
– user21820
Dec 12 '18 at 13:26
$begingroup$
One just omits the "basic arithmetical truths" part, and shows that any consistent r.e. extension of say PA, (or something far weaker) is incomplete.
$endgroup$
– André Nicolas
Jun 14 '13 at 21:23
$begingroup$
One just omits the "basic arithmetical truths" part, and shows that any consistent r.e. extension of say PA, (or something far weaker) is incomplete.
$endgroup$
– André Nicolas
Jun 14 '13 at 21:23
4
4
$begingroup$
After all one shows that there is some $Phi$ such that $Phi(lceil nrceil)$ is provable for all $n$, but $forall n:Phi(n)$ is not provable. This does not need models, only considering proofs syntactically.
$endgroup$
– Hagen von Eitzen
Jun 14 '13 at 21:28
$begingroup$
After all one shows that there is some $Phi$ such that $Phi(lceil nrceil)$ is provable for all $n$, but $forall n:Phi(n)$ is not provable. This does not need models, only considering proofs syntactically.
$endgroup$
– Hagen von Eitzen
Jun 14 '13 at 21:28
$begingroup$
Aside: the informal usage of "true" squashes together a number of different concepts that one often doesn't care to distinguish. But in a context like this, doing that means we misunderstand all of the subtleties of the issue! In my opinion, the word "true" and its derivatives should be avoided entirely, except in the special case where the top element of a boolean algebra actually appears in a mathematical equation and needs to be named.
$endgroup$
– Hurkyl
Dec 20 '17 at 21:55
$begingroup$
Aside: the informal usage of "true" squashes together a number of different concepts that one often doesn't care to distinguish. But in a context like this, doing that means we misunderstand all of the subtleties of the issue! In my opinion, the word "true" and its derivatives should be avoided entirely, except in the special case where the top element of a boolean algebra actually appears in a mathematical equation and needs to be named.
$endgroup$
– Hurkyl
Dec 20 '17 at 21:55
$begingroup$
For future readers, note that the mistake in this question is the failure to properly distinguish between the meta-system MS and the formal system being studied within MS. MS itself can be formalized, so the incompleteness theorems can be completely formalized. This has nothing to do with truth. At the same time, those theorems as stated and proven in MS of course talk about arithmetical truths, which are sentences that hold in some particular model of PA that MS proves or assumes to exist. But naturals cannot be absolutely pinned down.
$endgroup$
– user21820
Dec 12 '18 at 13:26
$begingroup$
For future readers, note that the mistake in this question is the failure to properly distinguish between the meta-system MS and the formal system being studied within MS. MS itself can be formalized, so the incompleteness theorems can be completely formalized. This has nothing to do with truth. At the same time, those theorems as stated and proven in MS of course talk about arithmetical truths, which are sentences that hold in some particular model of PA that MS proves or assumes to exist. But naturals cannot be absolutely pinned down.
$endgroup$
– user21820
Dec 12 '18 at 13:26
add a comment |
2 Answers
2
active
oldest
votes
$begingroup$
"A formal sentence being true iff every interpretation of it in every model is true". Not so. A sentence of formal arithmetic may be true on the intended, standard, interpretation while not a logical truth, not true on every interpretation.
"Gödel's theorem is completely formal." Not so. The theorem is a bit of ordinary informal mathematics. Its subject-matter is formal proofs in certain kinds of formal theories. But Gödel's theorem is a meta-result about those formal theories, and the usual proofs involve ordinary mathematical reasoning. [I say "ordinary" proofs because there have been projects to produce formal computer verifications of Gödel's theorem: but the theorem pre-dated the formal verifications by decades. And it is a nice question what we learn from having a formal proof in Coq, for example, all 37906 lines of it.]
"Gödel's theorem does not rely on any model-theoretic notion." Actually as perhaps Mostowski was the first to make really clear in his exposition, sixty years ago, there are two different versions of the first theorem, one that presupposes that we are dealing with a sound theory, another that assumes only that we are dealing with an [omega]-consistent theory. These are often referred to as the semantic vs the syntactic versions of the theorem. The semantic version, unsurprisingly, does rely on semantic notions.
"Are there proofs that use the apparatus of logic but do not not use any model theory at all?" Yes, some results, including the syntactic version of Gödel's first theorem, are purely proof-theoretic, i.e. about syntax. But again note that a theorem's being about syntax doesn't itself make it "completely formal". (For another example, proofs about the normalizability of formal natural deduction proofs in first-order logic are themselves bits of informal mathematics.)
answered Jun 14 '13 at 21:37
Peter SmithPeter Smith
40.6k340120
$endgroup$
$begingroup$
Does the semantic version of the theory use logical truth or just in the standard model? I assume this means that the model isn't categorial so we're using higher order logic.
$endgroup$
– Mozibur Ullah
Jun 14 '13 at 21:55
$begingroup$
The main benefit I see of the proof in Coq, although it is quite long, is that it helps reduce any worries about the second incompleteness theorem, of which part of the proof is famously "left as an exercise" in textbooks. However, the fact that the incompleteness theorems can be formalized in PRA is more important, because it shows that the incompleteness theorems are finitistically provable.
$endgroup$
– Carl Mummert
Jun 14 '13 at 23:10
$begingroup$
"Beware of bugs in the above code; I have only proved it correct, not tried it." — Donald Knuth Humans are not as good at spotting small errors as computers are.
$endgroup$
– dfeuer
Jun 14 '13 at 23:17
1
$begingroup$
Your formulation of the second point is interesting: Don't you consider the computer version, which came decades later, to be extensionally :) equivalent to Gödels theorem? Once it's formalized in some way, wouldn't you say Gödels theorem is fully formal as such?
$endgroup$
– Nikolaj-K
Jun 14 '13 at 23:40
1
$begingroup$
@NickKidman I'd prefer to say that Gödel's theorem is formalizable.
$endgroup$
– Peter Smith
Jun 15 '13 at 8:37
|
show 1 more comment
$begingroup$
Although it is not usually presented this way, the usual proof of the incompleteness theorem shows the following:
For any sufficiently strong effective theory $T$ of arithmetic, with Gödel-Rosser sentence $G$, there is an algorithm that will take any proof of $G$ within $T$ and turn it into a proof of $0=1$ within $T$, and there is an algorithm that will take a proof of the negation of $G$ within $T$ and turn it into a proof of $0=1$ within $T$.
This has the immediate corollary:
For any sufficiently strong effective theory $T$ of arithmetic, with Gödel-Rosser sentence $G$, if $T$ does not prove $0=1$ then $T$ does not prove $G$ and $T$ does not prove the negation of $G$.
Neither of these statements, nor their proofs, requires any model theory.
However, these syntactic statements leave open the question of whether $G$ is actually true. It's one thing to know that there is some sentence that is neither provable nor disprovable, but either $G$ or its negation has to be true as a statement about natural numbers, and it would be nice to know which one it is. The answer is that $G$ is true, rather than the negation of $G$.
answered Jun 14 '13 at 23:05
Carl MummertCarl Mummert
66.6k7132248
$endgroup$
$begingroup$
The first indented statement may seem somewhat weak, because we could just search for the proof of $0=1$ if it exists. But, if we add the fact that the proof of the incompleteness theorem establishes that the algorithm is given by a primitive recursive function, that removes any vacuousness.
$endgroup$
– Carl Mummert
Jun 14 '13 at 23:13
$begingroup$
'neither of these statements or their proofs don't require model theory' - does this include interpretation in the standard model of the integers N? To tally with Peter Smiths answer (that there are two proofs - sound & syntactic) is the proof you're considering use omega-consistency?
$endgroup$
– Mozibur Ullah
Jun 14 '13 at 23:14
$begingroup$
No, no model theory at all is required for that, and there is no need to mention the standard model. The proof shows that there is a fixed algorithm that, solely by syntactic manipulation of formulas and proofs, will take a proof of $G$ and turn it into a proof of $0=1$. But the cost of this is that you lose part of the conclusion.
$endgroup$
– Carl Mummert
Jun 14 '13 at 23:15
2
$begingroup$
No, the theorem can be proved entirely syntactically, as I keep saying.
$endgroup$
– Carl Mummert
Jun 14 '13 at 23:37
1
$begingroup$
I'm trying to understand what you mean by saying 'these syntactic statements leave open the question of whether G is actually true' which implies that truth isn't something that is captured purely syntactically, and your explanation showed 'there is some sentence that is neither provable nor disprovable'. But you finally assert that 'The answer is that G is true'. Now when truth is mentioned I usually think of model interpretation. Obviously after your comments that can't be correct. So what notion of truth are you using in your last statement?
$endgroup$
– Mozibur Ullah
Jun 14 '13 at 23:53
|
show 8 more comments
Your Answer
StackExchange.ifUsing("editor", function () {
return StackExchange.using("mathjaxEditing", function () {
StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix) {
StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
});
});
}, "mathjax-editing");
StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "69"
};
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function() {
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled) {
StackExchange.using("snippets", function() {
createEditor();
});
}
else {
createEditor();
}
});
function createEditor() {
StackExchange.prepareEditor({
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
noCode: true, onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});
}
});
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f420574%2fis-g%25c3%25b6dels-incompleteness-theorem-provable-without-any-model-theoretic-notion%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
2 Answers
2
active
oldest
votes
2 Answers
2
active
oldest
votes
active
oldest
votes
active
oldest
votes
$begingroup$
"A formal sentence being true iff every interpretation of it in every model is true". Not so. A sentence of formal arithmetic may be true on the intended, standard, interpretation while not a logical truth, not true on every interpretation.
"Gödel's theorem is completely formal." Not so. The theorem is a bit of ordinary informal mathematics. Its subject-matter is formal proofs in certain kinds of formal theories. But Gödel's theorem is a meta-result about those formal theories, and the usual proofs involve ordinary mathematical reasoning. [I say "ordinary" proofs because there have been projects to produce formal computer verifications of Gödel's theorem: but the theorem pre-dated the formal verifications by decades. And it is a nice question what we learn from having a formal proof in Coq, for example, all 37906 lines of it.]
"Gödel's theorem does not rely on any model-theoretic notion." Actually as perhaps Mostowski was the first to make really clear in his exposition, sixty years ago, there are two different versions of the first theorem, one that presupposes that we are dealing with a sound theory, another that assumes only that we are dealing with an [omega]-consistent theory. These are often referred to as the semantic vs the syntactic versions of the theorem. The semantic version, unsurprisingly, does rely on semantic notions.
"Are there proofs that use the apparatus of logic but do not not use any model theory at all?" Yes, some results, including the syntactic version of Gödel's first theorem, are purely proof-theoretic, i.e. about syntax. But again note that a theorem's being about syntax doesn't itself make it "completely formal". (For another example, proofs about the normalizability of formal natural deduction proofs in first-order logic are themselves bits of informal mathematics.)
answered Jun 14 '13 at 21:37
Peter SmithPeter Smith
40.6k340120
$endgroup$
$begingroup$
Does the semantic version of the theory use logical truth or just in the standard model? I assume this means that the model isn't categorial so we're using higher order logic.
$endgroup$
– Mozibur Ullah
Jun 14 '13 at 21:55
$begingroup$
The main benefit I see of the proof in Coq, although it is quite long, is that it helps reduce any worries about the second incompleteness theorem, of which part of the proof is famously "left as an exercise" in textbooks. However, the fact that the incompleteness theorems can be formalized in PRA is more important, because it shows that the incompleteness theorems are finitistically provable.
$endgroup$
– Carl Mummert
Jun 14 '13 at 23:10
$begingroup$
"Beware of bugs in the above code; I have only proved it correct, not tried it." — Donald Knuth Humans are not as good at spotting small errors as computers are.
$endgroup$
– dfeuer
Jun 14 '13 at 23:17
1
$begingroup$
Your formulation of the second point is interesting: Don't you consider the computer version, which came decades later, to be extensionally :) equivalent to Gödels theorem? Once it's formalized in some way, wouldn't you say Gödels theorem is fully formal as such?
$endgroup$
– Nikolaj-K
Jun 14 '13 at 23:40
1
$begingroup$
@NickKidman I'd prefer to say that Gödel's theorem is formalizable.
$endgroup$
– Peter Smith
Jun 15 '13 at 8:37
|
show 1 more comment
$begingroup$
"A formal sentence being true iff every interpretation of it in every model is true". Not so. A sentence of formal arithmetic may be true on the intended, standard, interpretation while not a logical truth, not true on every interpretation.
"Gödel's theorem is completely formal." Not so. The theorem is a bit of ordinary informal mathematics. Its subject-matter is formal proofs in certain kinds of formal theories. But Gödel's theorem is a meta-result about those formal theories, and the usual proofs involve ordinary mathematical reasoning. [I say "ordinary" proofs because there have been projects to produce formal computer verifications of Gödel's theorem: but the theorem pre-dated the formal verifications by decades. And it is a nice question what we learn from having a formal proof in Coq, for example, all 37906 lines of it.]
"Gödel's theorem does not rely on any model-theoretic notion." Actually as perhaps Mostowski was the first to make really clear in his exposition, sixty years ago, there are two different versions of the first theorem, one that presupposes that we are dealing with a sound theory, another that assumes only that we are dealing with an [omega]-consistent theory. These are often referred to as the semantic vs the syntactic versions of the theorem. The semantic version, unsurprisingly, does rely on semantic notions.
"Are there proofs that use the apparatus of logic but do not not use any model theory at all?" Yes, some results, including the syntactic version of Gödel's first theorem, are purely proof-theoretic, i.e. about syntax. But again note that a theorem's being about syntax doesn't itself make it "completely formal". (For another example, proofs about the normalizability of formal natural deduction proofs in first-order logic are themselves bits of informal mathematics.)
answered Jun 14 '13 at 21:37
Peter SmithPeter Smith
40.6k340120
$endgroup$
$begingroup$
Does the semantic version of the theory use logical truth or just in the standard model? I assume this means that the model isn't categorial so we're using higher order logic.
$endgroup$
– Mozibur Ullah
Jun 14 '13 at 21:55
$begingroup$
The main benefit I see of the proof in Coq, although it is quite long, is that it helps reduce any worries about the second incompleteness theorem, of which part of the proof is famously "left as an exercise" in textbooks. However, the fact that the incompleteness theorems can be formalized in PRA is more important, because it shows that the incompleteness theorems are finitistically provable.
$endgroup$
– Carl Mummert
Jun 14 '13 at 23:10
$begingroup$
"Beware of bugs in the above code; I have only proved it correct, not tried it." — Donald Knuth Humans are not as good at spotting small errors as computers are.
$endgroup$
– dfeuer
Jun 14 '13 at 23:17
1
$begingroup$
Your formulation of the second point is interesting: Don't you consider the computer version, which came decades later, to be extensionally :) equivalent to Gödels theorem? Once it's formalized in some way, wouldn't you say Gödels theorem is fully formal as such?
$endgroup$
– Nikolaj-K
Jun 14 '13 at 23:40
1
$begingroup$
@NickKidman I'd prefer to say that Gödel's theorem is formalizable.
$endgroup$
– Peter Smith
Jun 15 '13 at 8:37
|
show 1 more comment
$begingroup$
"A formal sentence being true iff every interpretation of it in every model is true". Not so. A sentence of formal arithmetic may be true on the intended, standard, interpretation while not a logical truth, not true on every interpretation.
"Gödel's theorem is completely formal." Not so. The theorem is a bit of ordinary informal mathematics. Its subject-matter is formal proofs in certain kinds of formal theories. But Gödel's theorem is a meta-result about those formal theories, and the usual proofs involve ordinary mathematical reasoning. [I say "ordinary" proofs because there have been projects to produce formal computer verifications of Gödel's theorem: but the theorem pre-dated the formal verifications by decades. And it is a nice question what we learn from having a formal proof in Coq, for example, all 37906 lines of it.]
"Gödel's theorem does not rely on any model-theoretic notion." Actually as perhaps Mostowski was the first to make really clear in his exposition, sixty years ago, there are two different versions of the first theorem, one that presupposes that we are dealing with a sound theory, another that assumes only that we are dealing with an [omega]-consistent theory. These are often referred to as the semantic vs the syntactic versions of the theorem. The semantic version, unsurprisingly, does rely on semantic notions.
"Are there proofs that use the apparatus of logic but do not not use any model theory at all?" Yes, some results, including the syntactic version of Gödel's first theorem, are purely proof-theoretic, i.e. about syntax. But again note that a theorem's being about syntax doesn't itself make it "completely formal". (For another example, proofs about the normalizability of formal natural deduction proofs in first-order logic are themselves bits of informal mathematics.)
answered Jun 14 '13 at 21:37
Peter SmithPeter Smith
40.6k340120
$endgroup$
"A formal sentence being true iff every interpretation of it in every model is true". Not so. A sentence of formal arithmetic may be true on the intended, standard, interpretation while not a logical truth, not true on every interpretation.
"Gödel's theorem is completely formal." Not so. The theorem is a bit of ordinary informal mathematics. Its subject-matter is formal proofs in certain kinds of formal theories. But Gödel's theorem is a meta-result about those formal theories, and the usual proofs involve ordinary mathematical reasoning. [I say "ordinary" proofs because there have been projects to produce formal computer verifications of Gödel's theorem: but the theorem pre-dated the formal verifications by decades. And it is a nice question what we learn from having a formal proof in Coq, for example, all 37906 lines of it.]
"Gödel's theorem does not rely on any model-theoretic notion." Actually as perhaps Mostowski was the first to make really clear in his exposition, sixty years ago, there are two different versions of the first theorem, one that presupposes that we are dealing with a sound theory, another that assumes only that we are dealing with an [omega]-consistent theory. These are often referred to as the semantic vs the syntactic versions of the theorem. The semantic version, unsurprisingly, does rely on semantic notions.
"Are there proofs that use the apparatus of logic but do not not use any model theory at all?" Yes, some results, including the syntactic version of Gödel's first theorem, are purely proof-theoretic, i.e. about syntax. But again note that a theorem's being about syntax doesn't itself make it "completely formal". (For another example, proofs about the normalizability of formal natural deduction proofs in first-order logic are themselves bits of informal mathematics.)
answered Jun 14 '13 at 21:37
Peter SmithPeter Smith
40.6k340120
edited Jan 8 at 22:02
answered Jun 14 '13 at 21:37
Peter SmithPeter Smith
40.6k340120
answered Jun 14 '13 at 21:37
Peter SmithPeter Smith
40.6k340120
answered Jun 14 '13 at 21:37
Peter SmithPeter Smith
40.6k340120
40.6k340120
$begingroup$
Does the semantic version of the theory use logical truth or just in the standard model? I assume this means that the model isn't categorial so we're using higher order logic.
$endgroup$
– Mozibur Ullah
Jun 14 '13 at 21:55
$begingroup$
The main benefit I see of the proof in Coq, although it is quite long, is that it helps reduce any worries about the second incompleteness theorem, of which part of the proof is famously "left as an exercise" in textbooks. However, the fact that the incompleteness theorems can be formalized in PRA is more important, because it shows that the incompleteness theorems are finitistically provable.
$endgroup$
– Carl Mummert
Jun 14 '13 at 23:10
$begingroup$
"Beware of bugs in the above code; I have only proved it correct, not tried it." — Donald Knuth Humans are not as good at spotting small errors as computers are.
$endgroup$
– dfeuer
Jun 14 '13 at 23:17
1
$begingroup$
Your formulation of the second point is interesting: Don't you consider the computer version, which came decades later, to be extensionally :) equivalent to Gödels theorem? Once it's formalized in some way, wouldn't you say Gödels theorem is fully formal as such?
$endgroup$
– Nikolaj-K
Jun 14 '13 at 23:40
1
$begingroup$
@NickKidman I'd prefer to say that Gödel's theorem is formalizable.
$endgroup$
– Peter Smith
Jun 15 '13 at 8:37
|
show 1 more comment
$begingroup$
Does the semantic version of the theory use logical truth or just in the standard model? I assume this means that the model isn't categorial so we're using higher order logic.
$endgroup$
– Mozibur Ullah
Jun 14 '13 at 21:55
$begingroup$
The main benefit I see of the proof in Coq, although it is quite long, is that it helps reduce any worries about the second incompleteness theorem, of which part of the proof is famously "left as an exercise" in textbooks. However, the fact that the incompleteness theorems can be formalized in PRA is more important, because it shows that the incompleteness theorems are finitistically provable.
$endgroup$
– Carl Mummert
Jun 14 '13 at 23:10
$begingroup$
"Beware of bugs in the above code; I have only proved it correct, not tried it." — Donald Knuth Humans are not as good at spotting small errors as computers are.
$endgroup$
– dfeuer
Jun 14 '13 at 23:17
1
$begingroup$
Your formulation of the second point is interesting: Don't you consider the computer version, which came decades later, to be extensionally :) equivalent to Gödels theorem? Once it's formalized in some way, wouldn't you say Gödels theorem is fully formal as such?
$endgroup$
– Nikolaj-K
Jun 14 '13 at 23:40
1
$begingroup$
@NickKidman I'd prefer to say that Gödel's theorem is formalizable.
$endgroup$
– Peter Smith
Jun 15 '13 at 8:37
$begingroup$
Does the semantic version of the theory use logical truth or just in the standard model? I assume this means that the model isn't categorial so we're using higher order logic.
$endgroup$
– Mozibur Ullah
Jun 14 '13 at 21:55
$begingroup$
Does the semantic version of the theory use logical truth or just in the standard model? I assume this means that the model isn't categorial so we're using higher order logic.
$endgroup$
– Mozibur Ullah
Jun 14 '13 at 21:55
$begingroup$
The main benefit I see of the proof in Coq, although it is quite long, is that it helps reduce any worries about the second incompleteness theorem, of which part of the proof is famously "left as an exercise" in textbooks. However, the fact that the incompleteness theorems can be formalized in PRA is more important, because it shows that the incompleteness theorems are finitistically provable.
$endgroup$
– Carl Mummert
Jun 14 '13 at 23:10
$begingroup$
The main benefit I see of the proof in Coq, although it is quite long, is that it helps reduce any worries about the second incompleteness theorem, of which part of the proof is famously "left as an exercise" in textbooks. However, the fact that the incompleteness theorems can be formalized in PRA is more important, because it shows that the incompleteness theorems are finitistically provable.
$endgroup$
– Carl Mummert
Jun 14 '13 at 23:10
$begingroup$
"Beware of bugs in the above code; I have only proved it correct, not tried it." — Donald Knuth Humans are not as good at spotting small errors as computers are.
$endgroup$
– dfeuer
Jun 14 '13 at 23:17
$begingroup$
"Beware of bugs in the above code; I have only proved it correct, not tried it." — Donald Knuth Humans are not as good at spotting small errors as computers are.
$endgroup$
– dfeuer
Jun 14 '13 at 23:17
1
1
$begingroup$
Your formulation of the second point is interesting: Don't you consider the computer version, which came decades later, to be extensionally :) equivalent to Gödels theorem? Once it's formalized in some way, wouldn't you say Gödels theorem is fully formal as such?
$endgroup$
– Nikolaj-K
Jun 14 '13 at 23:40
$begingroup$
Your formulation of the second point is interesting: Don't you consider the computer version, which came decades later, to be extensionally :) equivalent to Gödels theorem? Once it's formalized in some way, wouldn't you say Gödels theorem is fully formal as such?
$endgroup$
– Nikolaj-K
Jun 14 '13 at 23:40
1
1
$begingroup$
@NickKidman I'd prefer to say that Gödel's theorem is formalizable.
$endgroup$
– Peter Smith
Jun 15 '13 at 8:37
$begingroup$
@NickKidman I'd prefer to say that Gödel's theorem is formalizable.
$endgroup$
– Peter Smith
Jun 15 '13 at 8:37
|
show 1 more comment
$begingroup$
Although it is not usually presented this way, the usual proof of the incompleteness theorem shows the following:
For any sufficiently strong effective theory $T$ of arithmetic, with Gödel-Rosser sentence $G$, there is an algorithm that will take any proof of $G$ within $T$ and turn it into a proof of $0=1$ within $T$, and there is an algorithm that will take a proof of the negation of $G$ within $T$ and turn it into a proof of $0=1$ within $T$.
This has the immediate corollary:
For any sufficiently strong effective theory $T$ of arithmetic, with Gödel-Rosser sentence $G$, if $T$ does not prove $0=1$ then $T$ does not prove $G$ and $T$ does not prove the negation of $G$.
Neither of these statements, nor their proofs, requires any model theory.
However, these syntactic statements leave open the question of whether $G$ is actually true. It's one thing to know that there is some sentence that is neither provable nor disprovable, but either $G$ or its negation has to be true as a statement about natural numbers, and it would be nice to know which one it is. The answer is that $G$ is true, rather than the negation of $G$.
answered Jun 14 '13 at 23:05
Carl MummertCarl Mummert
66.6k7132248
$endgroup$
$begingroup$
The first indented statement may seem somewhat weak, because we could just search for the proof of $0=1$ if it exists. But, if we add the fact that the proof of the incompleteness theorem establishes that the algorithm is given by a primitive recursive function, that removes any vacuousness.
$endgroup$
– Carl Mummert
Jun 14 '13 at 23:13
$begingroup$
'neither of these statements or their proofs don't require model theory' - does this include interpretation in the standard model of the integers N? To tally with Peter Smiths answer (that there are two proofs - sound & syntactic) is the proof you're considering use omega-consistency?
$endgroup$
– Mozibur Ullah
Jun 14 '13 at 23:14
$begingroup$
No, no model theory at all is required for that, and there is no need to mention the standard model. The proof shows that there is a fixed algorithm that, solely by syntactic manipulation of formulas and proofs, will take a proof of $G$ and turn it into a proof of $0=1$. But the cost of this is that you lose part of the conclusion.
$endgroup$
– Carl Mummert
Jun 14 '13 at 23:15
2
$begingroup$
No, the theorem can be proved entirely syntactically, as I keep saying.
$endgroup$
– Carl Mummert
Jun 14 '13 at 23:37
1
$begingroup$
I'm trying to understand what you mean by saying 'these syntactic statements leave open the question of whether G is actually true' which implies that truth isn't something that is captured purely syntactically, and your explanation showed 'there is some sentence that is neither provable nor disprovable'. But you finally assert that 'The answer is that G is true'. Now when truth is mentioned I usually think of model interpretation. Obviously after your comments that can't be correct. So what notion of truth are you using in your last statement?
$endgroup$
– Mozibur Ullah
Jun 14 '13 at 23:53
|
show 8 more comments
$begingroup$
Although it is not usually presented this way, the usual proof of the incompleteness theorem shows the following:
For any sufficiently strong effective theory $T$ of arithmetic, with Gödel-Rosser sentence $G$, there is an algorithm that will take any proof of $G$ within $T$ and turn it into a proof of $0=1$ within $T$, and there is an algorithm that will take a proof of the negation of $G$ within $T$ and turn it into a proof of $0=1$ within $T$.
This has the immediate corollary:
For any sufficiently strong effective theory $T$ of arithmetic, with Gödel-Rosser sentence $G$, if $T$ does not prove $0=1$ then $T$ does not prove $G$ and $T$ does not prove the negation of $G$.
Neither of these statements, nor their proofs, requires any model theory.
However, these syntactic statements leave open the question of whether $G$ is actually true. It's one thing to know that there is some sentence that is neither provable nor disprovable, but either $G$ or its negation has to be true as a statement about natural numbers, and it would be nice to know which one it is. The answer is that $G$ is true, rather than the negation of $G$.
answered Jun 14 '13 at 23:05
Carl MummertCarl Mummert
66.6k7132248
$endgroup$
$begingroup$
The first indented statement may seem somewhat weak, because we could just search for the proof of $0=1$ if it exists. But, if we add the fact that the proof of the incompleteness theorem establishes that the algorithm is given by a primitive recursive function, that removes any vacuousness.
$endgroup$
– Carl Mummert
Jun 14 '13 at 23:13
$begingroup$
'neither of these statements or their proofs don't require model theory' - does this include interpretation in the standard model of the integers N? To tally with Peter Smiths answer (that there are two proofs - sound & syntactic) is the proof you're considering use omega-consistency?
$endgroup$
– Mozibur Ullah
Jun 14 '13 at 23:14
$begingroup$
No, no model theory at all is required for that, and there is no need to mention the standard model. The proof shows that there is a fixed algorithm that, solely by syntactic manipulation of formulas and proofs, will take a proof of $G$ and turn it into a proof of $0=1$. But the cost of this is that you lose part of the conclusion.
$endgroup$
– Carl Mummert
Jun 14 '13 at 23:15
2
$begingroup$
No, the theorem can be proved entirely syntactically, as I keep saying.
$endgroup$
– Carl Mummert
Jun 14 '13 at 23:37
1
$begingroup$
I'm trying to understand what you mean by saying 'these syntactic statements leave open the question of whether G is actually true' which implies that truth isn't something that is captured purely syntactically, and your explanation showed 'there is some sentence that is neither provable nor disprovable'. But you finally assert that 'The answer is that G is true'. Now when truth is mentioned I usually think of model interpretation. Obviously after your comments that can't be correct. So what notion of truth are you using in your last statement?
$endgroup$
– Mozibur Ullah
Jun 14 '13 at 23:53
|
show 8 more comments
$begingroup$
Although it is not usually presented this way, the usual proof of the incompleteness theorem shows the following:
For any sufficiently strong effective theory $T$ of arithmetic, with Gödel-Rosser sentence $G$, there is an algorithm that will take any proof of $G$ within $T$ and turn it into a proof of $0=1$ within $T$, and there is an algorithm that will take a proof of the negation of $G$ within $T$ and turn it into a proof of $0=1$ within $T$.
This has the immediate corollary:
For any sufficiently strong effective theory $T$ of arithmetic, with Gödel-Rosser sentence $G$, if $T$ does not prove $0=1$ then $T$ does not prove $G$ and $T$ does not prove the negation of $G$.
Neither of these statements, nor their proofs, requires any model theory.
However, these syntactic statements leave open the question of whether $G$ is actually true. It's one thing to know that there is some sentence that is neither provable nor disprovable, but either $G$ or its negation has to be true as a statement about natural numbers, and it would be nice to know which one it is. The answer is that $G$ is true, rather than the negation of $G$.
answered Jun 14 '13 at 23:05
Carl MummertCarl Mummert
66.6k7132248
$endgroup$
Although it is not usually presented this way, the usual proof of the incompleteness theorem shows the following:
For any sufficiently strong effective theory $T$ of arithmetic, with Gödel-Rosser sentence $G$, there is an algorithm that will take any proof of $G$ within $T$ and turn it into a proof of $0=1$ within $T$, and there is an algorithm that will take a proof of the negation of $G$ within $T$ and turn it into a proof of $0=1$ within $T$.
This has the immediate corollary:
For any sufficiently strong effective theory $T$ of arithmetic, with Gödel-Rosser sentence $G$, if $T$ does not prove $0=1$ then $T$ does not prove $G$ and $T$ does not prove the negation of $G$.
Neither of these statements, nor their proofs, requires any model theory.
However, these syntactic statements leave open the question of whether $G$ is actually true. It's one thing to know that there is some sentence that is neither provable nor disprovable, but either $G$ or its negation has to be true as a statement about natural numbers, and it would be nice to know which one it is. The answer is that $G$ is true, rather than the negation of $G$.
answered Jun 14 '13 at 23:05
Carl MummertCarl Mummert
66.6k7132248
edited Jun 14 '13 at 23:39
answered Jun 14 '13 at 23:05
Carl MummertCarl Mummert
66.6k7132248
answered Jun 14 '13 at 23:05
Carl MummertCarl Mummert
66.6k7132248
answered Jun 14 '13 at 23:05
Carl MummertCarl Mummert
66.6k7132248
66.6k7132248
$begingroup$
The first indented statement may seem somewhat weak, because we could just search for the proof of $0=1$ if it exists. But, if we add the fact that the proof of the incompleteness theorem establishes that the algorithm is given by a primitive recursive function, that removes any vacuousness.
$endgroup$
– Carl Mummert
Jun 14 '13 at 23:13
$begingroup$
'neither of these statements or their proofs don't require model theory' - does this include interpretation in the standard model of the integers N? To tally with Peter Smiths answer (that there are two proofs - sound & syntactic) is the proof you're considering use omega-consistency?
$endgroup$
– Mozibur Ullah
Jun 14 '13 at 23:14
$begingroup$
No, no model theory at all is required for that, and there is no need to mention the standard model. The proof shows that there is a fixed algorithm that, solely by syntactic manipulation of formulas and proofs, will take a proof of $G$ and turn it into a proof of $0=1$. But the cost of this is that you lose part of the conclusion.
$endgroup$
– Carl Mummert
Jun 14 '13 at 23:15
2
$begingroup$
No, the theorem can be proved entirely syntactically, as I keep saying.
$endgroup$
– Carl Mummert
Jun 14 '13 at 23:37
1
$begingroup$
I'm trying to understand what you mean by saying 'these syntactic statements leave open the question of whether G is actually true' which implies that truth isn't something that is captured purely syntactically, and your explanation showed 'there is some sentence that is neither provable nor disprovable'. But you finally assert that 'The answer is that G is true'. Now when truth is mentioned I usually think of model interpretation. Obviously after your comments that can't be correct. So what notion of truth are you using in your last statement?
$endgroup$
– Mozibur Ullah
Jun 14 '13 at 23:53
|
show 8 more comments
$begingroup$
The first indented statement may seem somewhat weak, because we could just search for the proof of $0=1$ if it exists. But, if we add the fact that the proof of the incompleteness theorem establishes that the algorithm is given by a primitive recursive function, that removes any vacuousness.
$endgroup$
– Carl Mummert
Jun 14 '13 at 23:13
$begingroup$
'neither of these statements or their proofs don't require model theory' - does this include interpretation in the standard model of the integers N? To tally with Peter Smiths answer (that there are two proofs - sound & syntactic) is the proof you're considering use omega-consistency?
$endgroup$
– Mozibur Ullah
Jun 14 '13 at 23:14
$begingroup$
No, no model theory at all is required for that, and there is no need to mention the standard model. The proof shows that there is a fixed algorithm that, solely by syntactic manipulation of formulas and proofs, will take a proof of $G$ and turn it into a proof of $0=1$. But the cost of this is that you lose part of the conclusion.
$endgroup$
– Carl Mummert
Jun 14 '13 at 23:15
2
$begingroup$
No, the theorem can be proved entirely syntactically, as I keep saying.
$endgroup$
– Carl Mummert
Jun 14 '13 at 23:37
1
$begingroup$
I'm trying to understand what you mean by saying 'these syntactic statements leave open the question of whether G is actually true' which implies that truth isn't something that is captured purely syntactically, and your explanation showed 'there is some sentence that is neither provable nor disprovable'. But you finally assert that 'The answer is that G is true'. Now when truth is mentioned I usually think of model interpretation. Obviously after your comments that can't be correct. So what notion of truth are you using in your last statement?
$endgroup$
– Mozibur Ullah
Jun 14 '13 at 23:53
$begingroup$
The first indented statement may seem somewhat weak, because we could just search for the proof of $0=1$ if it exists. But, if we add the fact that the proof of the incompleteness theorem establishes that the algorithm is given by a primitive recursive function, that removes any vacuousness.
$endgroup$
– Carl Mummert
Jun 14 '13 at 23:13
$begingroup$
The first indented statement may seem somewhat weak, because we could just search for the proof of $0=1$ if it exists. But, if we add the fact that the proof of the incompleteness theorem establishes that the algorithm is given by a primitive recursive function, that removes any vacuousness.
$endgroup$
– Carl Mummert
Jun 14 '13 at 23:13
$begingroup$
'neither of these statements or their proofs don't require model theory' - does this include interpretation in the standard model of the integers N? To tally with Peter Smiths answer (that there are two proofs - sound & syntactic) is the proof you're considering use omega-consistency?
$endgroup$
– Mozibur Ullah
Jun 14 '13 at 23:14
$begingroup$
'neither of these statements or their proofs don't require model theory' - does this include interpretation in the standard model of the integers N? To tally with Peter Smiths answer (that there are two proofs - sound & syntactic) is the proof you're considering use omega-consistency?
$endgroup$
– Mozibur Ullah
Jun 14 '13 at 23:14
$begingroup$
No, no model theory at all is required for that, and there is no need to mention the standard model. The proof shows that there is a fixed algorithm that, solely by syntactic manipulation of formulas and proofs, will take a proof of $G$ and turn it into a proof of $0=1$. But the cost of this is that you lose part of the conclusion.
$endgroup$
– Carl Mummert
Jun 14 '13 at 23:15
$begingroup$
No, no model theory at all is required for that, and there is no need to mention the standard model. The proof shows that there is a fixed algorithm that, solely by syntactic manipulation of formulas and proofs, will take a proof of $G$ and turn it into a proof of $0=1$. But the cost of this is that you lose part of the conclusion.
$endgroup$
– Carl Mummert
Jun 14 '13 at 23:15
2
2
$begingroup$
No, the theorem can be proved entirely syntactically, as I keep saying.
$endgroup$
– Carl Mummert
Jun 14 '13 at 23:37
$begingroup$
No, the theorem can be proved entirely syntactically, as I keep saying.
$endgroup$
– Carl Mummert
Jun 14 '13 at 23:37
1
1
$begingroup$
I'm trying to understand what you mean by saying 'these syntactic statements leave open the question of whether G is actually true' which implies that truth isn't something that is captured purely syntactically, and your explanation showed 'there is some sentence that is neither provable nor disprovable'. But you finally assert that 'The answer is that G is true'. Now when truth is mentioned I usually think of model interpretation. Obviously after your comments that can't be correct. So what notion of truth are you using in your last statement?
$endgroup$
– Mozibur Ullah
Jun 14 '13 at 23:53
$begingroup$
I'm trying to understand what you mean by saying 'these syntactic statements leave open the question of whether G is actually true' which implies that truth isn't something that is captured purely syntactically, and your explanation showed 'there is some sentence that is neither provable nor disprovable'. But you finally assert that 'The answer is that G is true'. Now when truth is mentioned I usually think of model interpretation. Obviously after your comments that can't be correct. So what notion of truth are you using in your last statement?
$endgroup$
– Mozibur Ullah
Jun 14 '13 at 23:53
|
show 8 more comments
Thanks for contributing an answer to Mathematics Stack Exchange!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
Use MathJax to format equations. MathJax reference.
To learn more, see our tips on writing great answers.
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f420574%2fis-g%25c3%25b6dels-incompleteness-theorem-provable-without-any-model-theoretic-notion%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
$begingroup$
One just omits the "basic arithmetical truths" part, and shows that any consistent r.e. extension of say PA, (or something far weaker) is incomplete.
$endgroup$
– André Nicolas
Jun 14 '13 at 21:23
4
$begingroup$
After all one shows that there is some $Phi$ such that $Phi(lceil nrceil)$ is provable for all $n$, but $forall n:Phi(n)$ is not provable. This does not need models, only considering proofs syntactically.
$endgroup$
– Hagen von Eitzen
Jun 14 '13 at 21:28
$begingroup$
Aside: the informal usage of "true" squashes together a number of different concepts that one often doesn't care to distinguish. But in a context like this, doing that means we misunderstand all of the subtleties of the issue! In my opinion, the word "true" and its derivatives should be avoided entirely, except in the special case where the top element of a boolean algebra actually appears in a mathematical equation and needs to be named.
$endgroup$
– Hurkyl
Dec 20 '17 at 21:55
$begingroup$
For future readers, note that the mistake in this question is the failure to properly distinguish between the meta-system MS and the formal system being studied within MS. MS itself can be formalized, so the incompleteness theorems can be completely formalized. This has nothing to do with truth. At the same time, those theorems as stated and proven in MS of course talk about arithmetical truths, which are sentences that hold in some particular model of PA that MS proves or assumes to exist. But naturals cannot be absolutely pinned down.
$endgroup$
– user21820
Dec 12 '18 at 13:26