Proving the Soundness of a Proof System for Intuitionistic Hybrid Propositional Logic

At least two proof systems for modal hybrid intuitionistic logic have been shown to be complete, which is a promising direction of research. However, there has not yet been developed a complete proof system for non-modal hybrid intuitionistic logic. In this thesis I prove the soundness of a proof system for such a propositional hybrid intuitionistic logic, which provides the necessary axioms and proof rules for proving completeness of hybrid intuitionistic propositional logic (HIPL). This is accomplished by first introducing modal logic, intuitionistic logic, and classical hybrid logic, as well as the Kripke semantics for each of them. Some derivable formulas and generally interesting results about HIpL are noted and discussed throughout the latter half of the text.