Mathematical Structures in Computer Science

Table of Contents - 2001 - Volume 11, Issue 04  

Special Issue: Modalities in Type Theory

The Russell–Prawitz modality

PETER ACZEL a1
a1 Departments of Mathematics and Computer Science, Manchester University, Manchester M13 9PL, England

Abstract

In his 1903, Principles of Mathematics, Bertrand Russell mentioned possible definitions of conjunction, disjunction, negation and existential quantification in terms of implication and universal quantification, exploiting impredicative universal quantifiers over all propositions. In his 1965 Ph.D. thesis Dag Prawitz showed that these definitions hold in intuitionistic second order logic. More recently, these definitions have been used to represent logic in various impredicative type theories. This treatment of logic is distinct from the more standard Curry–Howard representation of logic in a dependent type theory.

The main aim of this paper is to compare, in a purely logical, non type-theoretic setting, this Russell–Prawitz representation of intuitionistic logic with other possible representations. It turns out that associated with the Russell–Prawitz representation is a lax modal operator, which we call the Russell–Prawitz modality, and that any lax modal operator can be used to give a translation of intuitionistic logic into itself that generalises both the double negation interpretation, double negation being a paradigm example of a lax modality, and the Russell–Prawitz representation.

(Received October 20 1999)
(Revised May 23 2000)