A Kripke-style Semantics for the Intuitionistic Logic of Pragmatics ILP
Gianluigi Bellin · Journal of Logic and Computation · 2003
We give a Kripke-style semantics for the intuitionistic logic of pragmatics ILP and show completeness with respect to thissemantics. 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.