Meaning and identity of proofs in a bilateralist setting: A two-sorted typed lambda-calculus for proofs and refutations

TL;DR

This paper develops a two-sorted typed lambda-calculus for bi-intuitionistic logic, providing formal tools to analyze proofs and refutations, and explores their implications for sense, denotation, and identity of proofs in a bilateralist framework.

Contribution

It introduces lambda-2Int, a novel lambda-calculus for bi-intuitionistic logic, extending Curry-Howard correspondence to include proofs and refutations, and establishes a Dualization Theorem.

Findings

Formal proof system for 2Int with annotated terms

Dualization Theorem relating proofs and refutations

Insights into sense, denotation, and identity of proofs

Abstract

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, 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 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.