Santa Exists!
Here is a theorem that I like to mention during the first week when I teach set theory.
Theorem. Santa exists!
Proof. Consider the set
Then The forward implication of \eqref{hohoho} gives that
But then, the backward implication of gives that
Knowing that and , we conclude that Santa does exist! QED
As you probably noticed, this is actually a disguised version of Russell’s Paradox, which is due to Haskell Curry. Should Santa fail to exist, would simply become the usual paradoxical set (but we all know that simply consists of all sets).
What I like about this variant of Russell’s Paradox is that it does not rely on the law of excluded middle.^{1} The usual argument for Russell’s Paradox proceeds by reaching a contradiction from and another contradiction from . In order to reach a final contradiction, this argument assumes that is true, so all of your intuitionist students will immediately be disappointed.
On the other hand, Curry’s Paradox works even in minimal logic! The only sketchy step is the deduction of from \eqref{hohoho}. The forward implication actually is
and the desired conclusion is reached by contraction (the fact that assuming twice is not more powerful than assuming it once). Odds are that very few students will bother counting how many times the assumption is used in this step.
This shows that selfreference is not a problem unique to classical logic. It applies equally well to intuitionistic and minimal logic. In fact, to avoid selfreferential paradoxes through logic it seems necessary to reject the contraction rule (as in linear logic). This is rather extreme from the foundational perspective, so we’re probably better off resolving selfreferential issues by other means.
My personal conclusion from this story is that logicians will never be out of work… so Santa does exist!!!

As Andreas Blass pointed out in the comments, one can derive Russell’s Paradox in intuitionistic logic. (By the same argument, replacing Santa exists by .) The real strength of Curry’s Paradox is that it does not even use negation! ↩
Originally posted on by François G. Dorais. To the extent possible under law, François G. Dorais has waived all copyright and neigboring rights to this work.
Comments

Andreas Blass wrote
I don’t think the Russell paradox needs the law of the excluded middle. Once you’ve derived (as you said) a contradiction from and another contradiction from , the first proves (even intuitionistically) that (thanks to the intuitionistic meaning of negation as implying a contradiction), and then the second gives you an outright contradiction.

François G. Dorais replied to Andreas Blass
Right! The same argument works replacing “Santa exists” by …
I was thinking of a different argument (which I think is how the paradox is usually described): Since and , from we conclude .
I guess the real difference is that Curry’s version doesn’t require negation (or ).

Buschi Sergio wrote
This is simply (seem to me) a wrong proof (no a different version of Russel paradox).
When you write: “The forward implication of (∗) gives that…” forget to mention

François G. Dorais replied to Buschi Sergio
This is explained later on in the post. The forward implication is which gives by contraction.
Of course, this is an invalid proof in linear logic, which does not admit the contraction rule, but then I would have to be more precise about what implication means…