On the structure of paradoxes (Q1204111)

Most of the well-known paradoxes are produced by presenting a formula \(\psi\) such that \(\psi\leftrightarrow \neg \psi\) --- whereupon everything can be proved. In section I of this paper, a general pattern is described, which many constructions of \(\psi\) follow: e.g., the famous arguments of Cantor, Russell and Gödel. The structure uncovered behind them is generalized in section II. This allows us to show that Reynolds' construction of a type \(A\simeq \wp\wp A\) in polymorphic \(\lambda\)- calculus (where \(\wp A\) represents the ``powerset of \(A\)'') cannot be extended, as conjectured, to give a fixed point of \textit{every} variable type derived from the exponentiation: for some (contravariant) types, such a fixed point causes a paradox. If the categorical interpretation of type theory is viewed as an extension of the (Lindenbaum-Tarski's) algebraic approach to logic, the language of categories appears to be a natural medium for reasoning about paradoxes. It allows us to abstract from the specific predicates that appear in them, and to display the underlying constructions in ``pure state''. The essential role of Cartesian closed categories in this context has been pointed out by Lawvere. The paradoxes studied in this paper remain within the limits of the Cartesian closed structure of types. Our results can be translated into simply typed \(\lambda\)-calculus in a straightforward way (although some of them do become a bit messy).