Constructive CK for Contexts
This note describes possible world semantics for a constructive modal logic CK. The system CK is weaker than other constructive modal logics K as it does not satisfy distribution of possibility over disjunctions, neither binary (3(A _ B) ! 3A _ 3B) nor nullary (3? ! ?). We are interested in this version of constructive K for its application to contexts in AI (dP03). However, our previous work on CK described only a categorical semantics (BdPR01) for the system, while most logicians interested in contexts prefer their semantics pos- sible worlds style. This note fills the gap by providing the possible worlds model theory for the constructive modal system CK, showing soundness and complete- ness of the proposed semantics, as well as the finite model property and (hence) decidability of the system. Wijesekera (Wij90) investigated possible worlds se- mantics of a system similar to CK, without the binary distribution, but satisfying the nullary one. The semantics presented here for CK is new and considerably simpler than the one of Wijesekera.