Can we extend a version of MK with that coding function?
$begingroup$
Lets weaken the limitation of size axiom of MK to that of sets, i.e. every class that is subnumerous to a set is a set, now to that version of $MK$ lets add to the language of it a primitive unary coding function $Cd$, and restrict class comprehension axiom of $MK$ to pure class theoretic formulas (i.e. formulas not using $Cd$), and add an axiom that all codes are sets, i.e. $[y=Cd(x) to y in V]$, where $V$ is the class of all sets. Also axiomatize that the coding function is bijective. Now to the resulting theory can we add the following schemata?
Class coding schema: if $varphi(z)$ is a formula in $L(=,in)$, in which $x$ is not free, then: $$exists x forall y (y in x leftrightarrow exists z (varphi(z) wedge y=Cd(z)))$$
Set coding scheme: if $varphi^V(z)$ is a formula in which all of its quantifiers are bounded in $V$, then for all set closures we have:
$$exists x forall y (y in x leftrightarrow exists z in V (varphi^V(z) wedge y=Cd(z)))$$
In English: The class coding scheme states that we can construct any class of codes of classes as long as the latter ones are predicated in pure class language. While the set coding schema states that we can construct any class of codes of sets predicated by formulas restricted to sets but allowed to use the coding function.
From that we can for example define Cardinality by a modification of Scott's trick, as Cardinality of any class $x$ is the class of all codes of classes equinumerous to $x$ of the lowest possible rank. Also I think we can code an embedding from $V$ to $V$ by using the Set coding scheme.
first-order-logic alternative-set-theories
asked Jan 6 at 10:46
ZuhairZuhair
354212
$endgroup$
add a comment |
$begingroup$
Lets weaken the limitation of size axiom of MK to that of sets, i.e. every class that is subnumerous to a set is a set, now to that version of $MK$ lets add to the language of it a primitive unary coding function $Cd$, and restrict class comprehension axiom of $MK$ to pure class theoretic formulas (i.e. formulas not using $Cd$), and add an axiom that all codes are sets, i.e. $[y=Cd(x) to y in V]$, where $V$ is the class of all sets. Also axiomatize that the coding function is bijective. Now to the resulting theory can we add the following schemata?
Class coding schema: if $varphi(z)$ is a formula in $L(=,in)$, in which $x$ is not free, then: $$exists x forall y (y in x leftrightarrow exists z (varphi(z) wedge y=Cd(z)))$$
Set coding scheme: if $varphi^V(z)$ is a formula in which all of its quantifiers are bounded in $V$, then for all set closures we have:
$$exists x forall y (y in x leftrightarrow exists z in V (varphi^V(z) wedge y=Cd(z)))$$
In English: The class coding scheme states that we can construct any class of codes of classes as long as the latter ones are predicated in pure class language. While the set coding schema states that we can construct any class of codes of sets predicated by formulas restricted to sets but allowed to use the coding function.
From that we can for example define Cardinality by a modification of Scott's trick, as Cardinality of any class $x$ is the class of all codes of classes equinumerous to $x$ of the lowest possible rank. Also I think we can code an embedding from $V$ to $V$ by using the Set coding scheme.
first-order-logic alternative-set-theories
asked Jan 6 at 10:46
ZuhairZuhair
354212
$endgroup$
$begingroup$
Presumably you want to include additional axioms - what if $Cd(y)=emptyset$ for every $y$? At the very least you want $Cd$ to be injective I think ...
$endgroup$
– Noah Schweber
Jan 6 at 11:00
$begingroup$
Yes, that's perfectly correct, actually I need it to bijective. Thanks
$endgroup$
– Zuhair
Jan 6 at 11:01
add a comment |
$begingroup$
Lets weaken the limitation of size axiom of MK to that of sets, i.e. every class that is subnumerous to a set is a set, now to that version of $MK$ lets add to the language of it a primitive unary coding function $Cd$, and restrict class comprehension axiom of $MK$ to pure class theoretic formulas (i.e. formulas not using $Cd$), and add an axiom that all codes are sets, i.e. $[y=Cd(x) to y in V]$, where $V$ is the class of all sets. Also axiomatize that the coding function is bijective. Now to the resulting theory can we add the following schemata?
Class coding schema: if $varphi(z)$ is a formula in $L(=,in)$, in which $x$ is not free, then: $$exists x forall y (y in x leftrightarrow exists z (varphi(z) wedge y=Cd(z)))$$
Set coding scheme: if $varphi^V(z)$ is a formula in which all of its quantifiers are bounded in $V$, then for all set closures we have:
$$exists x forall y (y in x leftrightarrow exists z in V (varphi^V(z) wedge y=Cd(z)))$$
In English: The class coding scheme states that we can construct any class of codes of classes as long as the latter ones are predicated in pure class language. While the set coding schema states that we can construct any class of codes of sets predicated by formulas restricted to sets but allowed to use the coding function.
From that we can for example define Cardinality by a modification of Scott's trick, as Cardinality of any class $x$ is the class of all codes of classes equinumerous to $x$ of the lowest possible rank. Also I think we can code an embedding from $V$ to $V$ by using the Set coding scheme.
first-order-logic alternative-set-theories
asked Jan 6 at 10:46
ZuhairZuhair
354212
$endgroup$
Lets weaken the limitation of size axiom of MK to that of sets, i.e. every class that is subnumerous to a set is a set, now to that version of $MK$ lets add to the language of it a primitive unary coding function $Cd$, and restrict class comprehension axiom of $MK$ to pure class theoretic formulas (i.e. formulas not using $Cd$), and add an axiom that all codes are sets, i.e. $[y=Cd(x) to y in V]$, where $V$ is the class of all sets. Also axiomatize that the coding function is bijective. Now to the resulting theory can we add the following schemata?
Class coding schema: if $varphi(z)$ is a formula in $L(=,in)$, in which $x$ is not free, then: $$exists x forall y (y in x leftrightarrow exists z (varphi(z) wedge y=Cd(z)))$$
Set coding scheme: if $varphi^V(z)$ is a formula in which all of its quantifiers are bounded in $V$, then for all set closures we have:
$$exists x forall y (y in x leftrightarrow exists z in V (varphi^V(z) wedge y=Cd(z)))$$
In English: The class coding scheme states that we can construct any class of codes of classes as long as the latter ones are predicated in pure class language. While the set coding schema states that we can construct any class of codes of sets predicated by formulas restricted to sets but allowed to use the coding function.
From that we can for example define Cardinality by a modification of Scott's trick, as Cardinality of any class $x$ is the class of all codes of classes equinumerous to $x$ of the lowest possible rank. Also I think we can code an embedding from $V$ to $V$ by using the Set coding scheme.
first-order-logic alternative-set-theories
first-order-logic alternative-set-theories
asked Jan 6 at 10:46
ZuhairZuhair
354212
asked Jan 6 at 10:46
ZuhairZuhair
354212
edited Jan 6 at 21:10
Zuhair
asked Jan 6 at 10:46
ZuhairZuhair
354212
asked Jan 6 at 10:46
ZuhairZuhair
354212
asked Jan 6 at 10:46
ZuhairZuhair
354212
354212
$begingroup$
Presumably you want to include additional axioms - what if $Cd(y)=emptyset$ for every $y$? At the very least you want $Cd$ to be injective I think ...
$endgroup$
– Noah Schweber
Jan 6 at 11:00
$begingroup$
Yes, that's perfectly correct, actually I need it to bijective. Thanks
$endgroup$
– Zuhair
Jan 6 at 11:01
add a comment |
$begingroup$
Presumably you want to include additional axioms - what if $Cd(y)=emptyset$ for every $y$? At the very least you want $Cd$ to be injective I think ...
$endgroup$
– Noah Schweber
Jan 6 at 11:00
$begingroup$
Yes, that's perfectly correct, actually I need it to bijective. Thanks
$endgroup$
– Zuhair
Jan 6 at 11:01
$begingroup$
Presumably you want to include additional axioms - what if $Cd(y)=emptyset$ for every $y$? At the very least you want $Cd$ to be injective I think ...
$endgroup$
– Noah Schweber
Jan 6 at 11:00
$begingroup$
Presumably you want to include additional axioms - what if $Cd(y)=emptyset$ for every $y$? At the very least you want $Cd$ to be injective I think ...
$endgroup$
– Noah Schweber
Jan 6 at 11:00
$begingroup$
Yes, that's perfectly correct, actually I need it to bijective. Thanks
$endgroup$
– Zuhair
Jan 6 at 11:01
$begingroup$
Yes, that's perfectly correct, actually I need it to bijective. Thanks
$endgroup$
– Zuhair
Jan 6 at 11:01
add a comment |
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: "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%2f3063708%2fcan-we-extend-a-version-of-mk-with-that-coding-function%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 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%2f3063708%2fcan-we-extend-a-version-of-mk-with-that-coding-function%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$
Presumably you want to include additional axioms - what if $Cd(y)=emptyset$ for every $y$? At the very least you want $Cd$ to be injective I think ...
$endgroup$
– Noah Schweber
Jan 6 at 11:00
$begingroup$
Yes, that's perfectly correct, actually I need it to bijective. Thanks
$endgroup$
– Zuhair
Jan 6 at 11:01