In this chapter bi-intuitionism is interpreted as an intensional logic which is about the justification conditions of assertions and hypotheses, extending C. Dalla Pozza and C. Garola’s pragmatic interpretation [18] of intuitionism, seen as a logic of assertions according to a suggestion by M. Dummett. Revising our previous work on this matter [5], we consider two additional illocutionary forces, (i) conjecturing, seen as making the hypothesis that a proposition is epistemically necessary, and (ii) expecting, regarded as asserting that a propostion is epistemically possible; we show that a logic of expectations justifies the double negation law. We formalize our logic in a calculus of sequents and study bimodal Kripke semantics of bi-intuitionism based on translations in S4. We look at rough set semantics following P. Pagliani’s analysis of “intrinsic co-Heyting boundaries” [40] (after Lawvere). A Natural Deduction system for co-intuitionistic logic is given where proofs are represented as upside down Prawitz trees. We give a computational interpretation of co-intuitionism, based on T. Crolard’s notion of coroutine [16] as the programming construction corresponding to subtraction introduction. Our typed calculus of co-routines is dual to the simply typed lambda calculus and shows features of concurrent and distributed computations.

Assertions, hypotheses, conjectures, expectations: Rough-set semantics and proof-theory

BELLIN, Gianluigi
2014-01-01

Abstract

In this chapter bi-intuitionism is interpreted as an intensional logic which is about the justification conditions of assertions and hypotheses, extending C. Dalla Pozza and C. Garola’s pragmatic interpretation [18] of intuitionism, seen as a logic of assertions according to a suggestion by M. Dummett. Revising our previous work on this matter [5], we consider two additional illocutionary forces, (i) conjecturing, seen as making the hypothesis that a proposition is epistemically necessary, and (ii) expecting, regarded as asserting that a propostion is epistemically possible; we show that a logic of expectations justifies the double negation law. We formalize our logic in a calculus of sequents and study bimodal Kripke semantics of bi-intuitionism based on translations in S4. We look at rough set semantics following P. Pagliani’s analysis of “intrinsic co-Heyting boundaries” [40] (after Lawvere). A Natural Deduction system for co-intuitionistic logic is given where proofs are represented as upside down Prawitz trees. We give a computational interpretation of co-intuitionism, based on T. Crolard’s notion of coroutine [16] as the programming construction corresponding to subtraction introduction. Our typed calculus of co-routines is dual to the simply typed lambda calculus and shows features of concurrent and distributed computations.
9789400775480
Proof Theory
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/877783
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact