论文标题
双音逻辑2int的无剪切顺序
A cut-free sequent calculus for the bi-intuitionistic logic 2Int
论文作者
论文摘要
本文的目的是引入双关键的序列微积分，并证明其结构规则。我将提出的演算称为SC2INT，是双元素逻辑2INT的顺序演算。该逻辑的分石代表了一种双边推理，因为它们不仅会内部化验证或可预订性的过程，而且还可以在伪造或所谓的双重可供应性方面进行双重过程。已经陈述了一种自然扣除微积分的正常形式定理，在本文中，我想证明SC2INT的切割定理，即如果成功的话，这将扩展到迄今为止存在的结果。
The purpose of this paper is to introduce a bi-intuitionistic sequent calculus and to give proofs of admissibility for its structural rules. The calculus I will present, called SC2Int, is a sequent calculus for the bi-intuitionistic logic 2Int. Calculi for this logic represent a kind of bilateralist reasoning, since they do not only internalize processes of verification or provability but also the dual processes in terms of falsification or what is called dual provability. A normal form theorem for a natural deduction calculus of 2Int has already been stated, in this paper I want to prove a cut-elimination theorem for SC2Int, i.e. if successful, this would extend the results existing so far.
