直觉主义否定自由逻辑中限定描述的两种处理方式

包含限定描述（即“那个 $F$”形式的表达式）的句子可以使用二元量词 $\iota$ 来形式化，该量词由两个谓词构成一个公式，其中 $\iota x[F, G]$ 读作“那个 $F$ 是 $G$”。这是对通常用语项形成算子形式化限定描述的一种创新。本文比较了这两种方法。在简要概述由 \citep{kurbisiotaI} 提出的、经此类量词扩展的直觉主义否定自由逻辑系统 $\mathbf{INF}^\iota$ 之后，首先将 $\mathbf{INF}^\iota$ 与 Tennant 的一个系统以及直觉主义否定自由逻辑内语项形成 $\iota$ 算子的公理化处理进行比较。两个系统都被证明等价于 $\mathbf{INF}^\iota$ 中 $\iota x[F, G]$ 的 $G$ 被限制为同一性的子系统。然后将 $\mathbf{INF}^\iota$ 与 Lambert 系统的一个直觉主义版本进行比较，该版本除语项形成算子外还有一个用于谓词抽象以指示辖域区别的算子。将通过两种系统各自语言之间的翻译证明它们是等价的。讨论中指出了本方法相对于其他方法的优势。