Optimal axiomatizations for multiple-valued operators and quantifiers based on semi-lattices

Abstract

We investigate the problem of finding optimal axiomatizations for operators and distribution quantifiers in finitely-valued first-order logics. We show that the problem can be viewed as the minimization of certain two-valued prepositional formulas. We outline a general procedure leading to optimized quantifier rules for the sequent calculus, for natural deduction and for clause formation. In the case of operators and quantifiers based on semi-lattices, rules with a minimal branching degree can be obtained by instantiating a schema, which can also be used for optimal tableaux with sets-as-signs.