Refutation in Dummett Logic Using a Sign to Express the Truth at the Next Possible World

1 Introduction

In this paper we present a tableau calculus and theorem prover for propositional Dummett logic. By exploiting the linearly ordered Kripke semantics of Dummett logic, we devise a tableau calculus working on two semantical levels: the present and the next possible world. In this way we can guarantee that as the construction of the tableau proceeds, moving from a world to another, the known (forced) information strictly increases. Moreover, the calculus can be equipped with specialized rules to reduce the branching. As a result, the decision procedure is speeded up.

Dummett logic has been extensively investigated both by people working in computer science and in logic. The history of this logic starts with G¨odel, who studied the family of logics semantically characterizable by a sequence of nvalued (n > 2) matrices [G¨odel, 1986]. In paper [Dummett, 1959] Dummett studied the logic semantically characterized by an infinite valued matrix which is included in the family of logics studied by G¨odel and proved that such a logic is axiomatizable by adding to any Hilbert system for propositional intuitionistic logic the axiom scheme (p → q) ∨ (q → p). Moreover, it is well-known that such a logic is semantically characterizable by linearly ordered Kripke models. Dummett logic has been extensively studied also in recent years for its relationships with computer science [Avron, 1991] and fuzzy logics [Hajek, 1998]. For a survey in proof theory in G¨odelDummett logics we quote [Baaz et al., 2003].

To perform automated deduction both tableau and sequent calculi have been proposed. Paper [Avellone et al., 1999] provides tableau calculi whose distinguishing feature is a multiple premise rule for implicative formulas that are notforced. The syntactical way to express this semantical meaning is by the sign F. We recall that the sign F comes from Smullyan [Smullyan, 1968; Fitting, 1969] and labels those formulas that in a sequent calculus occur in the right-hand side of ⇒. A tableau calculus derived from those of [Avellone et al., 1999] is provided in paper [Fiorino, 2001]. Its main feature is that the depth of every deduction is linearly bounded in the length of the formula to be proved. Hypersequent systems for the implicative fragment of propositional Dummett logic are provided in [Metcalfe et al., 2003].

The approach of [Avellone et al., 1999], based on characterizing Dummett logic by means of the multiple premise rule, has been criticized because, from the perspective of worst case analysis, there are simple examples of sets of formulas giving rise to a factorial number of branches in the number of formulas in the set. Paper [Avron and Konikowska, 2001] shows how to get rid of the multiple premise rule. New rules are provided whose correctness is strictly related to the semantics of Dummett logic. These ideas have been further developed and in paper [Larchey-Wendling, 2007] a graphtheoretic decision procedure is described and implemented. The approach introduced in [Avron and Konikowska, 2001] has also disadvantages with respect to the multiple premise rule proposed in [Avellone et al., 1999] and these disadvantages have been considered in [Fiorino, 2010], where also a new version of the multiple premise rule is proposed. This version, from a practical point of view, can reduce the branching when compared with the original one. Paper [Fiorino, 2010] also provides an implementation that outperforms the one of [Larchey-Wendling, 2007], thus proving that the approach based on the multiple premise rule of [Avellone et al., 1999] deserves attention also from the practical point of view. As a matter of fact, on the one hand the rules of [Avron and Konikowska, 2001] give rise to two branches at most, on the other hand there are cases of formulas that multiple premise calculi decide with a number of steps lower than the calculi based on [Avron and Konikowska, 2001].

In this paper we continue our investigation around multiple premise calculi for Dummett logic. The tool we use to prove our results is the characterization of Dummett logic via linearly ordered Kripke models, whose elements are considered worlds ordered w.r.t. ≤ and α ≤ β means that, roughly speaking, β is in a subsequent point of the time w.r.t. α.

With the aim to reduce the size of the proofs, we provide a calculus whose main feature is the way the non-forced formulas are handled. In tableau calculi proofs start by supposing that at the present world A is not forced. A proof of our calculus starts by adding a further semantical constraint, namely, by supposing that the present world is the last where A is not forced. This further constraint implies that in the present we have information about a different semantical status of A in the future: if we conclude that there exists the next world, then we deduce that in such a future world A is forced (this implies that starting from such a next world, A is equivalent to ⊤). Such information can be handled to draw deductions about the semantical status of the formulas both in the present and in the next world (hereafter, when is clear from the context, we omit "world" after "present" and and "future"). As a consequence, our calculus handles two kinds of signed formulas: the first kind describes the semantical status of a formula at the present, the second kind describes the semantical status of a formula at the next world. The introduction of the signs related to the future allows to introduce specialized rules that exploit the knowledge about the future to draw deductions about the present. In particular, we refer to the introduction of specialized and single conclusion rules to handle the formulas of the kind F(A → B) (to be read "at the present world the fact A → B is not known"), thus reducing the branching generated by the multiple premise rule.

