Mixing
Why is ${#Fmidmathcal{N}models F text{ and $F$ is an $exists$-formula} }$ a recursive set?
$begingroup$
Let $mathcal{N}=(mathbb{N},+,cdot,0,1)$. I want to show that ${#Fmidmathcal{N}models F text{ and $F$ is an $exists$-formula} }$ is a recursive set. Here $#F$ is the Gödel number of $F$ and I think that $exists$-formula just means a formula on the form $exists v_0 dotsexists v_n F$, without any occurrence of universal quantifiers. The problem is from an old mock-exam from a second-level logic course given at my university.
This was my original attempt, which, as Carl Mummert pointed out, is clearly wrong:
My idea is to show that ${#Fmidmathcal{N}models F }$ is
recursive and then just multiply its characteristic funtion with
something like $f(x)=left[1,dot{-},sg(vert beta_3^3(x)-7vert )right]$, i.e. something that takes the Gödel number of $x$ and
returns $0$ if the last digit is not $7$ and $1$ if it is (i.e. if it
is an $exists$-formula). That would give me the characteristic
funtion for the original set. But then my problem is that I don't know
how to show that ${#Fmidmathcal{N}models F }$ is recursive.
logic recursion computability incompleteness
edited Jan 15 at 18:09
Asaf Karagila♦
305k32435765
asked Jan 15 at 16:52
KurtKnödelKurtKnödel
474
$endgroup$
add a comment |
$begingroup$
Let $mathcal{N}=(mathbb{N},+,cdot,0,1)$. I want to show that ${#Fmidmathcal{N}models F text{ and $F$ is an $exists$-formula} }$ is a recursive set. Here $#F$ is the Gödel number of $F$ and I think that $exists$-formula just means a formula on the form $exists v_0 dotsexists v_n F$, without any occurrence of universal quantifiers. The problem is from an old mock-exam from a second-level logic course given at my university.
This was my original attempt, which, as Carl Mummert pointed out, is clearly wrong:
My idea is to show that ${#Fmidmathcal{N}models F }$ is
recursive and then just multiply its characteristic funtion with
something like $f(x)=left[1,dot{-},sg(vert beta_3^3(x)-7vert )right]$, i.e. something that takes the Gödel number of $x$ and
returns $0$ if the last digit is not $7$ and $1$ if it is (i.e. if it
is an $exists$-formula). That would give me the characteristic
funtion for the original set. But then my problem is that I don't know
how to show that ${#Fmidmathcal{N}models F }$ is recursive.
logic recursion computability incompleteness
edited Jan 15 at 18:09
Asaf Karagila♦
305k32435765
asked Jan 15 at 16:52
KurtKnödelKurtKnödel
474
$endgroup$
1
$begingroup$
The set of true formulas of arithmetic - ${ #phi : mathbb{N} vDash phi}$ - is very far from being recursive. So that method will not work. Instead you would need to look at the special structure of a $exists$ formula and use that to show that there is a way specific to those formula to tell if they are true.
$endgroup$
– Carl Mummert
Jan 15 at 16:58
$begingroup$
You could improve the post by adding a little more background. What book is the problem from? What is your specific definition of a $exists$ formula?
$endgroup$
– Carl Mummert
Jan 15 at 16:59
$begingroup$
Yes of course, now that you phrase it that way... The problem is from an old mock-exam from a logic course given at my university. Now, unfortunately this is the first time I see the term "$exists$-formula" but I am assuming they just mean that it is on the form $exists v_0 G$. But thanks, I'll add that to my question.
$endgroup$
– KurtKnödel
Jan 15 at 17:07
$begingroup$
midproduces the correct spacing.
$endgroup$
– Asaf Karagila♦
Jan 15 at 18:09
$begingroup$
Are you sure the text you got the problem from intended you to show the set is recursively decidable, rather than recursively enumerable (which is semidecidable) ?
$endgroup$
– DanielV
Jan 15 at 21:10
add a comment |
$begingroup$
Let $mathcal{N}=(mathbb{N},+,cdot,0,1)$. I want to show that ${#Fmidmathcal{N}models F text{ and $F$ is an $exists$-formula} }$ is a recursive set. Here $#F$ is the Gödel number of $F$ and I think that $exists$-formula just means a formula on the form $exists v_0 dotsexists v_n F$, without any occurrence of universal quantifiers. The problem is from an old mock-exam from a second-level logic course given at my university.
This was my original attempt, which, as Carl Mummert pointed out, is clearly wrong:
My idea is to show that ${#Fmidmathcal{N}models F }$ is
recursive and then just multiply its characteristic funtion with
something like $f(x)=left[1,dot{-},sg(vert beta_3^3(x)-7vert )right]$, i.e. something that takes the Gödel number of $x$ and
returns $0$ if the last digit is not $7$ and $1$ if it is (i.e. if it
is an $exists$-formula). That would give me the characteristic
funtion for the original set. But then my problem is that I don't know
how to show that ${#Fmidmathcal{N}models F }$ is recursive.
logic recursion computability incompleteness
edited Jan 15 at 18:09
Asaf Karagila♦
305k32435765
asked Jan 15 at 16:52
KurtKnödelKurtKnödel
474
$endgroup$
Let $mathcal{N}=(mathbb{N},+,cdot,0,1)$. I want to show that ${#Fmidmathcal{N}models F text{ and $F$ is an $exists$-formula} }$ is a recursive set. Here $#F$ is the Gödel number of $F$ and I think that $exists$-formula just means a formula on the form $exists v_0 dotsexists v_n F$, without any occurrence of universal quantifiers. The problem is from an old mock-exam from a second-level logic course given at my university.
This was my original attempt, which, as Carl Mummert pointed out, is clearly wrong:
My idea is to show that ${#Fmidmathcal{N}models F }$ is
recursive and then just multiply its characteristic funtion with
something like $f(x)=left[1,dot{-},sg(vert beta_3^3(x)-7vert )right]$, i.e. something that takes the Gödel number of $x$ and
returns $0$ if the last digit is not $7$ and $1$ if it is (i.e. if it
is an $exists$-formula). That would give me the characteristic
funtion for the original set. But then my problem is that I don't know
how to show that ${#Fmidmathcal{N}models F }$ is recursive.
logic recursion computability incompleteness
logic recursion computability incompleteness
edited Jan 15 at 18:09
Asaf Karagila♦
305k32435765
asked Jan 15 at 16:52
KurtKnödelKurtKnödel
474
edited Jan 15 at 18:09
Asaf Karagila♦
305k32435765
asked Jan 15 at 16:52
KurtKnödelKurtKnödel
474
edited Jan 15 at 18:09
Asaf Karagila♦
305k32435765
edited Jan 15 at 18:09
Asaf Karagila♦
305k32435765
edited Jan 15 at 18:09
Asaf Karagila♦
305k32435765
305k32435765
asked Jan 15 at 16:52
KurtKnödelKurtKnödel
474
asked Jan 15 at 16:52
KurtKnödelKurtKnödel
474
asked Jan 15 at 16:52
KurtKnödelKurtKnödel
474
474
1
$begingroup$
The set of true formulas of arithmetic - ${ #phi : mathbb{N} vDash phi}$ - is very far from being recursive. So that method will not work. Instead you would need to look at the special structure of a $exists$ formula and use that to show that there is a way specific to those formula to tell if they are true.
$endgroup$
– Carl Mummert
Jan 15 at 16:58
$begingroup$
You could improve the post by adding a little more background. What book is the problem from? What is your specific definition of a $exists$ formula?
$endgroup$
– Carl Mummert
Jan 15 at 16:59
$begingroup$
Yes of course, now that you phrase it that way... The problem is from an old mock-exam from a logic course given at my university. Now, unfortunately this is the first time I see the term "$exists$-formula" but I am assuming they just mean that it is on the form $exists v_0 G$. But thanks, I'll add that to my question.
$endgroup$
– KurtKnödel
Jan 15 at 17:07
$begingroup$
midproduces the correct spacing.
$endgroup$
– Asaf Karagila♦
Jan 15 at 18:09
$begingroup$
Are you sure the text you got the problem from intended you to show the set is recursively decidable, rather than recursively enumerable (which is semidecidable) ?
$endgroup$
– DanielV
Jan 15 at 21:10
add a comment |
1
$begingroup$
The set of true formulas of arithmetic - ${ #phi : mathbb{N} vDash phi}$ - is very far from being recursive. So that method will not work. Instead you would need to look at the special structure of a $exists$ formula and use that to show that there is a way specific to those formula to tell if they are true.
$endgroup$
– Carl Mummert
Jan 15 at 16:58
$begingroup$
You could improve the post by adding a little more background. What book is the problem from? What is your specific definition of a $exists$ formula?
$endgroup$
– Carl Mummert
Jan 15 at 16:59
$begingroup$
Yes of course, now that you phrase it that way... The problem is from an old mock-exam from a logic course given at my university. Now, unfortunately this is the first time I see the term "$exists$-formula" but I am assuming they just mean that it is on the form $exists v_0 G$. But thanks, I'll add that to my question.
$endgroup$
– KurtKnödel
Jan 15 at 17:07
$begingroup$
midproduces the correct spacing.
$endgroup$
– Asaf Karagila♦
Jan 15 at 18:09
$begingroup$
Are you sure the text you got the problem from intended you to show the set is recursively decidable, rather than recursively enumerable (which is semidecidable) ?
$endgroup$
– DanielV
Jan 15 at 21:10
1
1
$begingroup$
The set of true formulas of arithmetic - ${ #phi : mathbb{N} vDash phi}$ - is very far from being recursive. So that method will not work. Instead you would need to look at the special structure of a $exists$ formula and use that to show that there is a way specific to those formula to tell if they are true.
$endgroup$
– Carl Mummert
Jan 15 at 16:58
$begingroup$
The set of true formulas of arithmetic - ${ #phi : mathbb{N} vDash phi}$ - is very far from being recursive. So that method will not work. Instead you would need to look at the special structure of a $exists$ formula and use that to show that there is a way specific to those formula to tell if they are true.
$endgroup$
– Carl Mummert
Jan 15 at 16:58
$begingroup$
You could improve the post by adding a little more background. What book is the problem from? What is your specific definition of a $exists$ formula?
$endgroup$
– Carl Mummert
Jan 15 at 16:59
$begingroup$
You could improve the post by adding a little more background. What book is the problem from? What is your specific definition of a $exists$ formula?
$endgroup$
– Carl Mummert
Jan 15 at 16:59
$begingroup$
Yes of course, now that you phrase it that way... The problem is from an old mock-exam from a logic course given at my university. Now, unfortunately this is the first time I see the term "$exists$-formula" but I am assuming they just mean that it is on the form $exists v_0 G$. But thanks, I'll add that to my question.
$endgroup$
– KurtKnödel
Jan 15 at 17:07
$begingroup$
Yes of course, now that you phrase it that way... The problem is from an old mock-exam from a logic course given at my university. Now, unfortunately this is the first time I see the term "$exists$-formula" but I am assuming they just mean that it is on the form $exists v_0 G$. But thanks, I'll add that to my question.
$endgroup$
– KurtKnödel
Jan 15 at 17:07
$begingroup$
mid produces the correct spacing.$endgroup$
– Asaf Karagila♦
Jan 15 at 18:09
$begingroup$
mid produces the correct spacing.$endgroup$
– Asaf Karagila♦
Jan 15 at 18:09
$begingroup$
Are you sure the text you got the problem from intended you to show the set is recursively decidable, rather than recursively enumerable (which is semidecidable) ?
$endgroup$
– DanielV
Jan 15 at 21:10
$begingroup$
Are you sure the text you got the problem from intended you to show the set is recursively decidable, rather than recursively enumerable (which is semidecidable) ?
$endgroup$
– DanielV
Jan 15 at 21:10
add a comment |
1 Answer
1
active
oldest
votes
$begingroup$
It's not recursive.
Whether this is easy or very hard to show depends on exactly what "$exists$-sentence" means.
Specifically, the issue is whether "bounded quantifiers" (like $forall x<5$, $exists y<z+w$) are permitted. Formulas of the form $exists x_1,...,x_n G$ where $G$ uses only bounded quantifiers are called "$Sigma_1$" (or "$Sigma^0_1$"); to me, "$exists$-formula" sounds like a stronger condition, namely we require that the matrix $G$ be genuinely quantifier-free (and this is your interpretation in the comments above).
But in each case, the resulting set is non-recursive.
Showing that the $Sigma_1$ theory of $mathcal{N}$ is non-recursive isn't too hard. There is a $Sigma_1$ formula $Halt(x)$ such that for each $ninmathbb{N}$ we have $mathcal{N}models Halt(underline{n})$ iff $varphi_n(n)downarrow$ - writing "$varphi_e(x)downarrow$" for "the $e$th Turing machine halts on input $x$" and "$underline{k}$" for the numeral corresponding to $k$ - but this means that the $Sigma_1$-theory of $mathcal{N}$ is at least as complicated as (in fact, it's equivalent to) the halting problem, which is non-recursive.
Gauging the complexity of the genuinely $exists$-theory of $mathcal{N}$ is harder, but ultimately still the same. This is the MRDP theorem: that the set of Diophantine equations with solutions (which is about as $exists$ as it gets) is non-recursive, and in fact has complexity again equal to that of the halting problem.
answered Jan 15 at 17:47
Noah SchweberNoah Schweber
125k10150287
$endgroup$
$begingroup$
Thank you very much for this! This explains why it's been so hard to prove it... Actually, the original problem was to show that ${F,vert,mathcal{N}models F text{ and $F$ is an $exists$-formula} }cup PA$ is an incomplete theory. Do you reckon this is still possible (using the first incompleteness theorem), despite the theory not being recursive?
$endgroup$
– KurtKnödel
Jan 15 at 17:56
$begingroup$
@KurtKnödel Ah, that's a very different problem. It is indeed correct, and I have two hints. $(1)$ For a "nuke," use Craig's trick and the strong version of GIT ("no consistent recursively axiomatizable extensionof PA is complete"). $(2)$ For the optimal solution, show that PA already proves every true $exists$-sentence, so you don't even need strong GIT.
$endgroup$
– Noah Schweber
Jan 15 at 17:58
$begingroup$
Your second suggestion was actually my idea all along, but then somewhere someone mentioned recursive sets and I just lost it at that point. Thank you for clarifying things!
$endgroup$
– KurtKnödel
Jan 15 at 18:06
add a comment |
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%2f3074636%2fwhy-is-f-mid-mathcaln-models-f-text-and-f-is-an-exists-formula%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
$begingroup$
It's not recursive.
Whether this is easy or very hard to show depends on exactly what "$exists$-sentence" means.
Specifically, the issue is whether "bounded quantifiers" (like $forall x<5$, $exists y<z+w$) are permitted. Formulas of the form $exists x_1,...,x_n G$ where $G$ uses only bounded quantifiers are called "$Sigma_1$" (or "$Sigma^0_1$"); to me, "$exists$-formula" sounds like a stronger condition, namely we require that the matrix $G$ be genuinely quantifier-free (and this is your interpretation in the comments above).
But in each case, the resulting set is non-recursive.
Showing that the $Sigma_1$ theory of $mathcal{N}$ is non-recursive isn't too hard. There is a $Sigma_1$ formula $Halt(x)$ such that for each $ninmathbb{N}$ we have $mathcal{N}models Halt(underline{n})$ iff $varphi_n(n)downarrow$ - writing "$varphi_e(x)downarrow$" for "the $e$th Turing machine halts on input $x$" and "$underline{k}$" for the numeral corresponding to $k$ - but this means that the $Sigma_1$-theory of $mathcal{N}$ is at least as complicated as (in fact, it's equivalent to) the halting problem, which is non-recursive.
Gauging the complexity of the genuinely $exists$-theory of $mathcal{N}$ is harder, but ultimately still the same. This is the MRDP theorem: that the set of Diophantine equations with solutions (which is about as $exists$ as it gets) is non-recursive, and in fact has complexity again equal to that of the halting problem.
answered Jan 15 at 17:47
Noah SchweberNoah Schweber
125k10150287
$endgroup$
$begingroup$
Thank you very much for this! This explains why it's been so hard to prove it... Actually, the original problem was to show that ${F,vert,mathcal{N}models F text{ and $F$ is an $exists$-formula} }cup PA$ is an incomplete theory. Do you reckon this is still possible (using the first incompleteness theorem), despite the theory not being recursive?
$endgroup$
– KurtKnödel
Jan 15 at 17:56
$begingroup$
@KurtKnödel Ah, that's a very different problem. It is indeed correct, and I have two hints. $(1)$ For a "nuke," use Craig's trick and the strong version of GIT ("no consistent recursively axiomatizable extensionof PA is complete"). $(2)$ For the optimal solution, show that PA already proves every true $exists$-sentence, so you don't even need strong GIT.
$endgroup$
– Noah Schweber
Jan 15 at 17:58
$begingroup$
Your second suggestion was actually my idea all along, but then somewhere someone mentioned recursive sets and I just lost it at that point. Thank you for clarifying things!
$endgroup$
– KurtKnödel
Jan 15 at 18:06
add a comment |
$begingroup$
It's not recursive.
Whether this is easy or very hard to show depends on exactly what "$exists$-sentence" means.
Specifically, the issue is whether "bounded quantifiers" (like $forall x<5$, $exists y<z+w$) are permitted. Formulas of the form $exists x_1,...,x_n G$ where $G$ uses only bounded quantifiers are called "$Sigma_1$" (or "$Sigma^0_1$"); to me, "$exists$-formula" sounds like a stronger condition, namely we require that the matrix $G$ be genuinely quantifier-free (and this is your interpretation in the comments above).
But in each case, the resulting set is non-recursive.
Showing that the $Sigma_1$ theory of $mathcal{N}$ is non-recursive isn't too hard. There is a $Sigma_1$ formula $Halt(x)$ such that for each $ninmathbb{N}$ we have $mathcal{N}models Halt(underline{n})$ iff $varphi_n(n)downarrow$ - writing "$varphi_e(x)downarrow$" for "the $e$th Turing machine halts on input $x$" and "$underline{k}$" for the numeral corresponding to $k$ - but this means that the $Sigma_1$-theory of $mathcal{N}$ is at least as complicated as (in fact, it's equivalent to) the halting problem, which is non-recursive.
Gauging the complexity of the genuinely $exists$-theory of $mathcal{N}$ is harder, but ultimately still the same. This is the MRDP theorem: that the set of Diophantine equations with solutions (which is about as $exists$ as it gets) is non-recursive, and in fact has complexity again equal to that of the halting problem.
answered Jan 15 at 17:47
Noah SchweberNoah Schweber
125k10150287
$endgroup$
$begingroup$
Thank you very much for this! This explains why it's been so hard to prove it... Actually, the original problem was to show that ${F,vert,mathcal{N}models F text{ and $F$ is an $exists$-formula} }cup PA$ is an incomplete theory. Do you reckon this is still possible (using the first incompleteness theorem), despite the theory not being recursive?
$endgroup$
– KurtKnödel
Jan 15 at 17:56
$begingroup$
@KurtKnödel Ah, that's a very different problem. It is indeed correct, and I have two hints. $(1)$ For a "nuke," use Craig's trick and the strong version of GIT ("no consistent recursively axiomatizable extensionof PA is complete"). $(2)$ For the optimal solution, show that PA already proves every true $exists$-sentence, so you don't even need strong GIT.
$endgroup$
– Noah Schweber
Jan 15 at 17:58
$begingroup$
Your second suggestion was actually my idea all along, but then somewhere someone mentioned recursive sets and I just lost it at that point. Thank you for clarifying things!
$endgroup$
– KurtKnödel
Jan 15 at 18:06
add a comment |
$begingroup$
It's not recursive.
Whether this is easy or very hard to show depends on exactly what "$exists$-sentence" means.
Specifically, the issue is whether "bounded quantifiers" (like $forall x<5$, $exists y<z+w$) are permitted. Formulas of the form $exists x_1,...,x_n G$ where $G$ uses only bounded quantifiers are called "$Sigma_1$" (or "$Sigma^0_1$"); to me, "$exists$-formula" sounds like a stronger condition, namely we require that the matrix $G$ be genuinely quantifier-free (and this is your interpretation in the comments above).
But in each case, the resulting set is non-recursive.
Showing that the $Sigma_1$ theory of $mathcal{N}$ is non-recursive isn't too hard. There is a $Sigma_1$ formula $Halt(x)$ such that for each $ninmathbb{N}$ we have $mathcal{N}models Halt(underline{n})$ iff $varphi_n(n)downarrow$ - writing "$varphi_e(x)downarrow$" for "the $e$th Turing machine halts on input $x$" and "$underline{k}$" for the numeral corresponding to $k$ - but this means that the $Sigma_1$-theory of $mathcal{N}$ is at least as complicated as (in fact, it's equivalent to) the halting problem, which is non-recursive.
Gauging the complexity of the genuinely $exists$-theory of $mathcal{N}$ is harder, but ultimately still the same. This is the MRDP theorem: that the set of Diophantine equations with solutions (which is about as $exists$ as it gets) is non-recursive, and in fact has complexity again equal to that of the halting problem.
answered Jan 15 at 17:47
Noah SchweberNoah Schweber
125k10150287
$endgroup$
It's not recursive.
Whether this is easy or very hard to show depends on exactly what "$exists$-sentence" means.
Specifically, the issue is whether "bounded quantifiers" (like $forall x<5$, $exists y<z+w$) are permitted. Formulas of the form $exists x_1,...,x_n G$ where $G$ uses only bounded quantifiers are called "$Sigma_1$" (or "$Sigma^0_1$"); to me, "$exists$-formula" sounds like a stronger condition, namely we require that the matrix $G$ be genuinely quantifier-free (and this is your interpretation in the comments above).
But in each case, the resulting set is non-recursive.
Showing that the $Sigma_1$ theory of $mathcal{N}$ is non-recursive isn't too hard. There is a $Sigma_1$ formula $Halt(x)$ such that for each $ninmathbb{N}$ we have $mathcal{N}models Halt(underline{n})$ iff $varphi_n(n)downarrow$ - writing "$varphi_e(x)downarrow$" for "the $e$th Turing machine halts on input $x$" and "$underline{k}$" for the numeral corresponding to $k$ - but this means that the $Sigma_1$-theory of $mathcal{N}$ is at least as complicated as (in fact, it's equivalent to) the halting problem, which is non-recursive.
Gauging the complexity of the genuinely $exists$-theory of $mathcal{N}$ is harder, but ultimately still the same. This is the MRDP theorem: that the set of Diophantine equations with solutions (which is about as $exists$ as it gets) is non-recursive, and in fact has complexity again equal to that of the halting problem.
answered Jan 15 at 17:47
Noah SchweberNoah Schweber
125k10150287
answered Jan 15 at 17:47
Noah SchweberNoah Schweber
125k10150287
answered Jan 15 at 17:47
Noah SchweberNoah Schweber
125k10150287
answered Jan 15 at 17:47
Noah SchweberNoah Schweber
125k10150287
125k10150287
$begingroup$
Thank you very much for this! This explains why it's been so hard to prove it... Actually, the original problem was to show that ${F,vert,mathcal{N}models F text{ and $F$ is an $exists$-formula} }cup PA$ is an incomplete theory. Do you reckon this is still possible (using the first incompleteness theorem), despite the theory not being recursive?
$endgroup$
– KurtKnödel
Jan 15 at 17:56
$begingroup$
@KurtKnödel Ah, that's a very different problem. It is indeed correct, and I have two hints. $(1)$ For a "nuke," use Craig's trick and the strong version of GIT ("no consistent recursively axiomatizable extensionof PA is complete"). $(2)$ For the optimal solution, show that PA already proves every true $exists$-sentence, so you don't even need strong GIT.
$endgroup$
– Noah Schweber
Jan 15 at 17:58
$begingroup$
Your second suggestion was actually my idea all along, but then somewhere someone mentioned recursive sets and I just lost it at that point. Thank you for clarifying things!
$endgroup$
– KurtKnödel
Jan 15 at 18:06
add a comment |
$begingroup$
Thank you very much for this! This explains why it's been so hard to prove it... Actually, the original problem was to show that ${F,vert,mathcal{N}models F text{ and $F$ is an $exists$-formula} }cup PA$ is an incomplete theory. Do you reckon this is still possible (using the first incompleteness theorem), despite the theory not being recursive?
$endgroup$
– KurtKnödel
Jan 15 at 17:56
$begingroup$
@KurtKnödel Ah, that's a very different problem. It is indeed correct, and I have two hints. $(1)$ For a "nuke," use Craig's trick and the strong version of GIT ("no consistent recursively axiomatizable extensionof PA is complete"). $(2)$ For the optimal solution, show that PA already proves every true $exists$-sentence, so you don't even need strong GIT.
$endgroup$
– Noah Schweber
Jan 15 at 17:58
$begingroup$
Your second suggestion was actually my idea all along, but then somewhere someone mentioned recursive sets and I just lost it at that point. Thank you for clarifying things!
$endgroup$
– KurtKnödel
Jan 15 at 18:06
$begingroup$
Thank you very much for this! This explains why it's been so hard to prove it... Actually, the original problem was to show that ${F,vert,mathcal{N}models F text{ and $F$ is an $exists$-formula} }cup PA$ is an incomplete theory. Do you reckon this is still possible (using the first incompleteness theorem), despite the theory not being recursive?
$endgroup$
– KurtKnödel
Jan 15 at 17:56
$begingroup$
Thank you very much for this! This explains why it's been so hard to prove it... Actually, the original problem was to show that ${F,vert,mathcal{N}models F text{ and $F$ is an $exists$-formula} }cup PA$ is an incomplete theory. Do you reckon this is still possible (using the first incompleteness theorem), despite the theory not being recursive?
$endgroup$
– KurtKnödel
Jan 15 at 17:56
$begingroup$
@KurtKnödel Ah, that's a very different problem. It is indeed correct, and I have two hints. $(1)$ For a "nuke," use Craig's trick and the strong version of GIT ("no consistent recursively axiomatizable extensionof PA is complete"). $(2)$ For the optimal solution, show that PA already proves every true $exists$-sentence, so you don't even need strong GIT.
$endgroup$
– Noah Schweber
Jan 15 at 17:58
$begingroup$
@KurtKnödel Ah, that's a very different problem. It is indeed correct, and I have two hints. $(1)$ For a "nuke," use Craig's trick and the strong version of GIT ("no consistent recursively axiomatizable extensionof PA is complete"). $(2)$ For the optimal solution, show that PA already proves every true $exists$-sentence, so you don't even need strong GIT.
$endgroup$
– Noah Schweber
Jan 15 at 17:58
$begingroup$
Your second suggestion was actually my idea all along, but then somewhere someone mentioned recursive sets and I just lost it at that point. Thank you for clarifying things!
$endgroup$
– KurtKnödel
Jan 15 at 18:06
$begingroup$
Your second suggestion was actually my idea all along, but then somewhere someone mentioned recursive sets and I just lost it at that point. Thank you for clarifying things!
$endgroup$
– KurtKnödel
Jan 15 at 18:06
add a comment |
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%2f3074636%2fwhy-is-f-mid-mathcaln-models-f-text-and-f-is-an-exists-formula%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
1
$begingroup$
The set of true formulas of arithmetic - ${ #phi : mathbb{N} vDash phi}$ - is very far from being recursive. So that method will not work. Instead you would need to look at the special structure of a $exists$ formula and use that to show that there is a way specific to those formula to tell if they are true.
$endgroup$
– Carl Mummert
Jan 15 at 16:58
$begingroup$
You could improve the post by adding a little more background. What book is the problem from? What is your specific definition of a $exists$ formula?
$endgroup$
– Carl Mummert
Jan 15 at 16:59
$begingroup$
Yes of course, now that you phrase it that way... The problem is from an old mock-exam from a logic course given at my university. Now, unfortunately this is the first time I see the term "$exists$-formula" but I am assuming they just mean that it is on the form $exists v_0 G$. But thanks, I'll add that to my question.
$endgroup$
– KurtKnödel
Jan 15 at 17:07
$begingroup$
midproduces the correct spacing.$endgroup$
– Asaf Karagila♦
Jan 15 at 18:09
$begingroup$
Are you sure the text you got the problem from intended you to show the set is recursively decidable, rather than recursively enumerable (which is semidecidable) ?
$endgroup$
– DanielV
Jan 15 at 21:10