Skip to main content
1 of 2
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?

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 \|$).

King Kong
  • 631
  • 3
  • 16