A note on calculi for non-deterministic many-valued logics

TL;DR

This paper introduces two deductively equivalent calculi for non-deterministic many-valued logics, establishing their soundness, completeness, and cut elimination, thus advancing formal proof systems for such logics.

Contribution

It provides the first pair of calculi for non-deterministic many-valued logics derived directly from truth tables, with proven soundness, completeness, and cut elimination.

Findings

Both calculi are sound and strongly complete.

The calculi are obtained straightforwardly from truth tables.

Cut elimination is proven for the rule-based calculus.

Abstract

We present two deductively equivalent calculi for non-deterministic many-valued logics. One is defined by axioms and the other - by rules of inference. The two calculi are obtained from the truth tables of the logic under consideration in a straightforward manner. We prove soundness and strong completeness theorems for both calculi and also prove the cut elimination theorem for the calculi defined by rules of inference.