We introduce a generic notion of categorical propositional logic and provide a construction of a preorder-enriched institution out of such a logic, following the Curry-Howard-Tait paradigm. The logics are speci ed as theories of a meta-logic within the logical framework LF such that institution comorphisms are obtained from theory morphisms of the meta-logic. We prove several logic-independent results including soundness and completeness theorems and instantiate our framework with a number of examples: classical, intuitionistic,linear and modal propositional logic.
Reference
Related
Cited by
Get Citation
Joseph Goguen, Till Mossakowski, Valeria de Paiva, Florian Rabe, Lutz Schr?der. An Institutional View on Categorical Logic. International Journal of Software and Informatics, 2007,1(1):129~152