Mixing
Models of $mathrm{Vneq HOD}$
$begingroup$
This is basically a proof verification question. I want to find a model $mathrm{ZFC+Vneq HOD}$ where $mathrm{HOD}$ is the class of heriditarilly ordinal definable sets. The idea is to add one Cohen real and show that it is not ordinal definable in the extension. So let $M$ be a ground model and $Pin M$ be Cohen forcing. Let $G$ be $M$-generic for $P$ and let $c=bigcup G$.
Assume for a contradiction that $cinmathrm{OD}$. Then since there is a well-order $<_{mathrm{OD}}$ of $mathrm{OD}$ definable without parameters, we can define $c$ as the $alpha$-th element of $<_{mathrm{OD}}$ for some ordinal $alphain M$. In particular there is an $in$-formula $varphi(x,y)$ with (this is the part which I'm not sure about)
begin{equation}tag{1}
M[G]modelsforall i<omega(c(i)=1 leftrightarrow varphi(i,alpha))
end{equation}
By the forcing theorem we can take $pin G$ with
begin{equation}tag{2}
pVdashforall i<checkomega(bigcup dot G(i)=1 leftrightarrow varphi(i,checkalpha))
end{equation}
where $dot G$ is the canonical name for the generic filter. Now take any $nnotinoperatorname{dom}(p)$ and consider the embedding $pi_n:Pto P$ with
$$pi_n(q):operatorname{dom}(q)to2 qquadtext{with}qquad pi_n(q)(i)=begin{cases}q(i) & ineq n\ 1-q(i) & i=nend{cases}$$
Let $G':=pi_n[G]$ and $c':=bigcup G'$. Then (3) $G'$ is $M$-generic for $P$ (because $pi_n$ is an embedding) with $pin G'$ and (4) $M[G']=M[G]$ because the filters are easily definable from one another. Therefore
begin{align*}
c(n)=1 &iff M[G]modelsvarphi(n,alpha) tag{by (1)}\
&iff M[G']modelsvarphi(n,alpha) tag{by (4)}\
&iff c'(n)=1 tag{by (2) and (3)}
end{align*}
a contradiction.
Is this proof correct? Can some steps be done better/more elegantly? Are there other nice models of $mathrm{Vneq HOD}$?
proof-verification set-theory forcing
asked Jan 14 at 16:31
AchillesAchilles
877518
$endgroup$
add a comment |
$begingroup$
This is basically a proof verification question. I want to find a model $mathrm{ZFC+Vneq HOD}$ where $mathrm{HOD}$ is the class of heriditarilly ordinal definable sets. The idea is to add one Cohen real and show that it is not ordinal definable in the extension. So let $M$ be a ground model and $Pin M$ be Cohen forcing. Let $G$ be $M$-generic for $P$ and let $c=bigcup G$.
Assume for a contradiction that $cinmathrm{OD}$. Then since there is a well-order $<_{mathrm{OD}}$ of $mathrm{OD}$ definable without parameters, we can define $c$ as the $alpha$-th element of $<_{mathrm{OD}}$ for some ordinal $alphain M$. In particular there is an $in$-formula $varphi(x,y)$ with (this is the part which I'm not sure about)
begin{equation}tag{1}
M[G]modelsforall i<omega(c(i)=1 leftrightarrow varphi(i,alpha))
end{equation}
By the forcing theorem we can take $pin G$ with
begin{equation}tag{2}
pVdashforall i<checkomega(bigcup dot G(i)=1 leftrightarrow varphi(i,checkalpha))
end{equation}
where $dot G$ is the canonical name for the generic filter. Now take any $nnotinoperatorname{dom}(p)$ and consider the embedding $pi_n:Pto P$ with
$$pi_n(q):operatorname{dom}(q)to2 qquadtext{with}qquad pi_n(q)(i)=begin{cases}q(i) & ineq n\ 1-q(i) & i=nend{cases}$$
Let $G':=pi_n[G]$ and $c':=bigcup G'$. Then (3) $G'$ is $M$-generic for $P$ (because $pi_n$ is an embedding) with $pin G'$ and (4) $M[G']=M[G]$ because the filters are easily definable from one another. Therefore
begin{align*}
c(n)=1 &iff M[G]modelsvarphi(n,alpha) tag{by (1)}\
&iff M[G']modelsvarphi(n,alpha) tag{by (4)}\
&iff c'(n)=1 tag{by (2) and (3)}
end{align*}
a contradiction.
Is this proof correct? Can some steps be done better/more elegantly? Are there other nice models of $mathrm{Vneq HOD}$?
proof-verification set-theory forcing
asked Jan 14 at 16:31
AchillesAchilles
877518
$endgroup$
$begingroup$
Question - why do you need to go through the well-ordering of $OD$, and can't get the formula $varphi$ straight from $c$ being ordinal definable?
$endgroup$
– tzoorp
Jan 21 at 12:40
$begingroup$
Hmm, I think my thoughts behind that was that the formula you get from ordinal definability could potentially be nonstandard.
$endgroup$
– Achilles
Jan 21 at 20:56
add a comment |
$begingroup$
This is basically a proof verification question. I want to find a model $mathrm{ZFC+Vneq HOD}$ where $mathrm{HOD}$ is the class of heriditarilly ordinal definable sets. The idea is to add one Cohen real and show that it is not ordinal definable in the extension. So let $M$ be a ground model and $Pin M$ be Cohen forcing. Let $G$ be $M$-generic for $P$ and let $c=bigcup G$.
Assume for a contradiction that $cinmathrm{OD}$. Then since there is a well-order $<_{mathrm{OD}}$ of $mathrm{OD}$ definable without parameters, we can define $c$ as the $alpha$-th element of $<_{mathrm{OD}}$ for some ordinal $alphain M$. In particular there is an $in$-formula $varphi(x,y)$ with (this is the part which I'm not sure about)
begin{equation}tag{1}
M[G]modelsforall i<omega(c(i)=1 leftrightarrow varphi(i,alpha))
end{equation}
By the forcing theorem we can take $pin G$ with
begin{equation}tag{2}
pVdashforall i<checkomega(bigcup dot G(i)=1 leftrightarrow varphi(i,checkalpha))
end{equation}
where $dot G$ is the canonical name for the generic filter. Now take any $nnotinoperatorname{dom}(p)$ and consider the embedding $pi_n:Pto P$ with
$$pi_n(q):operatorname{dom}(q)to2 qquadtext{with}qquad pi_n(q)(i)=begin{cases}q(i) & ineq n\ 1-q(i) & i=nend{cases}$$
Let $G':=pi_n[G]$ and $c':=bigcup G'$. Then (3) $G'$ is $M$-generic for $P$ (because $pi_n$ is an embedding) with $pin G'$ and (4) $M[G']=M[G]$ because the filters are easily definable from one another. Therefore
begin{align*}
c(n)=1 &iff M[G]modelsvarphi(n,alpha) tag{by (1)}\
&iff M[G']modelsvarphi(n,alpha) tag{by (4)}\
&iff c'(n)=1 tag{by (2) and (3)}
end{align*}
a contradiction.
Is this proof correct? Can some steps be done better/more elegantly? Are there other nice models of $mathrm{Vneq HOD}$?
proof-verification set-theory forcing
asked Jan 14 at 16:31
AchillesAchilles
877518
$endgroup$
This is basically a proof verification question. I want to find a model $mathrm{ZFC+Vneq HOD}$ where $mathrm{HOD}$ is the class of heriditarilly ordinal definable sets. The idea is to add one Cohen real and show that it is not ordinal definable in the extension. So let $M$ be a ground model and $Pin M$ be Cohen forcing. Let $G$ be $M$-generic for $P$ and let $c=bigcup G$.
Assume for a contradiction that $cinmathrm{OD}$. Then since there is a well-order $<_{mathrm{OD}}$ of $mathrm{OD}$ definable without parameters, we can define $c$ as the $alpha$-th element of $<_{mathrm{OD}}$ for some ordinal $alphain M$. In particular there is an $in$-formula $varphi(x,y)$ with (this is the part which I'm not sure about)
begin{equation}tag{1}
M[G]modelsforall i<omega(c(i)=1 leftrightarrow varphi(i,alpha))
end{equation}
By the forcing theorem we can take $pin G$ with
begin{equation}tag{2}
pVdashforall i<checkomega(bigcup dot G(i)=1 leftrightarrow varphi(i,checkalpha))
end{equation}
where $dot G$ is the canonical name for the generic filter. Now take any $nnotinoperatorname{dom}(p)$ and consider the embedding $pi_n:Pto P$ with
$$pi_n(q):operatorname{dom}(q)to2 qquadtext{with}qquad pi_n(q)(i)=begin{cases}q(i) & ineq n\ 1-q(i) & i=nend{cases}$$
Let $G':=pi_n[G]$ and $c':=bigcup G'$. Then (3) $G'$ is $M$-generic for $P$ (because $pi_n$ is an embedding) with $pin G'$ and (4) $M[G']=M[G]$ because the filters are easily definable from one another. Therefore
begin{align*}
c(n)=1 &iff M[G]modelsvarphi(n,alpha) tag{by (1)}\
&iff M[G']modelsvarphi(n,alpha) tag{by (4)}\
&iff c'(n)=1 tag{by (2) and (3)}
end{align*}
a contradiction.
Is this proof correct? Can some steps be done better/more elegantly? Are there other nice models of $mathrm{Vneq HOD}$?
proof-verification set-theory forcing
proof-verification set-theory forcing
asked Jan 14 at 16:31
AchillesAchilles
877518
asked Jan 14 at 16:31
AchillesAchilles
877518
asked Jan 14 at 16:31
AchillesAchilles
877518
asked Jan 14 at 16:31
AchillesAchilles
877518
asked Jan 14 at 16:31
AchillesAchilles
877518
877518
$begingroup$
Question - why do you need to go through the well-ordering of $OD$, and can't get the formula $varphi$ straight from $c$ being ordinal definable?
$endgroup$
– tzoorp
Jan 21 at 12:40
$begingroup$
Hmm, I think my thoughts behind that was that the formula you get from ordinal definability could potentially be nonstandard.
$endgroup$
– Achilles
Jan 21 at 20:56
add a comment |
$begingroup$
Question - why do you need to go through the well-ordering of $OD$, and can't get the formula $varphi$ straight from $c$ being ordinal definable?
$endgroup$
– tzoorp
Jan 21 at 12:40
$begingroup$
Hmm, I think my thoughts behind that was that the formula you get from ordinal definability could potentially be nonstandard.
$endgroup$
– Achilles
Jan 21 at 20:56
$begingroup$
Question - why do you need to go through the well-ordering of $OD$, and can't get the formula $varphi$ straight from $c$ being ordinal definable?
$endgroup$
– tzoorp
Jan 21 at 12:40
$begingroup$
Question - why do you need to go through the well-ordering of $OD$, and can't get the formula $varphi$ straight from $c$ being ordinal definable?
$endgroup$
– tzoorp
Jan 21 at 12:40
$begingroup$
Hmm, I think my thoughts behind that was that the formula you get from ordinal definability could potentially be nonstandard.
$endgroup$
– Achilles
Jan 21 at 20:56
$begingroup$
Hmm, I think my thoughts behind that was that the formula you get from ordinal definability could potentially be nonstandard.
$endgroup$
– Achilles
Jan 21 at 20:56
add a comment |
1 Answer
1
active
oldest
votes
$begingroup$
Yes, the proof seems fine.
You can also check out Why does $mathsf{HOD}^{V[G]} subseteq mathsf{HOD}^V$ hold for weakly homogeneous forcings? where it is shown that if $Bbb P$ is a weakly homogeneous forcing (e.g. the Cohen forcing, various Levy collapses, and many other natural forcings), then $rm HOD^{it V[G]}subseteq HOD^{it V}(Bbb P)$.
In particular, if $V=rm HOD$ holds in the ground model, then the result follows. So practically any homogeneous forcing over $L$ will violate $V=rm HOD$, for example.
answered Jan 14 at 16:56
Asaf Karagila♦Asaf Karagila
304k32434764
$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%2f3073412%2fmodels-of-mathrmv-neq-hod%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$
Yes, the proof seems fine.
You can also check out Why does $mathsf{HOD}^{V[G]} subseteq mathsf{HOD}^V$ hold for weakly homogeneous forcings? where it is shown that if $Bbb P$ is a weakly homogeneous forcing (e.g. the Cohen forcing, various Levy collapses, and many other natural forcings), then $rm HOD^{it V[G]}subseteq HOD^{it V}(Bbb P)$.
In particular, if $V=rm HOD$ holds in the ground model, then the result follows. So practically any homogeneous forcing over $L$ will violate $V=rm HOD$, for example.
answered Jan 14 at 16:56
Asaf Karagila♦Asaf Karagila
304k32434764
$endgroup$
add a comment |
$begingroup$
Yes, the proof seems fine.
You can also check out Why does $mathsf{HOD}^{V[G]} subseteq mathsf{HOD}^V$ hold for weakly homogeneous forcings? where it is shown that if $Bbb P$ is a weakly homogeneous forcing (e.g. the Cohen forcing, various Levy collapses, and many other natural forcings), then $rm HOD^{it V[G]}subseteq HOD^{it V}(Bbb P)$.
In particular, if $V=rm HOD$ holds in the ground model, then the result follows. So practically any homogeneous forcing over $L$ will violate $V=rm HOD$, for example.
answered Jan 14 at 16:56
Asaf Karagila♦Asaf Karagila
304k32434764
$endgroup$
add a comment |
$begingroup$
Yes, the proof seems fine.
You can also check out Why does $mathsf{HOD}^{V[G]} subseteq mathsf{HOD}^V$ hold for weakly homogeneous forcings? where it is shown that if $Bbb P$ is a weakly homogeneous forcing (e.g. the Cohen forcing, various Levy collapses, and many other natural forcings), then $rm HOD^{it V[G]}subseteq HOD^{it V}(Bbb P)$.
In particular, if $V=rm HOD$ holds in the ground model, then the result follows. So practically any homogeneous forcing over $L$ will violate $V=rm HOD$, for example.
answered Jan 14 at 16:56
Asaf Karagila♦Asaf Karagila
304k32434764
$endgroup$
Yes, the proof seems fine.
You can also check out Why does $mathsf{HOD}^{V[G]} subseteq mathsf{HOD}^V$ hold for weakly homogeneous forcings? where it is shown that if $Bbb P$ is a weakly homogeneous forcing (e.g. the Cohen forcing, various Levy collapses, and many other natural forcings), then $rm HOD^{it V[G]}subseteq HOD^{it V}(Bbb P)$.
In particular, if $V=rm HOD$ holds in the ground model, then the result follows. So practically any homogeneous forcing over $L$ will violate $V=rm HOD$, for example.
answered Jan 14 at 16:56
Asaf Karagila♦Asaf Karagila
304k32434764
answered Jan 14 at 16:56
Asaf Karagila♦Asaf Karagila
304k32434764
answered Jan 14 at 16:56
Asaf Karagila♦Asaf Karagila
304k32434764
answered Jan 14 at 16:56
Asaf Karagila♦Asaf Karagila
304k32434764
304k32434764
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%2f3073412%2fmodels-of-mathrmv-neq-hod%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$
Question - why do you need to go through the well-ordering of $OD$, and can't get the formula $varphi$ straight from $c$ being ordinal definable?
$endgroup$
– tzoorp
Jan 21 at 12:40
$begingroup$
Hmm, I think my thoughts behind that was that the formula you get from ordinal definability could potentially be nonstandard.
$endgroup$
– Achilles
Jan 21 at 20:56