Let $P$ be an arbitrary proposition.

Let a proposition $C$ be defined:

$C \implies P$

Aiming for a contradiction, suppose that $\neg C$.

Then $C \implies P$ is vacuously true.

By definition, $C$ is true, a contradiction.

This contradiction shows $C$ to be true.

By definition, $C \implies P$.

By Modus Ponendo Ponens, we conclude $P$, where $P$ is arbitrary.

But this means that any proof system expressing the above is inconsistent.

Also known as

Curry's Paradox can also be seen referred to as Löb's Paradox after Martin Hugo Löb.

Source of Name

This entry was named for Haskell Brooks Curry.