The unprovability of Pierce's law in a certain system.

Pierce's law is the rule:

((P implies Q) implies P) implies P.

This can be verified by a truth table, or by the following reasoning: if P is false, then P implies Q is true and P is false, so ((P implies Q) implies P) is false. Therefore P is implied by ((P implies Q) implies P).

However, it is interesting to ask for a syntactic proof of Pierce's law, that is, one that does not use the meaning of the word `implies' but only some rules for manipulating statements involving the implication symbol, and in particular deducing them from other such statements. There is a beautiful proof (shown to me by Thomas Forster) that Pierce's law does not follow in this way from certain other axioms. The proof uses three-valued logic to construct a simple model where the rules for deduction are valid and the other axioms true, but Pierce's law is false.