proof theoretic ordinal for Robinson's arithmetic
$begingroup$
Does a theory like Robinson's arithmetic have a proof-theoretic ordinal? If so, what is it?
logic ordinal-analysis
edited Dec 6 '18 at 4:32
Andrés E. Caicedo
65.1k8158247
asked Oct 19 '16 at 21:03
Cecil BurrowCecil Burrow
362
$endgroup$
add a comment |
$begingroup$
Does a theory like Robinson's arithmetic have a proof-theoretic ordinal? If so, what is it?
logic ordinal-analysis
edited Dec 6 '18 at 4:32
Andrés E. Caicedo
65.1k8158247
asked Oct 19 '16 at 21:03
Cecil BurrowCecil Burrow
362
$endgroup$
add a comment |
$begingroup$
Does a theory like Robinson's arithmetic have a proof-theoretic ordinal? If so, what is it?
logic ordinal-analysis
edited Dec 6 '18 at 4:32
Andrés E. Caicedo
65.1k8158247
asked Oct 19 '16 at 21:03
Cecil BurrowCecil Burrow
362
$endgroup$
Does a theory like Robinson's arithmetic have a proof-theoretic ordinal? If so, what is it?
logic ordinal-analysis
logic ordinal-analysis
edited Dec 6 '18 at 4:32
Andrés E. Caicedo
65.1k8158247
asked Oct 19 '16 at 21:03
Cecil BurrowCecil Burrow
362
edited Dec 6 '18 at 4:32
Andrés E. Caicedo
65.1k8158247
asked Oct 19 '16 at 21:03
Cecil BurrowCecil Burrow
362
edited Dec 6 '18 at 4:32
Andrés E. Caicedo
65.1k8158247
edited Dec 6 '18 at 4:32
Andrés E. Caicedo
65.1k8158247
edited Dec 6 '18 at 4:32
Andrés E. Caicedo
65.1k8158247
65.1k8158247
asked Oct 19 '16 at 21:03
Cecil BurrowCecil Burrow
362
asked Oct 19 '16 at 21:03
Cecil BurrowCecil Burrow
362
asked Oct 19 '16 at 21:03
Cecil BurrowCecil Burrow
362
362
add a comment |
add a comment |
2 Answers
2
active
oldest
votes
$begingroup$
Well, since $Q$ doesn't even have induction along $mathbb{N}$, I'm dubious that the notion of proof-theoretic ordinal makes sense for it; but if forced, I'd say the answer has to be $omega$. Induction along finite orderings is trivial, so $omega$ is the first ordinal for which it makes sense to ask "Does $Q$ prove induction along this ordinal?," and $Q$ doesn't.
answered Oct 20 '16 at 0:43
Noah SchweberNoah Schweber
122k10149284
$endgroup$
$begingroup$
Well, I guess I was hoping for some ordinal $alpha$ such that the principlw of transfinite induction up to $alpha$ plus some minimal theory (e.g., PRA) proves Con(Q).
$endgroup$
– Cecil Burrow
Oct 20 '16 at 3:10
$begingroup$
@CecilBurrow I believe PRA already proves Con(Q), but I could be wrong. Note that, interestingly, EFA does not prove Con(Q) (see section 3 of this message on the FOM mailing list); Friedman cites Paris and Wilkie for that.
$endgroup$
– Noah Schweber
Oct 20 '16 at 3:19
$begingroup$
I don't know of any proof that PRA proves Con(Q) - a reference would be wonderful!
$endgroup$
– Cecil Burrow
Oct 20 '16 at 3:38
$begingroup$
@CecilBurrow Hm, I'm having trouble finding a source. Section 3H of Moschovakis' notes is where I remember the fact cropping up, but it's not there (although it may still be interesting to you). I'll keep looking . . .
$endgroup$
– Noah Schweber
Oct 20 '16 at 3:44
$begingroup$
On the other hand, the proof theoretic ordinal of PRA is $omega^omega$, while the proof theoretic ordinal of EFA is just $omega^3$. So that suggests that PRA proves Con(EFA) and hence Con(Q) . . .
$endgroup$
– Noah Schweber
Oct 20 '16 at 3:46
add a comment |
$begingroup$
Noah is correct that PRA $vdash$ Con(Q): On p. 139 of the Handbook of Proof Theory, Chapter 2 (available here), Buss shows that $IDelta_0$ + "tetration is total" $vdash$ Con($IDelta_0$), so it certainly proves Con(Q). Since $IDelta_0 subseteq$ PRA and PRA proves tetration total, the result follows.
(This is in response to a side question that came up in the comment thread of Noah's answer, but I don't have the karma to post this as a comment).
answered Sep 24 '18 at 4:11
Morgan SinclaireMorgan Sinclaire
284
$endgroup$
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%2f1976297%2fproof-theoretic-ordinal-for-robinsons-arithmetic%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$
Well, since $Q$ doesn't even have induction along $mathbb{N}$, I'm dubious that the notion of proof-theoretic ordinal makes sense for it; but if forced, I'd say the answer has to be $omega$. Induction along finite orderings is trivial, so $omega$ is the first ordinal for which it makes sense to ask "Does $Q$ prove induction along this ordinal?," and $Q$ doesn't.
answered Oct 20 '16 at 0:43
Noah SchweberNoah Schweber
122k10149284
$endgroup$
$begingroup$
Well, I guess I was hoping for some ordinal $alpha$ such that the principlw of transfinite induction up to $alpha$ plus some minimal theory (e.g., PRA) proves Con(Q).
$endgroup$
– Cecil Burrow
Oct 20 '16 at 3:10
$begingroup$
@CecilBurrow I believe PRA already proves Con(Q), but I could be wrong. Note that, interestingly, EFA does not prove Con(Q) (see section 3 of this message on the FOM mailing list); Friedman cites Paris and Wilkie for that.
$endgroup$
– Noah Schweber
Oct 20 '16 at 3:19
$begingroup$
I don't know of any proof that PRA proves Con(Q) - a reference would be wonderful!
$endgroup$
– Cecil Burrow
Oct 20 '16 at 3:38
$begingroup$
@CecilBurrow Hm, I'm having trouble finding a source. Section 3H of Moschovakis' notes is where I remember the fact cropping up, but it's not there (although it may still be interesting to you). I'll keep looking . . .
$endgroup$
– Noah Schweber
Oct 20 '16 at 3:44
$begingroup$
On the other hand, the proof theoretic ordinal of PRA is $omega^omega$, while the proof theoretic ordinal of EFA is just $omega^3$. So that suggests that PRA proves Con(EFA) and hence Con(Q) . . .
$endgroup$
– Noah Schweber
Oct 20 '16 at 3:46
add a comment |
$begingroup$
Well, since $Q$ doesn't even have induction along $mathbb{N}$, I'm dubious that the notion of proof-theoretic ordinal makes sense for it; but if forced, I'd say the answer has to be $omega$. Induction along finite orderings is trivial, so $omega$ is the first ordinal for which it makes sense to ask "Does $Q$ prove induction along this ordinal?," and $Q$ doesn't.
answered Oct 20 '16 at 0:43
Noah SchweberNoah Schweber
122k10149284
$endgroup$
$begingroup$
Well, I guess I was hoping for some ordinal $alpha$ such that the principlw of transfinite induction up to $alpha$ plus some minimal theory (e.g., PRA) proves Con(Q).
$endgroup$
– Cecil Burrow
Oct 20 '16 at 3:10
$begingroup$
@CecilBurrow I believe PRA already proves Con(Q), but I could be wrong. Note that, interestingly, EFA does not prove Con(Q) (see section 3 of this message on the FOM mailing list); Friedman cites Paris and Wilkie for that.
$endgroup$
– Noah Schweber
Oct 20 '16 at 3:19
$begingroup$
I don't know of any proof that PRA proves Con(Q) - a reference would be wonderful!
$endgroup$
– Cecil Burrow
Oct 20 '16 at 3:38
$begingroup$
@CecilBurrow Hm, I'm having trouble finding a source. Section 3H of Moschovakis' notes is where I remember the fact cropping up, but it's not there (although it may still be interesting to you). I'll keep looking . . .
$endgroup$
– Noah Schweber
Oct 20 '16 at 3:44
$begingroup$
On the other hand, the proof theoretic ordinal of PRA is $omega^omega$, while the proof theoretic ordinal of EFA is just $omega^3$. So that suggests that PRA proves Con(EFA) and hence Con(Q) . . .
$endgroup$
– Noah Schweber
Oct 20 '16 at 3:46
add a comment |
$begingroup$
Well, since $Q$ doesn't even have induction along $mathbb{N}$, I'm dubious that the notion of proof-theoretic ordinal makes sense for it; but if forced, I'd say the answer has to be $omega$. Induction along finite orderings is trivial, so $omega$ is the first ordinal for which it makes sense to ask "Does $Q$ prove induction along this ordinal?," and $Q$ doesn't.
answered Oct 20 '16 at 0:43
Noah SchweberNoah Schweber
122k10149284
$endgroup$
Well, since $Q$ doesn't even have induction along $mathbb{N}$, I'm dubious that the notion of proof-theoretic ordinal makes sense for it; but if forced, I'd say the answer has to be $omega$. Induction along finite orderings is trivial, so $omega$ is the first ordinal for which it makes sense to ask "Does $Q$ prove induction along this ordinal?," and $Q$ doesn't.
answered Oct 20 '16 at 0:43
Noah SchweberNoah Schweber
122k10149284
answered Oct 20 '16 at 0:43
Noah SchweberNoah Schweber
122k10149284
answered Oct 20 '16 at 0:43
Noah SchweberNoah Schweber
122k10149284
answered Oct 20 '16 at 0:43
Noah SchweberNoah Schweber
122k10149284
122k10149284
$begingroup$
Well, I guess I was hoping for some ordinal $alpha$ such that the principlw of transfinite induction up to $alpha$ plus some minimal theory (e.g., PRA) proves Con(Q).
$endgroup$
– Cecil Burrow
Oct 20 '16 at 3:10
$begingroup$
@CecilBurrow I believe PRA already proves Con(Q), but I could be wrong. Note that, interestingly, EFA does not prove Con(Q) (see section 3 of this message on the FOM mailing list); Friedman cites Paris and Wilkie for that.
$endgroup$
– Noah Schweber
Oct 20 '16 at 3:19
$begingroup$
I don't know of any proof that PRA proves Con(Q) - a reference would be wonderful!
$endgroup$
– Cecil Burrow
Oct 20 '16 at 3:38
$begingroup$
@CecilBurrow Hm, I'm having trouble finding a source. Section 3H of Moschovakis' notes is where I remember the fact cropping up, but it's not there (although it may still be interesting to you). I'll keep looking . . .
$endgroup$
– Noah Schweber
Oct 20 '16 at 3:44
$begingroup$
On the other hand, the proof theoretic ordinal of PRA is $omega^omega$, while the proof theoretic ordinal of EFA is just $omega^3$. So that suggests that PRA proves Con(EFA) and hence Con(Q) . . .
$endgroup$
– Noah Schweber
Oct 20 '16 at 3:46
add a comment |
$begingroup$
Well, I guess I was hoping for some ordinal $alpha$ such that the principlw of transfinite induction up to $alpha$ plus some minimal theory (e.g., PRA) proves Con(Q).
$endgroup$
– Cecil Burrow
Oct 20 '16 at 3:10
$begingroup$
@CecilBurrow I believe PRA already proves Con(Q), but I could be wrong. Note that, interestingly, EFA does not prove Con(Q) (see section 3 of this message on the FOM mailing list); Friedman cites Paris and Wilkie for that.
$endgroup$
– Noah Schweber
Oct 20 '16 at 3:19
$begingroup$
I don't know of any proof that PRA proves Con(Q) - a reference would be wonderful!
$endgroup$
– Cecil Burrow
Oct 20 '16 at 3:38
$begingroup$
@CecilBurrow Hm, I'm having trouble finding a source. Section 3H of Moschovakis' notes is where I remember the fact cropping up, but it's not there (although it may still be interesting to you). I'll keep looking . . .
$endgroup$
– Noah Schweber
Oct 20 '16 at 3:44
$begingroup$
On the other hand, the proof theoretic ordinal of PRA is $omega^omega$, while the proof theoretic ordinal of EFA is just $omega^3$. So that suggests that PRA proves Con(EFA) and hence Con(Q) . . .
$endgroup$
– Noah Schweber
Oct 20 '16 at 3:46
$begingroup$
Well, I guess I was hoping for some ordinal $alpha$ such that the principlw of transfinite induction up to $alpha$ plus some minimal theory (e.g., PRA) proves Con(Q).
$endgroup$
– Cecil Burrow
Oct 20 '16 at 3:10
$begingroup$
Well, I guess I was hoping for some ordinal $alpha$ such that the principlw of transfinite induction up to $alpha$ plus some minimal theory (e.g., PRA) proves Con(Q).
$endgroup$
– Cecil Burrow
Oct 20 '16 at 3:10
$begingroup$
@CecilBurrow I believe PRA already proves Con(Q), but I could be wrong. Note that, interestingly, EFA does not prove Con(Q) (see section 3 of this message on the FOM mailing list); Friedman cites Paris and Wilkie for that.
$endgroup$
– Noah Schweber
Oct 20 '16 at 3:19
$begingroup$
@CecilBurrow I believe PRA already proves Con(Q), but I could be wrong. Note that, interestingly, EFA does not prove Con(Q) (see section 3 of this message on the FOM mailing list); Friedman cites Paris and Wilkie for that.
$endgroup$
– Noah Schweber
Oct 20 '16 at 3:19
$begingroup$
I don't know of any proof that PRA proves Con(Q) - a reference would be wonderful!
$endgroup$
– Cecil Burrow
Oct 20 '16 at 3:38
$begingroup$
I don't know of any proof that PRA proves Con(Q) - a reference would be wonderful!
$endgroup$
– Cecil Burrow
Oct 20 '16 at 3:38
$begingroup$
@CecilBurrow Hm, I'm having trouble finding a source. Section 3H of Moschovakis' notes is where I remember the fact cropping up, but it's not there (although it may still be interesting to you). I'll keep looking . . .
$endgroup$
– Noah Schweber
Oct 20 '16 at 3:44
$begingroup$
@CecilBurrow Hm, I'm having trouble finding a source. Section 3H of Moschovakis' notes is where I remember the fact cropping up, but it's not there (although it may still be interesting to you). I'll keep looking . . .
$endgroup$
– Noah Schweber
Oct 20 '16 at 3:44
$begingroup$
On the other hand, the proof theoretic ordinal of PRA is $omega^omega$, while the proof theoretic ordinal of EFA is just $omega^3$. So that suggests that PRA proves Con(EFA) and hence Con(Q) . . .
$endgroup$
– Noah Schweber
Oct 20 '16 at 3:46
$begingroup$
On the other hand, the proof theoretic ordinal of PRA is $omega^omega$, while the proof theoretic ordinal of EFA is just $omega^3$. So that suggests that PRA proves Con(EFA) and hence Con(Q) . . .
$endgroup$
– Noah Schweber
Oct 20 '16 at 3:46
add a comment |
$begingroup$
Noah is correct that PRA $vdash$ Con(Q): On p. 139 of the Handbook of Proof Theory, Chapter 2 (available here), Buss shows that $IDelta_0$ + "tetration is total" $vdash$ Con($IDelta_0$), so it certainly proves Con(Q). Since $IDelta_0 subseteq$ PRA and PRA proves tetration total, the result follows.
(This is in response to a side question that came up in the comment thread of Noah's answer, but I don't have the karma to post this as a comment).
answered Sep 24 '18 at 4:11
Morgan SinclaireMorgan Sinclaire
284
$endgroup$
add a comment |
$begingroup$
Noah is correct that PRA $vdash$ Con(Q): On p. 139 of the Handbook of Proof Theory, Chapter 2 (available here), Buss shows that $IDelta_0$ + "tetration is total" $vdash$ Con($IDelta_0$), so it certainly proves Con(Q). Since $IDelta_0 subseteq$ PRA and PRA proves tetration total, the result follows.
(This is in response to a side question that came up in the comment thread of Noah's answer, but I don't have the karma to post this as a comment).
answered Sep 24 '18 at 4:11
Morgan SinclaireMorgan Sinclaire
284
$endgroup$
add a comment |
$begingroup$
Noah is correct that PRA $vdash$ Con(Q): On p. 139 of the Handbook of Proof Theory, Chapter 2 (available here), Buss shows that $IDelta_0$ + "tetration is total" $vdash$ Con($IDelta_0$), so it certainly proves Con(Q). Since $IDelta_0 subseteq$ PRA and PRA proves tetration total, the result follows.
(This is in response to a side question that came up in the comment thread of Noah's answer, but I don't have the karma to post this as a comment).
answered Sep 24 '18 at 4:11
Morgan SinclaireMorgan Sinclaire
284
$endgroup$
Noah is correct that PRA $vdash$ Con(Q): On p. 139 of the Handbook of Proof Theory, Chapter 2 (available here), Buss shows that $IDelta_0$ + "tetration is total" $vdash$ Con($IDelta_0$), so it certainly proves Con(Q). Since $IDelta_0 subseteq$ PRA and PRA proves tetration total, the result follows.
(This is in response to a side question that came up in the comment thread of Noah's answer, but I don't have the karma to post this as a comment).
answered Sep 24 '18 at 4:11
Morgan SinclaireMorgan Sinclaire
284
answered Sep 24 '18 at 4:11
Morgan SinclaireMorgan Sinclaire
284
answered Sep 24 '18 at 4:11
Morgan SinclaireMorgan Sinclaire
284
answered Sep 24 '18 at 4:11
Morgan SinclaireMorgan Sinclaire
284
284
add a comment |
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%2f1976297%2fproof-theoretic-ordinal-for-robinsons-arithmetic%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
