On the structure of paradoxes
type: Item
instance of: scholarly article
title: On the structure of paradoxes
zbMATH Open document ID: 0776.03005
DOI: 10.1007/BF01277482
published in: Archive for Mathematical Logic
publication date: 1993-09-01T00:00:00Z
review text: 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).
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 03G30
Mathematics Subject Classification ID: 18D15
zbMATH DE Number: 126090
zbMATH Keywords: Russel's paradox
zbMATH Keywords: Cantor's diagonalization
zbMATH Keywords: Gödel's incompleteness theorems
zbMATH Keywords: paradoxical structures
zbMATH Keywords: paradoxes
zbMATH Keywords: polymorphic \(\lambda\)- calculus
zbMATH Keywords: categorical interpretation of type theory
zbMATH Keywords: Cartesian closed categories
zbMATH Keywords: simply typed \(\lambda\)-calculus
author: Dusko Pavlovic
MaRDI profile type: Publication
cites work: Q3727946
cites work: Constructivism in mathematics. An introduction. Volume I
description: scientific article; zbMATH DE number 126090