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.