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


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.



External links

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

Through your library


Added to PP

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