6
$\begingroup$

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.

$\endgroup$
5
$\begingroup$

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)

$\endgroup$
  • 1
    $\begingroup$ A propos of this answer, there is an article of John Bell which asserts the same thing: publish.uwo.ca/~jbell/BOOLCON.pdf $\endgroup$ – Todd Trimble Mar 15 '16 at 12:09
  • $\begingroup$ Thanks for the precision, I did not know this references. The proof in the article is a little more "High tech", but it's good to have a confirmation. $\endgroup$ – Simon Henry Mar 15 '16 at 12:32
  • $\begingroup$ The article also seems to claim that it does not implies more than the De Morgan's law (it uses this as an argument to say that this form of the ultrafilter lemma does not implies stone representation theorem because stone representation would implies the law of excluded middle) but I don't see a proof of this in the article. $\endgroup$ – Simon Henry Mar 15 '16 at 12:35
4
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Thanks! I've edited the question to take into account your point about the subtlety of stating the ultrafilter principle in constructive settings. $\endgroup$ – Sebastian Conybeare Mar 15 '16 at 4:09

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.