Generating proof systems for three-valued propositional logics

TL;DR

This paper presents a method to automatically generate finite axiomatizations for three-valued propositional logics using two formal systems, simplifying the process by converting matrix semantics into inference rules.

Contribution

It introduces a unified procedure to axiomatize three-valued logics via two formalisms, enabling effective translations and simplifications based on matrix properties.

Findings

Automated generation of axiomatizations for three-valued logics.

Effective translations between two formal systems for these logics.

Simplification of rule sets based on Tarskian consequence properties.

Abstract

In general, providing an axiomatization for an arbitrary logic is a task that may require some ingenuity. In the case of logics defined by a finite logical matrix (three-valued logics being a particularly simple example), the generation of suitable finite axiomatizations can be completely automatized, essentially by expressing the matrix tables via inference rules. In this chapter we illustrate how two formalisms, the 3-labelled calculi of Baaz, Ferm\"uller and Zach and the multiple-conclusion (or Set-Set) Hilbert-style calculi of Shoesmith and Smiley, may be uniformly employed to axiomatize logics defined by a three-valued logical matrix. The generating procedure common to both formalisms can be described as follows: first (i) convert the matrix semantics into rule form (we refer to this step as the generating subprocedure) and then (ii) simplify the set of rules thus obtained, essentially relying on the defining properties of any Tarskian consequence relation (we refer to this step as the streamlining subprocedure). We illustrate through some examples that, if a minimal expressiveness assumption is met (namely, if the matrix defining the logic is monadic), then it is straightforward to define effective translations guaranteeing the equivalence between the 3-labelled and the Set-Set approach.