Reflection principle for intuitionistic Zermelo–Fraenkel?
$begingroup$
The well-known reflection principle for classical Zermelo–Fraenkel states:
For any formula $varphi(x_1,ldots,x_n)$ of the language of ZFC with free variables $x_1,ldots,x_n$, ZFC proves
$$ forall M_0. exists M supseteq M_0. forall x_1,ldots,x_n in M. (varphi(x_1,ldots,x_n) Leftrightarrow varphi^M(x_1,ldots,x_n)), $$
where $varphi^M$ is the $M$-relativization of $varphi$.
Question. Does the analogous theorem hold with ZFC replaced by IZF, intuitionistic Zermelo–Fraenkel? All proofs of the reflection principle for ZFC that I know of don't obviously carry over to IZF, firstly because of the failure of Scott's trick and secondly because we cannot, unlike in classical texts, assume without loss of generality that formulas don't contain universal quantifiers.
Surely this has been studied before, but I wasn't able to track down a reference.
Motivation. With such a reflection principle in place, we could mimic the definition of ZFC/S, a conservative extension of ZFC useful for category theory, to create IZF/S. The reflection principle is what powers the automatic transfer from a given theorem formulated, for instance, for all small groups, to one formulated for all groups, and this leap shouldn't require non-intuitionistic techniques.
set-theory lo.logic constructive-mathematics
edited Dec 20 '18 at 23:45
David Roberts
17.4k462176
asked Dec 15 '18 at 21:00
Ingo BlechschmidtIngo Blechschmidt
1,7831321
$endgroup$
migrated from math.stackexchange.com Dec 20 '18 at 23:39
This question came from our site for people studying math at any level and professionals in related fields.
|
show 16 more comments
$begingroup$
The well-known reflection principle for classical Zermelo–Fraenkel states:
For any formula $varphi(x_1,ldots,x_n)$ of the language of ZFC with free variables $x_1,ldots,x_n$, ZFC proves
$$ forall M_0. exists M supseteq M_0. forall x_1,ldots,x_n in M. (varphi(x_1,ldots,x_n) Leftrightarrow varphi^M(x_1,ldots,x_n)), $$
where $varphi^M$ is the $M$-relativization of $varphi$.
Question. Does the analogous theorem hold with ZFC replaced by IZF, intuitionistic Zermelo–Fraenkel? All proofs of the reflection principle for ZFC that I know of don't obviously carry over to IZF, firstly because of the failure of Scott's trick and secondly because we cannot, unlike in classical texts, assume without loss of generality that formulas don't contain universal quantifiers.
Surely this has been studied before, but I wasn't able to track down a reference.
Motivation. With such a reflection principle in place, we could mimic the definition of ZFC/S, a conservative extension of ZFC useful for category theory, to create IZF/S. The reflection principle is what powers the automatic transfer from a given theorem formulated, for instance, for all small groups, to one formulated for all groups, and this leap shouldn't require non-intuitionistic techniques.
set-theory lo.logic constructive-mathematics
edited Dec 20 '18 at 23:45
David Roberts
17.4k462176
asked Dec 15 '18 at 21:00
Ingo BlechschmidtIngo Blechschmidt
1,7831321
$endgroup$
migrated from math.stackexchange.com Dec 20 '18 at 23:39
This question came from our site for people studying math at any level and professionals in related fields.
$begingroup$
I added the top-level arXiv tag lo.logic, and a link to the IZF axioms (are they the ones you are thinking of, Ingo?)
$endgroup$
– David Roberts
Dec 20 '18 at 23:46
$begingroup$
For how large a fragment of logic can you prove the reflection principle for IZF?
$endgroup$
– Andrej Bauer
Dec 21 '18 at 7:08
2
$begingroup$
@IngoBlechschmidt you can prove that using full separation and collection. Define $X := { x in {0} | (exists y)y in C }$, then by collection there exists a set $C'$ such that if $X$ is inhabited, then so is $C' cap C$. Note that $C'$ is not definable, and in fact by a result due to Friedman and Scedrov it is impossible in general for such a $C'$ to be definable. Even with this trick it is difficult to deal with formulas of the form $(exists y)phi(x, y)$, with reflection as you stated it, because it is necessary to repeat transfinitely.
$endgroup$
– aws
Dec 24 '18 at 15:25
1
$begingroup$
@aws Lubarsky provides an answer of the independence of Reflection over $mathbf{CZF}$ in his article Independence Results around Constructive ZF.
$endgroup$
– Hanul Jeon
Feb 19 at 4:15
1
$begingroup$
@HanulJeon Thanks. I discussed this with Ingo a bit offlist and he noticed that reflection implies full separation, so in fact reflection is not even provable in $mathbf{CZF}$ with powerset and $mathbf{RDC}$. But Lubarsky's proof is interesting too - it shows reflection is not provable even with full separation (but without powerset).
$endgroup$
– aws
Feb 19 at 9:21
|
show 16 more comments
$begingroup$
The well-known reflection principle for classical Zermelo–Fraenkel states:
For any formula $varphi(x_1,ldots,x_n)$ of the language of ZFC with free variables $x_1,ldots,x_n$, ZFC proves
$$ forall M_0. exists M supseteq M_0. forall x_1,ldots,x_n in M. (varphi(x_1,ldots,x_n) Leftrightarrow varphi^M(x_1,ldots,x_n)), $$
where $varphi^M$ is the $M$-relativization of $varphi$.
Question. Does the analogous theorem hold with ZFC replaced by IZF, intuitionistic Zermelo–Fraenkel? All proofs of the reflection principle for ZFC that I know of don't obviously carry over to IZF, firstly because of the failure of Scott's trick and secondly because we cannot, unlike in classical texts, assume without loss of generality that formulas don't contain universal quantifiers.
Surely this has been studied before, but I wasn't able to track down a reference.
Motivation. With such a reflection principle in place, we could mimic the definition of ZFC/S, a conservative extension of ZFC useful for category theory, to create IZF/S. The reflection principle is what powers the automatic transfer from a given theorem formulated, for instance, for all small groups, to one formulated for all groups, and this leap shouldn't require non-intuitionistic techniques.
set-theory lo.logic constructive-mathematics
edited Dec 20 '18 at 23:45
David Roberts
17.4k462176
asked Dec 15 '18 at 21:00
Ingo BlechschmidtIngo Blechschmidt
1,7831321
$endgroup$
The well-known reflection principle for classical Zermelo–Fraenkel states:
For any formula $varphi(x_1,ldots,x_n)$ of the language of ZFC with free variables $x_1,ldots,x_n$, ZFC proves
$$ forall M_0. exists M supseteq M_0. forall x_1,ldots,x_n in M. (varphi(x_1,ldots,x_n) Leftrightarrow varphi^M(x_1,ldots,x_n)), $$
where $varphi^M$ is the $M$-relativization of $varphi$.
Question. Does the analogous theorem hold with ZFC replaced by IZF, intuitionistic Zermelo–Fraenkel? All proofs of the reflection principle for ZFC that I know of don't obviously carry over to IZF, firstly because of the failure of Scott's trick and secondly because we cannot, unlike in classical texts, assume without loss of generality that formulas don't contain universal quantifiers.
Surely this has been studied before, but I wasn't able to track down a reference.
Motivation. With such a reflection principle in place, we could mimic the definition of ZFC/S, a conservative extension of ZFC useful for category theory, to create IZF/S. The reflection principle is what powers the automatic transfer from a given theorem formulated, for instance, for all small groups, to one formulated for all groups, and this leap shouldn't require non-intuitionistic techniques.
set-theory lo.logic constructive-mathematics
set-theory lo.logic constructive-mathematics
edited Dec 20 '18 at 23:45
David Roberts
17.4k462176
asked Dec 15 '18 at 21:00
Ingo BlechschmidtIngo Blechschmidt
1,7831321
edited Dec 20 '18 at 23:45
David Roberts
17.4k462176
asked Dec 15 '18 at 21:00
Ingo BlechschmidtIngo Blechschmidt
1,7831321
edited Dec 20 '18 at 23:45
David Roberts
17.4k462176
edited Dec 20 '18 at 23:45
David Roberts
17.4k462176
edited Dec 20 '18 at 23:45
David Roberts
17.4k462176
17.4k462176
asked Dec 15 '18 at 21:00
Ingo BlechschmidtIngo Blechschmidt
1,7831321
asked Dec 15 '18 at 21:00
Ingo BlechschmidtIngo Blechschmidt
1,7831321
asked Dec 15 '18 at 21:00
Ingo BlechschmidtIngo Blechschmidt
1,7831321
1,7831321
migrated from math.stackexchange.com Dec 20 '18 at 23:39
This question came from our site for people studying math at any level and professionals in related fields.
migrated from math.stackexchange.com Dec 20 '18 at 23:39
This question came from our site for people studying math at any level and professionals in related fields.
$begingroup$
I added the top-level arXiv tag lo.logic, and a link to the IZF axioms (are they the ones you are thinking of, Ingo?)
$endgroup$
– David Roberts
Dec 20 '18 at 23:46
$begingroup$
For how large a fragment of logic can you prove the reflection principle for IZF?
$endgroup$
– Andrej Bauer
Dec 21 '18 at 7:08
2
$begingroup$
@IngoBlechschmidt you can prove that using full separation and collection. Define $X := { x in {0} | (exists y)y in C }$, then by collection there exists a set $C'$ such that if $X$ is inhabited, then so is $C' cap C$. Note that $C'$ is not definable, and in fact by a result due to Friedman and Scedrov it is impossible in general for such a $C'$ to be definable. Even with this trick it is difficult to deal with formulas of the form $(exists y)phi(x, y)$, with reflection as you stated it, because it is necessary to repeat transfinitely.
$endgroup$
– aws
Dec 24 '18 at 15:25
1
$begingroup$
@aws Lubarsky provides an answer of the independence of Reflection over $mathbf{CZF}$ in his article Independence Results around Constructive ZF.
$endgroup$
– Hanul Jeon
Feb 19 at 4:15
1
$begingroup$
@HanulJeon Thanks. I discussed this with Ingo a bit offlist and he noticed that reflection implies full separation, so in fact reflection is not even provable in $mathbf{CZF}$ with powerset and $mathbf{RDC}$. But Lubarsky's proof is interesting too - it shows reflection is not provable even with full separation (but without powerset).
$endgroup$
– aws
Feb 19 at 9:21
|
show 16 more comments
$begingroup$
I added the top-level arXiv tag lo.logic, and a link to the IZF axioms (are they the ones you are thinking of, Ingo?)
$endgroup$
– David Roberts
Dec 20 '18 at 23:46
$begingroup$
For how large a fragment of logic can you prove the reflection principle for IZF?
$endgroup$
– Andrej Bauer
Dec 21 '18 at 7:08
2
$begingroup$
@IngoBlechschmidt you can prove that using full separation and collection. Define $X := { x in {0} | (exists y)y in C }$, then by collection there exists a set $C'$ such that if $X$ is inhabited, then so is $C' cap C$. Note that $C'$ is not definable, and in fact by a result due to Friedman and Scedrov it is impossible in general for such a $C'$ to be definable. Even with this trick it is difficult to deal with formulas of the form $(exists y)phi(x, y)$, with reflection as you stated it, because it is necessary to repeat transfinitely.
$endgroup$
– aws
Dec 24 '18 at 15:25
1
$begingroup$
@aws Lubarsky provides an answer of the independence of Reflection over $mathbf{CZF}$ in his article Independence Results around Constructive ZF.
$endgroup$
– Hanul Jeon
Feb 19 at 4:15
1
$begingroup$
@HanulJeon Thanks. I discussed this with Ingo a bit offlist and he noticed that reflection implies full separation, so in fact reflection is not even provable in $mathbf{CZF}$ with powerset and $mathbf{RDC}$. But Lubarsky's proof is interesting too - it shows reflection is not provable even with full separation (but without powerset).
$endgroup$
– aws
Feb 19 at 9:21
$begingroup$
I added the top-level arXiv tag lo.logic, and a link to the IZF axioms (are they the ones you are thinking of, Ingo?)
$endgroup$
– David Roberts
Dec 20 '18 at 23:46
$begingroup$
I added the top-level arXiv tag lo.logic, and a link to the IZF axioms (are they the ones you are thinking of, Ingo?)
$endgroup$
– David Roberts
Dec 20 '18 at 23:46
$begingroup$
For how large a fragment of logic can you prove the reflection principle for IZF?
$endgroup$
– Andrej Bauer
Dec 21 '18 at 7:08
$begingroup$
For how large a fragment of logic can you prove the reflection principle for IZF?
$endgroup$
– Andrej Bauer
Dec 21 '18 at 7:08
2
2
$begingroup$
@IngoBlechschmidt you can prove that using full separation and collection. Define $X := { x in {0} | (exists y)y in C }$, then by collection there exists a set $C'$ such that if $X$ is inhabited, then so is $C' cap C$. Note that $C'$ is not definable, and in fact by a result due to Friedman and Scedrov it is impossible in general for such a $C'$ to be definable. Even with this trick it is difficult to deal with formulas of the form $(exists y)phi(x, y)$, with reflection as you stated it, because it is necessary to repeat transfinitely.
$endgroup$
– aws
Dec 24 '18 at 15:25
$begingroup$
@IngoBlechschmidt you can prove that using full separation and collection. Define $X := { x in {0} | (exists y)y in C }$, then by collection there exists a set $C'$ such that if $X$ is inhabited, then so is $C' cap C$. Note that $C'$ is not definable, and in fact by a result due to Friedman and Scedrov it is impossible in general for such a $C'$ to be definable. Even with this trick it is difficult to deal with formulas of the form $(exists y)phi(x, y)$, with reflection as you stated it, because it is necessary to repeat transfinitely.
$endgroup$
– aws
Dec 24 '18 at 15:25
1
1
$begingroup$
@aws Lubarsky provides an answer of the independence of Reflection over $mathbf{CZF}$ in his article Independence Results around Constructive ZF.
$endgroup$
– Hanul Jeon
Feb 19 at 4:15
$begingroup$
@aws Lubarsky provides an answer of the independence of Reflection over $mathbf{CZF}$ in his article Independence Results around Constructive ZF.
$endgroup$
– Hanul Jeon
Feb 19 at 4:15
1
1
$begingroup$
@HanulJeon Thanks. I discussed this with Ingo a bit offlist and he noticed that reflection implies full separation, so in fact reflection is not even provable in $mathbf{CZF}$ with powerset and $mathbf{RDC}$. But Lubarsky's proof is interesting too - it shows reflection is not provable even with full separation (but without powerset).
$endgroup$
– aws
Feb 19 at 9:21
$begingroup$
@HanulJeon Thanks. I discussed this with Ingo a bit offlist and he noticed that reflection implies full separation, so in fact reflection is not even provable in $mathbf{CZF}$ with powerset and $mathbf{RDC}$. But Lubarsky's proof is interesting too - it shows reflection is not provable even with full separation (but without powerset).
$endgroup$
– aws
Feb 19 at 9:21
|
show 16 more comments
0
active
oldest
votes
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: "504"
};
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%2fmathoverflow.net%2fquestions%2f319179%2freflection-principle-for-intuitionistic-zermelo-fraenkel%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
0
active
oldest
votes
0
active
oldest
votes
active
oldest
votes
active
oldest
votes
Thanks for contributing an answer to MathOverflow!
- 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%2fmathoverflow.net%2fquestions%2f319179%2freflection-principle-for-intuitionistic-zermelo-fraenkel%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 added the top-level arXiv tag lo.logic, and a link to the IZF axioms (are they the ones you are thinking of, Ingo?)
$endgroup$
– David Roberts
Dec 20 '18 at 23:46
$begingroup$
For how large a fragment of logic can you prove the reflection principle for IZF?
$endgroup$
– Andrej Bauer
Dec 21 '18 at 7:08
2
$begingroup$
@IngoBlechschmidt you can prove that using full separation and collection. Define $X := { x in {0} | (exists y)y in C }$, then by collection there exists a set $C'$ such that if $X$ is inhabited, then so is $C' cap C$. Note that $C'$ is not definable, and in fact by a result due to Friedman and Scedrov it is impossible in general for such a $C'$ to be definable. Even with this trick it is difficult to deal with formulas of the form $(exists y)phi(x, y)$, with reflection as you stated it, because it is necessary to repeat transfinitely.
$endgroup$
– aws
Dec 24 '18 at 15:25
1
$begingroup$
@aws Lubarsky provides an answer of the independence of Reflection over $mathbf{CZF}$ in his article Independence Results around Constructive ZF.
$endgroup$
– Hanul Jeon
Feb 19 at 4:15
1
$begingroup$
@HanulJeon Thanks. I discussed this with Ingo a bit offlist and he noticed that reflection implies full separation, so in fact reflection is not even provable in $mathbf{CZF}$ with powerset and $mathbf{RDC}$. But Lubarsky's proof is interesting too - it shows reflection is not provable even with full separation (but without powerset).
$endgroup$
– aws
Feb 19 at 9:21