We implement an algorithm for extracting appropriate collections of classic-like sound and complete tableaux rules for a large class of finite-valued logics. Its output consists of Isabelle theories. 1
This note will report on the first developments towards the implementation of a fully automated system for the extraction of adequate proof-theoretical counterparts for sufficiently expressive logics characterized by way of a finite set of finite-valued truth-tables. The underlying algorithm was first described in [2]. Surveys on tableaux for many-valued logics can be found in [4,1]. The implementation has been performed in ML, and its application gives rise to an Isabelle theory (check [5]) formalizing a given finite-valued logic in terms of two-signed tableau rules.
The survey paper [4] points at a few very good theoretical motivations for studying tableaux for many-valued logics, among them:
tableau systems are a particularly well-suited starting point for the development of computational insights into many-valued logics; a close interplay between model-theoretic and proof-theoretic tools is necessary and fruitful during the development of proof procedures for non-classical logics. Section 2, right below, recalls the relevant definitions and results concerning many-valued logics as well as their homologous presentation in terms of bivalent semantics defined by clauses of a certain format we call 'gentzenian'. An algorithm for endowing any sufficiently expressive finite-valued logic with an adequate bivalent semantics is exhibited and illustrated for the case of L 3 , the well-known 3-valued logic of Lukasiewicz.
The concepts concerning tableau systems in general and the particular results that allow one to transform any computable gentzenian semantics into a corresponding collection of tableau rules are illustrated in section 3, for the case of L 3 . Section 4 discusses our current implementation, carefully explaining its expected inputs and outputs, and again illustrates its functioning for the case of L 3 . Advantages and shortcomings of our system, in its present state of completion, as well as conclusions and some directions for future work are mentioned in section 5.
Given a denumerable set At of atoms and a finite family Cct = { c i j } j∈J of connectives, where arity( c i j ) = i, let S denote the term algebra freely generated by Cct over At. Here, a semantics Sem for the algebra S will be given by any collection of mappings { § V k } k∈K where dom( § V k ) = S and codom( § V k ) = V k , and where each collection of truth-values V k is partitioned into sets of designated values, D k , and undesignated ones, U k . The mappings § V k themselves may be called (ν-valued) valuations, where ν = Card(V k ). A bivalent semantics is any semantics where D k and U k are singleton sets, for any k ∈ K. For bivalent semantics, valuations are often called bivaluations.
The canonical notion of (single-conclusion) entailment |= Sem ⊆ Pow(S) × S induced by a semantics Sem is defined by setting
The pair S, |= Sem may be called a generic ν-valued logic, where ν = Max k∈K (Card(V k )).
If one now fixes the sets of truth-values V, D and U, and considers, for each connective c i j an interpretation c i j : V i −→ V, one may immediately build from that an associated algebra of truth-values T V = V, D, { c i j } j∈J (in the present paper, whenever there is no risk of confusion, we shall not differentiate notationally between a connective symbol c and its interpretation c ). A truthfunctional semantics is then defined by the collection of all homomorphisms of S into T V. In this paper, the shorter expression ν-valued logic will be used to qualify any generic ν-valued truth-functional logic, for some finite ν, where ν is the minimal value for which the mentioned logic can be given a truth-functional semantics characterizing the same associated notion of entailment.
The canonical notion of entailment of any given semantics, and in particular of any given truth-functional semantics, may be emulated by a bivalent semantics. Indeed, consider V 2 = {T, F } and D 2 = {T }, and consider the 'binary print' of the algebraic truth-values produced by the total mapping t : V −→ V 2 , defined by t(v) = T iff v ∈ D. For any ν-valuation § V of a given semantics Sem, consider now the characteristic total function b § = t • § V . Now, collect all such bivaluations b § 's into a new semantics Sem(2), and note that Γ Sem(2) ϕ iff Γ Sem ϕ. The standard 2-valued notion of inference of Classical Logic is characterized indeed by a bivalent truth-functional semantics. In general, though, a bivalent characterization of a logic with a ν-valued truth-functional semantics explores the trade-off between the 'algebraic perspective' of many-valuedness, with its many 'algebraic truth-values' and its semantic characterization in terms of a set of homomorphisms, on the one hand, and the classic-inclined 'logical perspective', with its emphasis on characterizations based on 2 'logical values', ontheotherhand(formoredetaileddiscussionsofthisissue,check [2,7]).Our interest in this paper is to probe some of the practical advantages of the bivalent classic-like perspective as applied to the wider domain of finite-valued truth-functional logics.
Our running example in this paper will involve Lukasiewicz's well-known 3-valued logic L 3 , characterized by the algebra of truth-values {1, 1 2 , 0}, {1}, {¬, →,∨, ∧} , where the interpretation of the unary negation connective ¬ sets
. The binary symbols ∨ and ∧ can be introduced as primitive interpreting them through (v
), but they can also more simply be introduced by definition just like in Classical Logic, setting
The binary print of an arbitrary atom of L 3 and of its negation is illustrated in the table below.
Given some finite-valued logic L based on a set of truth-values V, we say that L is functionally complete over V if any n-valued operation, for n = Card(V), may be defined with the help of a suitable combination of its primitive operators { c i j } j∈J . When L is not functionally complete from the start, we may consider L fc as any functionally complete n-valued conservative extension of L. Given truth-values v 1 , v 2 ∈ V, we say that they are separated, and we write v 1 v 2 , in case v 1 and v 2 belong to different classes of truth-values, that is, in case either v 1 ∈ D and v 2 ∈ U, or v 1 ∈ U and v 2 ∈ D. Given a unary, primitive or defined, connective of a given truth-functional logic, with interpretation , we say that separates v 1 and v 2 in case (v 1 ) (v 2 ). Obviously, for any pair of truth-values of L fc it is possible to find or to define in the corresponding term algebra an appropriate separating connective . When that separation can be done exclusively with the help of the original language of L, we say that V is effectively separable and the logic L, in that case, will be considered to be sufficiently expressive for our purposes. It should be noticed that the vast majority of the most well-known finite-valued logics enjoy this expressivity property.
Notice in particular, from Table 1, how the negation connective of L 3 separates the two undesignated truth-values. Based on Table 1, one may in fact easily provide a unique identification to each of the 3 initial algebraic truth-values, by way of the following statements:
One can also use this separating connective : λu.¬u in order to provide a bivalent description of each of the operators of the language. Consider for instance the cases of A : λvw.(v → w) and
From those tables it is clear for instance that:
Let's write T : ϕ and F : ϕ, respectively, as abbreviations for t( §(ϕ)) = T and t( §(ϕ)) = F . Then, the statement (II) may be described in bivalent form, with the help of (I), by writing:
In [2] an algorithm that constructively specifies a bivalent semantics for any sufficiently expressive finite-valued logic was proposed. The output of the algorithm is a computable class of clauses governing the behavior of all the bivaluations that together will define a notion of entailment that coincides with the original entailment defined with the help of the algebra of truth-values T V. Moreover, all those clauses are in a specific format we call gentzenian, namely, they are conditional expressions of the form (Φ ⇒ Ψ ) where both Φ and Ψ are (meta)formulas of the form (top), ⊥ (bottom) or a clause of the form b(ϕ
Here, w j i ∈ {T, F }, each ϕ j i is a formula of L, the symbol ⇒ represents implication (and ⇔ shall represent bi-implication, abbreviating the conjunction of two clauses of the form (G)), the symbol & represents conjunction, and | represents disjunction. The (meta)logic governing these clauses is fol, First-Order Classical Logic. One may alternatively represent a clause of the form (G) as 1≤k≤m 1≤s≤nm (b(ϕ s k ) = w s k ). With a slight notational change and using fol, one can see (III) as a description done in an abbreviated gentzenian format:
Following the above line of reasoning, it is also correct to write, for instance, the clause:
According to the reductive algorithm described in [2], a sound and complete bivalent version of any sufficiently expressive finite-valued logic L is obtained if: (i) the above illustrated procedure is iterated in order to obtain clauses describing exactly in which situation one may assert T : c i j (α 1 , . . . , α i ) and F : c i j (α 1 , . . . , α i ), as well as T : c i j (α 1 , . . . , α i ) and F : c i j (α 1 , . . . , α i ), for each c i k ∈ Cct and each one of the separating connectives of L; (ii) to all those clauses one adds the following extra axioms governing the behavior of the admissible collection of bivaluations:
(C1)
mn : mn (α) for every α ∈ S, where mn is the unary (primitive or defined) connective that we use to separate the truth-values m and n, and w v mn = t( mn (v)).
Generic tableau systems for finite-valued logics are known at least since [3]. In the corresponding tableaux, however, formulas may receive as many labels as the number of truth-values in V, and that somewhat obstructs the task of comparing for instance the associated notions of proof and of consequence relation to the corresponding classical notions. But with the help of the bivalent semantics illustrated in the previous section it is now straightforward to produce sound and complete collections of classic-like two-signed tableau rules (i.e., each formula appears with exactly one of two labels at the head of each rule).
The basic idea, explained in [2], is to dispose the gentzenian clauses governing the admissible bivaluations in an appropriate way. For that matter, clauses such as (IV) and (V) can be rendered, respectively, as the following tableau rules:
(IV) tab T : ¬(α → β)
To those rules corresponding to the truth-tables of the operators and the separating connectives, one should also add rules corresponding to the extra axioms (C1)-(C4). In practical cases, however, axioms (C3) and (C4) can often be proven from the remaining ones. Moreover, axiom (C2) expresses just the usual closure condition on tableau branches. On the other hand, axiom (C1) gives rise in general to the following 'dual-cut' branching rule, for arbitrary α:
All other definitions and concepts concerning the construction of tableaux are standard (check [6]).
One might be worried, with good reason, that the unrestrained use of the branching rule may potentially make the corresponding tableaux non-analytic. We will discuss that in the conclusion. The tableau rules originated from the above procedure can naturally be used in order to prove theorems, check conjectures and suggest counter-models, but also, in the meta-theory, to formulate and prove derived rules that can be used to simplify the original presentation of the logic as originated by our algorithm. So, for instance, the above illustrated complex three-branching rule for F : (α → β) can eventually be simplified into one of the following equivalent two-branching rules:
We used the functional programming language ML to automate the axiom extraction process. ML provides us, among other advantages, with an elegant and suggestive syntax, and a very handy compile-time type checking and type inference that guarantees that we never run into unexpected run-time problems with our program, once it is proved correct with respect to the specification. The relevant inputs of our program include the detailed definition of a finitevalued logic, such as the logic L 3 presented in the previous sections, together with an appropriate set of separating connectives for that logic.
Here's an example of a input for the logic L 3 , presented above, where the functions CSym, CAri and CTab take a connective and return its symbol (for printing), arity and truth-table, respectively. A truth-table of a given connective c is represented as the list of all pairs ([x 1 , . . . , x n ], y) such that c (x 1 , . . . , x n ) = y. In this theory, consts lists the formula constructors. TR :: "a => o" means that the constructor TR takes a formula (typed a) and returns a signed formula (typed o). We also extract from the logic received as input each constructor's name to use as syntactic sugar, as well as its associativity rules and priority order.
In the generated axioms corresponding to the tableau rules, T:X and F:X are (signed) formulas, $H and $E are sequences of such formulas (contexts) that are not directly involved in the rule, each sequence between square brackets represents a tableau branch, and a collection of branches is delimited by [| and |]. The symbol ==> denotes Isabelle's meta-implication. In Isabelle, the application of a rule means that is possible to achieve the goal (sequence on the right of the meta-implication) once it's possible to prove the hypotheses (sequences on the left of the meta-implication), which constitute the collection of new subgoals at each step. The branching rule corresponds to axiom axC1, and the closure rule for a branch of the tableau corresponds to the axioms axC21 and axC22.
Note for instance that ax5 corresponds to rule (V) tab from the last section. The simpler rule (V * * ) tab , mentioned in the same section, can of course be written in Isabelle as:
The proof that ax5 and ax5S are indeed equivalent tableau rules, i.e., that one can derive one from the other in the presence of the remaining rules of our theory, can now be done directly with the help of Isabelle's meta-logic. One might notice that, while in [3] the number of rules for each given primitive connective is exponential in its arity, here the number of rules for each such connective is always polynomial both in the arity and in the number of separating connectives of the input logic. The worst-case number of nodes involved in each tableau rule, however, using our algorithm, is exponential in the arity of the corresponding connective. Using Isabelle's meta-logic to prove simplifications such as the one illustrated above, for the case of rule (V), the number of nodes involved in each tableau rule may be substantially reduced.
The present note has reported on the first concrete implementation of a certain constructive procedure for obtaining adequate two-signed tableau systems for a large number of finite-valued logics. Expressing a variety of logics in the same framework is quite useful for the development of comparisons between such logics, including their expressive and deductive powers.
There still remains some room for improvement and extension of both our algorithm (which should still, for instance, be upgraded in order to deal in general with first-order truth-functional logics) and its implementation. By way of an example, we have assumed from the start that the logics received as inputs to our program came together with a suitable collection of separating connectives. This second input, however, could be dispensed with, as the set of all definable unary connectives can in fact be automatically generated in finite time from any given initial set of operators of the input logic. That generation, however, may be costly for logics with a large number of truth-values and is not as yet performed by our system. Another direction that must be better explored, from the theoretical perspective, concerns the conditions for the admissibility or at least for the explicit control of the application of the dual-cut branching rule. On the one hand, the elimination of dual-cut has an obvious favorable effect on the definition of completely automated theorem-proving tacticals for our logics. If that result cannot be obtained in general but if we can at least guarantee, on the other hand, that this branching rule will never be needed, in each case, for more than a finite number of known formulas -say, the ones related to the original goal as constituting its subformulas or being the result of applying the separating connectives to its subformulas-then again this will make it possible to devise tacticals for obtaining fully automated derivations using the above described tableaux for our finite-valued logics.
val CTab fun CTab Neg = [ (["0"], "1"), (["1/2"], "1/2"), (["1"], "0") ] | CTab Imp = [ (["0", "0"], "1"), (["0", "1/2"], "1"), (["0", "1"], "1"), (["1/2", "0"], "1/2"), (...) (["1", "1"], "1") ] end;
To perform the extraction, our program first generates a list of all necessary rules, as explained in section 2.
Next, the program converts each connective's truth-table, here given by the function CTab, into a table where each value is exchanged by its binary print. The binary print of a value is calculated based on the separating connectives given as input (SeparatingD for designated values and SeparatingND for undesignated values). For instance, for the case of the connective Neg, the clauses are the following:
Now, for each formula in the list of rules, a search is performed through all tables generated in the latter step, and all clauses in which the given formula appears on the right hand side are returned. The left hand side of these clauses represents the branches of the desired tableau rule. For instance, the rules for T:~A and F:~A are:
The next steps include the calculus of axioms (C3) and (C4), and the printing of all definitions, concrete syntax and rules into a text file containing the full theory ready to use in Isabelle. Isabelle, also written in ML, is a generic theorem-proving environment based on a higher-order meta-logic in which it is quite simple to create theories with rules and axioms for various kinds of deductive formalisms, and equally straightforward to define tacticals for the automation of routine tasks and to prove theorems about these systems.
For the case of L 3 , here is the corresponding theory produced as output by our program: