The Russell-Prawitz modality (Q2746758)

Bertrand Russell's \textit{The Principles of Mathematics} [Cambridge: University Press (1903; JFM 34.0062.14), London: Routledge (1992; Zbl 0873.01049)] contains possible definitions of conjunction, disjunction, negation and existential quantifier in terms of implication and universal quantifier, exploiting impredicative universal quantification over all propositions. For instance, conjunction \(A\wedge B\) is defined as \(\forall p(((A\to(B\to p))\to p)\), where the variable \(p\) is intended to range over all propositions. \textit{D. Prawitz} [Natural deduction: a proof-theoretical study, Almqvist and Wiksell, Stockholm (1965; Zbl 0173.00205)] showed that these definitions hold in second-order intuitionistic logic, and even in ramified second-order logic, provided that in each case the level of the bounded propositional variable is suitably chosen. In distinction from the standard Curry-Howard representation of logic in a dependent type theory, the definitions mentioned above have been used in the literature in order to represent logic in various impredicative type theories. In this paper the author compares, in a purely logical, non type-theoretic setting, the Russell-Prawitz representation of intuitionistic logic with other possible representations. It is shown that a lax modal operator, \(\neg\neg\) being the paradigm example, is associated with the Russell-Prawitz representation, and that any lax operator can be used to give a translation of intuitionistic logic into itself that generalizes both the double negation interpretation and the Russell-Prawitz representation.