Timeline for Dedekind reals in heyting valued models
Current License: CC BY-SA 3.0
11 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 17, 2014 at 16:19 | comment | added | King Kong | thanks, that's helpful, but I'm still quite confused. How exactly are $u$ and $v$ being defined here, and how are we guaranteed that $V^{H}$ says that they are Dedekind reals? | |
| Jan 17, 2014 at 15:47 | comment | added | Andreas Blass | Here's a $V^H$ translation of the simplest special case of Simon Henry's comment. Let $H$ be the 4-element Boolean algebra $\{0,1,b,\neg b\}$. Let $u$ and $v$ be the elements of $V^H$ satisfying $\Vert u=1\Vert=\Vert v=0\Vert=b$ and $\Vert u=0\Vert=\Vert v=1\Vert=\neg b$. Then $\Vert u\neq v\Vert=1$, but no (genuine, external) rational number $q$ satisfies the conclusion you want. To get $\Vert\hat q\in u \Vert=1$, you'd need $q\geq 1$, but then $\Vert\hat q\in v\Vert=1$ also; and similarly with the roles of $u$ and $v$ interchanged. | |
| Jan 17, 2014 at 13:58 | comment | added | King Kong | It seems that you are talking about the topos of sheaves over $H$, which I believe is equivalent to $V^{H}$? However, I'm not too familiar with the sheaf of Dedekind reals in this kind of topos. Is there any way you could translate your proposed counterexamples into elements of $V^{H}$ using this equivalence? | |
| Jan 17, 2014 at 13:31 | history | edited | King Kong | CC BY-SA 3.0 |
clarification
|
| Jan 17, 2014 at 13:16 | comment | added | King Kong | I think that we are working with different notions here. I'm adding a bit more explanation to the question. Hopefully that will clarify things somewhat. | |
| Jan 17, 2014 at 13:11 | comment | added | Simon Henry | In fact, in my understanding of your notation, if by dedekind real you mean one sided Dedekind cut, then as soon as $H$ (a Heyting algebra) as a non trivial element $X$ one can define a dedekind real $u$ which is one on $X$ and zero outside of $X$, and take $v$ to be zero (or one, depending on if you consider upper or lower Dedekind cut) everywhere and it give a counterexample... | |
| Jan 17, 2014 at 13:03 | comment | added | Simon Henry | Ok then I definitely do not understand your notations. As I understand, if $H$ is a non trivial boolean algebra, and if X is any non trivial element of $H$ then I can consider $u$ and $v$ the two Dedekind reals over $H$ such that $u$ is 1 on $X$ and $0$ and its complementary and $v$ is $0$ on $X$ and $1$ on its complementary, then $u$ and $v$ are nowhere equal but you cannot find an external rational element that will attest it. I don't know if I can help you, but maybe you should make your notation clearer... | |
| Jan 17, 2014 at 10:46 | comment | added | King Kong | Here's a non trivial example where the claim holds. Let $H$ be any Heyting algebra such that $V^{H} \models (P(\omega)) \hat{} = P(\hat{\omega})$ (if H is a Boolean algebra, this holds whenever H satisfies the countable chain condition. I'm not sure if this is still the case when H is non-Boolean). Then $V^{H}$ satisfies the claim. For, in this case, there will be $\lambda$, $\mu \in \mathbb{R}$ such that $V^{H} \models u = \hat{\lambda}$ and $V^{H} \models v = \hat{\mu}$. So, given $q \in \mathbb{Q}$ such that $q \in \lambda$ and $q \notin \mu$, q will satisfy the claim. | |
| Jan 17, 2014 at 10:22 | comment | added | Simon Henry | If I understand your question well, I would says that it is nearly impossible. It seems that it imply $H=\{0,1\}$ | |
| Jan 17, 2014 at 9:13 | review | Low quality posts | |||
| Jan 17, 2014 at 11:09 | |||||
| Jan 17, 2014 at 8:33 | history | asked | King Kong | CC BY-SA 3.0 |