NORAD, it seems, believe Father Christmas exists. So here's a proof of his existence, that I found in Logics, Categories, and Colimits for Artificial Intelligence: Exercise Sheet 9 by Till Mossakowski of the University of Freiburg.

To prove that Father Christmas exists, we'll assume the opposite and
show that it leads to a contradiction. So assume that *Father Christmas
does
not exist*:

does_not_exist(father_christmas) | (1) |

But then we
can apply the rule of
existential-quantifier introduction. This is the formal
equivalent of inferring from *John is fat*
that *someone is fat*, i.e. that *there exists an x such that x is
fat*. So we infer from *Father Christmas does
not exist* that *there exists an x such that x does not exist*:

∃x does_not_exist(x) | (2) |

But (2) is a contradiction.

Therefore, our assumption (1) must be wrong.

Therefore, Father Christmas exists. ∎

Of course, there could be an unnoticed bug
in this proof technique. So before posting,
I tested it on the existence of: (a) wasps;
(b) winter; (c) Windows 7. Wasps
are something I've never seen the
point of, but they
exist, and so do the other things.
When tested with each, the proof technique
ran to completion in my brain, *and* gave a
result that's consistent with reality. Therefore,
I claim it adequately tested. Any programmer will
tell you that three test runs is enough.