Logic Seminar

Harold HodesCornell University
Modal logics, intuitionistic and classical, within moodal logics

Tuesday, March 26, 2019 - 2:55pm
Malott 206

This paper "looks under the hood" of the usual sorts of proof-theoretic systems for certain intuitionistic and classical propositional modal logics. Let a marked formula be the result of prefixing a formula in a propositional modal language with a moodal marker, for this talk either 0 or 1: These markers can be thought of as a logical aspect of grammatical mood.

I will present Natural Deduction formalizations of several normal modal logics using marked formulas; deductions in these systems display deductive structure covered over in familiar "mono-moodal" proof-theoretic systems for such logics. I will start with the dy-moodal intuitionistic version of K, IK, in which box and diamond are governed by Introduction and Elimination rules. In IK the familiar K rule and Necessitation are derived (i.e. admissible) rules. Time permitting, I will also present proof-theoretic systems formalizing familiar logics stronger than IK; these are defined by adding rules none of which involve iterating box or diamond: I will discuss models, and proofs of soundness and completeness for these systems. Time permitting, I will also consider inclusion and non-inclusion relations between the consequence relations defined by these systems, focusing on the intuitionistic systems.