The semantical constraint used in calculus has also the advantage to change the effect of the application of the noninvertible rules. Roughly speaking, non-invertible rules draw conclusions about the next world having as premise facts about the present. The application of these rules has an effect in the proof-search, usually requiring the introduction of backtracking to guarantee the completeness of the proofsearch procedure. The semantical effect is that in the construction of the counter model a new state of knowledge is added, corresponding to the facts derived by the noninvertible rule. In the known sequent/tableau calculi for intermediate logics there is no guarantee that in the conclusion of the non-invertible rules at least one fact that in the premise was explicitly unknown becomes explicitly known in the conclusion. In the semantical construction this means that there is no guarantee that between two subsequent worlds, knowledge increases. The two semantical levels used in our calculus allow us to provide non-invertible rules such that there is at least one fact that in the premise is explicitly signed as not known and in the conclusion is explicitly signed as known. This implies that moving from the present to the next state of knowledge there is at least one explicitly unknown fact of the present that becomes explicitly known in the future. This has also a correspondence in the construction of the Kripke counter model, where there are no two elements exactly forcing the same propositional variables. The knowledge that a formula A is equivalent to ⊤ can be exploited to replace all the occurrences of A with ⊤. Such a replacement reduces the size of the set to be decided. Further reductions are possible by applying replacements based on the truth table of the connectives. Rules based on the replacement have been proved effective to dramatically reduce the search space both in classical and intuitionistic logic [Avellone et al., 2008; Massacci, 1998]. The idea of reasoning on two states of knowledge can be used also in other intermediate logics. As an example it can be used to develop a loop-free analytic calculus for propositional intuitionistic logic.

2 Basic definitions, the calculus and general considerations

We consider the propositional language based on a denumerable set of propositional variables PV, the boolean constants ⊤ and ⊥ and the logical connectives ¬, ∧, ∨,→. We call atoms the elements of PV ∪{⊤, ⊥}. In the following, formulas (respectively set of formulas and propositional variables) are denoted by letters A, B, C. . . (respectively S, T , U,. . . and p, q, r,. . . ) possibly with subscripts or superscripts.

From the introduction we recall that Dummett Logic (Dum) can be axiomatized by adding to any axiom system for propositional intuitionistic logic the axiom scheme (p → q) ∨ (q → p) and a well-known semantical characterization of Dum is by linearly ordered Kripke models. In the paper model means a linearly ordered Kripke model, namely a structure K = 〈P,≤,ρ,⊩〉, where 〈P, ≤, ρ〉 is a linearly ordered set with ρ minimum with respect to ≤ and ⊩ is the forcing relation, a binary relation on P × (PV ∪ {⊤,⊥}) such that: (i) if α ⊩ p and α ≤ β, then β ⊩ p; (ii) for every α ∈ P , α ⊩ ⊤ holds and α ⊩ ⊥ does not hold. Hereafter we denote the members of P by means of lowercase letters of the Greek alphabet.

The forcing relation is extended in a standard way to arbitrary formulas of our language as follows:

1. α ⊩ A∧B iff α ⊩ A and α ⊩ B;
2. α ⊩ A∨B iff α ⊩ A or α ⊩ B;
3. α ⊩ A → B iff, for every β ∈ P such that α ≤ β, β ⊩ A implies β ⊩ B;
4. α ⊩ ¬A iff for every β ∈ P such that α ≤ β, β ⊩ A does not hold.

We write α ⊮ A when α ⊩ A does not hold. It is easy to prove that for every formula A the persistence property holds: If α ⊩ A and α ≤ β, then β ⊩ A. We say that β is immediate successor of α iff α < β and there is no γ ∈ P such that α < γ < β. A formula A is valid in a model K = 〈P,≤,ρ,⊩〉 if and only if ρ ⊩ A. It is well-known that Dum coincides with the set of formulas valid in all models.

