Semi-recursive ω-rule












2












$begingroup$


I thought of the following semi-recursive ω-rule for a sequence of first-order theories $PA_k$ that extend $PA_0 = PA$:




Semi-recursive ω-rule: For each $1$-parameter arithmetical sentence $Q$, if (using the usual encoding) $PA_k vdash forall n ( PA_k vdash Q(n) )$, then we add $∀n ( Q(n) )$ as an axiom of $PA_{k+1}$.




$PA_k$ clearly has a semi-recursive axiom set for each natural $k$, so it has a theorem generator and will still be arithmetically-incomplete by the generalized incompleteness theorems. Anyway if PA is sound then $PA_k$ would also be sound. My questions are:




(1) What is the strength of each $PA_k$ for natural $k$?



(2) What happens if I go further by defining $PA_ω = bigcup_{k in ω} PA_k$ and carry on iterating all the way up the computable ordinals?



(3) What if we start with ACA instead? In general, what happens to the strength of the system on applying this semi-recursive ω-rule?






Assuming $PA$ is sound, I cannot even think of a single sentence that $PA_1$ proves that $PA$ does not. So I am actually guessing that this rule is completely useless. Can anyone prove that $PA_1 = PA$ and $ACA_1 = ACA$? If not, does the hierarchy reach a fixed point?










share|cite|improve this question











$endgroup$












  • $begingroup$
    Note that Craig's trick lets you go from a semirecursive axiomatization to a recursive axiomatization.
    $endgroup$
    – Noah Schweber
    Oct 4 '17 at 20:07










  • $begingroup$
    @NoahSchweber: I'm aware of that trick, but it's doesn't help to answer the question, right?
    $endgroup$
    – user21820
    Oct 5 '17 at 15:20












  • $begingroup$
    I thought it was worth mentioning given your use of the term "semi-recursive." Also: what do you mean when you say "does not have a proof verifier program"? It's an r.e. theory, the set of its theorems is r.e.
    $endgroup$
    – Noah Schweber
    Oct 5 '17 at 15:31










  • $begingroup$
    @NoahSchweber: Well I just meant that there is no program that decides the validity of a proof of a sentence. Perhaps my use of the word "verifier" is slightly misleading, but I can't think of a better English word. Anyway do you have any idea what this kind of hierarchy gives? I'm curious to know whether the strength of the theory stabilizes at some point, and where that point is.
    $endgroup$
    – user21820
    Oct 5 '17 at 15:37










  • $begingroup$
    It's a more subtle question than I thought, I like it !
    $endgroup$
    – Xoff
    Nov 29 '18 at 19:38
















2












$begingroup$


I thought of the following semi-recursive ω-rule for a sequence of first-order theories $PA_k$ that extend $PA_0 = PA$:




Semi-recursive ω-rule: For each $1$-parameter arithmetical sentence $Q$, if (using the usual encoding) $PA_k vdash forall n ( PA_k vdash Q(n) )$, then we add $∀n ( Q(n) )$ as an axiom of $PA_{k+1}$.




$PA_k$ clearly has a semi-recursive axiom set for each natural $k$, so it has a theorem generator and will still be arithmetically-incomplete by the generalized incompleteness theorems. Anyway if PA is sound then $PA_k$ would also be sound. My questions are:




(1) What is the strength of each $PA_k$ for natural $k$?



(2) What happens if I go further by defining $PA_ω = bigcup_{k in ω} PA_k$ and carry on iterating all the way up the computable ordinals?



(3) What if we start with ACA instead? In general, what happens to the strength of the system on applying this semi-recursive ω-rule?






Assuming $PA$ is sound, I cannot even think of a single sentence that $PA_1$ proves that $PA$ does not. So I am actually guessing that this rule is completely useless. Can anyone prove that $PA_1 = PA$ and $ACA_1 = ACA$? If not, does the hierarchy reach a fixed point?










share|cite|improve this question











