We introduce prefixed tableau systems for many-valued model logics (MVMLs). Semantically, we follow Fitting [ 1, 2] in allowing both the truth values of propositional variables at states as well as relational links between states in many-valued Kripke frames to take values in an arbitrary, finite Heyting algebra. Fitting [ 3] introduced tableau systems for these logics which, however, are not amenable to specialization to the MVMLs of certain frame classes, e.g. generalized symmetric frames. We overcome this dificulty through the use of prefixes which keep explicit track of the many-valued accessibility relation constructed on each branch. We prove soundness and completeness of the systems for the MVMLs of the classes of all many-valued frames and all generalized symmetric many-valued frames. We prove that these systems provide decision procedures and discuss and demonstrate their implementations. Further we derive the finite model property for the two logics under consideration.
via generalized Kripke models, in which both propositions and accessibility relations take on values from an arbitrary finite Heyting algebra ℋ. A study of the proof theory of these logics was initiated by Fitting himself when they were first introduced. Specifically, [ 2] gives a Gentzen sequent calculus for Kℋ – the ℋ-valued analogue of the basic modal logic K. Koutras et al. [19] introduce ℋ-frame generalizations of standard Kripke frame properties such as seriality, reflexivity, symmetry and transitivity. These generalized frame properties are parameterized by an arbitrary ℋ-value , and for a given , they define the logics Dℋ, Tℋ, KBℋ and K4ℋ – the ℋ-valued analogs of the basic modal logics D, T, KB and K4 respectively. They then go on to extend
a cut rule. In [3], Fitting defines a cut-free semantic tableau system for Kℋ. Extending this system to cut-free tableau systems for Tℋ, KBℋ and K4ℋ, parameterized by some ℋ-value , is relatively straightforward, and is done by the corresponding author in their master’s thesis. However, KBℋ requires that we introduce prefixes to our tableaux. And, the resulting prefixed systems lend themselves naturally to defining decision procedures.
We now briefly survey some related work. In [ 20], Priest introduces tableau systems (as well as nice philosophical applications) for certain four and three-valued crisp modal logics. His tableau system is a prefixed one, which, along with the prefixed systems defined in [ 21], provide the underlying inspiration for the prefixed system presented in this work. More recently, [ 22] presents what essentially amounts to a prefixed tableau system for a fuzzy version of Halpern and Shoham’s Interval Temporal Logic. In [23, 24], a broad basis for the study of MVMLs based on finite residuated lattices is established, thus generalizing Fitting’s work. Since then, there has been much work on the axiomatizibility and decidability of various MVMLs.
of this recent work shifts focus from Fitting’s finite valued Heyting semantics to more fuzzy, real valued semantics. The works most closely related to what we present here are [27, 28, 29], in that they focus on Fitting’s framework. [27] provides a cut-free sequent calculus for Kℋ, and as such, is essentially the first work to provide a decidability result for this logic. [28] and [29] study tableaux for the crisp versions of the logics we consider here. In particular, [28] provides prefixed tableau systems for such crisp logics with very general modalities. It is not entirely clear how to adapt that work to the non-crisp setting, and the present paper may be viewed as a step in that direction. Also very worth noting is the possibility of translating the logics we deal with to appropriate first order many-valued logics. Questions regarding decision procedures for these logics were studied by Hähnle [30, 31].
The paper is structured as follows. In Section 2 we provide the relevant background. Section 3 defines (prefixed) tableaux and presents the system Kℋ. We go on to prove that Kℋ is sound wrt the class of all ℋ-frames in Section 4. Section 5 proves the completeness of Kℋ by way of using the rules to construct a decision procedure for Kℋ. This also leads us to a finite model property for Kℋ. Finally, in Section 6, we modify Kℋ to obtain a prefixed tableau system (and resulting decision procedure and finite model property) for the logic KBℋ.
(also called pseudo-Boolean algebras) model the algebraic structure of intuitionistic logic (see [32]). For a detailed exposition of the theory of Heyting algebras and related topics, see [33]. One may approach defining
join), denoted by ∨ , and an infimum (or meet), denoted by ∧ . If there exists a least and greatest element of , then the lattice is said to be bounded. The greatest and least element of any bounded lattice shall be denoted by 0 and 1 respectively. For arbitrary ⊆ , we define ⋀︀ := inf and ⋁︀ := sup . In the case in which is finite, these objects always exist.
there exists a ∈ which is the greatest element of {′ ∈ | ∧ ′ ≤ }, or equivalently, ≤ if ∧ ≤ for every ∈ . Such a is unique, and we call it the pseudo-complement of relative to (and denote it by ⇒ ).
Example 2.2. The simplest, non-Boolean Heyting algebra is ℋ3 = ({0, ℎ, 1}, ≤ ), where ≤ is a total order.
Finite Heyting algebras will serve as the truth value spaces of our logics. The syntax and semantics of the logics we study are parameterized by the specific Heyting algebra we choose to act as the underlying truth value space. So, let us once and for all fix an arbitrary finite Heyting algebra ℋ = (, ≤ ). We continue to use ∧, ∨, ⇒ for the meet, join and relative pseudo-complement. We shall refer to elements of as ℋ-truth values2 and include in our language a set of propositional constant = { | ∈ }, one for each element of . Let us also fix some non-empty countable set Φ of propositional variables. The language for our MVML, which we denote by ℒℋ(Φ), consists of finite strings constructed from the alphabet ∪ Φ ∪ {∧, ∨, ⊃ , ♢ , □ , (, )}3. The set of ℋ-valued modal formulas (or simply ‘formulas’ from now on), denoted (ℒℋ(Φ)), is generated by the following grammar:
::= | | 1 ∧ 2 | 1 ∨ 2 | 1 ⊃ 2 | □ 1 | ♢ 1 where ranges over ℋ-truth value and over propositional variables (these are our atomic formulas). For ∈ (ℒℋ(Φ)), the modal degree, denoted ( ), is the number of occurrences of the symbols ♢ and □ in . Further, ( ) denotes the set of all subformulas of .
is a tuple F = (, ), where is a non-empty set of worlds (or states) and : × → is a function assigning ℋ-truth values to ordered pairs of worlds.
An ℋ-model is a structure M = ((, ), ), where F = (, ) is an ℋ-frame (we say that M is based on frame F) and is a valuation on Φ ∪ . By this, we mean that : × (Φ ∪ ) → is a function assigning ℋ-truth values to atomic formulas in each world, s.t. (s, ) = for all s ∈ and ∈ . That is, propositional constants are always mapped by a valuation to the ℋ-truth values that they represent.
Definition 2.3. Let M = ((, ), ) be an ℋ-model. The extension of , : × (ℒℋ(Φ)) → , is the unique function where for any s ∈ and , ∈ (ℒℋ(Φ)), we have • (s, ) = (s, ) for every ∈ Φ ∪ , • (s, ( ∧ )) = (s, ) ∧ (s, ), • (s, ( ∨ )) = (s, ) ∨ (s, ), • (s, ( ⊃ )) = (s, ) ⇒ (s, ), • (s, □ ) = ⋀︁{(s, v) ⇒ (v, ) | v ∈ }, • (s, ♢ ) = ⋁︁{(s, v) ∧ (v, ) | v ∈ }.
its extension. We say that is satisfied by M at s ∈ (denoted as M, s ⊩ ) if (s, ) = 1. Further, is globally satisfied by M (denoted as M ⊩ ) if (s, ) = 1 for every s ∈ . We say M is a counter model for if M ⊮ .
introduced reduces to the standard two-valued modal logic. In this standard case, it is clear that some of our 2We will often drop the ℋ and just speak of truth values. 3In line with Fitting’s presentation, we use ∧, ∨ to denote the meet and join operations in ℋ as well as symbols occurring in ℒℋ(Φ). Context should make it clear exactly which objects we are referring to. Further, the use of an underline for elements of will help diferentiate between syntactic and semantic objects. This, in turn, allows us to diferentiate between formulas such as ( ∧ ⊃ ) vs ( ∧ ⊃ ). This becomes important in some tableau rules, for example see rule (K □ ). connectives are redundant. However, in the general case, the connectives we have in our language are not interdefinable. As such, we need to explicitly include them.
and be two new formal symbols. A signed formula consists of a formula with either the symbol or prepended to it. Given some ℋ-model M = ((, ), ) and s ∈ , we shall say that a signed formula is satisfied by M at s if it is and M, s ⊩ ; or it is and M, s ⊮ .
Definition 2.4 (Validity). Let F = (, ) be an ℋ-frame and ∈ (ℒℋ(Φ)). We say that is valid in F (denoted as F ⊩ ) if for every ℋ-model M = (F, ) based on F, we have M ⊩ . Let ℱ be some class of ℋ-frames. is said to be valid in ℱ , or ℱ -valid (denoted as ℱ ⊩ ) if F ⊩ for all F ∈ ℱ . In the case where ℱ is the class of all ℋ-frames, we simply say that is valid. We define Λℱ to be { ∈ (ℒℋ) | ℱ ⊩ }, and call it the logic of ℱ .
We denote the logic of all ℋ-frames by Kℋ. In the context of standard modal logic, various other classes of frames have been characterized in terms of conditions on the two-valued accessibility relation and extensively studied. Classes of ℋ-frames which are characterized by many-valued generalizations of some of these conditions are defined in [ 19]. These conditions on the many-valued accessibility relation are parameterized by an arbitrary ℋ-truth value . In the case of ‘many-valued symmetry’, we say that an ℋ-frame (, ) is -symmetric if ∧ (s, v) = ∧ (v, s) for every s, v ∈ . Letting Symmℋ denote the class of all -symmetric ℋ-frames, we use KBℋ to denote4 ΛSymmℋ .
widely adapted to be used for various non-classical logics [31]. Fitting gives a detailed account of their use for standard modal logics in [21], and this particular text motivated much of the work in this paper.
of strings that can occur in the derivations in our system. First and foremost, we will make use of signed bounding implications, which, as the name suggests, provide a syntactic means by which we can ‘bound’ the value of a formula. More precisely, a formula is a bounding implication if it is of the form ⊃ or ⊃ for some ∈ and ∈ (ℒℋ(Φ)).
For a formula , it will also be useful to talk about the bounded subformulas of , which are the bounding implications of the form ⊃ or ⊃ , where ∈ and ∈ ( )5.
A signed bounding implication is simply a signed formula in which the formula is a bounding implication.
of the form ( ⊃ ), ( ⊃ ), ( ⊃ ) or ( ⊃ ). We shall use ⊥ as an abbreviation for (0 ⊃ 1).
shall be concerned with an object language in which elements of are augmented with prefixes . Fixing some countably infinite set of symbols Σ, a prefix is a tuple (, ), where ∈ Σ and ⊆ Σ × Σ × . A prefixed signed bounding implication is a string of the form (, ) , consisting of a prefix (, ) prepended to a signed bounding implication . We denote the set of all prefixed signed bounding implication by , and this will play the role of object language for what we call prefixed tableaux.
The system in [3] is in the tradition of Smullyan [36], and Fitting presents his (unprefixed) tableaux as trees where each node is labelled by a single element of . However, although not explicitly stated by Fitting, the destructive nature of his modal rules requires that, technically, tableaux are more abstract objects than trees. 4The names of the logics are in keeping with convention, as the definitions collapse to the standard case when = 1 and ℋ = 2. For instance, KB21 is the same as the standard modal logic KB of symmetric Kripke frames. The names in standard modal logic derive from the names for the axioms defining the frame properties. We are further justified in using these names since when we take these axioms to the ℋ-valued setting, the generalized frame properties are still defined by them. [ 34] gives a good account of why this is so. 5For any formula , the set of all bounded subformulas of has at most 2 × | | × | ( )| elements. Hence, since is finite, there is a finite number of bounded subformulas of .
We will use this abstract approach to define prefixed tableaux too. That is to say, the set of prefixed tableaux for some formula will be defined recursively as a subset of (()) that results from applying a finite sequence of permissible operations on some base tableau. The permissible operations are described via what we call tableau rules. A tableau rule = ( , (1, . . . , ), side condition) consists of a numerator , a ifnite list of denominators 1, . . . , , and a side condition. Schematically, is presented as follows. ( ) 1 . . .
side condition The numerator, denominators and side condition of a tableau rule are expressions of the metalanguage. They describe subsets of based on the membership of certain elements adhering to a particular syntactic form and syntactic conditions stated in the side condition. An instantiation of the numerator and denominator(s) of a rule are the sets that can result from a uniform substitution of sets, constants and formulas for metasymbols in the rule, s.t. the side condition is satisfied. As mentioned, the purpose of a tableau rule = ( , (1, . . . , ), side condition) is to describe a family of operations that can be applied to elements of (()). To be more precise, let : (()) → (()). We say is described by if for all ∈ (()), if ̸= ( ) then for some ∈ , is an instantiation of , ( ) contains 1, . . . which are corresponding instantiations of 1, . . . , respectively, and ∖ {} = ( ) ∖ {1, . . . , }.6 In most cases we will not make explicit reference to an operation described by a rule. If * = ( ) for some ∈ (()) and described by , we shall say that * was derived from through an application of . Sometimes, it will be useful to pick out the element of which acts as the instantiation of the numerator of the rule. So, if ∈ but ∈/ * , we may say was applied to to derive * .
and is defined recursively as follows.
• {} is a -tableau for • Suppose is a -tableau for . If * ∈ (()) can be derived from by applying some ∈ , then * is a -tableau for .
⊆ . We call the sets in a -tableau its branches7.
Given some set ∈ (), we shall say that is closed if (, ∅)⊥ ∈ for some ∈ Σ. Otherwise, we say that is open. A tableau is closed if all its branches are closed; otherwise it is open. We say that a formula is a theorem of if for some ∈ Σ, there exists a closed -tableau for {(, ∅) (1 ⊃ )}. In this case we also say that is provable in (denoted as ⊢ ), or that is a -proof of .
The unprefixed tableau systems introduced in [ 3] view the formulas in a branch as describing the valuation at a specific world of a hypothetical model. The application of certain ‘modal’ rules corresponds to a change in world with a concomitant loss of much of the information regarding the previous world. This ‘destructiveness’ makes basing a decision procedure upon this system dificult, and what is more, devising a system that is sound and complete wrt e.g. symmetric frames is impossible. To do the former would require a system of bookkeeping and backtracking. We now introduce “non-destructive” tableau systems with prefixes which take care of this bookkeeping naturally inside the system itself and ensure that we never have to backtrack. They do so by keeping track of all the worlds, past and present. For a prefix (, ), we think of ∈ Σ as denoting a world in an ℋ-frame, and call a world label. We think of (, , ) ∈ ⊆ Σ × Σ × as saying that the world denoted 6Note that the identity operation on (()) is described by every rule. 7The justification for this terminology will be made explicit in Section 5.1. by is accessible from the world denoted by to degree . We call (, , ) a constraint. We shall use the following convenient notation. For ∈ , ((, ) ) := ; ((, ) ) := ; ((, ) ) := ; and for a given set ⊆ , we let ( ) := ⋃︀∈ () and ( ) := {() | ∈ }.
Definition 3.2. Let be a subset of and let M = ((, ), ) be an ℋ-model. An interpretation of in M is any map : () → s.t. if (, , ) ∈ (), then is defined for and (i.e. , ∈ ()) and ( (), ()) = . We say is satisfied under if for each (, ) ∈ , it is the case that is satisfied by M at (). Further, let ℱ be a class of ℋ-frames. We say is ℱ -satisfiable if there exists an ℋ-model M based on a frame from ℱ , and an interpretation of in M s.t. is satisfied under .
We proceed to study a prefixed tableau system for Kℋ.
Kℋ :={⊥1, ⊥2, ⊥3, ⊥4, ⊥5, ≥ , ≥ , ≤ , ≤ , ∧, ∧, ∨, ∨,
⊃ , ⊃ , K □ , K ♢ , K □ , K ♢ } where these rules are defined below. Note that in all the rules, the entire numerator of the rule, denoted by , is carried to the denominator(s) of the rule. That is to say, all the rules extend branches, without deleting anything. While such extending rules are usually presented in the literature without placing the numerator in the denominator, we nonetheless do so here in keeping with our earlier abstract definition of tableau rules.
(⊥1) ; (, ) ( ⊃ )
; (, ∅)⊥ Where ≰ (⊥2) ; (, ) ( ⊃ )
; (, ∅)⊥ Where ≤ (⊥3) ; (, ) (0 ⊃ ) ; (, ∅)⊥ (⊥4) ; (, ) ( ⊃ 1) ; (, ∅)⊥ (⊥5) ; (, ) ( ⊃ ); (, ′) ( ⊃ )
; (, ∅)⊥ Where ≰ Where 1, . . . , are all the maximal ℋ-truth values not above , and ̸= 0.
Where 1, . . . , are all the minimal ℋ-truth values not below , and ̸= 1. ( ≥ ) ;;((,, ′))(( ⊃ ⊃ )) ( ≤ ) ; ;((,, ′))(( ⊃ ⊃ )) Where is any maximal ℋ-truth value not above , and ̸= 0.
Where is any minimal ℋ-truth value not below , and ̸= 1. 8In all the rules, the constraints introduced in the denominators extend ′ = ( ). We could just as well instead extend the of the numerator. However, the current approach is chosen as it makes the later termination result (Lemma 5.4) easier to prove.
Where ̸= 0.
Where ̸= 1. Where 1, . . . , are all the ℋ-truth values below except 0. ( ∧) ; (, ′);((, ⊃ ) (); (⊃,( ′∧) ())⊃ )
( ∧) ; (, ′);(( ⊃, )) ( ⊃ ;((∧, ′))) ( ⊃ ) ( ∨) ; (, ′);((, ⊃ )()(; (∨, )′)⊃ ( ) ⊃ ) ( ∨) ; (, ′);((⊃ , )) (( ∨; () ,⊃ ′)) ( ⊃ )
Where ̸= 0.
Where ̸= 1. ( ⊃ ) ; (, ′) ( ⊃ ) ; (, ) ( ⊃ ( ⊃ )) ; (, ′) ( ⊃ )
Where is any ℋ-truth value below except 0. (K □ ) ; (, ) ( ⊃ □ ) ; (, ′) ( ∧ ⊃ ) (K ♢ )
; (, ) (♢ ⊃ ) ; (, ′) ( ⊃ ⇒ ) Where is any member of Σ and any ℋ-truth value s.t. (, , ) ∈ ′.
Where is any member of Σ and any ℋ-truth value s.t.
(, , ) ∈ ′.
; (, ) ( ⊃ □ ) (K □ ) ; (, ′ ∪ {(, , 1)}) . . . ; (, ′ ∪ {(, , )})
( ∧ 1 ⊃ ) ( ∧ ⊃ ) Where is any symbol of Σ that is not in ( ), and 1, . . . , are all the ℋ-truth values s.t. ∧ ̸= 0.
; (, ) (♢ ⊃ ) (K ♢ ) ; (, ′ ∪ {(, , 1)}) . . . ; (, ′ ∪ {(, , )})
( ⊃ 1 ⇒ ) ( ⊃ ⇒ )
Where is any symbol of Σ that is not in ( ), and 1, . . . , are all the ℋ-truth values s.t. ⇒ ̸= 1.
ℱ -satisfiable. Consider some rule ∈ . We say preserves ℱ -satisfiability if for every -tableau , if is ℱ -satisfiable and * is a tableau that can be derived from via an application of , then * is ℱ -satisfiable.
Lemma 4.1. preserves ℱ -satisfiability for each ∈ Kℋ.
(the corresponding instantiation of) at least one of the denominators is ℱ -satisfiable.
M = ((, ), ) based on a frame from ℱ , and an interpretation of in M s.t. is satisfied under . We now need to consider each rule individually. We will do so for K □ ; leaving the other cases to the reader.
Case = K □ : Then = ; (, ) ( ⊃ □ ) and so ( ⊃ □ ) is satisefid by M at (). That is, ( (), ⊃ □ ) ̸= 1, or equivalently, ≰ ⋀︀{( (), s) ⇒ (s, ) | s ∈ }. Thus, for some s ∈ , we have ∧ ( (), s) ≰ (s, ). Suppose ( (), s) = ∈ . Let ∈ Σ be any symbol that is not already in ( ). We extend the interpretation to . Specifically, consider ′ := ∪ {(, s)}, which is an interpretation of = ; (, ( ) ∪ {(, , )}) ( ∧ ⊃ ) in M, and is satisfied under ′.
the abstract notion of a maximal-consistent set of prefixed formulas and use such sets to construct a (possibly infinite) canonical model 9. Rather, we do something that was not easily achieved with those systems. We use our prefixed system to describe a decision procedure that, given a formula , must produce a tableau proof for if one exists and, if one does not, will give us the information necessary to construct a counter model for .
just mentioned, a desired tableau for a non-valid formula is one that provides enough information to construct a counter model. This rough idea of ‘enough information’ is captured by the notion of downward saturation. For ⊆ . We define the relation := {((, ), ) ∈ Σ2 × | (, , ) ∈ ()}. Definition 5.1.
Let ⊆ . is said to be downward saturated if all of the following conditions hold: 1. If (, , ) ∈ () for some , ∈ Σ, ∈ , then , ∈ (). Further, is a partial function from ()2 to . 2. For each rule ∈ {⊥1, ⊥2, ⊥3, ⊥4, ⊥5}, is not an instantiation of the numerator of . 3. If (, ) ( ⊃ ( ∧ )) ∈ for some ∈ Σ, ⊆ Σ2 × and truth value ̸= 0, then we have (, ′) ( ⊃ ) ∈ and (, ′) ( ⊃ ) ∈ for some ′ ⊆ Σ2 × . 4. If (, ) ( ⊃ ( ∧ )) ∈ for some ∈ Σ, ⊆ Σ2 × and truth value ̸= 0, then we have (, ′) ( ⊃ ) ∈ or (, ′) ( ⊃ ) ∈ for some ′ ⊆ Σ2 × . 5. If (, ) (( ∨ ) ⊃ ) ∈ for some ∈ Σ, ⊆ Σ2 × and truth value ̸= 1, then we have (, ′) ( ⊃ ) ∈ and (, ′) ( ⊃ ) ∈ for some ′ ⊆ Σ2 × . 6. If (, ) (( ∨ ) ⊃ ) ∈ for some ∈ Σ, ⊆ Σ2 × and truth value ̸= 1, then we have (, ′) ( ⊃ ) ∈ or (, ′) ( ⊃ ) ∈ for some ′ ⊆ Σ2 × . 7. If (, ) ( ⊃ ( ⊃ )) ∈ for some ∈ Σ, ⊆ Σ2 × and truth value , then for some ∈ s.t.
≤ and ̸= 0, we have (, ′) ( ⊃ ) ∈ and (, ′) ( ⊃ ) ∈ for some ′ ⊆ Σ2 × . 8. If (, ) ( ⊃ ( ⊃ )) ∈ for some ∈ Σ, ⊆ Σ2 × and truth value , then for all ∈ s.t.
≤ and ̸= 0, we have (, ′) ( ⊃ ) ∈ or (, ′) ( ⊃ ) ∈ for some ′ ⊆ Σ2 × . 9. If (, ) ( ⊃ □ ) ∈ for some ∈ Σ, ⊆ Σ2 × and truth value , then for all ∈ Σ and ∈ s.t. (, , ) ∈ (), we have (, ′) ( ∧ ⊃ ) ∈ for some ′ ⊆ Σ2 × . 10. If (, ) (♢ ⊃ ) ∈ for some ∈ Σ, ⊆ Σ2 × and truth value , then for all ∈ Σ and ∈ s.t. (, , ) ∈ (), we have (, ′) ( ⊃ ⇒ ) ∈ for some ′ ⊆ Σ2 × . 11. If (, ) ( ⊃ □ ) ∈ for some ∈ Σ, ⊆ Σ2 × and truth value , then there exists some ∈ Σ and ∈ s.t. ∧ ̸= 0, (, , ) ∈ () and (, ′) ( ∧ ⊃ ) ∈ for some ′ ⊆ Σ2 × . 12. If (, ) (♢ ⊃ ) ∈ for some ∈ Σ, ⊆ Σ2 × and truth value , then there exists some ∈ Σ and ∈ s.t. ⇒ ̸= 1, (, , ) ∈ () and (, ′) ( ⊃ 1 ⇒ ) ∈ for some ′ ⊆ Σ2 × . 13. If (, ) ( ⊃ ) ∈ for some ∈ Σ, ⊆ Σ2 × and truth value ̸= 0; and has one of the following forms: (a propositional variable), ∨ or ♢ . Then, for some which is a maximal truth value not above , (, ′) ( ⊃ ) ∈ for some ′ ⊆ Σ2 × . 14. If (, ) ( ⊃ ) ∈ for some ∈ Σ, ⊆ Σ2 × and truth value ̸= 1; and has one of the following forms: (a propositional variable), ∧ , ⊃ or □ . Then, for some which is a minimal truth value not below , (, ′) ( ⊃ ) ∈ for some ′ ⊆ Σ2 × . 9See [37], in which this is done in the context of prefixed systems for standard modal logics. ℋ-frame (, ) where := () and for all Lemma 5.2. If ⊆ is downward saturated, then is satisfiable.
Proof. Suppose is downward saturated. Define the , ∈ , (, ) := {︃(, ) if (, ) defined
0 otherwise 15. If (, ) ( ⊃ ) ∈ for some ∈ Σ, ⊆ Σ2 × and truth value ; and has one of the following forms: ∨ or ♢ . Then, for all ∈ which are maximal truth values not above , (, ′) ( ⊃ ) ∈ for some ′ ⊆ Σ2 × . 16. If (, ) ( ⊃ ) ∈ for some ∈ Σ, ⊆ Σ2 × and truth value ; and has one of the following forms: ∧ , ⊃ or □ . Then, for all ∈ which are minimal truth values not below , (, ′) ( ⊃ ) ∈ for some ′ ⊆ Σ2 × .
∧, ∧, ∨, ∨, ⊃ , ⊃ , K □ , K ♢ , K □ and K ♢ respectively. Conditions (13) to (16) are in a sense restricted closure conditions for the reversal rules. Essentially, the restrictions reflect the fact that we will wish to block the indiscriminate application of reversal rules to branches so as to ensure the termination of a procedure that constructs tableaux (which we do in Section 5.1).
consider an ℋ-model M = ((, ), ) where is any valuation s.t. for every ∈ and propositional variable , ⋁︀{ ∈ | (, ) ( ⊃ ) ∈ for some ⊆ Σ2 × } ≤ (, ) ≤ ⋀︀{ ∈ | (, ) ( ⊃ ) ∈ for some ⊆ Σ2 × } 10. We call M an ℋ-model induced by11 .
( ) is the statement: For all ∈ Σ, ⊆ Σ2 × , ∈ and that bound by , if (, ) ∈ , then is satisfied by M at . For the base cases and inductive cases, we need to consider the sub-cases depending on the form of , which could be ( ⊃ ), ( ⊃ ), ( ⊃ ) or ( ⊃ ). Though there are many, each sub-case is quite routine, and we leave them to the reader.
the identity map : → . is an interpretation of in M. Suppose (, ) ∈ for some ∈ Σ and ⊂ Σ2 × , where ∈ . For some ∈ , must bound some formula by . But since ( ) holds, we can conclude that is satisfied by M at = (). Thus, is satisfied under . 5.1. Decision Procedure
either we have a closed tableau or a tableau in which a downward saturated branch exists. We use a labelled tree as the data structure representing the tableau. This is possible since, as apposed to the unprefixed systems of [3], none of our rules require us to discard elements in a branch. For us, a labeling of a tree T = (, ) is any function : → . A labeled tree is a pair (T, ) consisting of a tree and a labeling of that tree. For a branch B in T, we let (B) := ⋃︀{ ()}, where runs over the set of nodes in B.
to (T, ) (denoted (T,)) is simply the collection { (B)}∈ 12. We will say that a branch B of T is closed 10Such a must exist. For assuming the contrary, we must have some (, ) ( ⊃ ) ∈ and (, ′) ( ⊃ ) ∈ where ≰ .
But this implies that is an instantiation of the numerator of ⊥5, contradicting the fact that is downward saturated. 11Note that there may be multiple such models with distinct valuations. 12For an arbitrary labelled tree (T, ), (T,) is not necessarily a Kℋ-tableau, in the strict sense of Definition 3.1. However, the labeled trees that will crop up in our decision procedure will have the property that (T,) is in fact a Kℋ-tableau for { ()}, where is the root node of T (see Lemma 5.5). if (B) is closed. Otherwise, we say that B is open. We will say that (T, ) is closed if all the branches of
trees. Essentially, the following definition allows us to talk about ‘applying a rule to labelled tree (T, )’ as a shorthand for actually saying that we extend (T, ) s.t. the corresponding tableau is derivable via an application of to (T,). Suppose (T,) is a Kℋ-tableau. Let ∈ Kℋ, and suppose (*T,) is some Kℋ-tableau derived from (T,) via an application of . Then, any labeled tree (T* , * ) extending (T, ) for which (T* ,* ) = (*T,) can be said to have been derived via an application of to (T, ). Further, If
Require: formula 1: := (1 ⊃ ) 2: (T, ) := constructTableau( ) 3: if (T, ) is closed then return true, else return false constructTableau( ) returns a labelled tree (T, ) Require: ∈ 1: Initialize a labeled tree (T, ) with root node and () := (0, ∅) ◁ Pick any 0 ∈ Σ 2: Mark as being unfinished ◁ From now on we will assume that any newly created node is marked as unfinished by default
else if is of the form ( ⊃ ( ⊃ )) then for each ∈ { ∈ | ≤ and ̸= 0} do
Create nodes ′ and ′′, with (′) = (, ′) ( ⊃ ) and (′′) = (, ′) ( ⊃ )
Add ′ as a child of and ′′ as a child of ′ end for else if is of the form ( ⊃ ( ⊃ )) then for each ∈ { ∈ | ≤ and ̸= 0} do
Create nodes ′ and ′′, with (′) = (, ′) ( ⊃ ) and (′′) = (, ′) ( ⊃ ) if this is the first iteration of this for loop then
Add ′ and ′′ as children of 40: 41: 42: else 43: for each of the nodes added in the previous iteration of this for loop do 44: Add copies of ′ and ′′ as children of 45: end for 46: end if 47: end for 48: else if is of the form ( ⊃ □ ) then 49: for each ∈ Σ and ∈ s.t. (, , ) ∈ ′ do 50: Create a new node ′ with (′) = (, ′) ( ∧ ⊃ ) 51: Extend B with ′ 52: end for 53: else if is of the form (♢ ⊃ ) then. . . 54: else if is of the form ( ⊃ □ ) then 55: Pick some ∈ Σ that does not already occur in ( (B)). 56: for each ∈ s.t. ∧ ̸= 0 do 57: Create a new node ′ with (′) = (, ′ ∪ {(, , )}) ( ∧ ⊃ ) 58: Add ′ as a child of 59: end for 60: Reactivate() 61: else if is of the form (♢ ⊃ ) then. . . 62: end if 63: end for 64: Increment by 1 65: (T, ) := (T, ) 66: end while 67: return (T, ) 32: 33: 34: Require: Node 1: Assume () = (, ) 2: for each open branch B′ of T containing do 3: Let ′ = ( (B′)) 4: for each finished node in B′ do 5: if ( ()) is of the form ( ⊃ □ ) then 6: for each ∈ Σ and ∈ s.t. (, , ) ∈ ′ do 7: Create a new node ′ with (′) = (, ′) ( ∧ ⊃ ) 8: Extend B′ with ′ 9: end for 10: else if ( ()) is of the form (♢ ⊃ ) then. . . 11: end if 12: end for 13: end for
We omit some of the steps13, but the steps we do give illustrate the general theme: we are greedily applying rules to a branch of the labeled tree (T, ) with the aim of making a specific condition of Definition 5.1 hold for the set of labels in that branch. (T, ) denotes the labeled tree immediately after the ℎ iteration of the while loop. In other words, (T, ) is a snapshot of the continuously growing labeled tree (T, ), and there may be moments during the course of execution of the for loop on line 8 where they are not the same thing 14. 1 (0, ∅) (︀ 1 ⊃ (□ ⊃ □♢ ))︀ 2 (0, ∅) (︀ 1 ⊃ □ )︀ Example 5.3. Assume ℋ = ℋ3, and = □ ⊃ □♢ while loop and (T0, 0) is set to the current state of (T, ). going through the steps of the procedure. Line 2 of isValid( ) invokes constructTableau( (1 ⊃ )). By stepping through the iterations of the while loop, we can see how we construct the labeled tree shown in will grow as we progress. Line 1 of constructTableau initializes (T, ) to consist of only node 1, which is labeled with (0, ∅) (︀ 1 ⊃ )︀ and marked as unfinished in line 2. This concludes the 0ℎ iteration of the
branch of tree T with leaf node ). Node 1 is unfinished and clearly
of the while loop. In line 6 we pick node 1 and then line 7 amounts to setting = 0, = ∅, according to the label of node 1. We then enter the for loop on line 8, and set B = B01, which is the only open branch of T0 containing node 1. On line 12 we set ′ = (B) = ∅. The if condition on line 32 is met. So, the steps in lines 33 to 36 are performed. This amounts to adding nodes 2, 3, 4 and 5, which reflects an application of ⊃ to T. We now return to line 8, the beginning of the for loop over open branches of T0 15 containing node 1. However, there are no other open branches of T0 containing node 1 left to check, so we exit the for loop. This ends the 1 iteration of the while loop, and line 65 sets (T1, 1) to the current state of to denote the
= (︀ 1 ⊃ )︀ , . Then isValid( ) returns false. Let us see why by
We return to the start of the while loop at line 5. (T1, 1) consists of the unfinished nodes 2, 3, 4 and 5, and the open branches B13 and B15. So we enter the 2 iteration of the while loop. Assuming we pick the unfinished node 2 in line 6, the rest of the iteration amounts to performing an identity application of K □ to 13Omission is indicated by ellipses. 14As, for instance, will often be the case whenever we reach line 2 in Reactivate. 15Note that we are concerned with branches in T, not those in T, which may be diferent at some point of the ℎ iteration.
We return to the start of the while loop. (T2, 2) consists of the unfinished nodes 3, 4 and 5, and the open branches B23 and B25. So we enter the 3 iteration of the while loop. Suppose we pick node 3 in line 6. We then enter the for loop on line 8, and set B = B23, which is the only open branch of T2 containing node 3. Line 12 sets ′ = (B) = ∅. The if condition on line 54 is met. So, the steps in lines 55 to 60 are performed. Lines 55 to 59 amount to an application of K □ , which adds nodes 6 and 7 to T. In line 60, Reactivate is called on node 3. In essence, Reactivate ensures that, after a new constraint is added to a branch, any previous applications of K □ and K ♢ that were applied to the branch are ‘reactivated’ so as to ensure that Conditions (9) and (10) of downward saturation are maintained. In the current context, it leads us to adding nodes 8 and 9 to T, reflecting (non-identity) applications of K □ .
We return to the start of the while loop at line 5. (T3, 3) consists of the unfinished nodes 4, 5, 6, 7, 8, and 9, and the open branches B38, B39 and B35. So we enter the 4ℎ iteration of the while loop. Assuming we pick node 6 in line 6, the rest of the iteration leads to us adding node 10, reflecting an application of ≥ to B38.
We return to the start of the while loop at line 5. (T4, 4) consists of the unfinished nodes 4, 5, 7, 8, 9 and 10, and the open branches B410, B49 and B45. So we enter the 5ℎ iteration of the while loop. Assuming we pick node 8 in line 6, the rest of the iteration performs no rule applications.
In the 6ℎ iteration of the while loop, assuming we pick node 10, no new nodes are added, as we perform an identity application of K ♢ (since there are no (, , ) ∈ ′ for = 1).
We carry on in this manner, picking unfinished nodes, until either no unfinished nodes are left or (T, ) is closed. Consider the branch B = B610. Notice that all the nodes in this branch have been finished after iteration 6, and so no further iterations of the while loop will change this branch. Hence, this branch will be present in the final labeled tree returned by constructTableau( (1 ⊃ )), and this is what leads isValid( ) to return false. And in fact, (B) is downward saturated (A fact regarding open labeled trees constructed by our procedure that will be proven in general for Proposition 5.6). So, as in the proof of Lemma 5.2, (B) induces an ℋ3-model M(B), which can be represented as a labelled, weighted, directed graph as follows: 0 1 1 (1, ) = 1
Where we exclude 0-weighted edges and the absence of a label for 0 indicates that the valuation of propositions at that world can take on any value. As the reader can confirm, evaluating at 0 gives 0. And so, this model is indeed a countermodel for .
Also, observe that after each iteration of the while loop, (T, ) has resulted from a finite sequence of Kℋ-rule applications. As such, after termination, (T,) is a Kℋ-tableau for {(0, ∅) (1 ⊃ )}. As we shall see, this observation is a special case of Lemma 5.5.
the ℎ iteration, then for every node ′ added to B in iteration ≤ , we have ( (′)) ⊆ ( ()).
infinite, finitely generated tree must contain at least one infinite branch. Where a tree is said to be finitely generated if every node has a finite number of children.
Proposition 5.4. For all formulas , isValid( ) terminates.
Proof. Assume isValid( ) does not terminate. We derive a contradiction. isValid( ) does not terminate only if the while loop in constructTableau( (1 ⊃ )) goes on forever. And this can only be the case if we are constructing an infinite tree T. Each tableau rule has only a finite number of denominators, and so it is not hard to see that T is finitely generated. Thus, by König’s Lemma, T must have an infinite branch B. The procedure only adds a node to a branch if its label does not already occur in that branch (see line 10). Hence, (B) must be infinite. Further, it should be noted that () is a signed bounded subformula of for all ∈ (B).
For each ∈ N, let us define := { ∈ (B) | () has at most elements}, and := { ∈ (B) | () has exactly elements}. Firstly, we can argue by induction that |()| ≤ + 1 for every ∈ N.
Now consider an arbitrary ∈ N. We show that is finite. Since () is finite, () (which is a subset of ()) is finite. Let , ′ ∈ ′. So, |()| = |(′)|, where = () and ′ = (′) for some nodes , ′ in B. Without loss of generality, suppose was added to B after ′. Then (′) ⊆ () and so we must have () = (′). Thus, () is the same for every ∈ ; call it . We have ∈ if is of the form (, ) where ∈ () and is a signed bounded subformula of . There are only finitely many such . Thus, must be finite.
Note that the step in line 6 of constructTableau is nondeterministic in the sense that there may be multiple unfinished nodes to pick from. Any method of picking such a node will yield a terminating and correct procedure16. For the sake of simplifying this proof, let us assume that we pick an unfinished node with a label that has the maximum among unfinished nodes. Under this assumption, it is not too hard to see that as increases, ∑︀∈ () decreases. Thus, there must exist some for which all elements of have 0. But this means that ′ = ∅ for all ′ > . Therefore (B) = 0 ∪ . . . ∪ , where 0, . . . , are each finite. And so (B) must be finite, which is contrary to what we established earlier.
Let , ∈ N and suppose ≤ . We have ⊆ and so for all nodes in T, () = (). As such, we will usually just write (), where is the final labeling. The next useful property follows from the fact that branches are only extended and/or split from the leaf node. For all branches B of T , there exists a unique branch B of T s.t. B is a subpath of B starting at the root. And, (B) ⊆ (B ).
Lemma 5.5. Let ∈ . For the labeled tree (T, ) returned by constructTableau( ), (T,) is a Kℋ-tableau for {(0, ∅) }.
Tableau( ): (T,) is a Kℋ-tableau for{(0, ∅) }.
Then, since the while loop terminates, the labeled tree returned by constructTableau( ) is (T, ) for some ∈ N. And the required result follows from the loop invariant.
Proposition 5.6. For all formulas , isValid( ) returns true if is valid.
For the converse implication, suppose isValid( ) does not return true. Since the procedure terminates, the while loop performed by constructTableau( (1 ⊃ )) ends after iterations for some ∈ N, and it returns (T, ). But since isValid( ) returns false, (T, ) is not closed. Thus, (T, ) contains an open branch B and each node in B is marked as finished. Note that B being open implies that Bi is open for each 1 ≤ ≤ . We claim that each condition of Definition 5.1 holds for (B). This should not be surprising, since the applications of rules in constructTableau are essentially guided by the aim of ensuring that this claim holds. If (B) is in fact downward saturated, then, by Lemma 5.2, (B) is satisfiable. But (0, ∅) (1 ⊃ ) ∈ (B), and hence cannot be valid. For illustrative purposes, let us confirm here that
Suppose (, ) ( ⊃ □ ) ∈ (B) for some ∈ Σ, ⊆ Σ2 × and truth value . So, for some node in B, () = (, ) ( ⊃ □ ). Since each node in B is marked as finished, must have been picked during some iteration 1 ≤ ≤ . Let ∈ Σ, ∈ and suppose (, , ) ∈ ( (B)). There exists a minimal 1 ≤ ≤ s.t. (, , ) ∈ ( (B )). We have two cases. If < , then (, , ) ∈ ( (B )) ⊆ ( (B− 1)), and the steps in lines 48 to 52 performed for B− 1 ensure that (, ′) ( ∧ ⊃ ) ∈ (B) for some ′ ⊆ Σ2 × . If ≥ , then has already been marked as finished by the time we get to iteration .
16Not all such methods are equally eficient though, since the unfinished node we pick at a given stage can dramatically influence the subsequent size of the constructed tableau. for B− 1 ensures that (, ′ ∪ {(, , )}) ( ∧ ⊃ ) ∈ (B) for some ′ ⊆ Σ2 × . In either case, (, ′′) ( ∧ ⊃ ) ∈ (B) for some ′′ ⊆ Σ2 × . So, Condition (9) holds for (B). Corollary 5.7. Kℋ is (weakly) complete wrt the class of all ℋ-frames.
Kℋ-tableau for (, ∅) (1 ⊃ ). By Lemma 5.5, constructTableau( (1 ⊃ )) returns the labelled tree (T, ), where (T,) is a Kℋ-tableau for {(0, ) (1 ⊃ )}. This implies that isValid( ) cannot possibly return true, as such an eventuality relies on (T, ) being closed, which would imply that (T,) is a closed Kℋ-tableau for (0, ∅) (1 ⊃ ). Thus, by Proposition 5.6, we can conclude that is not valid.
implementation has been written in python and is provided as a package on PyPi. The source, along with documentation, is available on GitHub (https://github.com/WeAreDevo/Many-Valued-Modal-Tableau).
ℋ-frame F = (, ) is finite if the set of worlds is finite. A class of ℋ-frames ℱ is of finite character if each ℋ-frame in ℱ is finite. And, Λ ⊆ (ℒℋ(Φ)) is said to have the finite frame property if Λ = Λℱ for some class of frames ℱ of finite character.
Corollary 5.8. Kℋ has the finite frame property, and hence the finite model property.
Proof. Consider the class ℱ of all finite ℋ-frames. We claim that Kℋ = Λℱ . Clearly Kℋ ⊆ Λℱ (since ℱ is a subclass of the class of all ℋ-frames). To show Λℱ ⊆ Kℋ, consider a formula /∈ Kℋ. We argue that /∈ Λℱ . Since /∈ Kℋ, is not valid. So, as in the second part of the proof for Proposition 5.6, constructTableau( (1 ⊃ )) returns a labeled tree containing an open branch B, where (B) is downward saturated. (B) induces an ℋ-model M(B) which is a counter model for . M(B) is based on an ℋ-frame (, ) where = ( (B)). The only members of ( (B)) are the initial world 0, along with a distinct world introduced by each application of K □ or K ♢ . But the number of applications of K □ or K ♢ is bounded above by a finite function of ( ) and ||. Hence ( (B)) is ifnite. And since M(B) is a counter model for , we must have /∈ Λℱ .
In this subsection, we briefly consider simple modifications of the rules K □ and K ♢ , from which we obtain a prefixed tableau system for KBℋ for all ∈ . Let us fix an arbitrary ∈ . We proceed to argue that the tableau system KBℋ :={⊥1, ⊥2, ⊥3, ⊥4, ⊥5, ≥ , ≥ , ≤ , ≤ , ∧, ∧, ∨, ∨,
⊃ , ⊃ , K □ , K ♢ , KB □ , KB ♢ } is sound and complete wrt Symmℋ. KB □ and KB ♢ are defined as follows: ; (, ′ ∪ {(, , 1), (, , 11 )}) ( ∧ 1 ⊃ ) ; (, ) ( ⊃ □ ) . . . ; (, ′ ∪ {(, , ), (, , 1)}) ( ∧ ⊃ ) . . .
; (, ′ ∪ {(, , ), (, , )}) ( ∧ ⊃ ) (KB □ ) ; (, ′ ∪ {(, , 1), (, , 11)}) ( ∧ 1 ⊃ )
. . .
(KB ♢ ) Where is any symbol of Σ that is not in ( ), 1, . . . , are all the ℋ-truth values s.t. ∧ ̸= 0, and for each ∈ {1, . . . , }, {1 , . . . , } = { ∈ | ∧ = ∧ }.
; (, ′ ∪ {(, , 1), (, , 11)}) ( ⊃ 1 ⇒ ) Where is any symbol of Σ that is not in ( ), 1, . . . , are all the ℋ-truth values s.t. ⇒ ̸= 1, and for each ∈ {1, . . . , }, {1 , . . . , } = { ∈ | ∧ = ∧ }.
Proposition 6.1. KBℋ is sound wrt Symmℋ.
that the numerator of is Symmℋ-satisfiable. That is, there exists an ℋ-model M = ((, ), ) based on a frame from Symmℋ, and an interpretation of in M s.t. is satisfied under . We wish to show that at least one of the denominators is Symmℋ-satisfiable. We only need to consider the case in which = KB □ or = KB ♢ . The other cases follow from Lemma 4.1, with ℱ = Symmℋ. So consider = KB □ . Then = ; (, ) ( ⊃ □ ) and so ( ⊃ □ ) is satisfied by M at (). Thus, for some s ∈ , we have ≰ ((), s) ⇒ (s, ). Suppose ((), s) = ∈ and (s, ()) = ∈ . Clearly ∧ ̸= 0.
consider ′ := ∪ {(, s)}. ′ is an interpretation of = ; (, ′ ∪ {(, , ), (, , )}) ( ∧ ⊃ ) in M. The argument for = KB ♢ is similar.
is downward saturated (Definition 5.1), and 1’. For all , ∈ Σ, ∈ , if (, , ) ∈ (), then (, , ′) ∈ () for some ′ ∈ ℋ s.t.
∧ = ′ ∧ .
ℋ-model M and an interpretation of in M s.t. is satisfied under . In addition, since satisfies (1’), it is clear that the model M we construct is in fact based on a frame from Symmℋ. Hence, is Symmℋ-satisfiable whenever is downward KBℋ-saturated.
Then, suppose we modify constructTableau by replacing applications of K □ and K ♢ with applications of KB □ and KB ♢ respectively. With only slight modifications to the arguments given previously, we can show that the new version of isValid is a decision procedure for KBℋ. And from this we get the following results.
Proposition 6.2. KBℋ is (weakly) complete wrt Symmℋ.
Corollary 6.3. KBℋ has the finite frame property 17, and hence the finite model property.
Statistical Sciences (CoE-MaSS), South Africa. Opinions expressed and conclusions arrived at are those of the author and are not necessarily to be attributed to the CoE-MaSS.