Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Sara Ayhan

TL;DR

The paper develops a two-sorted, Curry-style lambda-calculus, $\lambda^{2Int}$, to formalize a bilateralist proof system for bi-intuitionistic logic $2Int$ that features both proof and refutation derivations. It extends Wansing's natural deduction for $2Int$ with term annotations, dual rules, and the co-implication connective $A \Yleft B$, enabling a first-order Curry-Howard correspondence in a bilateral setting. A central result, the Dualization Theorem, shows that for any proof (or refutation) of a formula, a dual derivation exists for the dual formula with the same derivation height, establishing a tight link between proofs and refutations. The author argues that proofs and refutations share the same denotation but retain distinct sense, thereby supporting a Fregean view of sense versus denotation in a bilateralist framework. The work lays groundwork for future connections to sequent calculi and potential applications in theoretical CS, while preserving a non-reductionist, bilateral stance on logical meaning.

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.

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

TL;DR

The paper develops a two-sorted, Curry-style lambda-calculus, , to formalize a bilateralist proof system for bi-intuitionistic logic that features both proof and refutation derivations. It extends Wansing's natural deduction for with term annotations, dual rules, and the co-implication connective , enabling a first-order Curry-Howard correspondence in a bilateral setting. A central result, the Dualization Theorem, shows that for any proof (or refutation) of a formula, a dual derivation exists for the dual formula with the same derivation height, establishing a tight link between proofs and refutations. The author argues that proofs and refutations share the same denotation but retain distinct sense, thereby supporting a Fregean view of sense versus denotation in a bilateralist framework. The work lays groundwork for future connections to sequent calculi and potential applications in theoretical CS, while preserving a non-reductionist, bilateral stance on logical meaning.

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.
Paper Structure (10 sections, 4 theorems)

This paper contains 10 sections, 4 theorems.

Table of Contents

  1. Introduction
  2. A two-sorted typed $\lambda$-calculus for 2Int: $\lambda^{2Int}$
  3. The term-annotated natural deduction calculus N2Int$_\lambda$ and some results for the system
  4. Duality in $\lambda^{2Int}$
  5. Meaning and identity of derivations in N2Int$_\lambda$
  6. Background: Distinguishing sense and denotation of proofs
  7. Identifying proofs and refutations
  8. Conclusion and Outlook
  9. Definition of compatibility
  10. Proof of Dualization Theorem

Key Result

Lemma 1

1. Assumptions 1.1 For every $x$, if $(\Gamma; \Delta) \Rightarrow^{+} x^{+}:A$, then $(x^{+}:A) \in \Gamma$. 1.2 For every $x$, if $(\Gamma; \Delta) \Rightarrow^{-} x^{-}:A$, then $(x^{-}:A) \in \Delta$. 2. $\top/\bot$-rules 2.1 If $(\Gamma; \Delta) \Rightarrow^{+} \texttt{top}^{+}:A$, then $A \equ

Theorems & Definitions (19)

  • Definition 1
  • Definition 2
  • Definition 3
  • Definition 4
  • Lemma 1: Generation Lemma
  • proof
  • Lemma 2: Substitution Lemma
  • proof
  • Definition 5: Reductions
  • Theorem 2.1: Subject Reduction Theorem for $\lambda^{2Int}$
  • ...and 9 more