Semi-recursive ω-rule
$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?
logic computability proof-theory incompleteness
asked Oct 4 '17 at 6:06
user21820user21820
38.8k543152
$endgroup$
|
show 1 more comment
$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?
logic computability proof-theory incompleteness
asked Oct 4 '17 at 6:06
user21820user21820
38.8k543152
$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
|
show 1 more comment
$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?
logic computability proof-theory incompleteness
asked Oct 4 '17 at 6:06
user21820user21820
38.8k543152
$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
logic computability proof-theory incompleteness
asked Oct 4 '17 at 6:06
user21820user21820
38.8k543152
asked Oct 4 '17 at 6:06
user21820user21820
38.8k543152
edited Dec 4 '18 at 3:11
user21820
asked Oct 4 '17 at 6:06
user21820user21820
38.8k543152
asked Oct 4 '17 at 6:06
user21820user21820
38.8k543152
asked Oct 4 '17 at 6:06
user21820user21820
38.8k543152
38.8k543152
$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
|
show 1 more comment
$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
|
show 1 more comment
1 Answer
1
active
oldest
votes
$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.
answered Jan 20 at 4:36
Noah SchweberNoah Schweber
123k10150285
$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
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%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
$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.
answered Jan 20 at 4:36
Noah SchweberNoah Schweber
123k10150285
$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
add a comment |
$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.
answered Jan 20 at 4:36
Noah SchweberNoah Schweber
123k10150285
$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
add a comment |
$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.
answered Jan 20 at 4:36
Noah SchweberNoah Schweber
123k10150285
$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.
answered Jan 20 at 4:36
Noah SchweberNoah Schweber
123k10150285
answered Jan 20 at 4:36
Noah SchweberNoah Schweber
123k10150285
answered Jan 20 at 4:36
Noah SchweberNoah Schweber
123k10150285
answered Jan 20 at 4:36
Noah SchweberNoah Schweber
123k10150285
123k10150285
$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
add a comment |
$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$
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
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%2f2456919%2fsemi-recursive-%25cf%2589-rule%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$
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