Luca Tranchini (Université de Tübingen)

Proof and paradox: some problems, some solutions

Developing early results of Prawitz, Tennant proposed a criterion for an expression to count as a paradox in the framework of Gentzen’s natural deduction: paradoxical expressions give rise to non-normalizing derivations. Two distinct kinds of cases seem to show that the criterion overgenerates, ie there are two kinds of derivations which are intuitively non-paradoxical but which fail to normalize.

Tennant’s proposed solution consists in rejecting modus ponens in favor of the so-called general (or parallelized) elimination rule for implication. On this basis, Tennant’s ends up reenacting Ramsey’s distinction between semantic and mathematical paradoxes: while the Liar paradox is inherently non-normalizing, Russell’s paradox can be cashed out as a normalizing derivation of the non-existence of Russell’s set (on the background of intuitionistic or, say, classical logic).

We first cast doubts on Tennant’s revival of the distinction between semantic and mathematical paradoxes: As Russell’s paradox can be cashed out as the non-existence of Russell’s set (on the background of classical or, say, intuitionistic logic), so the Liar paradox can be cashed out as the non-existence of a fully transparent truth-predicate (again on the background of classical or, say, intuitionistic logic).

We then show that the adoption of the general elimination rule is not enough to avoid normalization failure, and conclude by arguing that an appropriate solution to at least one of the problematic overgeneration cases can be attained by introducing a criterion to decide whether a given proof-transformation is acceptable.