As said in the comment, I'm not sure what to add to the paragraph, the point is that in a topos there is no functions $\Omega \to \Omega$ that has the property expected of a neccessity operator except the identity.

If I can give an intuitive explanation the idea is that if you only have two truth values "true" and "false", then you don't really have a choice, you need to define $\square true = true$ and $\square false = false$.

Now in a topos, you get in a sense more truth value, collected in the object $\Omega$, but to some extent the internal logic doesn't fully agree that you have more than two truth value: for example the following statement is always internally true

$$ \forall x \in \Omega, (x \neq true) \Rightarrow x = false $$

(which for course cannot be rewritten as "$x = false$ or $x = true$" as we don't have the law of excluded middle).

And it happen that this sort of thing is actually enough to prevent having an "internal" necessity operator.

An internal proof that there is not such operator look like:

Let $\square : \Omega \to \Omega$ a function such that $\square true = true$ and $\forall x \in \Omega, \square x \leqslant x$. Let $x \in \Omega$. Assume $x$ is true, them $\square x = \square true = true$, i.e. if $x$ then $\square x$. So we have proved that $x \Rightarrow \square x$. As we are also assuming $\square x \leqslant x$, this shows that $\square x = x$.

As said in the comment, I'm not sure what to add to the paragraph, the point is that in a topos there is no functions $\Omega \to \Omega$ that has the property expected of a neccessity operator except the identity.

$\newcommand\true{\mathrm{true}}\newcommand\false{\mathrm{false}}$If I can give an intuitive explanation the idea is that if you only have two truth values "$\true$" and "$\false$", then you don't really have a choice, you need to define $\square\true = \true$ and $\square\false = \false$.

Now in a topos, you get in a sense more truth value, collected in the object $\Omega$, but to some extent the internal logic doesn't fully agree that you have more than two truth value: for example the following statement is always internally true

$$ \forall x \in \Omega, (x \neq \true) \Rightarrow x = \false $$

(which of course cannot be rewritten as "$x = \false$ or $x = \true$" as we don't have the law of excluded middle).

And it happens that this sort of thing is actually enough to prevent having an "internal" necessity operator.

An internal proof that there is no such operator looks like:

Let $\square : \Omega \to \Omega$ be a function such that $\square\true = \true$ and $\forall x \in \Omega, \square x \leqslant x$. Let $x \in \Omega$. Assume $x$ is true, them $\square x = \square\true = \true$, i.e. if $x$ then $\square x$. So we have proved that $x \Rightarrow \square x$. As we are also assuming $\square x \leqslant x$, this shows that $\square x = x$.

As said in the comment, I'm not sure what to add to the paragraph, the point is that in a topos there is no functions $\Omega \to \Omega$ that has the property expected of a neccessity operator except the identity.

If I can give an intuitive explanation the idea is that if you only have two truth values "true" and "false", then you don't really have a choice, you need to define $\square true = true$ and $\square false = false$.

Now in a topos, you get in a sense more truth value, collected in the object $\Omega$, but to some extent the internal logic doesn't fully agree that you have more than two truth value: for example the following statement is always internally true

$$ \forall x \in \Omega, (x \neq true) \Rightarrow x = false $$

(which for course cannot be rewritten as "$x = false$ or $x = true$" as we don't have the law of excluded middle).

And it happen that this sort of thing is actually enough to present having an "internal" necessity operator.

An internal proof that there is not such operator look like:

Let $\square : \Omega \to \Omega$ a function such that $\square true = true$ and $\forall x \in \Omega, \square x \leqslant x$. Let $x \in \Omega$. Assume $x$ is true, them $\square x = \square true = true$, i.e. if $x$ then $\square x$. So we have proved that $x \Rightarrow \square x$. As we are also assuming $\square x \leqslant x$, this shows that $\square x = x$.

As said in the comment, I'm not sure what to add to the paragraph, the point is that in a topos there is no functions $\Omega \to \Omega$ that has the property expected of a neccessity operator except the identity.

If I can give an intuitive explanation the idea is that if you only have two truth values "true" and "false", then you don't really have a choice, you need to define $\square true = true$ and $\square false = false$.

Now in a topos, you get in a sense more truth value, collected in the object $\Omega$, but to some extent the internal logic doesn't fully agree that you have more than two truth value: for example the following statement is always internally true

$$ \forall x \in \Omega, (x \neq true) \Rightarrow x = false $$

(which for course cannot be rewritten as "$x = false$ or $x = true$" as we don't have the law of excluded middle).

And it happen that this sort of thing is actually enough to prevent having an "internal" necessity operator.

An internal proof that there is not such operator look like:

Let $\square : \Omega \to \Omega$ a function such that $\square true = true$ and $\forall x \in \Omega, \square x \leqslant x$. Let $x \in \Omega$. Assume $x$ is true, them $\square x = \square true = true$, i.e. if $x$ then $\square x$. So we have proved that $x \Rightarrow \square x$. As we are also assuming $\square x \leqslant x$, this shows that $\square x = x$.