$endgroup$












  • $begingroup$
    Note that Craig's trick lets you go from a semirecursive axiomatization to a recursive axiomatization.
    $endgroup$
    – Noah Schweber
    Oct 4 '17 at 20:07










  • $begingroup$
    @NoahSchweber: I'm aware of that trick, but it's doesn't help to answer the question, right?
    $endgroup$
    – user21820
    Oct 5 '17 at 15:20












  • $begingroup$
    I thought it was worth mentioning given your use of the term "semi-recursive." Also: what do you mean when you say "does not have a proof verifier program"? It's an r.e. theory, the set of its theorems is r.e.
    $endgroup$
    – Noah Schweber
    Oct 5 '17 at 15:31










  • $begingroup$
    @NoahSchweber: Well I just meant that there is no program that decides the validity of a proof of a sentence. Perhaps my use of the word "verifier" is slightly misleading, but I can't think of a better English word. Anyway do you have any idea what this kind of hierarchy gives? I'm curious to know whether the strength of the theory stabilizes at some point, and where that point is.
    $endgroup$
    – user21820
    Oct 5 '17 at 15:37










  • $begingroup$
    It's a more subtle question than I thought, I like it !
    $endgroup$
    – Xoff
    Nov 29 '18 at 19:38














2












2








2


2



$begingroup$


I thought of the following semi-recursive ω-rule for a sequence of first-order theories $PA_k$ that extend $PA_0 = PA$:




Semi-recursive ω-rule: For each $1$-parameter arithmetical sentence $Q$, if (using the usual encoding) $PA_k vdash forall n ( PA_k vdash Q(n) )$, then we add $∀n ( Q(n) )$ as an axiom of $PA_{k+1}$.




$PA_k$ clearly has a semi-recursive axiom set for each natural $k$, so it has a theorem generator and will still be arithmetically-incomplete by the generalized incompleteness theorems. Anyway if PA is sound then $PA_k$ would also be sound. My questions are:




(1) What is the strength of each $PA_k$ for natural $k$?



(2) What happens if I go further by defining $PA_ω = bigcup_{k in ω} PA_k$ and carry on iterating all the way up the computable ordinals?



(3) What if we start with ACA instead? In general, what happens to the strength of the system on applying this semi-recursive ω-rule?






Assuming $PA$ is sound, I cannot even think of a single sentence that $PA_1$ proves that $PA$ does not. So I am actually guessing that this rule is completely useless. Can anyone prove that $PA_1 = PA$ and $ACA_1 = ACA$? If not, does the hierarchy reach a fixed point?










share|cite|improve this question











$endgroup$




I thought of the following semi-recursive ω-rule for a sequence of first-order theories $PA_k$ that extend $PA_0 = PA$:




Semi-recursive ω-rule: For each $1$-parameter arithmetical sentence $Q$, if (using the usual encoding) $PA_k vdash forall n ( PA_k vdash Q(n) )$, then we add $∀n ( Q(n) )$ as an axiom of $PA_{k+1}$.




$PA_k$ clearly has a semi-recursive axiom set for each natural $k$, so it has a theorem generator and will still be arithmetically-incomplete by the generalized incompleteness theorems. Anyway if PA is sound then $PA_k$ would also be sound. My questions are:




(1) What is the strength of each $PA_k$ for natural $k$?



(2) What happens if I go further by defining $PA_ω = bigcup_{k in ω} PA_k$ and carry on iterating all the way up the computable ordinals?



(3) What if we start with ACA instead? In general, what happens to the strength of the system on applying this semi-recursive ω-rule?






Assuming $PA$ is sound, I cannot even think of a single sentence that $PA_1$ proves that $PA$ does not. So I am actually guessing that this rule is completely useless. Can anyone prove that $PA_1 = PA$ and $ACA_1 = ACA$? If not, does the hierarchy reach a fixed point?







logic computability proof-theory incompleteness






share|cite|improve this question















share|cite|improve this question













share|cite|improve this question




share|cite|improve this question








edited Dec 4 '18 at 3:11







user21820

















asked Oct 4 '17 at 6:06









user21820user21820

39.2k543154