The rules of our calculus D are in Figure 1 and 2. The calculus D works on signed formulas, that is well-formed formulas prefixed with one of the signs T (with TA to be read "the fact A is known at the present world"), F (with FA to be read "the fact A is not known at the present"), Fl (with FlA to be read "this is the last world where A is not known") and Fn (with FnA to be read "A is not known at the next world"), and on sets of signed formulas (hereafter we omit the word "signed" in front of "formula" in all the contexts where no confusion arises). Formally, the meaning of the signs is provided by the relation realizability (✄) defined as follows: Let K = 〈P,≤,ρ,⊩〉 be a model, let α ∈ P, let H be a signed formula and let S be a set of signed formulas. We say that α realizes H (respectively α realizes S and K realizes S), and we write α ✄ H (respectively α ✄ S and K ✄ S), if the following conditions hold:

1. α✄TA iff α ⊩ A;
2. α✄FA iff α ⊮ A;
3. α ✄FnA iff there exists β > α such that β ✄FA;

4. α ✄ FlA iff α ✄ FA and for every β > α, β ✄ TA;

5. α✄S iff α realizes every formula in S;

Before to enter into technical details, let us justify the introduction of the signs Fl and Fn in the object language by means of a motivating case. Let us suppose that a world α of a model K realizes SF→ = {F(A1 → B1), . . . , F(An → Bn)}. Then there exists the last element β ≥ α such that β ✄TAj , FBj , SF→ \ {F(Aj → Bj )}. Without loss of generality we let j = 1. Analogously, there exists an element γ ≥ β such that γ ✄ TAi,FBi,TA1, SF→ \ {F(A1 → B1), F(Ai → Bi)}. Without loss of generality we let i = 2. Now, β < γ or β = γ. If β < γ, then, since β is last element where FB1 holds, it follows that γ ✄ TB1 holds. If β = γ, then β is the last element where both B1 and B2 are not forced. The example shows that we can give a rule (F →) taking into account that if α✄F(Ai → Bi), for i = 1, . . . , n, then the set {TAi, FBi} is realized in θ ∈ {α, β} and for every world γ > θ, γ ✄TBi holds. The sign Fl aims to codify such a semantical property of Bi.

Generalizing the case given above, let SF→ = {F(A1 → B1), . . . ,F(An → Bn)} and let S be a set of formulas. Let us suppose that α ✄ S, SF→. Then, for i = 1, . . . , n, let us consider the element βi such that βi✄TAi, FBi and for every γ > βi, γ✄TAi, TBi. Thus βi is the maximum element such that βi ✄TAi, FBi. Since α✄F(Ai → Bi), such an element βi exists. Let βj = min{β1, . . . , βn}, with j ∈ {1, . . . , n}. There are two cases: (i) βj = α, then we conclude that β realizes the set S, TAj , FlBj , SF→ \ {F(Aj → Bj)}; (ii) βj > α, then βj realizes the set Sc,TAj,FlBj, SF→ \ {F(Aj → Bj)}, where, by the meaning of the signs, Sc consists of: (i) the formulas of S signed with T; (ii) the formulas TA such that FlA ∈ S.

With the aim of reducing the size of the proofs, we add further considerations justifying the introduction of the sign Fn. Let us suppose that beside α ✄ S, SF→ we also know that for every model β1, . . . , βj-1 > βj holds. This rules out that βj ✄TAi,FlBi, for i = 1, . . . , j - 1, and implies that there exists an element γ such that βj < γ and γ ✄ F(Ai → Bi). The sign Fn aims to codify that the formulas F(Ai → Bi) have the following semantical property: there exists an element γ such that βj < γ and γ ✄F(Ai → Bi), thus the element βj is not the maximum element realizing F(Ai →Bi). By the meaning of Fn it follows that βj ✄ Sc,Fn(A1 → B1), . . . , Fn(Aj-1 → Bj-1), TAj , FBj , SF→ \ {F(A1 → B1), . . . ,F(Aj-1 → Bj-1)}. These are the intuitions justifying the rules Fn and F →. In particular the aim of F → is to distinguish if the last element realizing F(A → B) is the same element α realizing the premise or an element β such that α < β. The rule Fn handles the formulas of the kind FnA. For every formula there exists a world β such that α < β and β is the last element such that β ⊮ A. The minimum of such β does not force any formula in evidence in the premise.

