Hong Jin's blog about Software Engineering

On Peirce's Law

Peirce's Law makes me uncomfortable. It encodes the law of excluded middle:

((x → y) → x) → x.

An example of it could be read as:

If there is a fact that the floor will be wet if it rains, and that if this fact implies that the floor will be wet, then the floor must be wet.

It sounds entirely absurd, but if you viewed this by drawing out a truth table, then it makes perfect sense. Unfortunately, people don't reason about things by drawing out truth tables.

One trick is that x->y (the innermost parenthesis) is true in all cases where x is false. Therefore, with ((x -> y) -> x), we exclude the cases in x->y where x is false. Hence, since those cases are removed, only the case where x is true is left.