Complete sets of connectives and complete

sequent calculus for Belnap's Logic

Paul Ruet

LIENS, Ecole Normale Sup?erieure

45 rue d'Ulm, 75005 Paris, France

Thomson - Laboratoire Central de Recherches

Domaine de Corbeville, 91404 Orsay Cedex, France

Email: ruet@dmi.ens.fr

Abstract
This paper presents a sequent calculus for Belnap's four-valued logic, and proves its soundness and completeness with respect to model theory. The proofs are adaptations of Gallier's proofs for classical logic.

It is also shown that the extensions of the classical connectives : and ^ to the fourvalued case do not form a complete set, and a new connective is introduced to obtain the completeness of the connectives.

1 INTRODUCTION

The interest of three-valued logic for computer science has been motivated by research on the semantics of negation in logic programming, from the model-theoretical [4, 11, 12] and the proof-theoretical viewpoints [14].

Moving from three-valued to four-valued logic provides a framework for logic programs dealing with missing or conflicting information, e.g information distributed over several sites [6]. It also sheds a new light on the stable model semantics for logic programming (see [3]), allowing to define a new stable model, the largest one in a certain ordering, and to recover at the same time the usual smallest stable model and alternating fixed points: the whole family of stable models is then enclosed between these 4 fixed points [8].

?
?
?
@
@@?
??
@
@
@

f t

?

>

-

6

<=t

<=k

The four-valued logic extending Kleene's three-valued logic was introduced by Belnap in [2]. Let us briefly recall its main features. The 4 truth values (denoted f, t, ? and >) can be