The intuition behind the rule Fn can be explained as follows. Let us suppose that α✄S, FnA1, . . . , FnAu. Thus there exists βi such that α < βi and βi ✄FlAi, for i = 1, . . . , u. We notice that βi realizes all the T formulas in S and βi✄TC if FlC ∈ S. Moreover, if β1 = min{β1, . . . , βu}, then β1 ✄ FlA1,FA2, . . . ,FAu. If β2 is the minimum and we know that there is no model realizing α✄S, FnA1, . . . , FnAu having β1 as the minimum, then, since β2 < β1 holds, we conclude that β2 ✄ FnA1,FlA2,FA3, . . . ,FAu. Analogously, if βi is the minimum and we know that there is no model realizing α ✄ S, FnA1, . . . , FnAu having β1,. . . or βi-1 as the minimum, then, since βi < β1, . . . , βi-1 holds, we conclude that βi ✄FnA1,. . . ,FnAi-1,FlAi,FAi+1,. . . ,FAu.

From the meaning of the signs we get the conditions that make a set of formulas inconsistent. A set S is inconsistent if one of the following conditions holds:

-{TA, FA} ⊆ S; -{TA, FlA} ⊆ S; -{TA, FnA} ⊆ S;

-{FlA, FnA} ⊆ S; -{FnA, Fl¬B} ⊆ S;

-{FnA, Fl⊥} ⊆ S.

We emphasize that inconsistency conditions involving Fn are related to the existence of a future world α and in such a α the other formula of the pair is not realizable. Moreover the case {FnA,FlA} ⊆ S is redundant since it is subsumed by {TA, FA} ⊆ S. It is easy to prove the following

Proposition 1. If a set of formulas S is inconsistent, then for every Kripke model K = 〈P,≤,ρ,⊩〉 and for every α ∈ P, α ⋫ S.

Proof. We only consider the case {FnA,Fl¬B} ⊆ S. By absurd, let us suppose that α✄S, then α✄Fl¬B and α✄FnA. Since α ✄ FnA, there exists β ∈ P such that α < β. By definition of Fl, it follows that α ⊮ ¬B and for every β ∈ P , if α < β, then β ⊩ ¬B. Note that such a β exists. Since K is a linearly ordered Kripke model, by definition of negation it follows that α ⊩ ¬B. Thus we have that α ⊮ ¬B and α ⊩ ¬B, absurd. The other cases are easy to prove.

A proof table (or proof tree) for S is a tree, rooted in S and obtained by the subsequent instantiation of the rules of the calculus. The premise of the rules are instantiated in a duplication-free style: in the application of the rules we always consider that the formulas in evidence in the premise are not in S. We say that a rule R applies to a set U when it is possible to instantiate the premise of R with the set U and we say that a rule R applies to a formula H ∈ U (respectively the set {H1, . . . ,Hn} ⊆ U) to mean that it is possible to instantiate the premise of R taking S as U \ {H} (respectively U \ {H1, . . . ,Hn}).

A closed proof table is a proof table whose leaves are all inconsistent sets. A closed proof table is a proof of the calculus and a formula A is provable iff there exists a closed proof table for {FlA}. Note that deductions in our proof system start with a formula signed with Fl. This corresponds to suppose that there exists the last element of a Kripke model where A is not forced. In the tableau systems the deduction starts with FA, that corresponds to suppose that there exists an element, not necessarily the last, of a Kripke model such that A is not forced. We refer to [H¨ahnle, 2001] for full details on tableaux systems.

Figure 1: The invertible rules of D.

Figure 3: Optmization rules

3 Correctness, completeness and termination

To obtain the correctness of D with respect to Dummett logic, we proceed by showing that the existence of a proof table for {FlA}, implies the validity of A in Dummett logic. The main step consists in establishing that the rules of the calculus preserve realizability:

Proposition 2. For every rule of D, if a model realizes the premise, then there exists a model realizing at least one of the conclusions.

The correctness of rule Fn proceeds following the considerations given in previous section to justify the introduction of Fn and is similar to the proof given in [Avellone et al., 1999]. Some other cases are given in [Fiorino, ]. We emphasize that rule T¬¬-Atom is correct also when A is not an atom.

Theorem 1. If there exists a closed proof table for A, then A is valid in Dum.

Proof. By hypothesis there exists a proof table starting from {FlA} whose leaves are all inconsistent sets. An inconsistent set is not realizable and the rules of D preserve the realizability, thus FlA is not realizable. By absurd, let us suppose that there exist a model K = 〈P,≤,ρ,⊩〉 and a world α ∈ P such that α ⊮ A. Then, there exists β ∈ P s.t. α ≤ β, β ⊮ A and for every γ ∈ P s.t β < γ, γ ⊩ A holds. Thus β ✄ FlA and, since the rules of D preserve the realizability, the leaves of the proof table are realized, which is impossible. We conclude that that for every model K = 〈P,≤,ρ,⊩〉 and every α ∈ P , α ⊩ A, that is A is valid in Dum.

