Free-Variable Calculi for the Modal Logics K45 and S5 : Extended to the Logic of Only Knowing

Abstract

This thesis presents a free-variable sequent calculi for the modal logics K45, S5 and the logic of Only Knowing. Labels act as placeholders for points in models, using label variables to postpone the choice of point until more knowledge of a putative satisfying model is gathered, allowing a least commitment search. The relation of contextually equivalents is used to obtain variable-sharing derivations baring tight connections to matrix systems and the goal directed Connection calculus. A system of indexed formulae is employed to enforce reuse of label parameters, establishing an upper bound for the search space. The calculus of the logic of Only Knowing is defined by combining the calculi established for K45 and S5, and utilizing an auxiliary derivation to test models for maximality.