39.2k543154












  • $begingroup$
    Note that Craig's trick lets you go from a semirecursive axiomatization to a recursive axiomatization.
    $endgroup$
    – Noah Schweber
    Oct 4 '17 at 20:07










  • $begingroup$
    @NoahSchweber: I'm aware of that trick, but it's doesn't help to answer the question, right?
    $endgroup$
    – user21820
    Oct 5 '17 at 15:20












  • $begingroup$
    I thought it was worth mentioning given your use of the term "semi-recursive." Also: what do you mean when you say "does not have a proof verifier program"? It's an r.e. theory, the set of its theorems is r.e.
    $endgroup$
    – Noah Schweber
    Oct 5 '17 at 15:31










  • $begingroup$
    @NoahSchweber: Well I just meant that there is no program that decides the validity of a proof of a sentence. Perhaps my use of the word "verifier" is slightly misleading, but I can't think of a better English word. Anyway do you have any idea what this kind of hierarchy gives? I'm curious to know whether the strength of the theory stabilizes at some point, and where that point is.
    $endgroup$
    – user21820
    Oct 5 '17 at 15:37










  • $begingroup$
    It's a more subtle question than I thought, I like it !
    $endgroup$
    – Xoff
    Nov 29 '18 at 19:38


















  • $begingroup$
    Note that Craig's trick lets you go from a semirecursive axiomatization to a recursive axiomatization.
    $endgroup$
    – Noah Schweber
    Oct 4 '17 at 20:07










  • $begingroup$
    @NoahSchweber: I'm aware of that trick, but it's doesn't help to answer the question, right?
    $endgroup$
    – user21820
    Oct 5 '17 at 15:20












  • $begingroup$
    I thought it was worth mentioning given your use of the term "semi-recursive." Also: what do you mean when you say "does not have a proof verifier program"? It's an r.e. theory, the set of its theorems is r.e.
    $endgroup$
    – Noah Schweber
    Oct 5 '17 at 15:31










  • $begingroup$
    @NoahSchweber: Well I just meant that there is no program that decides the validity of a proof of a sentence. Perhaps my use of the word "verifier" is slightly misleading, but I can't think of a better English word. Anyway do you have any idea what this kind of hierarchy gives? I'm curious to know whether the strength of the theory stabilizes at some point, and where that point is.
    $endgroup$
    – user21820
    Oct 5 '17 at 15:37










  • $begingroup$
    It's a more subtle question than I thought, I like it !
    $endgroup$
    – Xoff
    Nov 29 '18 at 19:38
















$begingroup$
Note that Craig's trick lets you go from a semirecursive axiomatization to a recursive axiomatization.
$endgroup$
– Noah Schweber
Oct 4 '17 at 20:07




$begingroup$
Note that Craig's trick lets you go from a semirecursive axiomatization to a recursive axiomatization.
$endgroup$
– Noah Schweber
Oct 4 '17 at 20:07












$begingroup$
@NoahSchweber: I'm aware of that trick, but it's doesn't help to answer the question, right?
$endgroup$
– user21820
Oct 5 '17 at 15:20






$begingroup$
@NoahSchweber: I'm aware of that trick, but it's doesn't help to answer the question, right?
$endgroup$
– user21820
Oct 5 '17 at 15:20














$begingroup$
I thought it was worth mentioning given your use of the term "semi-recursive." Also: what do you mean when you say "does not have a proof verifier program"? It's an r.e. theory, the set of its theorems is r.e.
$endgroup$
– Noah Schweber
Oct 5 '17 at 15:31




$begingroup$
I thought it was worth mentioning given your use of the term "semi-recursive." Also: what do you mean when you say "does not have a proof verifier program"? It's an r.e. theory, the set of its theorems is r.e.
$endgroup$
– Noah Schweber
Oct 5 '17 at 15:31












$begingroup$
@NoahSchweber: Well I just meant that there is no program that decides the validity of a proof of a sentence. Perhaps my use of the word "verifier" is slightly misleading, but I can't think of a better English word. Anyway do you have any idea what this kind of hierarchy gives? I'm curious to know whether the strength of the theory stabilizes at some point, and where that point is.
$endgroup$
– user21820
Oct 5 '17 at 15:37




$begingroup$
@NoahSchweber: Well I just meant that there is no program that decides the validity of a proof of a sentence. Perhaps my use of the word "verifier" is slightly misleading, but I can't think of a better English word. Anyway do you have any idea what this kind of hierarchy gives? I'm curious to know whether the strength of the theory stabilizes at some point, and where that point is.
$endgroup$
– user21820
Oct 5 '17 at 15:37












$begingroup$
It's a more subtle question than I thought, I like it !
$endgroup$
– Xoff
Nov 29 '18 at 19:38




$begingroup$
It's a more subtle question than I thought, I like it !
$endgroup$
– Xoff
Nov 29 '18 at 19:38










1 Answer
1






active

oldest

votes


















1












$begingroup$

Below, all theories are "appropriate" - that is, they are recursively axiomatizable, consistent, and contain PA. Of course this last bit is overkill, but what the hey.



I can't give a full answer, but let me address your question as to whether $PA=PA_1$. The answer is no, and indeed the "semirecursive $omega$-rule operator" has no nontrivial fixed points.



