Calculi for Logics of Thinking Computers and Computer Networks

Lecture by Reinhard Muskens, organized by Grolog

In a now famous paper published in 1976, Nuel Belnap argues that computer reasoning should be modeled on the basis of a four-valued logic in which each value is a combination of the two classical values. Belnap also considers two lattices on these four values, one corresponding to increase in truth and non-falsity, the other to increase of information. Together these two lattices form what is now called a /bilattice/.

More recently Yaroslav Shramko and Heinrich Wansing (2005) have in a sense repeated Belnap's move, arguing that the logic of the reasoning of computer /networks/ should be 16-valued, with each value corresponding to a set of Belnap's values. They consider what is called a /trilattice/ on these 16 values and distinguish between an entailment relation based on the notion of truth and one based on falsity. These two relations are not equal or each other's inverses.

In this talk, which reports on joint work with Stefan Wintein, I will look at syntactic characterisations for these logics, with particular reference to propositional logics that are functionally complete. Even in Belnap's logic entailment relations that are coextensional on some reasonable but incomplete fragment of the propositional language (e.g. the classical fragment) may be distinguished if larger fragments are considered. I will show that a language with connectives for the three meet operations on the 16-element trilattice, plus three negation connectives corresponding to certain involutions on this trilattice is functionally complete (and minimally so). This language will be provided with four semantic consequence relations, one based on truth, one on falsity, one on approximation, and one the intersection of the first two. An analytic signed tableau calculus will be given that can model each of these semantic consequence relations in a sound and complete way. It has the property that a single proof in general requires several tableaux, four tableaux for any of the first three consequence relations just mentioned, and six for the last. It will be shown how this calculus generalises a calculus for a functionally complete variant of Belnap's logic, which in its turn generalises a standard signed tableau calculus for classical logic. Time permitting I will also spend a few words on a simple theorem prover implementing the calculus.

When & where?

Thu 6 November, 3-5 pm
Faculty of Philosophy, room Beta