© 2003 by Oxford University Press
| ||||||||||||||||||||||||||||||||||||||||||||||||||||
Original Article |
A Kripke-style Semantics for the Intuitionistic Logic of Pragmatics ILP
1 Facolta' di Scienze, Universita' di Verona, Strada le Grazie, 37134 Verona, Italy. E-mail: bellin{at}sci.univr.it 2 Department of Computer Science, Queen Mary, University of London, Mile End Road, London E1 4NS, UK. E-mail: kurt{at}dcs.qmul.ac.uk
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.
Keywords: Substructural logic, Kripke semantics, proof search.
Received 5 February 2002.