Proof Systems for Logics Based on Non-deterministic Multiple-valued Structures

Non-deterministic matrices (Nmatrices) are multiple-valued structures in which the value assigned by a valuation to a complex formula can be chosen non-deterministically out of a certain nonempty set of options. We consider two different types of semantics which are based on Nmatrices: the dynamic one and the static one (the latter is new here). We use the Rasiowa-Sikorski (R-S) decomposition methodology to get sound and complete proof systems employing finite sets of mv-signed formulas for all propositional logics based on such structures with either of the above types of semantics. Later we demonstrate how these systems can be converted into cut-free ordinary Gentzen calculi which are also sound and complete for the corresponding non-deterministic semantics. As a by-product, we get new semantic characterizations for some well-known logics (like the logic CAR from [18, 28]).

---

Macierze niedeterministyczne to wielowartościowe struktury, w których wartość przypisaną przez wartościowanie złożonej formule można wybrać w niedeterministyczny sposób z pewnego niepustego zbioru opcji. Opracowujemy ogólne dedukcyjne systemy dowodzenia dla logik opartych na tych strukturach z użyciem mechanizmu n-sekwentów oraz dekompozycyjnej metodologii R-S. Później pokazujemy, jak można użyć tych systemów do uzyskania zwykłych rachunków Gentzenowskich bez reguły cięcia dla pewnych dobrze znanych logik tolerujących sprzeczność.