2
$\begingroup$

Let $V^{H}$ be a Heyting valued model of intuitionistic set theory. What conditions does $H$ have to satisfy in order for the following claim to hold? (where $\| \phi(u) \| \in H$ is the truth value of the sentence $\phi(u)$ of the language of IZF + the names of the elements of $V^{H}$ and for any $x \in V$, $\hat{x}$ is the canonical representative of $x$ in $V^{H}$)

Claim: For any $u, v \in V^{H}$, if

(a) $V^{H} \models u$ and $v$ are Dedekind real numbers,

and

(b)$\| u = v \| \neq 1 $,

then there exists a rational number $q \in \mathbb{Q}$ such that $\|\hat{q} \in u \| = 1 \neq \| \hat{q} \in v \|$ (or vice versa, i.e. $\|\hat{q} \in v \| = 1 \neq \| \hat{q} \in u \|$).

Note that it is always the case that if $u$ and $v$ satisfy (a) and (b), then there will exist $q \in \mathbb{Q}$ such that $\|\hat{q} \in u\| \neq \| \hat{q} \in v \|$. The quesiton is when we can use such a $q$ to build a rational that satisfies the claim.

The notion of Dedekind real I'm working with here is given by the formula

$r \subseteq \mathbb{Q} \wedge \exists x \in \mathbb{Q} (x \in r) \wedge \exists x \in \mathbb{Q} (x \notin r) \wedge \forall x \in \mathbb{Q} ( x \in r \leftrightarrow \forall y \in \mathbb{Q} (x \lneq y \rightarrow y \in r ))$

Call this formula $\phi(r)$. If $\| \phi(u) \| = 1$, then assuming that $H$ is uncountable, it is easy to show that there exists $q \in \mathbb{Q}$ such that $\|\hat{q} \in u \| = 1$. What other conditions does $H$ need to satisfy?

Improve this question
$\endgroup$
8
  • $\begingroup$ If I understand your question well, I would says that it is nearly impossible. It seems that it imply $H=\{0,1\}$ $\endgroup$
    – Simon Henry
    Commented Jan 17, 2014 at 10:22
  • $\begingroup$ 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. $\endgroup$
    – King Kong
    Commented Jan 17, 2014 at 10:46
  • $\begingroup$ 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... $\endgroup$
    – Simon Henry
    Commented Jan 17, 2014 at 13:03
  • $\begingroup$ 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... $\endgroup$
    – Simon Henry
    Commented Jan 17, 2014 at 13:11
  • 1
    $\begingroup$ 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. $\endgroup$
    – Andreas Blass
    Commented Jan 17, 2014 at 15:47

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .