2

Suppose that $E$ is an elementary topos. Thus, for every object $X\in E$ one has the corresponding existential quantifier $\exists_X:PX\rightarrow \Omega$. My question is:

Whats is the subobject of the power $PX$ classified by $\exists_X$?

My guess is that this subobject is nothing but the singleton map $\{\cdot\}_X:X\rightarrow PX$. Is this correct?

J. W. Tanner
  • 60,406
None
  • 31

1 Answers1

1

It is not just the singleton map, but the image of $\pi_2\circ\epsilon:\in\;\hookrightarrow X\times PX\to PX$. After all, given a formula $\varphi(x)$, you still want the existential quantifier map to return $\top$ if $\{x:\varphi(x)\}$ has more than one element--you want it to return $\top$ on any non-empty "subset" of $X$.

Malice Vidrine
  • 9,653
  • I see, @Malice Vidrine, thanks!... For instance, this means that, if $E$ is a sheaf topos, existence means externally just local existence? – None Oct 24 '20 at 21:57