Skip to main content
2 of 2
clarification
King Kong
  • 631
  • 3
  • 16

Dedekind reals in heyting valued models

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?

King Kong
  • 631
  • 3
  • 16