The Russell–Prawitz modality
The Russell–Prawitz modality
复制标题
罗素-普拉维茨模态
DOI：
--
复制
发表时间：
2001
影响因子：
0.5
通讯作者：
P. Aczel
中科院分区：
文献类型：
--
作者：
P. Aczel
伯特兰·罗素 (Bertrand Russell) 在其 1903 年出版的《数学原理》中，从蕴涵和全称量化的角度提到了合取、析取、否定和存在量化的可能定义，对所有命题利用了谓语全称量词。 1965 年，他获得博士学位。达格·普拉维茨 (Dag Prawitz) 的论文表明，这些定义在直觉二阶逻辑中成立。最近，这些定义已被用来表示各种谓语类型理论中的逻辑。这种逻辑处理不同于依赖类型理论中更标准的柯里-霍华德逻辑表示。本文的主要目的是在纯逻辑、非类型论的背景下，将直觉逻辑的罗素-普拉维茨表示与其他可能的表示进行比较。事实证明，与 Russell-Prawitz 表示相关的是一个宽松模态运算符，我们将其称为 Russell-Prawitz 模态，并且任何宽松模态运算符都可以用来将直觉逻辑翻译为自身，从而概括了双重否定解释（双重否定是宽松模态的范式示例）和 Russell-Prawitz 表示。
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.