English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

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

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