含有明确描述的句子，即“The $F$”形式的表达，可以使用二元量词$ι$来形式化，该量词由两个谓词组成一个公式，其中$ιx[F, G]$读作“The $F$ is $G$”。这是一个创新，通常形式化的明确的描述与长期形成运营商。本文对这两种方法进行了比较。在简要概述了\citep{kurbisiotaI}中提出的由这种量词扩展的直觉负自由逻辑系统$\mathbf{INF}^ι$之后，首先将$\mathbf{INF}^ι$与Tennant的系统和直觉负自由逻辑中形成$ι$算子的项的公理化处理进行了比较。这两个系统被证明是等价的子系统的$\mathbf{INF}^ι$，其中的$G$的$ιx[F, G]$被限制到身份。$\mathbf{INF}^ι$，然后比较一个直观的版本的系统的兰伯特的，除了长期形成运营商有一个运营商的谓词抽象表示范围的区别。这两个系统将通过各自语言之间的翻译来证明是等效的。讨论中指出了本方法相对于替代方法的优点。
英文摘要：
Sentences containing definite descriptions, expressions of the form `The $F$', can be formalised using a binary quantifier $ι$ that forms a formula out of two predicates, where $ιx[F, G]$ is read as `The $F$ is $G$'. This is an innovation over the usual formalisation of definite descriptions with a term forming operator. The present paper compares the two approaches. After a brief overview of the system $\mathbf{INF}^ι$ of intuitionist negative free logic extended by such a quantifier, which was presented in \citep{kurbisiotaI}, $\mathbf{INF}^ι$ is first compared to a system of Tennant's and an axiomatic treatment of a term forming $ι$ operator within intuitionist negative free logic. Both systems are shown to be equivalent to the subsystem of $\mathbf{INF}^ι$ in which the $G$ of $ιx[F, G]$ is restricted to identity. $\mathbf{INF}^ι$ is then compared to an intuitionist version of a system of Lambert's which in addition to the term forming operator has an operator for predicate abstraction for indicating scope distinctions. The two systems will be shown to be equivalent through a translation between their respective languages. Advantages of the present approach over the alternatives are indicated in the discussion.
Decidability of Intuitionistic Sentential Logic with Identity via Sequent Calculus
我们的论文有两个目的：本文首先在Chlebowski和Leszczynska-Jasion的论文“An Investigation into Intuitionistic Logic with Identity”中提出的演算的基础上，给出了一个直觉主义非Fregean逻辑ISCI的演算（Bulletin of the Section of Logic 48（4），p. 259-283，2019），其次，我们通过所获得的系统讨论ISCI的可判定性问题。上述论文中的原始演算没有为ISCI提供可判定性结果。为了得到这个结果，有两个问题需要解决：直觉逻辑的所谓循环特性和由于身份专用规则的形式而缺乏子公式性质。我们讨论可能的路线，以克服这些问题：我们考虑一个较弱的版本的子公式属性，守卫的复杂性公式，可以包括在它里面，我们还提出了一个证明搜索过程，当它失败时，然后存在一个反模型（在Kripke语义ISCI）。
