Cardinality of the set of truth values in a Heyting-valued model of IZF

155 Views Asked by At

I've very recently become interested in intuitionistic set theory. I'm now trying to get acquainted with the very basics, and I have a number of small silly questions, that might not make sense due to my current lack of knowledge (apologies if that's the case).

Can the cardinality of the set $\Omega$ of truth values/subobject classifier in a Heyting-valued model of intuitionistic ZF be defined (internally to the model)?

If so, can it be different from 2? And does it coincide with the cardinality of $\Omega$ as an ordinary set?

For example, taking $\Omega$ as the Heyting algebra from the third example here, would its internal cardinality be 2, 3 or undefined?

I've found this article that claims that the cardinality cannot generally be defined in constructive mathematics except for a special type of decidable sets, but the article doesn't go into much detail as to why; it only rules out the existence of a map assigning the cardinality 1 to singletons.