The key is the following fact: that PA is internally $Sigma_1$-complete, that is, that PA proves "PA proves every true $Sigma_1$ fact." See e.g. here. And of course this is hereditary upwards - all the theories we consider will share this property too. (Actually, we really only need $Delta_0$-completeness, but meh.)



Internal $Sigma_1$-completeness lets us make the following neat argument. Given an appropriate theory $S$, let $Q_S(x)$ be the formula "$x$ is not (the Godel number of) a proof of a contradiction in $S$." Then I claim that we have $$Svdashforall x(Svdash Q_S(x)).$$ Consequently the "next step up" from $S$ according to your semi-recursive $omega$-rule is at least (and indeed will wind up being much more than) $S+Con(S)$, since "$forall x(Q_S(x))$" is just "$Con(S)$."



To see this, we reason inside $S$ as follows:




"Fix $n$; we need to show that $S$ proves '$n$ is not (the Godel number of) an $S$-proof of a contradiction.' There are two possibilities. Maybe $n$ is the Godel number of a proof of a contradiction in $S$, in which case $S$ is inconsistent and so we have $Svdash Q_S(n)$ trivially. Otherwise, $n$ is not the Godel number of a proof of a contradiction in $S$, in which case we have $Svdash Q_S(n)$ since 'not-being-a-proof-of' is $Sigma_1$ (indeed, $Delta_0$) and $S$ is $Sigma_1$-complete. Either way, it must be the case that $Svdash Q_S(n)$, regardless of $n$ - if only for stupid reasons!"




The fact that $S$ knows itself to be $Sigma_1$-complete is what lets the "otherwise" case work.






share|cite|improve this answer









$endgroup$













  • $begingroup$
    Thanks a lot! It's the most jolly answer I've read from you. =) So $S_1$ proves $Con(S)$. Does $S_1$ prove $Con(S+Con(S))$? The argument doesn't work..
    $endgroup$
    – user21820
    Jan 20 at 15:00










  • $begingroup$
    Hi! Did you get any more ideas regarding my question (and comment)? =)
    $endgroup$
    – user21820
    Feb 20 at 6:52











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
});


}
});














draft saved

draft discarded


















StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f2456919%2fsemi-recursive-%25cf%2589-rule%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









1












$begingroup$

Below, all theories are "appropriate" - that is, they are recursively axiomatizable, consistent, and contain PA. Of course this last bit is overkill, but what the hey.



I can't give a full answer, but let me address your question as to whether $PA=PA_1$. The answer is no, and indeed the "semirecursive $omega$-rule operator" has no nontrivial fixed points.



The key is the following fact: that PA is internally $Sigma_1$-complete, that is, that PA proves "PA proves every true $Sigma_1$ fact." See e.g. here. And of course this is hereditary upwards - all the theories we consider will share this property too. (Actually, we really only need $Delta_0$-completeness, but meh.)



Internal $Sigma_1$-completeness lets us make the following neat argument. Given an appropriate theory $S$, let $Q_S(x)$ be the formula "$x$ is not (the Godel number of) a proof of a contradiction in $S$." Then I claim that we have $$Svdashforall x(Svdash Q_S(x)).$$ Consequently the "next step up" from $S$ according to your semi-recursive $omega$-rule is at least (and indeed will wind up being much more than) $S+Con(S)$, since "$forall x(Q_S(x))$" is just "$Con(S)$."



To see this, we reason inside $S$ as follows:




"Fix $n$; we need to show that $S$ proves '$n$ is not (the Godel number of) an $S$-proof of a contradiction.' There are two possibilities. Maybe $n$ is the Godel number of a proof of a contradiction in $S$, in which case $S$ is inconsistent and so we have $Svdash Q_S(n)$ trivially. Otherwise, $n$ is not the Godel number of a proof of a contradiction in $S$, in which case we have $Svdash Q_S(n)$ since 'not-being-a-proof-of' is $Sigma_1$ (indeed, $Delta_0$) and $S$ is $Sigma_1$-complete. Either way, it must be the case that $Svdash Q_S(n)$, regardless of $n$ - if only for stupid reasons!"




The fact that $S$ knows itself to be $Sigma_1$-complete is what lets the "otherwise" case work.






share|cite|improve this answer









$endgroup$













  • $begingroup$
    Thanks a lot! It's the most jolly answer I've read from you. =) So $S_1$ proves $Con(S)$. Does $S_1$ prove $Con(S+Con(S))$? The argument doesn't work..
    $endgroup$
    – user21820
    Jan 20 at 15:00










  • $begingroup$
    Hi! Did you get any more ideas regarding my question (and comment)? =)
    $endgroup$
    – user21820
    Feb 20 at 6:52
















