Mixing
Going beyond the strength of Peano arithmetic “without setsâ€
Clash Royale CLAN TAG#URR8PPP
up vote
3
down vote
favorite
First-order arithmetic is fairly weak, as measured for example by its consistency strength. When a stronger theory is desired, it is common to work with (fragments of) second-order arithmetic or set theory. However, such theories might fail to meet certain "strong" constructive criteria. (Examples below involve classical theories only because those are the ones I'm aware of.)
For example, the subsystem ACA0 of second-order arithmetic is equiconsistent with PA, but its axioms say that for every arithmetic formula there is a well-defined set of numbers which satisfy it, which could be considered to lack a constructive justification. (Here, "well-defined" means roughly that the set consists of a fixed collection of elements, and nothing else, in line with the law of excluded middle.)
Meanwhile, set theories often include an axiom that every set has a well-defined powerset, or at least an axiom asserting the existence of a well-defined set which is "actually" (as opposed to "potentially") infinite. Simply removing such axioms can lead to very weak theories: for instance, ZF - infinity + (not infinity) is bi-interpretable with PA.
On the other hand, the strengths of theories can often be quantified in terms of (notations for) recursive ordinals, and there are notations for some quite large ordinals which arguably satisfy stringent constructive principles; see for example the "ordinal systems" of Anton Setzer, which are "built from below" specifically for this purpose.
There are also theories of arithmetic (e.g. PRA) which, while weak, seem to me like they could be extended using such ordinal notations to considerably greater strength without any features that might be constructively objectionable in the above sense.
My question then is:
Can such ordinal notations indeed be used to bypass the aforementioned obstacles (in second-order arithmetic or set theory) to building "strongly constructive" theories beyond the strength of PA?
Could such theories have practical uses, e.g. in relation to the Curry-Howard correspondence?
Has any work already been done on this?
lo.logic proof-theory constructive-mathematics intuitionism ordinal-analysis
asked Sep 3 at 1:12
Robin Saunders
1,5061327
add a comment |Â
up vote
3
down vote
favorite
First-order arithmetic is fairly weak, as measured for example by its consistency strength. When a stronger theory is desired, it is common to work with (fragments of) second-order arithmetic or set theory. However, such theories might fail to meet certain "strong" constructive criteria. (Examples below involve classical theories only because those are the ones I'm aware of.)
For example, the subsystem ACA0 of second-order arithmetic is equiconsistent with PA, but its axioms say that for every arithmetic formula there is a well-defined set of numbers which satisfy it, which could be considered to lack a constructive justification. (Here, "well-defined" means roughly that the set consists of a fixed collection of elements, and nothing else, in line with the law of excluded middle.)
Meanwhile, set theories often include an axiom that every set has a well-defined powerset, or at least an axiom asserting the existence of a well-defined set which is "actually" (as opposed to "potentially") infinite. Simply removing such axioms can lead to very weak theories: for instance, ZF - infinity + (not infinity) is bi-interpretable with PA.
On the other hand, the strengths of theories can often be quantified in terms of (notations for) recursive ordinals, and there are notations for some quite large ordinals which arguably satisfy stringent constructive principles; see for example the "ordinal systems" of Anton Setzer, which are "built from below" specifically for this purpose.
There are also theories of arithmetic (e.g. PRA) which, while weak, seem to me like they could be extended using such ordinal notations to considerably greater strength without any features that might be constructively objectionable in the above sense.
My question then is:
Can such ordinal notations indeed be used to bypass the aforementioned obstacles (in second-order arithmetic or set theory) to building "strongly constructive" theories beyond the strength of PA?
Could such theories have practical uses, e.g. in relation to the Curry-Howard correspondence?
Has any work already been done on this?
lo.logic proof-theory constructive-mathematics intuitionism ordinal-analysis
asked Sep 3 at 1:12
Robin Saunders
1,5061327
I’d like this question more without the word “constructivistâ€Â, since mathematicians who produce constructive results so outnumber the dogmatic constructivists. The second paragraph can begin “such theories might not be ‘strongly’ constructive, in the sense that...â€Â, filling in the criteria as in the comment on Nik Weaver’s answer. The third paragraph can say “which should be considered constructiveâ€Â, this time filling in the criteria with whatever arguments are alluded to by the current word “arguablyâ€Â. Then the question would more clearly be about which theories meet which goals.
– Matt F.
Sep 3 at 5:11
Who are these constructivists who are "unhappy and unconvinced" by this or that notion? You might be setting up a strawman. As far as I can tell the old philosophically-motivated constructive mathematicians are by now heavily outnumbered by mathematicians and computer scientists who care about constructive mathematics (of one sort or another) because it is relevant to their work. And the latter ones will tell you that recursion principles in type theory are the applicable and useful constructive replacement of ordinals.
– Andrej Bauer
Sep 3 at 6:53
@MattF. Thanks. I intended "constructivist" in the broad sense, to include "mathematician wearing a constructivist hat". But I agree that philosophical principles are vaguer than their concrete consequences, so I've reworded things in a way that's hopefully more neutral.
– Robin Saunders
Sep 3 at 15:44
@AndrejBauer Thanks for the keyword. I'm new to type theory, and it's clearly a very big subject, so I'd be very grateful if you could suggest any introductions covering this aspect of it that don't require too much background.
– Robin Saunders
Sep 3 at 15:58
I second Robin's ask: please give us literature references on recursion principles in type theory
– Gergely
Sep 6 at 11:47
add a comment |Â
up vote
3
down vote
favorite
up vote
3
down vote
favorite
First-order arithmetic is fairly weak, as measured for example by its consistency strength. When a stronger theory is desired, it is common to work with (fragments of) second-order arithmetic or set theory. However, such theories might fail to meet certain "strong" constructive criteria. (Examples below involve classical theories only because those are the ones I'm aware of.)
For example, the subsystem ACA0 of second-order arithmetic is equiconsistent with PA, but its axioms say that for every arithmetic formula there is a well-defined set of numbers which satisfy it, which could be considered to lack a constructive justification. (Here, "well-defined" means roughly that the set consists of a fixed collection of elements, and nothing else, in line with the law of excluded middle.)
Meanwhile, set theories often include an axiom that every set has a well-defined powerset, or at least an axiom asserting the existence of a well-defined set which is "actually" (as opposed to "potentially") infinite. Simply removing such axioms can lead to very weak theories: for instance, ZF - infinity + (not infinity) is bi-interpretable with PA.
On the other hand, the strengths of theories can often be quantified in terms of (notations for) recursive ordinals, and there are notations for some quite large ordinals which arguably satisfy stringent constructive principles; see for example the "ordinal systems" of Anton Setzer, which are "built from below" specifically for this purpose.
There are also theories of arithmetic (e.g. PRA) which, while weak, seem to me like they could be extended using such ordinal notations to considerably greater strength without any features that might be constructively objectionable in the above sense.
My question then is:
Can such ordinal notations indeed be used to bypass the aforementioned obstacles (in second-order arithmetic or set theory) to building "strongly constructive" theories beyond the strength of PA?
Could such theories have practical uses, e.g. in relation to the Curry-Howard correspondence?
Has any work already been done on this?
lo.logic proof-theory constructive-mathematics intuitionism ordinal-analysis
asked Sep 3 at 1:12
Robin Saunders
1,5061327
First-order arithmetic is fairly weak, as measured for example by its consistency strength. When a stronger theory is desired, it is common to work with (fragments of) second-order arithmetic or set theory. However, such theories might fail to meet certain "strong" constructive criteria. (Examples below involve classical theories only because those are the ones I'm aware of.)
For example, the subsystem ACA0 of second-order arithmetic is equiconsistent with PA, but its axioms say that for every arithmetic formula there is a well-defined set of numbers which satisfy it, which could be considered to lack a constructive justification. (Here, "well-defined" means roughly that the set consists of a fixed collection of elements, and nothing else, in line with the law of excluded middle.)
Meanwhile, set theories often include an axiom that every set has a well-defined powerset, or at least an axiom asserting the existence of a well-defined set which is "actually" (as opposed to "potentially") infinite. Simply removing such axioms can lead to very weak theories: for instance, ZF - infinity + (not infinity) is bi-interpretable with PA.
On the other hand, the strengths of theories can often be quantified in terms of (notations for) recursive ordinals, and there are notations for some quite large ordinals which arguably satisfy stringent constructive principles; see for example the "ordinal systems" of Anton Setzer, which are "built from below" specifically for this purpose.
There are also theories of arithmetic (e.g. PRA) which, while weak, seem to me like they could be extended using such ordinal notations to considerably greater strength without any features that might be constructively objectionable in the above sense.
My question then is:
Can such ordinal notations indeed be used to bypass the aforementioned obstacles (in second-order arithmetic or set theory) to building "strongly constructive" theories beyond the strength of PA?
Could such theories have practical uses, e.g. in relation to the Curry-Howard correspondence?
Has any work already been done on this?
lo.logic proof-theory constructive-mathematics intuitionism ordinal-analysis
asked Sep 3 at 1:12
Robin Saunders
1,5061327
edited Sep 3 at 15:38
asked Sep 3 at 1:12
Robin Saunders
1,5061327
asked Sep 3 at 1:12
Robin Saunders
1,5061327
asked Sep 3 at 1:12
Robin Saunders
1,5061327
1,5061327
I’d like this question more without the word “constructivistâ€Â, since mathematicians who produce constructive results so outnumber the dogmatic constructivists. The second paragraph can begin “such theories might not be ‘strongly’ constructive, in the sense that...â€Â, filling in the criteria as in the comment on Nik Weaver’s answer. The third paragraph can say “which should be considered constructiveâ€Â, this time filling in the criteria with whatever arguments are alluded to by the current word “arguablyâ€Â. Then the question would more clearly be about which theories meet which goals.
– Matt F.
Sep 3 at 5:11
Who are these constructivists who are "unhappy and unconvinced" by this or that notion? You might be setting up a strawman. As far as I can tell the old philosophically-motivated constructive mathematicians are by now heavily outnumbered by mathematicians and computer scientists who care about constructive mathematics (of one sort or another) because it is relevant to their work. And the latter ones will tell you that recursion principles in type theory are the applicable and useful constructive replacement of ordinals.
– Andrej Bauer
Sep 3 at 6:53
@MattF. Thanks. I intended "constructivist" in the broad sense, to include "mathematician wearing a constructivist hat". But I agree that philosophical principles are vaguer than their concrete consequences, so I've reworded things in a way that's hopefully more neutral.
– Robin Saunders
Sep 3 at 15:44
@AndrejBauer Thanks for the keyword. I'm new to type theory, and it's clearly a very big subject, so I'd be very grateful if you could suggest any introductions covering this aspect of it that don't require too much background.
– Robin Saunders
Sep 3 at 15:58
I second Robin's ask: please give us literature references on recursion principles in type theory
– Gergely
Sep 6 at 11:47
add a comment |Â
I’d like this question more without the word “constructivistâ€Â, since mathematicians who produce constructive results so outnumber the dogmatic constructivists. The second paragraph can begin “such theories might not be ‘strongly’ constructive, in the sense that...â€Â, filling in the criteria as in the comment on Nik Weaver’s answer. The third paragraph can say “which should be considered constructiveâ€Â, this time filling in the criteria with whatever arguments are alluded to by the current word “arguablyâ€Â. Then the question would more clearly be about which theories meet which goals.
– Matt F.
Sep 3 at 5:11
Who are these constructivists who are "unhappy and unconvinced" by this or that notion? You might be setting up a strawman. As far as I can tell the old philosophically-motivated constructive mathematicians are by now heavily outnumbered by mathematicians and computer scientists who care about constructive mathematics (of one sort or another) because it is relevant to their work. And the latter ones will tell you that recursion principles in type theory are the applicable and useful constructive replacement of ordinals.
– Andrej Bauer
Sep 3 at 6:53
@MattF. Thanks. I intended "constructivist" in the broad sense, to include "mathematician wearing a constructivist hat". But I agree that philosophical principles are vaguer than their concrete consequences, so I've reworded things in a way that's hopefully more neutral.
– Robin Saunders
Sep 3 at 15:44
@AndrejBauer Thanks for the keyword. I'm new to type theory, and it's clearly a very big subject, so I'd be very grateful if you could suggest any introductions covering this aspect of it that don't require too much background.
– Robin Saunders
Sep 3 at 15:58
I second Robin's ask: please give us literature references on recursion principles in type theory
– Gergely
Sep 6 at 11:47
I’d like this question more without the word “constructivistâ€Â, since mathematicians who produce constructive results so outnumber the dogmatic constructivists. The second paragraph can begin “such theories might not be ‘strongly’ constructive, in the sense that...â€Â, filling in the criteria as in the comment on Nik Weaver’s answer. The third paragraph can say “which should be considered constructiveâ€Â, this time filling in the criteria with whatever arguments are alluded to by the current word “arguablyâ€Â. Then the question would more clearly be about which theories meet which goals.
– Matt F.
Sep 3 at 5:11
I’d like this question more without the word “constructivistâ€Â, since mathematicians who produce constructive results so outnumber the dogmatic constructivists. The second paragraph can begin “such theories might not be ‘strongly’ constructive, in the sense that...â€Â, filling in the criteria as in the comment on Nik Weaver’s answer. The third paragraph can say “which should be considered constructiveâ€Â, this time filling in the criteria with whatever arguments are alluded to by the current word “arguablyâ€Â. Then the question would more clearly be about which theories meet which goals.
– Matt F.
Sep 3 at 5:11
Who are these constructivists who are "unhappy and unconvinced" by this or that notion? You might be setting up a strawman. As far as I can tell the old philosophically-motivated constructive mathematicians are by now heavily outnumbered by mathematicians and computer scientists who care about constructive mathematics (of one sort or another) because it is relevant to their work. And the latter ones will tell you that recursion principles in type theory are the applicable and useful constructive replacement of ordinals.
– Andrej Bauer
Sep 3 at 6:53
Who are these constructivists who are "unhappy and unconvinced" by this or that notion? You might be setting up a strawman. As far as I can tell the old philosophically-motivated constructive mathematicians are by now heavily outnumbered by mathematicians and computer scientists who care about constructive mathematics (of one sort or another) because it is relevant to their work. And the latter ones will tell you that recursion principles in type theory are the applicable and useful constructive replacement of ordinals.
– Andrej Bauer
Sep 3 at 6:53
@MattF. Thanks. I intended "constructivist" in the broad sense, to include "mathematician wearing a constructivist hat". But I agree that philosophical principles are vaguer than their concrete consequences, so I've reworded things in a way that's hopefully more neutral.
– Robin Saunders
Sep 3 at 15:44
@MattF. Thanks. I intended "constructivist" in the broad sense, to include "mathematician wearing a constructivist hat". But I agree that philosophical principles are vaguer than their concrete consequences, so I've reworded things in a way that's hopefully more neutral.
– Robin Saunders
Sep 3 at 15:44
@AndrejBauer Thanks for the keyword. I'm new to type theory, and it's clearly a very big subject, so I'd be very grateful if you could suggest any introductions covering this aspect of it that don't require too much background.
– Robin Saunders
Sep 3 at 15:58
@AndrejBauer Thanks for the keyword. I'm new to type theory, and it's clearly a very big subject, so I'd be very grateful if you could suggest any introductions covering this aspect of it that don't require too much background.
– Robin Saunders
Sep 3 at 15:58
I second Robin's ask: please give us literature references on recursion principles in type theory
– Gergely
Sep 6 at 11:47
I second Robin's ask: please give us literature references on recursion principles in type theory
– Gergely
Sep 6 at 11:47
add a comment |Â
1 Answer
1
active
oldest
votes
up vote
4
down vote
A lot of work has been done on (1) various systems of ordinal notations ranging from very weak to very strong and (2) calibrating the proof theoretic strength of various formal systems, say in terms of the "provable ordinals" of those systems, i.e., the ordinals which have a notation that the system proves is well-ordered.
You seem specifically interested in constructivism, but that may not be a sufficiently well-defined position to support any definite answers. Constructivists typically accept Heyting arithmetic, which has the same consistency strength as PA. But I have also seen allegedly constructivist formal systems which go way beyond this, e.g., see this paper by Michael Rathjen which shows how far some Martin-Lof type theories go. The philosophical acceptability of such systems from a constructive standpoint probably depends heavily on who you ask. (I am not sure what you mean by "strongly constructive".)
answered Sep 3 at 1:47
Nik Weaver
17.9k142114
Thanks. I appreciate that "constructivism" is not well-defined. My main intention was to encompass rejection of the three specific classical notions above: that powerset is a well-defined operation, that all arithmetic sentences are either true or false, and that it is meaningful to speak about a completed infinite set of which every potential element either is or is not a member. I left the specifics open-ended because I would also be interested in any formalization of conceptually-related ideas, as long as they were strong enough.
– Robin Saunders
Sep 3 at 2:34
Intuitionistic type theories seem like a good place to start; I'll try to leave more comments or a follow-up question once I've read the paper you linked to, and perhaps some other material in this area.
– Robin Saunders
Sep 3 at 2:35
add a comment |Â
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
up vote
4
down vote
A lot of work has been done on (1) various systems of ordinal notations ranging from very weak to very strong and (2) calibrating the proof theoretic strength of various formal systems, say in terms of the "provable ordinals" of those systems, i.e., the ordinals which have a notation that the system proves is well-ordered.
You seem specifically interested in constructivism, but that may not be a sufficiently well-defined position to support any definite answers. Constructivists typically accept Heyting arithmetic, which has the same consistency strength as PA. But I have also seen allegedly constructivist formal systems which go way beyond this, e.g., see this paper by Michael Rathjen which shows how far some Martin-Lof type theories go. The philosophical acceptability of such systems from a constructive standpoint probably depends heavily on who you ask. (I am not sure what you mean by "strongly constructive".)
answered Sep 3 at 1:47
Nik Weaver
17.9k142114
Thanks. I appreciate that "constructivism" is not well-defined. My main intention was to encompass rejection of the three specific classical notions above: that powerset is a well-defined operation, that all arithmetic sentences are either true or false, and that it is meaningful to speak about a completed infinite set of which every potential element either is or is not a member. I left the specifics open-ended because I would also be interested in any formalization of conceptually-related ideas, as long as they were strong enough.
– Robin Saunders
Sep 3 at 2:34
Intuitionistic type theories seem like a good place to start; I'll try to leave more comments or a follow-up question once I've read the paper you linked to, and perhaps some other material in this area.
– Robin Saunders
Sep 3 at 2:35
add a comment |Â
up vote
4
down vote
A lot of work has been done on (1) various systems of ordinal notations ranging from very weak to very strong and (2) calibrating the proof theoretic strength of various formal systems, say in terms of the "provable ordinals" of those systems, i.e., the ordinals which have a notation that the system proves is well-ordered.
You seem specifically interested in constructivism, but that may not be a sufficiently well-defined position to support any definite answers. Constructivists typically accept Heyting arithmetic, which has the same consistency strength as PA. But I have also seen allegedly constructivist formal systems which go way beyond this, e.g., see this paper by Michael Rathjen which shows how far some Martin-Lof type theories go. The philosophical acceptability of such systems from a constructive standpoint probably depends heavily on who you ask. (I am not sure what you mean by "strongly constructive".)
answered Sep 3 at 1:47
Nik Weaver
17.9k142114
Thanks. I appreciate that "constructivism" is not well-defined. My main intention was to encompass rejection of the three specific classical notions above: that powerset is a well-defined operation, that all arithmetic sentences are either true or false, and that it is meaningful to speak about a completed infinite set of which every potential element either is or is not a member. I left the specifics open-ended because I would also be interested in any formalization of conceptually-related ideas, as long as they were strong enough.
– Robin Saunders
Sep 3 at 2:34
Intuitionistic type theories seem like a good place to start; I'll try to leave more comments or a follow-up question once I've read the paper you linked to, and perhaps some other material in this area.
– Robin Saunders
Sep 3 at 2:35
add a comment |Â
up vote
4
down vote
up vote
4
down vote
A lot of work has been done on (1) various systems of ordinal notations ranging from very weak to very strong and (2) calibrating the proof theoretic strength of various formal systems, say in terms of the "provable ordinals" of those systems, i.e., the ordinals which have a notation that the system proves is well-ordered.
You seem specifically interested in constructivism, but that may not be a sufficiently well-defined position to support any definite answers. Constructivists typically accept Heyting arithmetic, which has the same consistency strength as PA. But I have also seen allegedly constructivist formal systems which go way beyond this, e.g., see this paper by Michael Rathjen which shows how far some Martin-Lof type theories go. The philosophical acceptability of such systems from a constructive standpoint probably depends heavily on who you ask. (I am not sure what you mean by "strongly constructive".)
answered Sep 3 at 1:47
Nik Weaver
17.9k142114
A lot of work has been done on (1) various systems of ordinal notations ranging from very weak to very strong and (2) calibrating the proof theoretic strength of various formal systems, say in terms of the "provable ordinals" of those systems, i.e., the ordinals which have a notation that the system proves is well-ordered.
You seem specifically interested in constructivism, but that may not be a sufficiently well-defined position to support any definite answers. Constructivists typically accept Heyting arithmetic, which has the same consistency strength as PA. But I have also seen allegedly constructivist formal systems which go way beyond this, e.g., see this paper by Michael Rathjen which shows how far some Martin-Lof type theories go. The philosophical acceptability of such systems from a constructive standpoint probably depends heavily on who you ask. (I am not sure what you mean by "strongly constructive".)
answered Sep 3 at 1:47
Nik Weaver
17.9k142114
answered Sep 3 at 1:47
Nik Weaver
17.9k142114
answered Sep 3 at 1:47
Nik Weaver
17.9k142114
answered Sep 3 at 1:47
Nik Weaver
17.9k142114
17.9k142114
Thanks. I appreciate that "constructivism" is not well-defined. My main intention was to encompass rejection of the three specific classical notions above: that powerset is a well-defined operation, that all arithmetic sentences are either true or false, and that it is meaningful to speak about a completed infinite set of which every potential element either is or is not a member. I left the specifics open-ended because I would also be interested in any formalization of conceptually-related ideas, as long as they were strong enough.
– Robin Saunders
Sep 3 at 2:34
Intuitionistic type theories seem like a good place to start; I'll try to leave more comments or a follow-up question once I've read the paper you linked to, and perhaps some other material in this area.
– Robin Saunders
Sep 3 at 2:35
add a comment |Â
Thanks. I appreciate that "constructivism" is not well-defined. My main intention was to encompass rejection of the three specific classical notions above: that powerset is a well-defined operation, that all arithmetic sentences are either true or false, and that it is meaningful to speak about a completed infinite set of which every potential element either is or is not a member. I left the specifics open-ended because I would also be interested in any formalization of conceptually-related ideas, as long as they were strong enough.
– Robin Saunders
Sep 3 at 2:34
Intuitionistic type theories seem like a good place to start; I'll try to leave more comments or a follow-up question once I've read the paper you linked to, and perhaps some other material in this area.
– Robin Saunders
Sep 3 at 2:35
Thanks. I appreciate that "constructivism" is not well-defined. My main intention was to encompass rejection of the three specific classical notions above: that powerset is a well-defined operation, that all arithmetic sentences are either true or false, and that it is meaningful to speak about a completed infinite set of which every potential element either is or is not a member. I left the specifics open-ended because I would also be interested in any formalization of conceptually-related ideas, as long as they were strong enough.
– Robin Saunders
Sep 3 at 2:34
Thanks. I appreciate that "constructivism" is not well-defined. My main intention was to encompass rejection of the three specific classical notions above: that powerset is a well-defined operation, that all arithmetic sentences are either true or false, and that it is meaningful to speak about a completed infinite set of which every potential element either is or is not a member. I left the specifics open-ended because I would also be interested in any formalization of conceptually-related ideas, as long as they were strong enough.
– Robin Saunders
Sep 3 at 2:34
Intuitionistic type theories seem like a good place to start; I'll try to leave more comments or a follow-up question once I've read the paper you linked to, and perhaps some other material in this area.
– Robin Saunders
Sep 3 at 2:35
Intuitionistic type theories seem like a good place to start; I'll try to leave more comments or a follow-up question once I've read the paper you linked to, and perhaps some other material in this area.
– Robin Saunders
Sep 3 at 2:35
add a comment |Â
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
StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmathoverflow.net%2fquestions%2f309728%2fgoing-beyond-the-strength-of-peano-arithmetic-without-sets%23new-answer', 'question_page');
);
Post as a guest
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
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
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
I’d like this question more without the word “constructivistâ€Â, since mathematicians who produce constructive results so outnumber the dogmatic constructivists. The second paragraph can begin “such theories might not be ‘strongly’ constructive, in the sense that...â€Â, filling in the criteria as in the comment on Nik Weaver’s answer. The third paragraph can say “which should be considered constructiveâ€Â, this time filling in the criteria with whatever arguments are alluded to by the current word “arguablyâ€Â. Then the question would more clearly be about which theories meet which goals.
– Matt F.
Sep 3 at 5:11
Who are these constructivists who are "unhappy and unconvinced" by this or that notion? You might be setting up a strawman. As far as I can tell the old philosophically-motivated constructive mathematicians are by now heavily outnumbered by mathematicians and computer scientists who care about constructive mathematics (of one sort or another) because it is relevant to their work. And the latter ones will tell you that recursion principles in type theory are the applicable and useful constructive replacement of ordinals.
– Andrej Bauer
Sep 3 at 6:53
@MattF. Thanks. I intended "constructivist" in the broad sense, to include "mathematician wearing a constructivist hat". But I agree that philosophical principles are vaguer than their concrete consequences, so I've reworded things in a way that's hopefully more neutral.
– Robin Saunders
Sep 3 at 15:44
@AndrejBauer Thanks for the keyword. I'm new to type theory, and it's clearly a very big subject, so I'd be very grateful if you could suggest any introductions covering this aspect of it that don't require too much background.
– Robin Saunders
Sep 3 at 15:58
I second Robin's ask: please give us literature references on recursion principles in type theory
– Gergely
Sep 6 at 11:47