I used to be more confident about Curry's paradox.

The basic form of the paradox is:

( 0 *)  If this sentence is true, then Santa Claus exists.

Hypothetically, if this statement were true, then it would follow by modus ponens that Santa Claus exists. But this if-then implication is exactly what the sentence claims, so it is in fact true and therefore we must conclude that Santa Claus exists.

Since (spoiler alert) Santa Claus does not in fact exist, we have a contradiction.

The way I formerly resolved the problem was like this:

By asserting the existence (but not necessarily the truth) of the sentence in question, we are defining as follows:

( 1 *)  let P = (P → Q)

Superficially, this seems valid, since we are accustomed to presuming in favor of the legitimacy of assigning values to free variables (e.g. "let x = 3"). However, when the definition contains the variable being assigned, this presumption may not hold. By way of analogy, consider the following purported assignment:

( 2a*)  let x = (x + 1)

In this case, the invalidity of the statement is clear. One way to think about it is that we are first creating an anonymous expression:

( 3  )  (x + 1)

and then subsequently binding it as a value to a variable:

( 2b*)  let x = (x + 1)
( 4  )  let y = (x + 1)

Here, it is clearer that in (2b*), x is no longer free because it was used in (3).

I had been satisfied with this rebuttal until I thought of the argument in the next section.

Quining allows indirect, implicit self-reference.

Consider the following statement:

( 5 *)  If the quine of "If the quine of [____] is true, then Santa Claus exists."
        is true, then Santa Claus exists.

We can formalize this a bit as follows:

( 6 ?)  let Quine(f) = f(f),
        with domain restricted to functions f such that:
          f is a function of exactly one argument, and
          f is an element of the domain of f.

( 7  )  let C be false

(C might be taken to stand for Claus, Christmas, Contradiction, or Catastrophe.)

( 8 ?)  let Para(f) = (Quine(f) → C)

( 9 *)  let Para(Para) be a well-formed expression
        (not necessarily evaluating to TRUE)

(10 *)  Para(Para) = (Quine(Para) → C)

(11 *)  Para(Para) = (Para(Para) → C)

(12 *)  Para(Para) → (Para(Para) → C)

(13 *)  Para(Para) → C

(14 *)  (Para(Para) → C) → Para(Para)
        (from (11*))

(15 *)  Para(Para)
        (from (13*) and (14*))

(16 *)  C
        (from (13*) and (15*))

I'm pretty sure the error is introduced in step (6?), (8?), or (9*), but I'm not sure which or why. My current best guess is that Para is not an element of its own domain.

It occurs to me that, given (7), (8?) is strictly equivalent to:

(17 ?)  let Para(f) = ~Quine(f)

which can be further rewritten as:

(18 ?)  let Para(f) = ~f(f)

which looks a whole lot less interesting than (5*) – it's basically just the Mockingbird's evil twin.

So I'm pretty sure the final answer is "crisis averted, you can all go home, sorry for waking you up". Still, it would be nice to hear from someone who actually knows what they're talking about.