Proof Theory for Functional Modal Logic

We present some proof-theoretic results for the normal modal logic whose characteristic axiom is (mathord {sim }mathord {Box }Aequiv mathord {Box }mathord {sim }A). We present a sequent system for this logic and a hypersequent system for its first-order form and show that these are equivalent to Hilbert-style axiomatizations. We show that the question of validity for these logics reduces to that of classical tautologyhood and first-order logical truth, respectively. We close by proving equivalences with a Fitch-style proof system for revision theory.