A Kripke-style Semantics for the Intuitionistic Logic of Pragmatics ILP

摘要

We give a Kripke-style semantics for the intuitionistic logic of pragmatics ILP and show completeness with respect to this semantics. In order to prove the completeness theorem we give a decision procedure that given an ILP-sequent S, either returns a cut-free derivation of S or constructs a finite counter-model if S is not provable. Thus we have the finite model property and also a new proof that the cut rule is eliminable in ILP.