1












$begingroup$

Below, all theories are "appropriate" - that is, they are recursively axiomatizable, consistent, and contain PA. Of course this last bit is overkill, but what the hey.



I can't give a full answer, but let me address your question as to whether $PA=PA_1$. The answer is no, and indeed the "semirecursive $omega$-rule operator" has no nontrivial fixed points.



The key is the following fact: that PA is internally $Sigma_1$-complete, that is, that PA proves "PA proves every true $Sigma_1$ fact." See e.g. here. And of course this is hereditary upwards - all the theories we consider will share this property too. (Actually, we really only need $Delta_0$-completeness, but meh.)



Internal $Sigma_1$-completeness lets us make the following neat argument. Given an appropriate theory $S$, let $Q_S(x)$ be the formula "$x$ is not (the Godel number of) a proof of a contradiction in $S$." Then I claim that we have $$Svdashforall x(Svdash Q_S(x)).$$ Consequently the "next step up" from $S$ according to your semi-recursive $omega$-rule is at least (and indeed will wind up being much more than) $S+Con(S)$, since "$forall x(Q_S(x))$" is just "$Con(S)$."



To see this, we reason inside $S$ as follows:




"Fix $n$; we need to show that $S$ proves '$n$ is not (the Godel number of) an $S$-proof of a contradiction.' There are two possibilities. Maybe $n$ is the Godel number of a proof of a contradiction in $S$, in which case $S$ is inconsistent and so we have $Svdash Q_S(n)$ trivially. Otherwise, $n$ is not the Godel number of a proof of a contradiction in $S$, in which case we have $Svdash Q_S(n)$ since 'not-being-a-proof-of' is $Sigma_1$ (indeed, $Delta_0$) and $S$ is $Sigma_1$-complete. Either way, it must be the case that $Svdash Q_S(n)$, regardless of $n$ - if only for stupid reasons!"




The fact that $S$ knows itself to be $Sigma_1$-complete is what lets the "otherwise" case work.






share|cite|improve this answer









$endgroup$













  • $begingroup$
    Thanks a lot! It's the most jolly answer I've read from you. =) So $S_1$ proves $Con(S)$. Does $S_1$ prove $Con(S+Con(S))$? The argument doesn't work..
    $endgroup$
    – user21820
    Jan 20 at 15:00










  • $begingroup$
    Hi! Did you get any more ideas regarding my question (and comment)? =)
    $endgroup$
    – user21820
    Feb 20 at 6:52














1












1








1





$begingroup$

Below, all theories are "appropriate" - that is, they are recursively axiomatizable, consistent, and contain PA. Of course this last bit is overkill, but what the hey.



I can't give a full answer, but let me address your question as to whether $PA=PA_1$. The answer is no, and indeed the "semirecursive $omega$-rule operator" has no nontrivial fixed points.



The key is the following fact: that PA is internally $Sigma_1$-complete, that is, that PA proves "PA proves every true $Sigma_1$ fact." See e.g. here. And of course this is hereditary upwards - all the theories we consider will share this property too. (Actually, we really only need $Delta_0$-completeness, but meh.)



Internal $Sigma_1$-completeness lets us make the following neat argument. Given an appropriate theory $S$, let $Q_S(x)$ be the formula "$x$ is not (the Godel number of) a proof of a contradiction in $S$." Then I claim that we have $$Svdashforall x(Svdash Q_S(x)).$$ Consequently the "next step up" from $S$ according to your semi-recursive $omega$-rule is at least (and indeed will wind up being much more than) $S+Con(S)$, since "$forall x(Q_S(x))$" is just "$Con(S)$."



To see this, we reason inside $S$ as follows:




"Fix $n$; we need to show that $S$ proves '$n$ is not (the Godel number of) an $S$-proof of a contradiction.' There are two possibilities. Maybe $n$ is the Godel number of a proof of a contradiction in $S$, in which case $S$ is inconsistent and so we have $Svdash Q_S(n)$ trivially. Otherwise, $n$ is not the Godel number of a proof of a contradiction in $S$, in which case we have $Svdash Q_S(n)$ since 'not-being-a-proof-of' is $Sigma_1$ (indeed, $Delta_0$) and $S$ is $Sigma_1$-complete. Either way, it must be the case that $Svdash Q_S(n)$, regardless of $n$ - if only for stupid reasons!"




