In this paper I will develop a lambda-term calculus, lambda-2Int, for a bi-intuitionistic logic and discuss its implications for the notions of sense and denotation of derivations in a bilateralist setting. Thus, I will use the Curry-Howard correspondence, which has been well-established between the simply typed lambda-calculus and natural deduction systems for intuitionistic logic, and apply it to a bilateralist proof system displaying two derivability relations, one for proving and one for refuting. The basis will be the natural deduction system of Wansing's bi-intuitionistic logic 2Int (2016a; 2017), which I will turn into a term-annotated form. Therefore, we need a type theory that extends to a two-sorted typed lambda-calculus. I will present such a term-annotated proof system for 2Int and prove some properties and results for it, most importantly for this paper a Dualization Theorem relating proofs and refutations in this system. On the basis of these formal results I will argue that this gives us interesting insights into questions about sense and denotation as well as synonymy and identity of proofs from a bilateralist point of view.

翻译：本文将为双直觉主义逻辑建立一种λ-项演算——λ-2Int，并探讨其在双边主义框架下对推导的涵义与指称概念的启示。为此，我将运用在简单类型λ-演算与直觉主义逻辑自然演绎系统之间已确立的柯里-霍华德对应关系，将其应用于一个展现两种可推导性关系（一种用于证明，一种用于反驳）的双边主义证明系统。该研究的基础是Wansing双直觉主义逻辑2Int（2016a; 2017）的自然演绎系统，我将为其赋予项标注形式。因此，我们需要将类型理论扩展为双类类型λ-演算。我将呈现这样一个2Int的项标注证明系统，并证明其若干性质与结果——其中对本文最重要的成果是关联该系统中证明与反驳的对偶定理。基于这些形式化结果，我将论证从双边主义视角出发，这能为我们理解证明的涵义与指称、同义性及同一性等核心问题提供深刻洞见。