Which Heyting algbras arise out of some elementary topos which satisfies the ultrafilter principle?

Question

It is known that AC implies LEM constructively, and also that AC implies the ultrafilter principle. Is there a similar relationship between the ultrafilter principle and classical logic? In other words, are there any inference rules of propositional logic which are classically-but-not-constructively admissible, but are constructively admissible assuming the ultrafilter principle?

Edit: François G. Dorais points out that defining ultrafilters in constructive settings can be somewhat subtle. I'd naively guess that the "right" way to state it would be that every consistent boolean algebra $B$ admits a homomorphism $B \to 2$. This would be "right" in the sense of implying the completeness theorem of classical FOL. I think this works in François' example, since we can take the consistent boolean algebra $B$ of decidable subsets of $\mathbb{N}$, quotient by the Fréchet filter $F$, and then take the preimage of $\top$ under $B \to B/F \to 2$ to be our desired ultrafilter.

To clarify the question, consider this: we can associate to every elementary topos $E$ the subobject lattice of the terminal object $1$, which is equivalently the Heyting algebra of global elements of the subobject classifier $\Omega$. My question would then be to ask which Heyting algebras can arise this way from an elementary topos $E$ whose internal logic satisfies the ultrafilter principle.

Answer 1

I think your formulation of the ultrafilter principle implies the de Morgan law.

Let $U$ be any proposition, consider the boolean algebra $A$ freely generated by an element $v$.

so $A = \{ 0,1,v,\neg v \}$.

Consider the following equivalence relation on $A$:

$$ \{(0,0),(1,1),(v,v),(\neg v, \neg v) \} \cup U \times \{ (0,v),(1,\neg v) \} \cup (\neg U) \times \{ (1,v),(0,\neg v) \} $$

(I didn't write it, but of course, as soon as you have an element $(x,y)$ in the relation you also add the element $(y,x)$ in the relation)

A long and uninteresting case by case treatment shows that it is an equivalence relation compatible to the boolean algebra structure and hence the quotient is again a boolean algebra $B$.

$0$ and $1$ are different in $B$, so by the ultrafilter principle there should exist a morphism $B \rightarrow 2$. the image of $v$ is either $0$ or $1$.

If it is zero, then as $\neg U \Rightarrow v=1$ one has $\neg \neg U$ and if it is one then $\neg U$ for the same reason hence $\neg U $ or $\neg \neg U$ which is an equivalent form of De Morgan's law.

If you want to avoid this kind of problem you need to restrict to decidable boolean algebra, that is those which satisfies $\forall v \in B,v=0$ or $v \neq 0$ (this also prevent the example in François G dorsais's answer)

Answer 2

Yes, plenty! But this is subtle since it's hard to define what an ultrafilter is in constructive settings.

An ultrafilter $\mathcal{U}$ on $\mathbb{N}$, in the classical sense, easily allows the Limited Principle of Omniscience (LPO). That principle says that if $\alpha(n)$ is decidable (either true or false for every $n$) then either $\forall n \alpha(n)$ or $\exists n \lnot \alpha(n)$. Given an ultrafiler $\mathcal{U}$, just check whether $\{n \in \mathbb{N} : (\exists m < n)\lnot\alpha(m)\} \in \mathcal{U}$ to decide this.

Note that I needed the decidability of $\alpha(n)$ to make this work. It is not true in a constructive setting that every reasonable $\alpha$ is so decidable, so an ultrafilter might not help immediately. However, in most constructive settings, primitive recursive $\alpha(n)$ are decidable and this is already nontrivial. By induction, every arithmetical statement is decidable in this way given an ultrafilter $\mathcal{U}$. On the other hand, nothing else is since an ultrafilter predicate over second-order logic is conservative over arithmetic comprehension.