As regard the completeness, the calculus contains two noninvertible rules. It is possible to devise a complete strategy that relies on respecting a particular sequence in the application of the rules: T¬¬-Atom is applied if no other rule is applicable and Fn is applied if no other rule but T¬¬-Atom is applicable. We remark that Fn-formulas are introduced by rule F →, thus their main connective is the implication. Rules Fn and T¬¬-Atom apart, the other rules of D are invertible, thus they are applicable at any point of the deduction without affecting the completeness. We conclude that it is possible to devise a decision procedure based on D where no backtracking step is necessary (see [Fiorino, ] for the details).

By inspecting the rules of the calculus it follows that the procedure terminates. In particular the rightmost conclusion of the rule F → only change the sign of the formula in evidence in the premise, but we remark that the rule Fn handles these kind of formulas, thus the combined action of F →, Fn and Fl → allows us to prove that there is no an infinite loop due to the handling F →-formulas. Moreover, by the structure of the rules T¬¬∧, T¬¬∨, T¬¬ → and T¬¬¬, it follows that rules F¬ and T¬ → do not cause an infinite loop. Finally, if we split the rules F¬ and T¬ → in different cases according to A, by following [Fiorino, 2001] we can prove that the depth of every proof table of D is linear in the size of the formula to be proved.

4 Optimization rules and implementation

Additional rules can be introduced to D. Although unnecessary for completeness, in practice, they can be useful to reduce the search space. We discuss them in the following. The aim of the sign Fl is to label those formulas that after an application of Fn become equivalent to ⊤. As a matter of fact, after an application of the rule Fn, the formulas signed with Fl become signed with T, thus they are equivalent to ⊤. Hence the rule ReplaceT of Fig. 3 is applicable. The occurrences of ⊤ are removed by using the well-known boolean simplification rules [Fiorino, ;

Massacci, 1998]. The rule Replace T and the boolean simplification rules are examples of optimization rules allowing in many circumstances the reduction of search space. Another example is the rule ReplaceFl, that exploits the meaning of Fl and Fn to perform a replacement: if α✄FnA, FlB holds, then we conclude β ✄ FA, TB, with β immediate successor of α. Thus β ✄ FA[B/⊤] and α ✄ FA[B/⊤] hold. Compared with the calculus in paper [Fiorino, 2010], introducing the sign Fl has a price: proof tables can be wider, because of the combined action of F → and Fn. To reduce this problem there is the rule F →1, which is not necessary to the completeness and represents another example of optimization rule that exploits the information conveyed by the Fl-formulas. To better exploit Fl-formulas, D can be extended with the sign Tn: Let K = 〈P,≤,ρ,⊩〉 be a model and let α ∈ P , α✄TnA holds iff for every β > α, β ✄ TA. Given a set S, a further inconsistent condition is {FnA,Tn⊥} ⊆ S. The sign Tn makes explicit the semantical status of Fl-formulas in the next worlds. It is a derived sign and to get the completeness it is not necessary to provide rules to handle Tn-formulas. The sign Tn allows to draw conclusions about the next world, as an example:

Note that ReplaceTn-dup and ReplaceFl-dup copy the premise TA, thus loop-free mechanisms need to be implemented.

We have developed a prolog prototype based on the extension of D as described above, where to avoid infinite loops in the application of Replace Fl-dup and Replace Tn-dup a special labelling on the copied formulas is implemented. In Fig. 4 the implementations LC-cmodels [Larchey-Wendling, 2007], EPDL [Fiorino, 2010] and our prototype, called Dum-prover, are compared on the formulas of ILTP library [Raths et al., 2007]. We see that on many formulas Dum-prover outperforms EPDL. As regard family formulas SYJ202, the pigeon principle, the two provers produce the same proof.

5 Conclusions and future work

We have presented a calulus based on the idea that to prove a given formula A, the refutation starts by supposing that there exists the last world where A is not forced. The consequence of this semantical assumption is a calculus having rules that draw deductions about the (immediate) future and rules exploiting the information about facts known in the future to deduce information about the present. We have also developed the prolog prototype Dum-prover whose timings outperforms EPDL and LC-cmodels and show that the calculus is suitable to perform practical automated deduction in propositional Dummett logic. As regard to possible extensions, we plan to modify D to be able to decide n-valued G¨odel logics by bounding the number of applications of non-invertible rules inside proof-search branches. Finally, by exploiting the semantics of the sign Fl, we are working to develop a loopfree tableau calculus for propositional Dummett logic having the subformula property.