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.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
