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

We give a Kripke style semantics for an intuitionistic logic for pragmatics ILP, with consists of the Horn fragment of relevant logic to express causal relations between (elementary formulas for) assertions and obligations in the framework of propositional intuitionistic logic as a logic of assertions. 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. As a corollary we have the finite model property for ILP and also a new proof that the cut rule is eliminable in ILP.