The fact that $S$ knows itself to be $Sigma_1$-complete is what lets the "otherwise" case work.






share|cite|improve this answer









$endgroup$



Below, all theories are "appropriate" - that is, they are recursively axiomatizable, consistent, and contain PA. Of course this last bit is overkill, but what the hey.



I can't give a full answer, but let me address your question as to whether $PA=PA_1$. The answer is no, and indeed the "semirecursive $omega$-rule operator" has no nontrivial fixed points.



The key is the following fact: that PA is internally $Sigma_1$-complete, that is, that PA proves "PA proves every true $Sigma_1$ fact." See e.g. here. And of course this is hereditary upwards - all the theories we consider will share this property too. (Actually, we really only need $Delta_0$-completeness, but meh.)



Internal $Sigma_1$-completeness lets us make the following neat argument. Given an appropriate theory $S$, let $Q_S(x)$ be the formula "$x$ is not (the Godel number of) a proof of a contradiction in $S$." Then I claim that we have $$Svdashforall x(Svdash Q_S(x)).$$ Consequently the "next step up" from $S$ according to your semi-recursive $omega$-rule is at least (and indeed will wind up being much more than) $S+Con(S)$, since "$forall x(Q_S(x))$" is just "$Con(S)$."



To see this, we reason inside $S$ as follows:




"Fix $n$; we need to show that $S$ proves '$n$ is not (the Godel number of) an $S$-proof of a contradiction.' There are two possibilities. Maybe $n$ is the Godel number of a proof of a contradiction in $S$, in which case $S$ is inconsistent and so we have $Svdash Q_S(n)$ trivially. Otherwise, $n$ is not the Godel number of a proof of a contradiction in $S$, in which case we have $Svdash Q_S(n)$ since 'not-being-a-proof-of' is $Sigma_1$ (indeed, $Delta_0$) and $S$ is $Sigma_1$-complete. Either way, it must be the case that $Svdash Q_S(n)$, regardless of $n$ - if only for stupid reasons!"




The fact that $S$ knows itself to be $Sigma_1$-complete is what lets the "otherwise" case work.







share|cite|improve this answer












share|cite|improve this answer



share|cite|improve this answer










answered Jan 20 at 4:36









Noah SchweberNoah Schweber

126k10150289




126k10150289












  • $begingroup$
    Thanks a lot! It's the most jolly answer I've read from you. =) So $S_1$ proves $Con(S)$. Does $S_1$ prove $Con(S+Con(S))$? The argument doesn't work..
    $endgroup$
    – user21820
    Jan 20 at 15:00










  • $begingroup$
    Hi! Did you get any more ideas regarding my question (and comment)? =)
    $endgroup$
    – user21820
    Feb 20 at 6:52


















  • $begingroup$
    Thanks a lot! It's the most jolly answer I've read from you. =) So $S_1$ proves $Con(S)$. Does $S_1$ prove $Con(S+Con(S))$? The argument doesn't work..
    $endgroup$
    – user21820
    Jan 20 at 15:00










  • $begingroup$
    Hi! Did you get any more ideas regarding my question (and comment)? =)
    $endgroup$
    – user21820
    Feb 20 at 6:52
















$begingroup$
Thanks a lot! It's the most jolly answer I've read from you. =) So $S_1$ proves $Con(S)$. Does $S_1$ prove $Con(S+Con(S))$? The argument doesn't work..
$endgroup$
– user21820
Jan 20 at 15:00




$begingroup$
Thanks a lot! It's the most jolly answer I've read from you. =) So $S_1$ proves $Con(S)$. Does $S_1$ prove $Con(S+Con(S))$? The argument doesn't work..
$endgroup$
– user21820
Jan 20 at 15:00












$begingroup$
Hi! Did you get any more ideas regarding my question (and comment)? =)
$endgroup$
– user21820
Feb 20 at 6:52




$begingroup$
Hi! Did you get any more ideas regarding my question (and comment)? =)
$endgroup$
– user21820
Feb 20 at 6:52


















draft saved

draft discarded




















































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.




draft saved


draft discarded














StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f2456919%2fsemi-recursive-%25cf%2589-rule%23new-answer', 'question_page');
}
);

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







Popular posts from this blog

android studio warns about leanback feature tag usage required on manifest while using Unity exported app?

SQL update select statement

WPF add header to Image with URL pettitions [duplicate]