Demystifying $\hat{I}¼$

Abstract

We explore the theory of illfounded and cyclic proofs for the propositional modal $\hat{I}¼$-calculus. A fine analysis of provability for classical and intuitionistic modal logic provides a novel bridge between finitary, cyclic and illfounded conceptions of proof and re-enforces the importance of two normal form theorems for the logic: guardedness and disjunctiveness.