We consider the language ILP of Intuitionistict Formal Pragmatics proposed by Bellin and Dalla Pozza (Dagstuhl Seminar on Linear Logic 1999) focussing on the relation between the notions of causal implication, assertability and obligation. We give a Kripke-style semantics ILP and prove the completenes theorem for it. The decision procedure extends standard procedures for intuitionistic logic with one for a fragment of relevant implicational logic and of deontic logic: it takes a sequent S as input and yiels either a proof of S in the sequent calculus for ILP or a countermodel for S.