J. Inform. Process. Cybernet. EIK 29 (1994) 6, 333–355 (formerly: Elektron. Inform.verarb. Kybernet.) Elimination of Cuts in First-order Finite-valued Logics By Matthias Baaz, Christian G. Fermüller and Richard Zach Abstract: A uniform construction for sequent calculi for finite-valued first-order logics with distribution quantifiers is exhibited. Completeness, cut-elimination and midsequent theorems are established. As an application, an analog of Herbrand's theorem for the four-valued knowledgerepresentation logic of Belnap and Ginsberg is presented. It is indicated how this theorem can be used for reasoning about knowledge bases with incomplete and inconsistent information. 1 Introduction Why elimination of cuts? Cut-elimination procedures play a central rôle in proof theoretic investigations of logical calculi. Their importance lies in the fact that they are local procedures. This is in contrast to the results obtained by proofs of cut-free completeness, which are global (and do not take existing proofs into account). For the analysis of given proofs-and this makes cut-elimination so important for computer science-a local procedure, which operates on given data, is needed. It allows one to look at parts of proofs independently of others, e.g., making the assumptions of a proof explicit. Cut elimination is also essential for the extraction of programs from proofs. The constructive nature of the cut elimination procedure ensures that the extraction algorithm of a function encoded by a proof is primitive recursive, whereas cutfree completeness properties (as in the case of analytic tableaux) only guarantees termination of extraction algorithms. Cut elimination also provides a bound for the term complexity of the cut-free proof, and consequently a bound on the complexity of the extracted function relative to the complexity of the functions represented by primitive function symbols. Why many-valued logics? Many-valued logics have enjoyed rising interest in recent years in computer science. For instance, many-valued logics can be used to model knowledge bases, or more accurately, epistemic states of knowledge. In the following, we will illustrate our results with an example based on such a logic: Belnap [6] has introduced a logic with the truth values false (f), unknown (u), contradictory (⊥) and true (t), corresponding to the epistemic status of the given facts. Ginsberg [12] has extended the study of logics of this kind to the general theory of logics over bilattices and uses it to model non-monotonic knowledge bases. Belnap's logic has recently been used for a representation of (possibly contradictory) knowledge and the problem of knowledge revision and update in [17]. Bilattice logics also find applications in the study of logic programming, see, e.g., [9, 10]. Another recent application of many-valued logics is in the verification of switch-level circuit designs [16]. The success of a logic for use in the context of knowledge representation and reasoning depends crucially on the availability of computational calculi for this logic. Without such calculi, 334 the study of a logic in relation to its application in computer science and artificial intelligence is destined to remain purely theoretical. In the case of many-valued logics, computational calculi can be given. Analytic calculi for many-valued logics have been known for quite some time. Sequent systems similar to those presented here have also been introduced by Schröter [22], Rousseau [21], Takahashi [25], and Carnielli [8]; equivalent tableaux formulations were given by Surma [24] and Carnielli [7] (Hähnle's work is based on the latter [13, 14, 15]). Calculi for automated theorem proving in many-valued logics are also legion. Apart from Hähnle's work on tableauxbased theorem proving, various resolution methods have been proposed, e.g., by O'Hearn and Stachniak [19] or Baaz and Fermüller [1, 2]. For more detailed surveys of the work done in these areas see [15, 27]. We present here sequent calculi for arbitrary finite-valued first-order logics with distribution quantifiers. These calculi are essentially the ones of [21] but differ from those of [25] (our rules are more general, and also more compact) and [8] (which is a calculus dual to ours, cf. [4]). First we establish soundness and completeness for this calculus. In Section 4 we give a cutelimination algorithm schema for this calculus modulo a parametric operator for reducing cuts on composite formulas. In the usual proof of the Hauptsatz for classical logic, this operator is fixed and defined by case distinction. We, however, give (in Section 5) a general method based on the resolution principle for finding such reductions. This method is also applicable to the classical case. It provides a uniform way to show that cut-elimination holds in systems where any propositional connectives or distribution quantifiers (which are, of course, definable in classical logic) are taken as primitive. Our method can be extended so as to reduce the degree of the cut formula not only by one, but to reduce it arbitrarily. This suggests the possibility of interactively reducing cuts of higher complexity in one step. This may have an application for implementing cut-elimination procedures, an undertaking thwarted until now due to its prohibitive complexity. Finally, in Section 6, we give an analog of Herbrand's Theorem for a first-order version of Belnap's logic and show how this can be used to extract information from proofs in the sequent calculus. 2 Preliminaries D e f i n i t i o n 2.1. A language L for a logic consists of countably many free variables, bound variables, function symbols (including constants), predicate symbols, as well as propositional connectives, quantifiers, and auxiliary symbols: "(", ")", ",". We use a, b, c, . . . to denote free variables; x, y, z, . . . to denote bound variables; P , Q, R, . . . to denote predicate symbols; 2 to denote connectives; and Q to denote quantifiers. Terms, subterms, formulas and subformulas are defined as usual. The degree of a formula is its depth, more precisely: d(A) =  0 if A is atomic max{d(A1), . . . , d(An)}+ 1 if A ≡ 2(A1, . . . , An) d(B) + 1 if A ≡ (Qx)A D e f i n i t i o n 2.2. A matrix for a language L is given by: 1. a nonempty set of truth values V = {v1, . . . , vm} of size m, 2. an abstract algebra V with domain V of appropriate type: For every n-place connective 2 of L there is an associated truth function 2:V n → V , and 3. for every quantifier Q, an associated truth function Q:℘(V ) \ {∅} → V 335 A language and a matrix for it together fully determine a logic L. L is said to be m-valued. The intended meaning of a truth function for a propositional connective is analogous to the two-valued case: Given formulas A1, . . . , An, which take the truth values w1, . . . , wn, respectively, the truth value of 2(A1, . . . , An) is given by 2(w1, . . . , wn). A truth function for quantifiers is a mapping from nonempty sets of truth values to truth values: Given a quantified formula (Qx)F (x), such a set of truth values describes the situation where the ground instances of F take exactly the truth values in this set as values under a given interpretation. In other words, for a non-empty set M ⊆ V , (Qx)F (x) takes the truth value Q(M) if, for every truth value v ∈ V , it holds that v ∈ M iff there is a domain element d such that the truth value of F (d) is v. The set M is called the distribution of F . This generalization of quantifiers dates back to [18]. Quantifiers of this type have been called distribution quantifiers in [7]. Example 2.1. The matrix for Belnap's logic consists of: 1. The set of truth values V = {f, u,⊥, t}. V carries the structure of a bilattice with two partial orders ≤k and ≤t as follows: f <t u,⊥ <t t and u <k t, f <k ⊥. t ↗ ↖ u ⊥ ↖ ↗ f 2. The truth functions for the connectives ¬, ∧, ∨ (∧ and ∨ are the glb and lub in the order ≤t, respectively): ¬ t f u u ⊥ ⊥ f t ∧ t u ⊥ f t t u ⊥ f u u u f f ⊥ ⊥ f ⊥ f f f f f f ∨ t u ⊥ f t t t t t u t u t u ⊥ t t ⊥ ⊥ f t u ⊥ f Furthermore, we have unary connectives Jw for every w ∈ V where Jw(u) = t if u = w and Jw(u) = f otherwise. 3. In view of the application in Section 6, we introduce the quantifiers ∀ (classical for all) and U (uniformity) defined by the following truth functions: ∀(W ) = { t if W = {t} f otherwise Ũ(W ) = lub≤k(W ) D e f i n i t i o n 2.3. A structure M = 〈D,ΦM〉 for a language L (an L-structure) consists of the following: 1. A non-empty set D, called the domain (elements of D are called individuals. 2. A mapping ΦM that satisfies the following: (a) Each free variable of L is mapped to an element of D. (b) Each n-ary function symbol f of L is mapped to a function fM:Dn → D, or to an element of D if n = 0. Additionally, ΦM maps elements of D to themselves. (c) Each n-ary predicate symbol P of L is mapped to a function PM:Dn → V , or to and element of V if n = 0. 336 D e f i n i t i o n 2.4. Let M be an L-structure. An assignment s is a mapping from the free variables of L to individuals. D e f i n i t i o n 2.5. An interpretation I = 〈M, s〉 is an L-structure M = 〈D,Φ〉 together with an assignment s. D e f i n i t i o n 2.6. Let I = 〈〈D,ΦM〉, s〉 be an interpretation. The mapping Φ can be extended in the obvious way to a mapping from terms to individuals: 1. If t is a free variable, then ΦI(t) = s(t). 2. If t is of the form f(t1, . . . , t2), where f is a function symbol of arity n and t1, . . . , tn are terms, then ΦI(t) = fM ( ΦI(t1), . . . , ΦI(tn) ) . D e f i n i t i o n 2.7. Given an interpretation I = 〈M, s〉, we define the valuation valI for formulas F to be a mapping from formulas to truth values as follows: 1. If F is atomic, i.e., of the form P (t1, . . . , tn), where P is a predicate symbol of arity n and t1, . . . , tn are terms, then valI(F ) = PM ( ΦI(t1), . . . , ΦI(tn) ) . 2. If the outermost logical symbol of F is a propositional connective 2 of arity n, i.e., F is of the form 2(F1, . . . , Fn), where F1, . . . , Fn are formulas, then valI(F ) = 2 ( valI(F1), . . . , valI(Fn) ) . 3. If the outermost logical symbol of F is a quantifier Q, i.e., F is of the form (Qx)G(x), then valI(F ) = Q ( {valIG(d) | d ∈ D} ) . 3 Sequent calculi D e f i n i t i o n 3.1. An (m-valued) sequent Γ is an m-tuple of finite sequences Γ(i) of formulas written thus: Γ(1) | . . . | Γ(m). If Γ is a sequent, then Γ(i) denotes the i-th component of Γ . If ∆ is a sequence of formulas and I ⊆ M = {1, . . . ,m} (or W ⊆ V ), we denote by [I:∆] ([W :∆]) the sequent whose i-th component is ∆ if i ∈ I (vi ∈ W ), and is empty otherwise. For [{i, j, . . .}:∆] we write [i, j, . . . :∆]. If Γ and Γ ′ are sequents, then we write Γ, Γ ′ for the sequent Γ(1), Γ ′(1) | . . . | Γ(m), Γ ′ (m). D e f i n i t i o n 3.2. Let I be an interpretation. I satisfies a sequent Γ , iff there is an i, 1 ≤ i ≤ m, s.t., for some formula F ∈ Γ(i), valI(F ) = vi. I is called a model of Γ and we write I |= Γ . Γ is called satisfiable, iff there is an interpretation I s.t. I |= Γ , and valid , iff for every interpretation I, I |= Γ . The above definition boils down to the interpretation of an m-sided sequent as a disjunction of statements saying that a particular formula takes a particular truth value. Specifically, if a formula A occurs in Γ(i), the interpretation is "A takes the value vi." It is instructive to see that this interpretation yields the usual interpretation in the two-valued case: there, a sequent A1, . . . , Ar → B1, . . . , Bs is commonly read as being equivalent to (A1∧. . .∧Ar) ⊃ (B1∨. . .∨Bs). By propositional logic, this is equivalent to ¬A1 ∨ . . .∨¬Ar ∨B1 ∨ . . .∨Bs, or in plain English: either one of the Ai's is false or one of the Bj 's is true. R e m a r k 3.1. It is also possible to interpret sequents in a dual way, namely: if a formula A occurs in Γ(i), the interpretation is "A does not take the value vi." Sequent calculi for this semantics can also be uniformly obtained, they correspond to analytic tableaux [4, 27] 337 D e f i n i t i o n 3.3. An introduction rule for a connective 2 at place i is a schema of the form: 〈Γ,∆2:i(j)〉j∈I Γ, [i:2(A1, . . . , An)] 2:i where the arity of 2 is n, I is a finite set, frm ( ∆2:i(j) ) ⊆ {A1, . . . , An} (where frm(∆) denotes the set of formulas occurring in ∆) and the following condition holds: Let I be an interpretation. Then the following are equivalent: 1. 2(A1, . . . , An) takes the truth value vi under I. 2. For j ∈ I, M satisfies the sequents ∆2:i(j). It should be stressed that the introduction rules for a connective at a given place are far from being unique: Let the expression Avl denote the statement "A takes the truth value vl". Then every introduction rule for 2(A1, . . . , An) at place i corresponds to a conjunction of disjunctions of some Avl which is true iff 2(A1, . . . , An) takes the truth value vi (namely,∧k j=1 ∨m l=1 ∨ A∈∆2:i(j)(l) A vl). This represents an i-th partial normal form in the sense of [20]. Any such partial normal form for 2(A1, . . . , An)vi will do. In particular, the truth table for 2 immediately yields a complete conjunctive normal form, the corresponding rule is as in Definition 3.3, with: I ⊆ V n is the set of all n-tuples j = (w1, . . . , wn) of truth values such that 2(w1, . . . , wn) 6= vi; and ∆2:i(j)(l) = {Ak | 1 ≤ k ≤ n, vl 6= wk}. A rule constructed this way can have up to mn−1 premises (if 2 takes the value vi only once in the truth table), but standard methods for minimizing combinational functions, such as the Quine-McCluskey procedure, can be used to find rules that are minimal w.r.t. the number of premises and the number of formulas per premise. This procedure has been implemented in the system MULTLOG [3]. For an analysis of upper bounds for the number of premises for propositional and quantifier rules see [27, Ch. 1]. If a connective never takes a particular truth value vi, then the introduction rule at place i is actually a weakening rule (see below). Example 3.1. Consider the disjunction in Belnap's logic: The partial normal forms (A ∨B)f iff Af and Bf (A ∨B)u iff (Af or Au) and (Bf or Bu) and (Au or Bu) (A ∨B)⊥ iff (Af or A⊥) and (Bf or B⊥) and (A⊥ or B⊥) (A ∨B)t iff At or Bt yield the following introduction rules: Γ, [f :A] Γ, [f :B] Γ, [f :A ∨B] ∨:f Γ, [f, u:A] Γ, [f, u:B] Γ, [u:A,B] Γ, [u:A ∨B] ∨:u Γ, [t:A,B] Γ, [t:A ∨B] ∨:t Γ, [f,⊥:A] Γ, [f,⊥:B] Γ, [⊥:A,B] Γ, [⊥:A ∨B] ∨:⊥ The other rules are as follows: Γ, [f :A,B] Γ, [f :A ∧B] ∧:f Γ, [t, u:A] Γ, [t, u:B] Γ, [u:A,B] Γ, [u:A ∧B] ∧:u Γ, [t:A] Γ, [t:B] Γ, [t:A ∧B] ∧:t Γ, [f,⊥:A] Γ, [f,⊥:B] Γ, [⊥:A,B] Γ, [⊥:A ∧B] ∧:⊥ 338 Γ, [t:A] Γ, [f :¬A] ¬:f Γ, [u:A] Γ, [u:¬A] ¬:u Γ, [⊥:A] Γ, [⊥:¬A] ¬:⊥ Γ, [f :A] Γ, [t:¬A] ¬:t Γ, [f :A] Γ, [t: Jf (A)] Jf :t Γ, [u:A] Γ, [t: Ju(A)] Ju:t Γ, [⊥:A] Γ, [t: J⊥(A)] J⊥:t Γ, [t:A] Γ, [t: Jt(A)] Jt:t Γ, [u,⊥, t:A] Γ, [f : Jf (A)] Jf :f Γ, [f,⊥, t:A] Γ, [f : Ju(A)] Ju:f Γ, [f, u, t:A] Γ, [f : J⊥(A)] J⊥:f Γ, [f, u,⊥:A] Γ, [f : Jt(A)] Jt:f The remaining rules (Jv:w) for v 6= w are weakenings at place w. D e f i n i t i o n 3.4. An introduction rule for a quantifier Q at place i in the logic L is a schema of the form: 〈Γ,∆Q:i(j)〉j∈I Γ, [i: (Qx)A(x)] Q:i where I is a finite set, ∆Q:i(j)(k) ⊆ {A(α1), . . . , A(αq), A(τ1), . . . , A(τp)} (1 ≤ k ≤ m), the αr are metavariables for free variables (the eigenvariables of the rule) satisfying the condition that they do not occur in the lower sequent, the τs are metavariables for terms, and the following condition holds: For every interpretation I it holds that 1. If for all d1, . . . , dq ∈ D there are e1, . . . , ep ∈ D s.t. I |= ∆Q:i(j){e1/τ1, . . . , ep/τp, d1/α1, . . . , dq/αq} then valI ( (Qx)A(x) ) = vi. 2. If for all e1, . . . , ep ∈ D there are d1, . . . , dq ∈ D s.t. I 6|= ∆Q:i(j){e1/τ1, . . . , ep/τp, d1/α1, . . . , dq/αq} then valI ( (Qx)A(x) ) 6= vi. In the case of two-valued classical logic, we have the well-known introduction rules (at place "true") for ∀ and ∃: Γ → ∆, A(α) Γ → ∆, (∀x)A(x) ∀:t Γ → ∆, A(τ) Γ → ∆, (∃x)A(x) ∃:t Here, as above, α and τ are metavariables standing for free variables and terms, respectively. That is to say, in an actual proof A(α) is replaced by a formula A containing a free variable a (in place of α), and A(τ) is replaced by a formula A containing a term t (in place of τ). The "eigenvariable condition" imposed on ∀:> is that the free variable a must not occur in the lower sequent. In the case of two-valued logic it is common to use a and t instead of α and τ in the first place. In the general case considered here it is necessary to explicitly introduce the metavariables α and τ in order to state the conditions on the rule in the above definition. Intuitively, what the condition means is that the statements "for all domain elements d1, . . . , dq in place of the eigenvariables α1, . . . , αq, respectively, there are domain elements e1, . . . , ep in place of the terms τ1, . . . , τp, respectively, so that the sequents ∆Q:i(j) are all true" implies that "(Qx)A(x) takes the value vi," and conversely, that "(Qx)A(x) takes the value vi" implies that "there are domain elements e1, . . . , ep in place of the terms τ1, . . . , τp, respectively s.t. for all domain elements d1, . . . , dq in place of the eigenvariables α1, . . . , αq, respectively, the sequents ∆Q:i(j) are all true," hold. In the case of two-valued logic this means that, for any interpretation, (∀x)A(x) is true iff for all domain elements d, A(d) is true; (∃x)A(x) is true iff there is some domain element e s.t. A(e) is true. The subtlety here is that it is required 339 that there is a domain element and not a term (which evaluates to that domain element) for (∃x)A(x) to be true. In an actual proof, however, τ is replaced by a term. The truth function for a quantifier Q immediately yields introduction rules for place i in a way similar to the method described above for connectives: Let I = {j ⊆ {v1, . . . , vm} | Q(j) 6= vi}, then the rule is given as in Definition 3.4, with ∆Q:i(j)(l) = {A(αjw) | w ∈ j, w 6= vl} ∪ {A(τ j) | vl ∈ V \ {j}}. Again, we emphasize that in general this is not the only possible rule. Example 3.2. Consider the universal quantor ∀ for Belnap's logic: (∀x)A(x) takes the value t only if for all d ∈ D the instance A(d) takes t, and false otherwise, i.e., if there is a d ∈ D s.t. A(d) takes a value among f , u, ⊥. We obtain the following rules: Γ, [f, u,⊥:A(τ)] Γ, [f : (∀x)A(x)] ∀:f Γ, [t:A(α)] Γ, [t: (∀x)A(x)] ∀:t The remaining rules (∀:u) and (∀:⊥) are instances of weakening rules. Similarly, we obtain rules for U: Γ, [f :A(τ)] Γ, [f, u:A(α)] Γ, [f : (Ux)A(x)] U:f Γ, [u:A(α)] Γ, [u: (Ux)A(x)] U:u Γ, [t:A(τ)] Γ, [t, u:A(α)] Γ, [t: (Ux)A(x)] U:t Γ, [f,⊥:A(τ)] Γ, [t,⊥:A(τ ′)] Γ, [⊥: (Ux)A(x)] U:⊥ The sequents denoted by ∆ in the introduction rules for connectives and quantifiers are called auxiliary sequents. D e f i n i t i o n 3.5. A sequent calculus LM for a logic L is given by: 1. axiom schemas of the form: [V :A], 2. for every connective 2 and every truth value vi an introduction rule 2:i, 3. for every quantifier Q and every truth value vi an introduction rule Q:i, 4. weakening rules for every place i: Γ Γ, [i:A] w:i 5. contraction rules Γ, [i:A,A] Γ, [i:A] c:i 6. exchange rules Γ, [i:B,A],∆ Γ, [i:A,B],∆ x:i 7. cut rules for every two truth values vi 6= vj : Γ, [i:A] ∆, [j:A] Γ,∆ cut:ij The rules (4)–(7) are called structural rules. A sequent Γ is provable in a given sequent calculus, if there is an upward tree of sequents, rooted in Γ , s.t. every topmost sequent is an axiom and every other sequent is obtained from the ones standing immediately above it by an application of one of the rules. T h e o r e m 3.1. (Soundness) If a sequent is provable in LM, then it is valid. 340 P r o o f . By induction on the length of proofs: Axioms are obviously valid, since every formula has to take some truth value. Introduction rules preserve validity by definition. The weakening rules are obviously sound. The cut rules are sound, since no formula can take two different truth values. 2 T h e o r e m 3.2. (Completeness) If a sequent is valid, then it is provable in LM without cuts from atomic axioms. P r o o f . We use the method of reduction trees, due to Schütte [23] (see also [26, Ch. 1, § 8]). We show that every sequent S is either provable in the sequent calculus or has a counter-model. Let E be an enumeration of all tuples of terms over L. Call a free variable available at stage k iff it occurs in the tree constructed before stage k (if there is no such variable, pick any and call it available), and new otherwise. Call a p-tuple t of terms available for the reduction of F at place i with eigenvariables a1, . . . , aq at stage k on a branch B iff 1. t contains only variables which are available at stage k or are among a1, . . . , aq, and either 2(a). t has not been used for a reduction of F at place i on B in a stage before k, or 2(b). the instance of the premise lying on B of a reduction of F at place i in a stage before k where t has been used did not contain any term variables. A reduction tree is a tree of sequents constructed from Γ in stages as follows: Stage 0: Write Γ at the root of the tree. Stage k: If the topmost sequent Γ ′ of a branch contains an atomic formula A s.t. A ∈⋂ j∈I Γ ′ (j) then stop the reduction for this branch. Call a branch open if it does not have this property. Apply the following reduction steps for every formula F occurring at place i in the topmost sequent Γ ′ of an open branch, which has neither already been reduced at place i on this branch in this stage, nor is the result of a reduction at this stage: 1. F ≡ 2(A′1, . . . , A′n): Replace Γ ′ in the reduction tree by: 〈Γ ′,∆′2:i(j)〉j∈I Γ ′ where ∆′2:i(j) is an instance of ∆2:i(j) in the rule 2:i introducing F as in Definition 3.3, obtained by instantiating A1, . . . , An with A′1, . . . , A ′ n, respectively. 2. F ≡ (Qx)A′(x): Let α1, . . . , αp be all eigenvariables and τ1, . . . , τq be all term variables in the premises of the rule schema Q:i. Replace Γ ′ in the reduction tree by:〈 Γ ′,∆′Q:i(j) 〉 j∈I Γ ′ where ∆′Q:i(j) is an instance of ∆Q:i(j) in Q:i introducing F as in Definition 3.4, obtained by instantiating A with A′, the eigenvariables α1, . . . , αp with the first p-tuple a1, . . . , ap of new free variables in the enumeration E, and the term variables τ1, . . . , τq with the first available q-tuple t1, . . . , tq of terms in E containing variables which are either available or among a1, . . . , ap, Observe that F ∈ Γ ′(i) and thus F occurs in all upper sequents. Now let TS be the reduction tree constructed in this manner. If TS is finite, then every topmost sequent contains an atomic formula that occurs at each place in that sequent. A 341 cut-free proof of Γ from axioms containing these formulas is easily constructed by inserting weakenings and exchanges. If TS is infinite it has an infinite branch B by König's Lemma. For every atomic formula P (t1, . . . , tn) in B, there is an 1 ≤ l ≤ m s.t. P (t1, . . . , tn) never occurs at place l in any sequents in this branch. We construct an interpretation I as follows: the domain is the set of terms, ΦI(t) = t (t a term) and ΦI ( P (t1, . . . , tn) ) = vl, where vl is the truth value corresponding to the place l. If F is a formula occurring in B, and F occurs at place i anywhere in B, then valI(F ) 6= vi. This is easily seen by induction on the structure of F : In particular, no formula in Γ evaluates to the truth value corresponding to the position at which it stands. Hence I does not satisfy Γ . 2 We obtain as a consequence of the reduction tree construction the following P r o p o s i t i o n 3.1. Let F be any formula. The sequent [V :F ] is cut-free provable from atomic axioms. 4 Elimination of Cuts The completeness theorem above shows that for every valid sequent there is a cut-free proof of that sequent. When analyzing given arbitrary proofs-as in our application in Section 6-one would like to have a method of stepwise transformation to a cut-free proof. This corresponds to extracting algorithmic content from proofs. The proof of the cut-elimination theorem for the family LM of many-valued sequent calculi is analogous to the proof of the classical case given in [11]. It proceeds by moving the cuts in a given proof upwards and by reducing cuts to cuts on formulas of smaller complexity. The most important prerequisite for the proof is therefore the possibility to transform a cut on a composite formula to a derivation using only cuts acting on subformulas of the original cutformula. In this section, we give a cut-elimination procedure modulo such a notion of reduction of cuts in the form of a parametric operator. In Section 5 we will show how to obtain such an operator. Like in [11], we replace the cut rule by the obviously equivalent mix rule: Π Λ Πi\A, Λj\A mix:ij(A) where A occurs in Π(i) and Λ(j), and Πi\A (Λj\A) is obtained from Π (Λ) by deleting every occurrence of A in Π(i) (Λ(j)). Call the calculus obtained from LM by replacing the cut rule with the mix rule LM′. D e f i n i t i o n 4.1. The degree of a mix:ij(A) is the depth of the mix formula A. The degree of an LM′-proof P having only one mix:ij(A) as its last inference, denoted d(P ), is the degree of that mix. We call a thread (cf. [26, p. 14]) in P containing the left (right) upper sequent of the mix a left (right) thread. The rank of a left (right) thread is the number of consecutive sequents counting upwards from the left (right) upper sequent of the mix which contain the mix formula at place i (j). The left (right) rank of P , denoted rl(P ) (rr(P )) is the maximum of the ranks of its left (right) threads. The rank of P , denoted r(P ), is the sum of its left and right rank: r(P ) = rl(P ) + rr(P ). D e f i n i t i o n 4.2. An LM′-proof P is called regular, if every eigenvariable in P is the eigenvariable of only one quantifier introduction and occurs only in the subproof ending in that introduction. 342 In particular it cannot be the case in a regular proof that a free variable occurs as an eigenvariable in one inference and in a term which is replaced by a bound variable in another inference. It is easy to see that any proof can be transformed into a regular proof by renaming some eigenvariables. The crucial part of the cut-elimination theorem is the reduction of mixes. From a proof ending in one mix we pass to a proof containing several mixes acting on formulas of lower complexity. The important step is when the principal formula of the mix is introduced immediately above the mix. To deal with this case, we introduce the notion of mix reduction function Red below. Using this function we obtain from the premises of the introduction rules immediately preceding the mix a deduction of the conclusion of the mix from these premises, but using only cuts on the formulas occurring in the premises, thus lowering the degree. By applying Red to a mix we mean the modification of the proof by replacing the two introductions and the mix by this deduction. D e f i n i t i o n 4.3. Let A be a formula with outermost logical symbol f , let f :i and f :j be the introduction rules for f at places i and j, and let Π,∆f :i(k) (k ∈ Ii) and Λ, ∆f :j(l) (l ∈ Ij) be the premises of instances of f : i and f : j introducing A at places i and j, respectively. If f is a quantifier, then f : i and f : j have eigenvariables a1, . . . , ap and eliminate (i.e., replace by the bound variable) terms t1, . . . , tq. Then Red(A; f : i; f : j) = R is an LM′ derivation with the following properties: 1. The end sequent of R is the empty sequent, 2. Every topmost sequent of R is obtained from ∆f :i(s) or ∆f :j(r) by replacing some (including none) eigenvariables among a1, . . . , ap by terms among t1, . . . , tq, 3. R contains only mixes of degree < d(P ). The function Red is called a mix reduction function. R e m a r k 4.1. Note that Red eliminates only the outermost logical symbol of A, i.e., by applying Red once the degree of a mix is reduced by exactly one. It is also possible to work with a function Red which decreases the degree by more than one. When considering directly dependent rules, i.e., rules which can be replaced by a number of primitive rules, it is then evident how such an extension can be used to obtain cut-elimination procedures for the resulting calculi. It only requires some inspection of the proofs ending in the two introduction rules f : i and f : j and some manipulation to modify this extension so that mixes of degree d can be reduced in one step to mixes of degree < d− 1. This will be evident in the next section where we show how to obtain such a function Red. D e f i n i t i o n 4.4. Let R be an LM′-derivation with end-sequent Γ and let Π be a sequent. Then we denote by Π,R the derivation obtained from R by adding Π to the left of every sequent in R, and by appending exchanges and contractions as necessary so that the end-sequent of Π,R is Γ . We are now ready to state and prove the Hauptsatz for LM: T h e o r e m 4.1. Cuts can be eliminated in LM-proofs. For the reader not steeped in proof theory this statement seems curious. It seems that we have accomplished this result already (by the completeness theorem 3.2). A clarification is in order here: The phrase "cuts can be eliminated" has the status of a terminus technicus, and means much more than that for every proof there is one not using the cut rule. Roughly, it means that there is a primitive recursive procedure that transforms a given proof into a cut-free one, and moreover, this procedure is "local" in the sense that it eliminates one cut at a time (or in some variants a whole cluster of cuts). 343 L e m m a 4.1. Assume that from any proof P ′ which contains only one mix of degree < d that mix can be eliminated. Then all mixes can be eliminated from any LM′-proof P containing n mixes of degrees < d. P r o o f . By induction on the number n of mixes in P : For n = 1 this is the assumption. If n > 1, then let P ′ be some subproof of P which ends in a mix and contains only that mix. By assumption, the mix can be eliminated from P ′, yielding a proof P ′′ of the same end-sequent as P ′. By replacing P ′ in P by P ′′ we obtain a proof with n− 1 mixes, all of degree < d, and the induction hypothesis applies. 2 L e m m a 4.2. Let P be an LM′-proof containing only one mix:ij(A) as its last inference. Then P can be transformed to a mix-free LM′-proof P of the same end-sequent. P r o o f . Let P be an LM′-proof containing only one mix:ij(A) which occurs as the last inference in P . W.l.o.g. we assume that P is regular. P is of the form: .... P1 Π .... P2 Λ Πi\A, Λj\A mix:ij(A) The proof is by double induction on the rank and degree of P : 1. r(P ) = 2, i.e., left and right rank of P equal 1. We distinguish cases according to the type of the inferences immediately above the mix: (a) Π is an axiom [V :A]. P is of the form [V :A] .... P2 Λ [V \ vi:A], Λj\A mix:ij(A) We can derive Πi\A, ΛjA without a mix as follows: .... P2 Λ [j:A, . . . , A], Λj\A x [j:A], Λj\A c [V \ vi:A], Λj\A w (b) Λ is an axiom. Similarly. (c) Π is the conclusion of a structural inference. Since the left rank is 1, this inference must be a weakening introducing A at place i: .... P1 Πi\A Πi\A, [i:A] w: i .... P2 Λ Πi\A, Λj\A mix:ij(A) where Π is Πi\A, [i:A]. We obtain Πi\A, Λj\A without a mix as follows: .... P1 Πi\A Πi\A, Λj\A w 344 (d) Λ is the conclusion of a structural inference. Similarly. (e) Both Π and Λ are conclusions of introduction rules 2:i and 2:j for the connective 2:〈 .... Pir Π,∆2:i(r) 〉 r Π, [i:2(* * *)] 〈 .... Pjs Λ, ∆2:j(s) 〉 s Λ, [j:2(* * *)] Π,Λ mix:ij(2(* * *)) R = Red(A;2: i;2: j) is a derivation of the empty sequent with initial sequents among ∆2:i(r) and ∆2:j(s). Let P ′ir (P ′ js) be Pir (Pjs) with weakenings and exchanges appended so that the end sequent equals Π,Λ,∆2:i(r) (Π,Λ,∆2:j(s)). Let P ′ be the proof obtained from Π,Λ,R by writing P ′ir (P ′ js) above any topmost sequent of the form Π,Λ,∆2:i(r) (Π,Λ,∆2:j(s)). By the induction hypothesis and Lemma 4.1 the mixes can be eliminated from P ′. (f) Both Π and Λ are conclusions of introduction rules Q:i and Q:j for the quantifier Q:〈 .... Pir Π,∆Q:i(r) 〉 r Π, [i: (Qx)A(x)] 〈 .... Pjs Λ, ∆Q:j(s) 〉 s Λ, [j: (Qx)A(x)] Π,Λ mix:ij(Qx)A(x)) R = Red(A;Q: i;Q: j) is a derivation of the empty sequent. An initial sequent in R is of the form ∆Q:i(r)σ or ∆Q:j(s)σ, where σ is a substitution mapping some eigenvariables to terms. Let P ′ir (P ′ js) be Pir (Pjs) with weakenings and exchanges appended so that the end sequent equals Π,Λ,∆Q:i(r) (Π,Λ,∆Q:j(s)). Let P ′ be the proof obtained from Π,Λ,R by writing P ′irσ (P ′ jsσ) above any topmost sequent of the form Π,Λ,∆Q:i(r)σ (Π,Λ,∆Q:j(s)σ). P ′ is indeed a proof since (a) Π and Λ cannot contain any eigenvariables and (b) the terms in ranσ do not contain eigenvariables of any quantifier introductions in the Pir or Pjs. By the induction hypothesis and Lemma 4.1 the mixes can be eliminated from P ′. 2. rr(P ) > 1: Again, we distinguish cases: (a) Λ(i) contains A. We obtain the following mix-free proof: .... P1 Π Πi\A, [i:A, . . . , A] e Πi\A, [i:A] c Πi\A, Λj\A w (b) Π(j) contains A. Similarly. (c) Λ is the consequence of an inference J2, which is either structural (but not a mix), or a logical inference (not introducing A at place j). P is of the form .... P Π .... P1 Ψ1 . . . .... Pp Ψp Λ J2 Πi\A, Λj\A mix:ij(A) 345 Let j1, . . . , js, 1 ≤ jk ≤ p, be all indices s.t. Ψjk contains A. (There is at least one such jk, otherwise the right rank of P would equal 1). Consider the proofs P ′jk : .... Π .... Ψjk Πi\A, Ψjk j\A mix:ij(A) In P ′jk , rl(P ′ jk ) = rl(P ) and rr(P ′jk) ≤ rr(P )−1, and in sum r(P ′ jk ) ≤ r(P )−1. Hence the induction hypothesis applies and we have mix-free proofs P ′′jk of Π i\A, Ψjk j\A. For indices l not occurring in the above list, we have that Ψl equals Ψlj\A, and we define P ′′l as .... Pl Ψl Πi\A, Ψl w If J2 is a weakening at place j (and consequently, p = 1 and Ψ1j\A = Λj\A), then P ′′1 serves as our transformed proof. Otherwise, construct a proof as follows: .... P ′′ 1 Πi\A, Ψ1 j\A . . . .... P ′′ p Πi\A, Ψp j\A Πi\A, Λj\A J2 Πi\A, Λj\A x (d) Λ is the consequence of a logical inference J2 introducing A at place j. P is of the form .... P Π .... P1 Λ, ∆1 . . . .... Pp Λ, ∆p Λ, [j:A] J2 Πi\A, Λj\A mix:ij(A) Consider the proofs P ′k, 1 ≤ k ≤ p (Note that ∆k does not contain A-only proper subformulas of A-and hence ∆kj\A equals ∆k): .... P ′ Π .... Pk Λ, ∆k Πi\A, Λj\A,∆k (A, i, j) In Pk, rl(P ′k) = rl(P ), rr(P ′ k) ≤ rr(P )− 1 and in sum r(P ′k) ≤ r(P )− 1. Hence, the induction hypothesis applies and we obtain mix-free proofs P (k)′′ of Πi\A, Λj\A,∆k. Construct a proof P ′ as follows: .... P Π .... P ′′ 1 Πi\A, Λj\A,∆1 . . . .... P ′′ p Πi\A, Λj\A,∆p Πi\A, Λj\A, [j:A] J2 Πi\A,Πi\A, Λj\A mix:ij(A) Note that A does not occur at place j in Πi\A, since otherwise case 2.b would have applied, hence rr(P ′) = 1. With rl(P ′) = rl(P ) we have that r(P ′) < r(P ) and the 346 induction hypothesis yields a mix-free proof P ′′ of Πi\A,Πi\A, Λj\A. We obtain a mix-free proof: .... P ′ Πi\A,Πi\A, Λj\A Πi\A, Λj\A xc 3. rr(P ) = 1 and rl(P ) > 1: This case is dealt with in the same way as 2. above, mutatis mutandis. This completes the proof of the lemma (and the cut-elimination theorem). 2 5 Resolution-based Cut Reduction Operators In this section we give a definition of one of many possible cut reduction functions Red for the Hauptsatz. Our approach uses many-valued resolution. It is based on the observation that the soundness of the cut rule consists in the fact that a formula A cannot take two different truth values at the same time. Clauses are a convenient metalogical notation for expressing such negative statements, while sequents are not. There are, however, close relationships between clause and sequent calculi and in particular the resolution rule and the cut rule. It is not surprising, then, that resolution deductions can be translated to sequent calculus derivation using only cuts (or, as in our case, mixes). Many-valued resolution [1] is a straightforward extension of resolution for classical first-order logic. It is based on clause syntax: A clause is a set of literals, a literal is an atomic formula together with a truth value index. In usual resolution, the negation sign plays the rôle of the truth value index: ¬A means "A is false", A without negation sign means "A is true". In the many-valued case we have literals of the form Aw with the interpretation "A takes the value w." The free variables in a clause C are understood to be "universally quantified". More precisely, a structure M universally satisfies a clause C iff for all assignments s the interpretation 〈M, s〉 satisfies C (in the sense of Definition 3.2). M universally satisfies a set of clauses C iff M universally satisfies each clause C ∈ C. If no M universally satisfies C, then C is called universally unsatisfiable. The empty clause ∅ is, of course, universally unsatisfiable. In the following, we assume familiarity with basic resolution terminology. D e f i n i t i o n 5.1. Let C1 and C2 be variable disjoint clauses and let D1 = {Av1, . . . , Avp} ⊆ C1 and D2 = {Bw1 , . . . , Bwq } ⊆ C2 be subsets of C1 and C2 where v 6= w. If {A1, . . . , Ap, B1, . . . , Bq} is unifiable with most general unifier (mgu) σ, then R = (C1 \D1)σ∪ (C2 \D2)σ is called a resolvent of C1 and C2. A (tree-like) resolution deduction from a set of clauses C is an upward tree of clauses, where every clause either results from a clause in C by renaming of variables iff it is a topmost clause, or otherwise is a resolvent of the two clauses immediately above it. We write C ` D if there is a resolution deduction from C whose bottom clause is D. T h e o r e m 5.1. ([1, 27]) C ` ∅ iff C is universally unsatisfiable. D e f i n i t i o n 5.2. Let Γ be a sequent consisting of atomic formulas only. Then cl(Γ ) is defined as the clause cl(Γ ) = {Avi | A occurs in Γ(i)} Conversely, if C is a clause then the sequent seq(C) is defined by seq(C)(i) = A1, . . . , Ap 347 if Avi1 , . . . , A vi p are all literals with index vi in C. (We assume some arbitrary but fixed ordering of atoms.) Clearly, seq(cl(Γ )) is Γ up to exchanges and contractions. The mix reduction function Red takes as arguments a formula A with outermost symbol f and two rules f : i and f : j introducing f at places i and j. We shall now define one possible reduction function by showing how, for any two introduction rules, a schematic derivation of the empty sequent from the premises of the rules can be obtained. For any particular formula and rule applications the corresponding instance of the derivation is immediately obtained by matching formulas to schematic letters, terms to metavariables for terms, and variables to metavariables for eigenvariables. Consider the rule schemata 〈∆2:i(r)〉r∈Ii [i:2(A1, . . . , An)] 〈∆2:j(s)〉s∈Ij [j:2(A1, . . . , An)] Let ∆′2:i(r) (∆ ′ 2:j(s)) be obtained from ∆2:i(r) (∆2:j(s)) by replacing the schematic formula Ai by an atomic formula PAi . Let C be the set of clauses C = ⋃ r∈Ii {cl(∆′2:i(r)} ∪ ⋃ s∈Ij {cl(∆′2:j(r)} C is clearly universally unsatisfiable, since (the "conjunction" of) ∆′2:i(r) is equivalent to 2(*)vi and (the "conjunction" of) ∆′2:j(s) is equivalent to 2(*)vj , where i 6= j. By the completeness of many-valued resolution there is a resolution deduction R of ∅ from C. Note that the literals in C are all variable-free, and hence, in every resolution step, there is only one literal that is resolved upon. R can be translated to an LM′ deduction seq(R) of the empty sequent. We argue by induction: If R consists only of an initial clause cl(∆′), then seq(R) is the sequent seq(cl(∆′)). Otherwise, let .... R1 C1 ∪ {P vkAi } .... R2 C2 ∪ {P vlAi} C1 ∪ C2 be the last resolution step in R. We obtain seq(R) as follows: .... seq(R1) seq(C1 ∪ {P vkAi }) .... seq(R2) seq(C2 ∪ {P vlAi}) seq(C1), seq(C2) mix:ij(PAi) We can now take as Red(A;2: i;2: j) the derivation P where P is obtained from seq(R) by (a) replacing PAi by Ai and (b) adding (if necessary) derivations of seq(cl(∆)) from ∆ above the initial sequents (these require only exchanges). Example 5.1. Consider the case of a mix on two formulas with outermost logical symbol ∨ at places f and ⊥. The clause translation of the premises is C = {{P fA}, {P f B}, {P f A, P ⊥ A }, {P f B , P ⊥ B }, {P⊥A , P⊥B }} A possible resolution refutation is {P fB} {P fA} {P⊥A , P⊥B } {P⊥B } ∅ 348 From this we obtain the following deduction schema: [f :B] [f :A] [⊥:A,B] [⊥:B] mix:f⊥(A) ∅ mix:f⊥(B) For the quantifiers, consider the rule schemata 〈∆Q:i(r)〉r∈Ii [i: (Qx)A(x)] 〈∆Q:j(s)〉s∈Ij [j: (Qx)A(x)] Let ∆′Q:i(r) (∆ ′ Q:j(s)) be obtained from ∆Q:i(r) (∆Q:j(s)) by replacing the schematic formula A(α) by an atomic formula P (xα), and every formula A(τ) by P (cτ ). Let C be the set of clauses C = ⋃ r∈Ii {cl(∆′Q:i(r)} ∪ ⋃ s∈Ij {cl(∆′Q:j(r)} Again, C is universally unsatisfiable. Let R be a resolution deduction of ∅ from C. Since R is in tree form, the cumulative substitution ρ of R can be defined as usual. The initial clauses of R may be renamings of clauses in C. We choose these renamings so that a variable xα is renamed as xhα. We recursively translate Rρ into an LM ′-derivation as follows: If Rρ only consists of an initial clause cl(∆′), then seq(Rρ) is the sequent seq(cl(∆′λρ)) (λ is some renaming substitution). Otherwise, let .... R1 C1 ∪ {Lvl} .... R2 C2 ∪ {Lvk} C1 ∪ C2 be the last resolution step in Rρ, where L is an atom of the form P (x) or P (c) (x is a variable and c a constant symbol). Recall that the cumulative substitution has been applied to R, so resolution steps actually do take this special form with only one literal resolved upon. We obtain seq(Rρ) as follows: .... seq(R1) seq(C1 ∪ {Lvk}) .... seq(R2) seq(C2 ∪ {Lvl}) seq(C1), seq(C2) mix:ij(L) The substitution ρ replaces variables of the form xhα by constants cτ . take as Red(A;Q: i;Q: j) the derivation P where P is obtained from seq(Rρ) by (a) replacing P (xhα) resp. P (cτ ) by A(α) resp. A(τ) and (b) adding (if necessary) derivations of seq(cl(∆))λπ from ∆λπ above the initial sequents (these require only exchanges and contractions). Example 5.2. Consider the case of a mix on two formulas with outermost logical symbol U at places u and ⊥. The clause translation of the premises is C = { {P (xα)u}, {P (cτ )f , P (cτ )⊥}, {P (cτ ′)t, P (cτ ′)⊥} } One of the possible resolution refutations is {P (x′α)u} {P (xα)u} {P (cτ )f , P (cτ )⊥} {P (cτ )⊥} cτ/xα ∅ cτ/x ′ α 349 Note that two copies of the clause {P (xα)u} have been used. From this we obtain the following deduction schema: [u:A(τ/α)] [u:A(τ/α)] [f,⊥:A(τ)] [⊥:A(τ)] mix:uf(A(τ)) ∅ mix:u⊥(A(τ)) Similar considerations could also be used to obtain "macro-reductions" of composite formulas of depth > 1 in one step. This may lead to an algorithmic simplification of cut-elimination if the structure of the cut formula is of a specific type, e.g., monadic. 6 Reasoning about Knowledge in Belnap's Logic A consequence of the cut-elimination theorem is Gentzen's "Verschärfter Hauptsatz", also known as T h e o r e m 6.1. (Midsequent Theorem) Let Π be a sequent consisting only of prenex formulas. Any proof of Π can be effectively transformed to a cut-free proof of Π containing sequents Σ1, . . . , Σp, s.t., for all 1 ≤ j ≤ p, 1. Σj is quantifier-free, 2. every inference above Σj is either structural or propositional, and 3. every inference below Σj is either structural or a quantifier inference. P r o o f . By the cut-elimination theorem and Proposition 3.1, the given proof can be transformed to a cut-free proof P of Π from atomic axiom sequents. The order of a quantifier introduction (Q:i) in P is defined as the number of propositional inferences below (Q:i). The order o(P ) of P is the sum of the orders of all quantifier inferences occurring in P . We prove the theorem by induction on the order of P : 1. o(P ) = 0: There is no propositional inference occurring below any quantifier inferences. Let B be a branch in P . Let ΣB be the conclusion of the lowermost propositional inference on B, or the (atomic) axiom sequent on B if B does not contain any propositional inferences. If ΣB contains a quantified formula F , then F is introduced by weakenings. To see this, recall that Π contains only prenex formulas: By the subformula property, F is a subformula of a formula in Π, hence no propositional inferences apply to it. Eliminate F and all inferences applying to it from the part of B above ΣB , and add appropriate weakenings and exchanges directly below ΣB . After the above procedure has been applied to all branches B in P , the (finite) set of all ΣB serves as the set of Σj in the statement of the theorem. 2. o(P ) > 0: Then there is a quantifier inference (Q:i) with the following property: The topmost logical inference below (Q:i) is a propositional inference, say (2:j). The part of P between (Q:i) and (2:j) takes the following form: .... Γ1 . . . 〈 .... Γ ′,∆Q:i(k) 〉 k Γ ′, [i: (Qx)A(x)] Q:i .... ∗ Γ ′′ . . . .... Γn Γ 2:j 350 where the part denoted by ∗ contains only structural inferences, and Γ and Γ ′′ contain (Qx)A(x) as a sequent-formula. We can now lower the order by exchanging the positions of (Q:i) and (2:j): / ∖ .... Γ1 ∆Q:i(k), Γ1 . . . .... Γ ′,∆Q:i(k) Γ ′,∆Q:i(k), [i: (Qx)A(x)] w ∆Q:i(k), Γ ′, [i: (Qx)A(x)] e .... ∗ ∆Q:i(k), Γ ′′ . . . .... Γn ∆Q:i(k), Γn ∆, Γ 2:j Γ,∆Q:i(k) e ∖ / k Γ, [i: (Qx)A(x)] Q:i Γ e, c 2 Similar considerations can also be used for analyzing natural deduction proofs in many-valued logic as introduced in [5]. In the following example, we consider a representation of knowledge about (possibly inconsistent and incomplete) sets E of facts, using Belnap's logic enriched by the quantifiers ∀ and U. The facts are simply Boolean ground literals. These facts may be contradictory in the sense that both P and ¬P are present. Furthermore, it may be the case that for some ground atom A of the language, neither A nor ¬A is contained in the facts base. The facts may be thought of as evidences for certain state of affairs. They might, e.g., be protocols of certain experiments. The epistemic state s of a set of facts is the four-valued interpretation of all ground atoms induced by the facts base E: if both A and ¬A are facts, then s(A) = ⊥, if neither A nor ¬A is a fact then s(A) = u, if only A (¬A) is a fact then s(A) = t (f). The meta-knowledge is a set K of universal true sentences (∀x)B1(x), . . . , (∀x)Bq(x) of Belnap's logic. The meta-knowledge is assumed to be consistent with all possible epistemic states. In cases where the facts base is too large or unwieldy to work with, one might use instead the meta-knowledge to reason about the facts. For instance, we might deduce from K that the sentence (Ux)A(x) takes the truth value ⊥, expressing that the instances of A(x) are neither uniformly true nor uniformly false. This can be formalized in the sequent calculus by proving the sequent [f : (∀x)B1(x), . . . , (∀x)Bq(x)], [⊥: (Ux)A(x)]. A proof of this sequent can, by virtue of an analog of Herbrand's theorem, be analyzed to yield a finite sequence of critical pairs 〈A(t1), A(t′1)〉, . . . , 〈A(tp), A(t′p)〉 s.t. for every epistemic state under consideration, A(ti) and A(t′i) will take different truth values for some 1 ≤ i ≤ p. T h e o r e m 6.2. Let P be a proof of [f : (∀x)B1(x), . . . , (∀x)Bq(x)], [⊥: (Ux)A(x)] Then P can be transformed to proofs of [f : (∀x)B1(x), . . . , (∀x)Bq(x)], [w1:A(tw11 )], [⊥:A(t w1 1 )], . . . , [wr:A(t wr r )], [⊥:A(twrr )] for 〈w1, . . . , wr〉 ∈ {t, f}r. (The critical pairs then are 〈A(tt1), A(t f 1 )〉, . . . , 〈A(ttr), A(tfr )〉.) 351 P r o o f . Apply the midsequent theorem to P . None of the quantifier inferences in the proof have eigenvariable conditions (cf. Example 3.2). Let Σ1, . . . , Σp be the midsequents of this transformed proof. From each of these midsequents a sequent of the above form can be derived, possibly using weakenings. Observe that (∀:f) takes only one premise, hence one midsequent is sufficient in each case. 2 7 Conclusion We have introduced a general approach to obtaining sequent calculi for finite-valued firstorder logics. These sequent calculi enjoy cut-elimination and midsequent theorems. In special cases, the proof-theoretic properties can be exploited to obtain more specific results about the particular logics at hand. We illustrated this by exhibiting a version of Herbrand's theorem for a first-order extension of Belnap's four-valued logic suitable for reasoning about possibly inconsistent and incomplete knowledge bases. Similar results by proof-theoretic analysis such as interpolants constructed in Maehara's lemma (see [26, Ch. 1]) may be used for further classification of inconsistencies. References [1] M. Baaz and C. G. Fermüller. Resolution for many-valued logics. In A. Voronkov, editor, Logic Programming and Automated Reasoning. Proceedings LPAR'92, LNAI 624, pp. 107– 118, Berlin, 1992. Springer. [2] M. Baaz and C. G. Fermüller. Resolution-based theorem proving for many-valued logics. submitted, 1993. [3] M. Baaz, C. G. Fermüller, A. Ovrutcki, and R. Zach. MULTLOG: A system for axiomatizing many-valued logics. In A. Voronkov, editor, Logic Programming and Automated Reasoning. Proceedings LPAR'93, LNAI 698, pp. 345–347, Berlin, 1993. Springer. [4] M. Baaz, C. G. Fermüller, and R. Zach. Dual systems of sequents and tableaux for many-valued logics. Bull. EATCS, 51:192–197, 1993. paper read at 2nd Workshop on Tableau-based Deduction, Marseille, April 1993. [5] M. Baaz, C. G. Fermüller, and R. Zach. Systematic construction of natural deduction systems for many-valued logics. In Proc. 23rd International Symposium on Multiple-valued Logic, pp. 208–213, Sacramento, CA, May 24–27, 1993. IEEE Press. [6] N. D. Belnap. A useful four-valued logic. In J. M. Dunn and G. Epstein, editors, Modern Uses of Multiple-valued Logic, pp. 9–37. Reidel, 1975. [7] W. A. Carnielli. Systematization of finite many-valued logics through the method of tableaux. J. Symbolic Logic, 52(2):473–493, 1987. [8] W. A. Carnielli. On sequents and tableaux for many-valued logics. J. Non-Classical Logic, 8(1):59–76, 1991. [9] M. Fitting. Bilattices in logic programming. In Proc. 20th International Symposium on Multiple-valued Logic, pp. 238–246, Charlotte, NC, May 23–25, 1990. IEEE Press. [10] M. Fitting. Bilattices and the semantics of logic programming. J. Logic Programming, 11(1 & 2):91–116, July 1991. [11] G. Gentzen. Untersuchungen über das logische Schliessen I–II. Math. Z., 39:176–210, 405–431, 1934. [12] M. L. Ginsberg. Multivalued logics: A uniform approach to reasoning in artificial intelligence. Comput. Intell., 4:265–316, 1988. [13] R. Hähnle. Uniform notation of tableaux rules for multiple-valued logics. In Proc. 21st International Symposium on Multiple-valued Logic, pp. 238–245, 1991. 352 [14] R. Hähnle. Tableaux-Based Theorem Proving in Multiple-Valued Logics. PhD thesis, Universität Karlsruhe, Institut für Logik, Komplexität und Deduktionssysteme, May 1992. [15] R. Hähnle. Automated Deduction in Multiple-Valued Logics. Oxford University Press, Oxford, 1993. [16] R. Hähnle and W. Kernig. Verification of switch level designs with many-valued logic. In A. Voronkov, editor, Logic Programming and Automated Reasoning. Proceedings LPAR'93, LNAI 698, pp. 158–169, Berlin, 1993. Springer. [17] Y. Kaluzhny and A. Y. Muravitsky. A knowledge representation based on the Belnap's four-valued logic. J. Applied Non-Classical Logics, 1993. to appear. [18] A. Mostowski. The Hilbert epsilon function in many-valued logics. Acta Philos. Fenn., 16:169–188, 1963. [19] P. O'Hearn and Z. Stachniak. A resolution framework for finitely-valued first-order logics. J. Symbolic Computation, 13:235–254, 1992. [20] J. B. Rosser and A. R. Turquette. Many-Valued Logics. Studies in Logic. North-Holland, Amsterdam, 1952. [21] G. Rousseau. Sequents in many valued logic I. Fund. Math., 60:23–33, 1967. [22] K. Schröter. Methoden zur Axiomatisierung beliebiger Aussagenund Prädikatenkalküle. Z. Math. Logik Grundlag. Math., 1:241–251, 1955. [23] K. Schütte. Ein System des verknüpfenden Schliessens. Arch. Math. Logik Grundlag., 2:55–67, 1956. [24] S. J. Surma. An algorithm for axiomatizing every finite logic. In D. C. Rine, editor, Computer Science and Multiple-valued Logic: Theory and Applications, pages 137–143. North-Holland, Amsterdam, 1977. [25] M. Takahashi. Many-valued logics of extended Gentzen style I. Sci. Rep. Tokyo Kyoiku Daigaku Sect A, 9:271, 1967. [26] G. Takeuti. Proof Theory. Studies in Logic 81. North-Holland, Amsterdam, 2nd edition, 1987. [27] R. Zach. Proof Theory of Finite-valued Logics. Diplomarbeit, Technische Universität Wien, 1993. Zusammenfassung: Es wird eine uniforme Konstruktion von Sequentialkalkülen für endlichwertige Logiken erster Stufe mit sog. Distributionsquantoren vorgestellt. Für diese Kalküle werden Vollständigkeit, Schnittelimination und Mittelsequenzsätze gezeigt. Als eine Anwendung wird ein Analogon zum Herbrand'schen Satz für die vierwertige Wissensrepräsentationslogik von Belnap und Ginsberg abgeleitet. Dieser Satz kann zum Schliessen mit unvollständigen und inkonsistenten Daten verwendet werden. 353 Authors' addresses: Matthias Baaz Technische Universität Wien Institut für Algebra und diskrete Mathematik E118.2 Wiedner Hauptstrasse 8–10, A-1040 Wien, Austria baaz@logic.tuwien.ac.at Christian G. Fermüller Richard Zach Technische Universität Wien Institut für Computersprachen E185.2 Resselgasse 3/1, A-1040 Wien, Austria chrisf@logic.tuwien.ac.at zach@logic.tuwien.ac.at Erratum The introduction rules for ∧:f and ∨:t given in Example 3.1 on page 338 are erroneous. The correct partial normal form for ∨ is: (A ∨B)t iff (At or Au or A⊥ or Bt) and (At or Au or Bt or Bu) and (At or A⊥ or Bt or B⊥) and (At or Bt or Bu or B⊥) The correct rules are: Γ, [u,⊥, t:A], [t:B] Γ, [⊥, t:A,B] Γ, [u, t:A,B] Γ, [u,⊥, t:B], [t:A] Γ, [t:A ∨B] ∨:t Γ, [u,⊥, f :A], [f :B] Γ, [⊥, f :A,B] Γ, [u, f :A,B] Γ, [u,⊥, f :B], [f :A] Γ, [f :A ∨B] ∧:f We are indebted to E. Reznik and M. Ultlog for drawing our attention to this mistake.