|
Abstract : |
The aim of this paper is to emphasize the fact that for all nitely-many-valued logics there is a completely systematic relation between sequent calculi and tableau systems. More importantly, we show that for both of these systems there are always two dual proof sytems (not just only two ways to interpret the calculi). This phenomenon may easily escape one's attention since in the classical (two-valued) case the two systems coincide. (In two-valued logic the assignment of a truth value and the exclusion of the opposite truth value describe the same situation.) We employ the usual denitons of rst order languages, many-valued interpretations (M) and induced valuation functions (val M) (see e.g. Carnielli [1987]). In the following V = fv 1; : : : ; v m g always denotes the set of truth values of a logic. To stress the dualty of the two types of calculi we shall dene them simultanously: 1. Definition An (m-valued) sequent is an m-tuple of nite sets i of formulas, denoted as 1 j 2 j: : : j m. (As usual we abbreviate [ by; and [ fAg by; A.) 2. Definition An interpretation M is said to p(n)-satisfy a sequent 1 j: : : j m, if there is an i (1 i m) and a formula F 2 i, s.t. val M (F) = (6=)v i. A sequent is called p(n)-valid, if it is p(n)-satised by every interpretation. The concept of p-satisability was used by Rousseau [1967] (compare also Schr oter [1955]) in his formulation of many-valued sequents, whereas nsatis ablity essentially already appears in Carnielli [1991]. 3. Definition An introduction rule for a connective 2 at place i in the logic L is a schema of the form: D, |
