Small proof-theoretic ordinals
$begingroup$
Where to find proofs of the following:
1) proof-theoretic ordinal of $ISigma_0$, which is Robinson's Q arithmetic with induction on $Sigma_0$ formulas, is $omega^2$?
2) proof-theoretic ordinal of $ISigma_0+exp$, which is $ISigma_0$ augmented with the fact that exponentiation is total, is $omega^3$?
3) proof-theoretic ordinal of $ISigma_1$, which is Robinson's Q arithmetic with induction on $Sigma_1$ formulas, is $omega^omega$?
Is there any arithmetic (e.g. Robinson's $Q$ with induction on open formulas) with proof-theoretic ordinal less than $omega^2$?
logic reference-request proof-theory ordinal-analysis
$endgroup$
add a comment |
$begingroup$
Where to find proofs of the following:
1) proof-theoretic ordinal of $ISigma_0$, which is Robinson's Q arithmetic with induction on $Sigma_0$ formulas, is $omega^2$?
2) proof-theoretic ordinal of $ISigma_0+exp$, which is $ISigma_0$ augmented with the fact that exponentiation is total, is $omega^3$?
3) proof-theoretic ordinal of $ISigma_1$, which is Robinson's Q arithmetic with induction on $Sigma_1$ formulas, is $omega^omega$?
Is there any arithmetic (e.g. Robinson's $Q$ with induction on open formulas) with proof-theoretic ordinal less than $omega^2$?
logic reference-request proof-theory ordinal-analysis
$endgroup$
$begingroup$
I'm not really sure why this has votes to close as "unclear," it is a little vague but I think is still a reasonable question.
$endgroup$
– Noah Schweber
Jun 24 '17 at 17:21
6
$begingroup$
I think this closure was quite silly. Note that of those voting to close,only one appears to have any background in logic. I'm not sure what was unclear about this question - all terms used are standard in the literature, and the issue (that ordinal analysis is quite odd when the theory gets sufficiently weak) is a perfectly understandable one. We don't demand e.g. that a question on algebraic topology define the fundamental group - so what exactly is unclear, here? I've voted to reopen.
$endgroup$
– Noah Schweber
Jun 25 '17 at 16:33
$begingroup$
@NoahSchweber Thanks, Noah. I really hoped somebody would be able to help. What I can easily find in the literature is about theories stronger than PA. Wikipedia gives some results on weak theories, but without proper citations. I also read "Weak Systems of Arithmetic" by John Baez [golem.ph.utexas.edu/category/2011/10/weak_systems_of_arithmetic.html], but there is nothing substantial there, either.
$endgroup$
– George Levsky
Jun 25 '17 at 22:49
4
$begingroup$
George, this is a nice question. If you end up not receiving an answer after a reasonable amount of time (a week or two?), please consider reposting in on MathOverflow.
$endgroup$
– Andrés E. Caicedo
Jun 25 '17 at 23:47
add a comment |
$begingroup$
Where to find proofs of the following:
1) proof-theoretic ordinal of $ISigma_0$, which is Robinson's Q arithmetic with induction on $Sigma_0$ formulas, is $omega^2$?
2) proof-theoretic ordinal of $ISigma_0+exp$, which is $ISigma_0$ augmented with the fact that exponentiation is total, is $omega^3$?
3) proof-theoretic ordinal of $ISigma_1$, which is Robinson's Q arithmetic with induction on $Sigma_1$ formulas, is $omega^omega$?
Is there any arithmetic (e.g. Robinson's $Q$ with induction on open formulas) with proof-theoretic ordinal less than $omega^2$?
logic reference-request proof-theory ordinal-analysis
$endgroup$
Where to find proofs of the following:
1) proof-theoretic ordinal of $ISigma_0$, which is Robinson's Q arithmetic with induction on $Sigma_0$ formulas, is $omega^2$?
2) proof-theoretic ordinal of $ISigma_0+exp$, which is $ISigma_0$ augmented with the fact that exponentiation is total, is $omega^3$?
3) proof-theoretic ordinal of $ISigma_1$, which is Robinson's Q arithmetic with induction on $Sigma_1$ formulas, is $omega^omega$?
Is there any arithmetic (e.g. Robinson's $Q$ with induction on open formulas) with proof-theoretic ordinal less than $omega^2$?
logic reference-request proof-theory ordinal-analysis
logic reference-request proof-theory ordinal-analysis
edited Dec 6 '18 at 4:31
Andrés E. Caicedo
65.2k8158247
65.2k8158247
asked Jun 24 '17 at 13:03
George LevskyGeorge Levsky
613
613
$begingroup$
I'm not really sure why this has votes to close as "unclear," it is a little vague but I think is still a reasonable question.
$endgroup$
– Noah Schweber
Jun 24 '17 at 17:21
6
$begingroup$
I think this closure was quite silly. Note that of those voting to close,only one appears to have any background in logic. I'm not sure what was unclear about this question - all terms used are standard in the literature, and the issue (that ordinal analysis is quite odd when the theory gets sufficiently weak) is a perfectly understandable one. We don't demand e.g. that a question on algebraic topology define the fundamental group - so what exactly is unclear, here? I've voted to reopen.
$endgroup$
– Noah Schweber
Jun 25 '17 at 16:33
$begingroup$
@NoahSchweber Thanks, Noah. I really hoped somebody would be able to help. What I can easily find in the literature is about theories stronger than PA. Wikipedia gives some results on weak theories, but without proper citations. I also read "Weak Systems of Arithmetic" by John Baez [golem.ph.utexas.edu/category/2011/10/weak_systems_of_arithmetic.html], but there is nothing substantial there, either.
$endgroup$
– George Levsky
Jun 25 '17 at 22:49
4
$begingroup$
George, this is a nice question. If you end up not receiving an answer after a reasonable amount of time (a week or two?), please consider reposting in on MathOverflow.
$endgroup$
– Andrés E. Caicedo
Jun 25 '17 at 23:47
add a comment |
$begingroup$
I'm not really sure why this has votes to close as "unclear," it is a little vague but I think is still a reasonable question.
$endgroup$
– Noah Schweber
Jun 24 '17 at 17:21
6
$begingroup$
I think this closure was quite silly. Note that of those voting to close,only one appears to have any background in logic. I'm not sure what was unclear about this question - all terms used are standard in the literature, and the issue (that ordinal analysis is quite odd when the theory gets sufficiently weak) is a perfectly understandable one. We don't demand e.g. that a question on algebraic topology define the fundamental group - so what exactly is unclear, here? I've voted to reopen.
$endgroup$
– Noah Schweber
Jun 25 '17 at 16:33
$begingroup$
@NoahSchweber Thanks, Noah. I really hoped somebody would be able to help. What I can easily find in the literature is about theories stronger than PA. Wikipedia gives some results on weak theories, but without proper citations. I also read "Weak Systems of Arithmetic" by John Baez [golem.ph.utexas.edu/category/2011/10/weak_systems_of_arithmetic.html], but there is nothing substantial there, either.
$endgroup$
– George Levsky
Jun 25 '17 at 22:49
4
$begingroup$
George, this is a nice question. If you end up not receiving an answer after a reasonable amount of time (a week or two?), please consider reposting in on MathOverflow.
$endgroup$
– Andrés E. Caicedo
Jun 25 '17 at 23:47
$begingroup$
I'm not really sure why this has votes to close as "unclear," it is a little vague but I think is still a reasonable question.
$endgroup$
– Noah Schweber
Jun 24 '17 at 17:21
$begingroup$
I'm not really sure why this has votes to close as "unclear," it is a little vague but I think is still a reasonable question.
$endgroup$
– Noah Schweber
Jun 24 '17 at 17:21
6
6
$begingroup$
I think this closure was quite silly. Note that of those voting to close,only one appears to have any background in logic. I'm not sure what was unclear about this question - all terms used are standard in the literature, and the issue (that ordinal analysis is quite odd when the theory gets sufficiently weak) is a perfectly understandable one. We don't demand e.g. that a question on algebraic topology define the fundamental group - so what exactly is unclear, here? I've voted to reopen.
$endgroup$
– Noah Schweber
Jun 25 '17 at 16:33
$begingroup$
I think this closure was quite silly. Note that of those voting to close,only one appears to have any background in logic. I'm not sure what was unclear about this question - all terms used are standard in the literature, and the issue (that ordinal analysis is quite odd when the theory gets sufficiently weak) is a perfectly understandable one. We don't demand e.g. that a question on algebraic topology define the fundamental group - so what exactly is unclear, here? I've voted to reopen.
$endgroup$
– Noah Schweber
Jun 25 '17 at 16:33
$begingroup$
@NoahSchweber Thanks, Noah. I really hoped somebody would be able to help. What I can easily find in the literature is about theories stronger than PA. Wikipedia gives some results on weak theories, but without proper citations. I also read "Weak Systems of Arithmetic" by John Baez [golem.ph.utexas.edu/category/2011/10/weak_systems_of_arithmetic.html], but there is nothing substantial there, either.
$endgroup$
– George Levsky
Jun 25 '17 at 22:49
$begingroup$
@NoahSchweber Thanks, Noah. I really hoped somebody would be able to help. What I can easily find in the literature is about theories stronger than PA. Wikipedia gives some results on weak theories, but without proper citations. I also read "Weak Systems of Arithmetic" by John Baez [golem.ph.utexas.edu/category/2011/10/weak_systems_of_arithmetic.html], but there is nothing substantial there, either.
$endgroup$
– George Levsky
Jun 25 '17 at 22:49
4
4
$begingroup$
George, this is a nice question. If you end up not receiving an answer after a reasonable amount of time (a week or two?), please consider reposting in on MathOverflow.
$endgroup$
– Andrés E. Caicedo
Jun 25 '17 at 23:47
$begingroup$
George, this is a nice question. If you end up not receiving an answer after a reasonable amount of time (a week or two?), please consider reposting in on MathOverflow.
$endgroup$
– Andrés E. Caicedo
Jun 25 '17 at 23:47
add a comment |
1 Answer
1
active
oldest
votes
$begingroup$
While natural theories extending EFA (also called IΣ$_0$+exp or ERA or EA) appear well-ordered under $Π^0_2$ provability, the setting of exact $Π^0_2$ ordinal values for theories below PRA is a matter of convention. However, a reasonable convention is obtained using the Hardy hierarchy of functions:
Set $h_0(x) = x$
$h_{α+1}(x) = h_α(x+1)$
$h_{α}(x) = h_{α[x]}(x)$ for limit $α$ where $α[..]$ is a canonical fundamental sequence for $α$. The link defines a canonical choice below $Γ_0$, but basically we diagonalize over lower indices of $h$ in a reasonable way.
For a theory $T$ including basic arithmetic:
$|T|_{Π^0_2}$ = sup($α$: $T$ proves $h_α$ is total).
Note that $|T|_{Π^0_2}$ formally depends not only on the ordinal but also on the fundamental sequences (and on the formulas defining them). However, for canonical ordinal notation systems, different natural choices of fundamental sequences appear to be equivalent in that for $T$ extending EFA, they give the same $|T|_{Π^0_2}$. The reason is that different reasonable choices will give the same growth rate of $h_{α}(x)$ up to an elementary increase or decrease in the value of $x$.
The remarkable property is that for natural theories extending EFA, $Π^0_2$ provability is completely determined (and well-ordered) by $|T|_{Π^0_2}$. A caveat is that there are different notions of 'natural' (and counterexamples like EFA+Con(PA)), and also many natural theories are beyond known canonical ordinal notation systems.
Now, $h_{ωm+n}(x)=2^m (x+n)$, and for appropriate $α$ and $β$, $h_{α+β}(x) = h_α(h_β(x))$, and $h_{αω}(x)=h_α^x(x)$ (superscript indicates iteration). (The exact equality depends on the choice of fundamental sequences and that $α+β$ (resp. $αω$) does not truncate $α$.)
For every $m$, IΔ$_0$ (also called IΣ$_0$) proves that $2^m x$ is total, but it does not prove that $2^x x$ is total, so the ordinal is $ω^2$.
$h_{ω^2 n}$ approximately corresponds to a stack of $n$ exponentials, which is elementary for a particular $n$ but not as a function of $n$, hence the $ω^3$ ordinal.
$h_{ω^n}$ approximately corresponds to the $n$th level (or so) of the Ackermann function and thus provably total in PRA, but $h_{ω^ω}$ grows like the full Ackermann function, which is beyond PRA. $Σ^0_1$-PA (also called IΣ$_1$) is $Π^0_2$ conservative over PRA and thus has the same $Π^0_2$ ordinal.
A few notes:
* IΔ$_0$ is already interpretable in Robinson arithmetic Q, and there is no standard assignment of ordinals below that.
* Since total functions are closed under composition, every $|T|_{Π^0_2}$ is a power of $ω$.
* If we had set $h_{α+1}(x) = h_α(2^x)$, then $|mathrm{EFA}|_{Π^0_2}$ would be $ω$, hence the caveat about convention.
* There also are other approaches to ordinals for weak theories, including by embedding the theory into a second order theory using a free second order variable $X$ and extending induction (and other axioms) to formulas using $X$ as a predicate, and getting the $Π^1_1$ ordinal of that theory. I think you would still get the $ω^2$ and $ω^3$ (and $ω^ω$) ordinals, but I have not seen the proof either.
$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%2f2334724%2fsmall-proof-theoretic-ordinals%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$
While natural theories extending EFA (also called IΣ$_0$+exp or ERA or EA) appear well-ordered under $Π^0_2$ provability, the setting of exact $Π^0_2$ ordinal values for theories below PRA is a matter of convention. However, a reasonable convention is obtained using the Hardy hierarchy of functions:
Set $h_0(x) = x$
$h_{α+1}(x) = h_α(x+1)$
$h_{α}(x) = h_{α[x]}(x)$ for limit $α$ where $α[..]$ is a canonical fundamental sequence for $α$. The link defines a canonical choice below $Γ_0$, but basically we diagonalize over lower indices of $h$ in a reasonable way.
For a theory $T$ including basic arithmetic:
$|T|_{Π^0_2}$ = sup($α$: $T$ proves $h_α$ is total).
Note that $|T|_{Π^0_2}$ formally depends not only on the ordinal but also on the fundamental sequences (and on the formulas defining them). However, for canonical ordinal notation systems, different natural choices of fundamental sequences appear to be equivalent in that for $T$ extending EFA, they give the same $|T|_{Π^0_2}$. The reason is that different reasonable choices will give the same growth rate of $h_{α}(x)$ up to an elementary increase or decrease in the value of $x$.
The remarkable property is that for natural theories extending EFA, $Π^0_2$ provability is completely determined (and well-ordered) by $|T|_{Π^0_2}$. A caveat is that there are different notions of 'natural' (and counterexamples like EFA+Con(PA)), and also many natural theories are beyond known canonical ordinal notation systems.
Now, $h_{ωm+n}(x)=2^m (x+n)$, and for appropriate $α$ and $β$, $h_{α+β}(x) = h_α(h_β(x))$, and $h_{αω}(x)=h_α^x(x)$ (superscript indicates iteration). (The exact equality depends on the choice of fundamental sequences and that $α+β$ (resp. $αω$) does not truncate $α$.)
For every $m$, IΔ$_0$ (also called IΣ$_0$) proves that $2^m x$ is total, but it does not prove that $2^x x$ is total, so the ordinal is $ω^2$.
$h_{ω^2 n}$ approximately corresponds to a stack of $n$ exponentials, which is elementary for a particular $n$ but not as a function of $n$, hence the $ω^3$ ordinal.
$h_{ω^n}$ approximately corresponds to the $n$th level (or so) of the Ackermann function and thus provably total in PRA, but $h_{ω^ω}$ grows like the full Ackermann function, which is beyond PRA. $Σ^0_1$-PA (also called IΣ$_1$) is $Π^0_2$ conservative over PRA and thus has the same $Π^0_2$ ordinal.
A few notes:
* IΔ$_0$ is already interpretable in Robinson arithmetic Q, and there is no standard assignment of ordinals below that.
* Since total functions are closed under composition, every $|T|_{Π^0_2}$ is a power of $ω$.
* If we had set $h_{α+1}(x) = h_α(2^x)$, then $|mathrm{EFA}|_{Π^0_2}$ would be $ω$, hence the caveat about convention.
* There also are other approaches to ordinals for weak theories, including by embedding the theory into a second order theory using a free second order variable $X$ and extending induction (and other axioms) to formulas using $X$ as a predicate, and getting the $Π^1_1$ ordinal of that theory. I think you would still get the $ω^2$ and $ω^3$ (and $ω^ω$) ordinals, but I have not seen the proof either.
$endgroup$
add a comment |
$begingroup$
While natural theories extending EFA (also called IΣ$_0$+exp or ERA or EA) appear well-ordered under $Π^0_2$ provability, the setting of exact $Π^0_2$ ordinal values for theories below PRA is a matter of convention. However, a reasonable convention is obtained using the Hardy hierarchy of functions:
Set $h_0(x) = x$
$h_{α+1}(x) = h_α(x+1)$
$h_{α}(x) = h_{α[x]}(x)$ for limit $α$ where $α[..]$ is a canonical fundamental sequence for $α$. The link defines a canonical choice below $Γ_0$, but basically we diagonalize over lower indices of $h$ in a reasonable way.
For a theory $T$ including basic arithmetic:
$|T|_{Π^0_2}$ = sup($α$: $T$ proves $h_α$ is total).
Note that $|T|_{Π^0_2}$ formally depends not only on the ordinal but also on the fundamental sequences (and on the formulas defining them). However, for canonical ordinal notation systems, different natural choices of fundamental sequences appear to be equivalent in that for $T$ extending EFA, they give the same $|T|_{Π^0_2}$. The reason is that different reasonable choices will give the same growth rate of $h_{α}(x)$ up to an elementary increase or decrease in the value of $x$.
The remarkable property is that for natural theories extending EFA, $Π^0_2$ provability is completely determined (and well-ordered) by $|T|_{Π^0_2}$. A caveat is that there are different notions of 'natural' (and counterexamples like EFA+Con(PA)), and also many natural theories are beyond known canonical ordinal notation systems.
Now, $h_{ωm+n}(x)=2^m (x+n)$, and for appropriate $α$ and $β$, $h_{α+β}(x) = h_α(h_β(x))$, and $h_{αω}(x)=h_α^x(x)$ (superscript indicates iteration). (The exact equality depends on the choice of fundamental sequences and that $α+β$ (resp. $αω$) does not truncate $α$.)
For every $m$, IΔ$_0$ (also called IΣ$_0$) proves that $2^m x$ is total, but it does not prove that $2^x x$ is total, so the ordinal is $ω^2$.
$h_{ω^2 n}$ approximately corresponds to a stack of $n$ exponentials, which is elementary for a particular $n$ but not as a function of $n$, hence the $ω^3$ ordinal.
$h_{ω^n}$ approximately corresponds to the $n$th level (or so) of the Ackermann function and thus provably total in PRA, but $h_{ω^ω}$ grows like the full Ackermann function, which is beyond PRA. $Σ^0_1$-PA (also called IΣ$_1$) is $Π^0_2$ conservative over PRA and thus has the same $Π^0_2$ ordinal.
A few notes:
* IΔ$_0$ is already interpretable in Robinson arithmetic Q, and there is no standard assignment of ordinals below that.
* Since total functions are closed under composition, every $|T|_{Π^0_2}$ is a power of $ω$.
* If we had set $h_{α+1}(x) = h_α(2^x)$, then $|mathrm{EFA}|_{Π^0_2}$ would be $ω$, hence the caveat about convention.
* There also are other approaches to ordinals for weak theories, including by embedding the theory into a second order theory using a free second order variable $X$ and extending induction (and other axioms) to formulas using $X$ as a predicate, and getting the $Π^1_1$ ordinal of that theory. I think you would still get the $ω^2$ and $ω^3$ (and $ω^ω$) ordinals, but I have not seen the proof either.
$endgroup$
add a comment |
$begingroup$
While natural theories extending EFA (also called IΣ$_0$+exp or ERA or EA) appear well-ordered under $Π^0_2$ provability, the setting of exact $Π^0_2$ ordinal values for theories below PRA is a matter of convention. However, a reasonable convention is obtained using the Hardy hierarchy of functions:
Set $h_0(x) = x$
$h_{α+1}(x) = h_α(x+1)$
$h_{α}(x) = h_{α[x]}(x)$ for limit $α$ where $α[..]$ is a canonical fundamental sequence for $α$. The link defines a canonical choice below $Γ_0$, but basically we diagonalize over lower indices of $h$ in a reasonable way.
For a theory $T$ including basic arithmetic:
$|T|_{Π^0_2}$ = sup($α$: $T$ proves $h_α$ is total).
Note that $|T|_{Π^0_2}$ formally depends not only on the ordinal but also on the fundamental sequences (and on the formulas defining them). However, for canonical ordinal notation systems, different natural choices of fundamental sequences appear to be equivalent in that for $T$ extending EFA, they give the same $|T|_{Π^0_2}$. The reason is that different reasonable choices will give the same growth rate of $h_{α}(x)$ up to an elementary increase or decrease in the value of $x$.
The remarkable property is that for natural theories extending EFA, $Π^0_2$ provability is completely determined (and well-ordered) by $|T|_{Π^0_2}$. A caveat is that there are different notions of 'natural' (and counterexamples like EFA+Con(PA)), and also many natural theories are beyond known canonical ordinal notation systems.
Now, $h_{ωm+n}(x)=2^m (x+n)$, and for appropriate $α$ and $β$, $h_{α+β}(x) = h_α(h_β(x))$, and $h_{αω}(x)=h_α^x(x)$ (superscript indicates iteration). (The exact equality depends on the choice of fundamental sequences and that $α+β$ (resp. $αω$) does not truncate $α$.)
For every $m$, IΔ$_0$ (also called IΣ$_0$) proves that $2^m x$ is total, but it does not prove that $2^x x$ is total, so the ordinal is $ω^2$.
$h_{ω^2 n}$ approximately corresponds to a stack of $n$ exponentials, which is elementary for a particular $n$ but not as a function of $n$, hence the $ω^3$ ordinal.
$h_{ω^n}$ approximately corresponds to the $n$th level (or so) of the Ackermann function and thus provably total in PRA, but $h_{ω^ω}$ grows like the full Ackermann function, which is beyond PRA. $Σ^0_1$-PA (also called IΣ$_1$) is $Π^0_2$ conservative over PRA and thus has the same $Π^0_2$ ordinal.
A few notes:
* IΔ$_0$ is already interpretable in Robinson arithmetic Q, and there is no standard assignment of ordinals below that.
* Since total functions are closed under composition, every $|T|_{Π^0_2}$ is a power of $ω$.
* If we had set $h_{α+1}(x) = h_α(2^x)$, then $|mathrm{EFA}|_{Π^0_2}$ would be $ω$, hence the caveat about convention.
* There also are other approaches to ordinals for weak theories, including by embedding the theory into a second order theory using a free second order variable $X$ and extending induction (and other axioms) to formulas using $X$ as a predicate, and getting the $Π^1_1$ ordinal of that theory. I think you would still get the $ω^2$ and $ω^3$ (and $ω^ω$) ordinals, but I have not seen the proof either.
$endgroup$
While natural theories extending EFA (also called IΣ$_0$+exp or ERA or EA) appear well-ordered under $Π^0_2$ provability, the setting of exact $Π^0_2$ ordinal values for theories below PRA is a matter of convention. However, a reasonable convention is obtained using the Hardy hierarchy of functions:
Set $h_0(x) = x$
$h_{α+1}(x) = h_α(x+1)$
$h_{α}(x) = h_{α[x]}(x)$ for limit $α$ where $α[..]$ is a canonical fundamental sequence for $α$. The link defines a canonical choice below $Γ_0$, but basically we diagonalize over lower indices of $h$ in a reasonable way.
For a theory $T$ including basic arithmetic:
$|T|_{Π^0_2}$ = sup($α$: $T$ proves $h_α$ is total).
Note that $|T|_{Π^0_2}$ formally depends not only on the ordinal but also on the fundamental sequences (and on the formulas defining them). However, for canonical ordinal notation systems, different natural choices of fundamental sequences appear to be equivalent in that for $T$ extending EFA, they give the same $|T|_{Π^0_2}$. The reason is that different reasonable choices will give the same growth rate of $h_{α}(x)$ up to an elementary increase or decrease in the value of $x$.
The remarkable property is that for natural theories extending EFA, $Π^0_2$ provability is completely determined (and well-ordered) by $|T|_{Π^0_2}$. A caveat is that there are different notions of 'natural' (and counterexamples like EFA+Con(PA)), and also many natural theories are beyond known canonical ordinal notation systems.
Now, $h_{ωm+n}(x)=2^m (x+n)$, and for appropriate $α$ and $β$, $h_{α+β}(x) = h_α(h_β(x))$, and $h_{αω}(x)=h_α^x(x)$ (superscript indicates iteration). (The exact equality depends on the choice of fundamental sequences and that $α+β$ (resp. $αω$) does not truncate $α$.)
For every $m$, IΔ$_0$ (also called IΣ$_0$) proves that $2^m x$ is total, but it does not prove that $2^x x$ is total, so the ordinal is $ω^2$.
$h_{ω^2 n}$ approximately corresponds to a stack of $n$ exponentials, which is elementary for a particular $n$ but not as a function of $n$, hence the $ω^3$ ordinal.
$h_{ω^n}$ approximately corresponds to the $n$th level (or so) of the Ackermann function and thus provably total in PRA, but $h_{ω^ω}$ grows like the full Ackermann function, which is beyond PRA. $Σ^0_1$-PA (also called IΣ$_1$) is $Π^0_2$ conservative over PRA and thus has the same $Π^0_2$ ordinal.
A few notes:
* IΔ$_0$ is already interpretable in Robinson arithmetic Q, and there is no standard assignment of ordinals below that.
* Since total functions are closed under composition, every $|T|_{Π^0_2}$ is a power of $ω$.
* If we had set $h_{α+1}(x) = h_α(2^x)$, then $|mathrm{EFA}|_{Π^0_2}$ would be $ω$, hence the caveat about convention.
* There also are other approaches to ordinals for weak theories, including by embedding the theory into a second order theory using a free second order variable $X$ and extending induction (and other axioms) to formulas using $X$ as a predicate, and getting the $Π^1_1$ ordinal of that theory. I think you would still get the $ω^2$ and $ω^3$ (and $ω^ω$) ordinals, but I have not seen the proof either.
edited Aug 31 '17 at 4:06
answered Aug 31 '17 at 3:01
Dmytro TaranovskyDmytro Taranovsky
4511316
4511316
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%2f2334724%2fsmall-proof-theoretic-ordinals%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$
I'm not really sure why this has votes to close as "unclear," it is a little vague but I think is still a reasonable question.
$endgroup$
– Noah Schweber
Jun 24 '17 at 17:21
6
$begingroup$
I think this closure was quite silly. Note that of those voting to close,only one appears to have any background in logic. I'm not sure what was unclear about this question - all terms used are standard in the literature, and the issue (that ordinal analysis is quite odd when the theory gets sufficiently weak) is a perfectly understandable one. We don't demand e.g. that a question on algebraic topology define the fundamental group - so what exactly is unclear, here? I've voted to reopen.
$endgroup$
– Noah Schweber
Jun 25 '17 at 16:33
$begingroup$
@NoahSchweber Thanks, Noah. I really hoped somebody would be able to help. What I can easily find in the literature is about theories stronger than PA. Wikipedia gives some results on weak theories, but without proper citations. I also read "Weak Systems of Arithmetic" by John Baez [golem.ph.utexas.edu/category/2011/10/weak_systems_of_arithmetic.html], but there is nothing substantial there, either.
$endgroup$
– George Levsky
Jun 25 '17 at 22:49
4
$begingroup$
George, this is a nice question. If you end up not receiving an answer after a reasonable amount of time (a week or two?), please consider reposting in on MathOverflow.
$endgroup$
– Andrés E. Caicedo
Jun 25 '17 at 23:47