Seminar

Thursday, June 25th, 2020, 11:00, on Zoom.

Luca Tranchini (Tübingen)
Proof-terms for dual-intuitionistic logic and refutation-terms for intuitionistic logic (j.w.w. Gianluigi Bellin)

Abstract:

In the present paper, we present a term-assignment for the fragment of bi-intuitionistic logic whose only type-forming operation is the dual of intuitionistic implication. Typing judgements have the form x : C ⊢ t₁ : A₁, ..., t_n : A_n i.e. a set of terms is typed by declaring a single variable (somewhat dualizing the simply typed λ-calculus, where a single term is typed declaring a set of variables). The main distinguishing feature of our term calculus is its distributed nature: whereas in the λμ-calculus all conclusions but one are μ-variables, in our calculus the computational content is distributed among the conclusions, i.e. to each conclusion one assigns a possibly complex term; moreover, reduction is also distributed, in the sense that the reduction acts globally on a set of terms, and not on a single one. The duality between our calculus and the simply typed λ-calculus suggests the possibility to use it not only to encode the dual-intuitionistic notion of provability, but an intuitionistic notion of refutability as well. We spell out this idea by using our terms to decorate Prawitz’s rules of intuitionistic natural deduction from the bottom to the top, thereby expressing a backwards reading of intuitionistic rules: given refutations of the conclusions one computes refutations of the premises.

The seminar will be held on Zoom. In order to get access to the Zoom meeting, please contact Peter Schuster.