The principle of truth functionality (or compositionality) is a basic principle in many-valued logic in general, and in classical logic in particular. According to this principle, the truth-value of a complex formula is uniquely determined by the truth-values of its subformulas. However, real-world information is inescapably incomplete, uncertain, vague, imprecise or inconsistent, and these phenomena are in an obvious conflict with the principle of truth-functionality. One possible solution to this problem is to relax this principle by borrowing from automata and computability theory the idea of non-deterministic computations, and apply it in evaluations of truth-values of formulas. This has led to the introduction of non-deterministic matrices (Nmatrices) in [6 7] (see also [10] for a survey). These structures form a natural generalization of ordinary multi-valued matrices, in which the truth-value of a complex formula can be chosen non-deterministically out of some non-empty set of options.

Although various types of non-truth-functional semantics were proposed before (such as bivaluations semantics and possible translations semantics, see [13, 14]), the novelty of Nmatrices is in sharing a very important property with many-valued matrices: (semantic) analyticity. A semantics is analytic if to determine whether φ follows from T it always suffices to check only partial models involving solely subformulas of T∪{φ}. This naturally induces a decidability procedure for any logic characterized by a finite Nmatrix.

Nmatrices have proved to be a powerful tool, the use of which preserves all the advantages of ordinary propositional many-valued matrices (analyticity, decidability, compactness), but is applicable to a much wider range of logics. Indeed, there are many useful (propositional) non-classical logics, which have no finite many-valued characteristic matrices, but do have finite Nmatrices, and thus are decidable. Nmatrices have also another attractive property (not shared by standard matrices) - modularity, which means that in many natural cases, the semantic effect of a syntactic rule can be separately analyzed, and the semantics of a system can be straightforwardly obtained by combining the semantic effects of each of its rules.

In this tutorial we will present the framework of Nmatrices and describe their various applications in reasoning under uncertainty and proof theory. In particular, we plan to cover the following topics:

1. Introduction: We will describe the motivation for introducing non-determinism into truth-tables of logical connectives, provide the basic definitions of the framework of Nmatrices and discuss their properties.

2. Proof Theory: Non-deterministic semantics is a useful tool for characterizing syntactic properties of proof systems, such as (syntactic) analyticity (By syntactic analyticity of a calculus G we mean intuitively that whenever a proposition s is provable in G from a set of assumptions S, then it is also possible to prove s from S in G using only the ``syntactic material´´ available in S and s), cut-admissibility, invertibility of rules, etc. We present several classes of proof systems for which this tool can be successfully applied. One such example is canonical sequent calculi, which in addition to the standard axioms and structural rules have only logical rules in which exactly one occurrence of a connective is introduced and no other connective is mentioned. Cut-elimination in these systems is fully characterized by a simple constructive criterion called coherence. Moreover, there is a remarkable correspondence in these systems between the criterion of coherence, cut-elimination, analyticity and a semantic characterization of these systems in terms of two-valued Nmatrices. Another interesting link is between invertibility of logical rules in such calculi and the determinism of the corresponding two-valued Nmatrix. We will also examine other examples of systems for which the tool of non-determinism (combined in many cases with Kripke-style semantics) can be applied to characterize syntactic properties. These include (i) canonical labelled calculi ([19, 11, 12]), (ii) quasicanonical sequent calculi ([1]) (iii) basic sequent calculi ([4]), which include calculi for intuitionistic and modal logics, and (iv) canonical hypersequent calculi ([5]), which include the standard hypersequent calculus for Gödel logic.

3. Paraconsistent Reasoning: Paraconsistent logic is a logic for handling inconsistent information. One of the oldest and best known approaches to paraconsistency is da Costa's approach ([16, 17, 18]), which seeks to allow the use of classical logic whenever it is safe to do so, but behaves completely differently when contradictions are involved. This approach has led to the introduction of C-systems ([13, 14]), which employ a special unary connective for referring to consistency of propositions in the object language. We will demonstrate how the framework of Nmatrices can be used to provide simple, modular and analytic semantics for practically all the propositional C-systems considered in the literature (for the systems with finite-valued semantics, an algorithm for constructing such semantics was implemented in PROLOG [15]). Moreover, we describe an algorithm for a systematic generation of cut-free sequent calculi out of the obtained semantics for all these logics ([2], [3]).

4. The First-Order Case and Beyond: We show how the framework of Nmatrices can be extended to languages with quantifiers and discuss shortly the encountered problems that are not evident on the propositional level. We show the applications of the first-order framework for paraconsistent logics ([8]) and proof theory ([9, 19]).