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

Journal of Logic and Computation (forthcoming)
  Copy   BIBTEX

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.

Links

PhilArchive

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Analytics

Added to PP
2023-07-06

Downloads
170 (#117,360)

6 months
110 (#51,001)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Sara Ayhan
Ruhr-Universität Bochum

Citations of this work

No citations found.

Add more citations

References found in this work

The Connectives.Lloyd Humberstone - 2011 - MIT Press. Edited by Lloyd Humberstone.
Constructible falsity.David Nelson - 1949 - Journal of Symbolic Logic 14 (1):16-26.
Ideas and Results in Proof Theory.Dag Prawitz & J. E. Fenstad - 1971 - Journal of Symbolic Logic 40 (2):232-234.
Rejection.Timothy Smiley - 1996 - Analysis 56 (1):1–9.

View all 24 references / Add more references