Lattice-Based Paraconsistent Logic

In this paper we describe a procedure for developing models and associated proof systems for two styles of paraconsistent logic. We first give an Urquhart-style representation of bounded not necessarily discrete lattices using (grill, cogrill) pairs. From this we develop Kripke semantics for a logic permitting 3 truth values: true, false and both true and false. We then enrich the lattice by adding a unary operation of negation that is involutive and antimonotone and show that the representation may be extended to these lattices. This yields Kripke semantics for a nonexplosive 3-valued logic with negation.