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.
翻译:一般而言,为任意逻辑提供公理化系统需要一定程度的创造性。对于由有限逻辑矩阵定义的逻辑(其中三值逻辑是一个特别简单的例子),可完全自动化地生成合适的有限公理化系统,其本质是通过推理规则表达矩阵真值表。本章将阐述如何统一运用两种形式化框架——Baaz、Fermüller和Zach的三标记演算,以及Shoesmith与Smiley的多结论(或称集-集)希尔伯特式演算——来公理化由三值逻辑矩阵定义的逻辑系统。这两种框架共有的生成程序可描述如下:首先(i)将矩阵语义转换为规则形式(此步骤称为生成子程序),然后(ii)主要依据任意塔尔斯基后承关系的定义性质简化所获得的规则集(此步骤称为精简子程序)。通过若干实例将说明,在满足最小可表达性假设(即定义逻辑的矩阵是单一的)的前提下,可轻松定义有效的转换,从而保证三标记方法与集-集方法之间的等价性。