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 difficulty 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.
Many-valued modal logics (MVML) generalize the Kripke semantics of standard modal logic 1 by allowing for many-valued propositional valuations and/or accessibility relations. This is very useful when applying modal logic to reason about problems requiring a logical account of both modality and vagueness. Accordingly, many-valued modal logics have been used to model and reason about problems in a wide range of settings involving different kinds of gradation or vagueness. Fitting [1,7] suggests that Heyting-valued Kripke models provide natural models of the epistemic stances of committees of experts which elegantly capture the relations of influence or dominance among committee members. In [7], he provides a MVML-based analysis of the 'muddy children puzzle'. Many-valued modal logics are closely related to fuzzy description logics [8], widely applied in the context of the semantic web [9]. In [10], MVML is applied to the task of reasoning about fuzzy temporal relations. Many-valued generalizations of non-distributive modal logics have been employed to model and reason about competition among scientific theories [11] and to capture certain phenomena of socio-political competition [12]. In [13] many-valued modal logics are enlisted into a framework for reasoning about vague-concepts and categorization.
The literature contains numerous different approaches to extending modal logic to a many-valued setting. Some of the earliest proposals are [14,15,16,17,18]. All of these early works focus on many-valued worlds and do not stray from crisp accessibility relations. In other words, the notion of a Kripke frame is not modified. The first framework to generalize modal logic with both many-valued worlds and many-valued accessibility relations (thus generalizing Kripke frames) arose in the early 1990's, with a series of papers by Melvin Fitting [1,2]. The present paper is concerned with the particular approach to MVML established in [2]. There, Fitting introduces ℋ-valued modal logics. More precisely, he defines an interpretation of modal formulas 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 Fitting's sequent calculus for K ℋ to sequent calculi for these logics. The sequent calculi in [2] and [19] rely on 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. Vidal has contributed much to this area, and good overviews and references can be found in [25,26]. Much 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 ℋ 𝑑 .
Analogous to the connection between Boolean algebras and classical propositional logic, Heyting algebras (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 Heyting Algebras either in terms of orderings or purely algebraically. We choose the order theoretic approach.
A partially ordered set (𝐻, ≤) is a lattice iff every two-element subset {𝑎, 𝑏} of 𝐻 has a supremum (or 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.
A Heyting algebra ℋ is a bounded lattice (𝐻, ≤) with the property that for all 𝑎, 𝑏 ∈ 𝐻, there exists a 𝑐 ∈ 𝐻 which is the greatest element of {𝑐 ′ ∈ 𝐻 | 𝑎 ∧ 𝑐 ′ ≤ 𝑏}, or equivalently, 𝑑 ≤ 𝑐 iff 𝑎 ∧ 𝑑 ≤ 𝑏 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 values 2 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:
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 𝜙.
Formulas will be interpreted in ℋ-valued generalizations of standard Kripke structures. Namely, an ℋ-frame 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.
We can extend an ℋ-model's valuation to all formulas in 𝐹 𝑟𝑚(ℒ ℋ (Φ)) via a recursive definition.
Definition 2.3. Let M = ((𝑊, 𝑅), 𝑉 ) be an ℋ-model. The extension of 𝑉 , 𝑉 : 𝑊 × 𝐹 𝑟𝑚(ℒ ℋ (Φ)) → 𝐻, is the unique function where for any s ∈ 𝑊 and 𝜙, 𝜓 ∈ 𝐹 𝑟𝑚(ℒ ℋ (Φ)), we have
Henceforth, we employ the harmless abuse of notation in which 𝑉 is used to denote both a valuation and its extension. We say that 𝜙 is satisfied by M at s ∈ 𝑊 (denoted as M, s ⊩ 𝜙) iff 𝑉 (s, 𝜙) = 1. Further, 𝜙 is globally satisfied by M (denoted as M ⊩ 𝜙) iff 𝑉 (s, 𝜙) = 1 for every s ∈ 𝑊 . We say M is a counter model for 𝜙 iff M ⊮ 𝜙.
It should be noted that if ℋ is the Boolean algebra 2 consisting of two elements, then the MVML we have introduced reduces to the standard two-valued modal logic. In this standard case, it is clear that some of our 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.
We introduce new symbols which have 'negation-like' semantics which will be crucial for our tableaux. Let 𝑇 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 iff 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 ⊩ 𝜙) iff 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 ℱ ⊩ 𝜙) iff 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
Tableau systems were first introduced by Beth [35] and popularized by Smullyan [36]. They have since been 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. Before precisely defining prefixed tableaux, we need to define the relevant object language, i.e. the set 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 iff 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. We denote the set of all signed bounding implications by 𝑆𝐵𝐼, and say that 𝛽 ∈ 𝑆𝐵𝐼 bounds 𝜙 by 𝑎 iff 𝛽 is of the form 𝑇 (𝑎 ⊃ 𝜙), 𝑇 (𝜙 ⊃ 𝑎), 𝐹 (𝑎 ⊃ 𝜙) or 𝐹 (𝜙 ⊃ 𝑎). We shall use ⊥ as an abbreviation for 𝐹 (0 ⊃ 1).
Our system expands on the tableau system defined by Fitting in [3]. There, the object language is 𝑆𝐵𝐼. We 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. Specifically, a tableau in [3] is a collection in 𝒫(𝒫(𝑆𝐵𝐼)) (i.e., a set of sets of signed bounding implications). 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 finite list of denominators 𝒟 1 , . . . , 𝒟 𝑛 , and a side condition. Schematically, 𝜌 is presented as follows.
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 𝜌 iff for all 𝑇 ∈ 𝒫(𝒫(𝑝𝑆𝐵𝐼)), if 𝑇 ̸ = 𝑓 (𝑇 ) then for some 𝑆 ∈ 𝑇 , 𝑆 is an instantiation of 𝒩 , 𝑓 (𝑇 ) contains 𝑆 1 , . . . 𝑆 𝑛 which are corresponding instantiations of 𝒟 1 , . . . , 𝒟 𝑛 respectively, and 𝑇 ∖ {𝑆} = 𝑓 (𝑇 ) ∖ {𝑆 1 , . . . , 𝑆 𝑛 }. 6In 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 𝑇 * . Now, we call any finite collection of tableau rules, 𝒞, a tableau system. Definition 3.1. Let 𝑋 be a finite subset of 𝑝𝑆𝐵𝐼. The set of 𝒞-tableaux for 𝑋 is a subset of 𝒫(𝒫(𝑝𝑆𝐵𝐼)) 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 𝑋.
Further, the set of all 𝒞-tableaux is simply the set of all 𝑇 ∈ 𝒫(𝒫(𝑝𝑆𝐵𝐼)) s.t. 𝑇 is a 𝒞-tableau for some finite 𝑋 ⊆ 𝑝𝑆𝐵𝐼. We call the sets in a 𝒞-tableau its branches 7 . Given some set 𝑆 ∈ 𝒫(𝑝𝑆𝐵𝐼), we shall say that 𝑆 is closed iff (𝑤, ∅)⊥ ∈ 𝑆 for some 𝑤 ∈ Σ. Otherwise, we say that 𝑆 is open. A tableau is closed iff all its branches are closed; otherwise it is open. We say that a formula 𝜙 is a theorem of 𝒞 iff 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 difficult, 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 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 𝑤𝑜𝑟𝑙𝑑𝑠(𝑋) := {𝑤𝑜𝑟𝑙𝑑(𝑥) | 𝑥 ∈ 𝑋}. With prefixes in hand, we view branches of a tableau as describing an entire hypothetical satisfying modelnot just a valuation at a specific world. These intuitions are made precise as follows: 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 iff there exists an ℋ-model M based on a frame from ℱ, and an interpretation 𝐼 of 𝑆 in M s.t. 𝑆 is satisfied under 𝐼.
In the case where ℱ is the class of all ℋ-frames, we simply say that 𝑆 is satisfiable.
We proceed to study a prefixed tableau system for 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. Furthermore, we use 𝜎 ′ as an abbreviation for 𝑐𝑜𝑛𝑠(𝒩 )8 . Where 𝑎 ≰ 𝑏
Closing rules
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.
Reversal rules Where 𝑎 ̸ = 1.
Where 𝑡1, . . . , 𝑡𝑛 are all the ℋ-truth values below 𝑎 except 0.
Where 𝑡𝑖 is any ℋ-truth value below 𝑎 except 0.
Propositional rules
Where 𝑣 is any member of Σ and 𝑡 any ℋ-truth value s.t. (𝑤, 𝑣, 𝑡) ∈ 𝜎 ′ .
Where 𝑣 is any member of Σ and 𝑡 any ℋ-truth value s.t.
Where 𝑣 is any symbol of Σ that is not in 𝑤𝑜𝑟𝑙𝑑𝑠(𝒩 ), and 𝑡1, . Where 𝑣 is any symbol of Σ that is not in 𝑤𝑜𝑟𝑙𝑑𝑠(𝒩 ), and 𝑡1, . . . , 𝑡𝑛 are all the ℋ-truth values s.t. 𝑡𝑖 ⇒ 𝑎 ̸ = 1.
Modal rules
Let ℱ be an arbitrary class of ℋ-frames. A 𝒞-tableau 𝑇 is ℱ-satisfiable iff at least one branch 𝑆 ∈ 𝑇 is ℱ-satisfiable. Consider some rule 𝜌 ∈ 𝒞. We say 𝜌 preserves ℱ-satisfiability iff for every 𝒞-tableau 𝑇 , if 𝑇 is ℱ-satisfiable and 𝑇 * is a tableau that can be derived from 𝑇 via an application of 𝜌, then 𝑇 * is ℱ-satisfiable.
To prove 𝒞 is sound wrt ℱ, it suffices to show that each rule of 𝒞 preserves ℱ-satisfiability. Proof. We need to show that for each such rule, if (an instantiation of) the numerator 𝒩 is ℱ-satisfiable, then (the corresponding instantiation of) at least one of the denominators 𝒟 is ℱ-satisfiable.
Let 𝜌 ∈ 𝑝𝒞K ℋ and suppose that the numerator 𝒩 of 𝜌 is ℱ-satisfiable. That is, there exists an ℋ-model 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 satisfied 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 𝐼 ′ .
We may now approach proving completeness in much the same way as is done in [3]. That is, we could define 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 𝜙. This will also allow us to prove a finite frame property.
We use a labeled tree as the main data structure in the decision procedure for deriving a desired tableau. As 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 iff all of the following conditions hold: 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 × 𝐻.
We will mainly be concerned with this definition in the context in which 𝑆 is a branch of a 𝑝𝒞K ℋ -tableau. Then, Conditions (3) to ( 12) may be seen as asserting that the branch is closed under applications of the rules 𝑝𝑇 ∧, 𝑝𝐹 ∧, 𝑝𝑇 ∨, 𝑝𝐹 ∨, 𝑝𝑇 ⊃, 𝑝𝐹 ⊃, 𝑝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). 10 . We call M 𝑆 an ℋ-model induced by 11 𝑆.
We proceed to prove, by induction on the structure of formulas, that for every formula 𝜙, 𝑃 (𝜙) holds. Where 𝑃 (𝜙) 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.
Once we have established that 𝑃 (𝜙) holds for all formulas 𝜙, the staisfiablily of 𝑆 follows easily. For consider 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 𝐼.
Essentially, the decision procedure amounts to constructing a tableau by systematically applying rules until 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. Let (T, 𝑈 ) be a labelled tree, and suppose {B 𝑖 } 𝑖∈𝐼 are all of the branches of T. The tableau corresponding to (T, 𝑈 ) (denoted 𝑇 (T,𝑈 ) ) is simply the collection {𝑈 (B 𝑖 )} 𝑖∈𝐼 12 . We will say that a branch B of T is closed iff 𝑈 (B) is closed. Otherwise, we say that B is open. We will say that (T, 𝑈 ) is closed iff all the branches of T are closed; otherwise, we say it is open. Let us also introduce the notion of applying tableau rules to labelled 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 B is a branch of T but not of T * , we say that 𝜌 was applied to branch B. ◁ From now on we will assume that any newly created node is marked as unfinished by default 3: 𝑖 := 0 4: (T 𝑖 , 𝑈 𝑖 ) := (T, 𝑈 ) 5: while there are unfinished nodes and (T, 𝑈 ) is not closed do 6:
Pick some unfinished node 𝑛 and mark it as finished. 7:
Assume 𝑈 (𝑛) = (𝑤, 𝜎)𝛽
for each open branch B of T 𝑖 containing 𝑛 do 9:
We now proceed to extend or fork B depending on the form of 𝑈 (𝑛).
In what follows, assume we only add a node labelled with (𝑢, 𝜎 ′ )𝛽 ′ if (𝑢, 𝜎 ′′ )𝛽 ′ / ∈ 𝑈 (B) for all 𝜎 ′′ 11:
Assume 𝑙 is the leaf of B. 12:
Let 𝜎 ′ = 𝑐𝑜𝑛𝑠(𝑈 (B)) 13:
if 𝑈 (B) is an instantiation of the numerator of the rule 𝑝⊥ 1 , 𝑝⊥ We omit some of the steps 13 , 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 . . By stepping through the iterations of the while loop, we can see how we construct the labeled tree shown in Figure 5.1 above. (T, 𝑈 ) is used throughout the procedure to denote the current state of a labeled tree that 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 while loop and (T 0 , 𝑈 0 ) is set to the current state of (T, 𝑈 ).
The branch B 1 0 containing only node 1 is a branch of T 0 (Note, in this example we shall use B 𝑗 𝑖 to denote the branch of tree T 𝑖 with leaf node 𝑗). Node 1 is unfinished and clearly B 1 0 is open, so we enter the 1 𝑠𝑡 iteration of the while loop. In line 6 we pick node 1 and then line 7 amounts to setting 𝑤 = 𝑤 0 , 𝜎 = ∅, 𝛽 = 𝐹 (︀ 1 ⊃ 𝜙 )︀ , according to the label of node 1. We then enter the for loop on line 8, and set B = B 1 0 , which is the only open branch of T 0 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 T 0 15 containing node 1. However, there are no other open branches of T 0 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 (T 1 , 𝑈 1 ) to the current state of (T, 𝑈 ).
We return to the start of the while loop at line 5. (T 1 , 𝑈 1 ) consists of the unfinished nodes 2, 3, 4 and 5, and the open branches B 3 1 and B 5 1 . 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 B 3 1 . 13 Omission is indicated by ellipses. 14 As, for instance, will often be the case whenever we reach line 2 in Reactivate. 15 Note that we are concerned with branches in T𝑖, not those in T, which may be different at some point of the 𝑖 𝑡ℎ iteration.
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.
Proof. We prove the contrapositive. Suppose ⊬ 𝑝𝒞K ℋ 𝜙. That is, taking any 𝑤 ∈ Σ, there does not exist a closed 𝑝𝒞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.
Propositions 5.4 and 5.6 amount to saying that isValid is a decision procedure for the logic K ℋ . A concrete 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).
The decision procedure also suggests a finite frame property, which we present now. Let us say that an ℋ-frame F = (𝑊, 𝑅) is finite iff the set of worlds 𝑊 is finite. A class of ℋ-frames ℱ is of finite character iff each ℋ-frame in ℱ is finite. And, Λ ⊆ 𝐹 𝑟𝑚(ℒ ℋ (Φ)) is said to have the finite frame property iff Λ = Λ ℱ 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
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 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. Let 𝑣 ∈ Σ be any symbol that is not already in 𝑤𝑜𝑟𝑙𝑑𝑠(𝒩 ). We extend the interpretation 𝐼 to 𝑣. Specifically, consider 𝐼 ′ := 𝐼 ∪ {(𝑣, s)}. 𝐼 ′ is an interpretation of 𝒟 = 𝒩 ; (𝑣, 𝜎 ′ ∪ {(𝑤, 𝑣, 𝑡 𝑖 ), (𝑣, 𝑤, 𝑡)})𝐹 (𝑎 ∧ 𝑡 𝑖 ⊃ 𝜙) in M. The argument for 𝜌 = 𝑝KB𝐹 ♢ 𝑑 is similar.
Let us introduce the notion of 𝑝𝒞KB ℋ 𝑑 -saturation. Say that 𝑆 ⊆ 𝑝𝑆𝐵𝐼 is downward 𝑝𝒞KB ℋ 𝑑 -saturated iff 𝑆 is downward saturated (Definition 5.1), and 1'. For all 𝑤, 𝑣 ∈ Σ, 𝑡 ∈ 𝐻, if (𝑤, 𝑣, 𝑡) ∈ 𝑐𝑜𝑛𝑠(𝑆), then (𝑣, 𝑤, 𝑡 ′ ) ∈ 𝑐𝑜𝑛𝑠(𝑆) for some 𝑡 ′ ∈ ℋ s.t.
𝑡 ∧ 𝑑 = 𝑡 ′ ∧ 𝑑.
If 𝑆 is downward 𝑝𝒞KB ℋ 𝑑 -saturated, we may use the same approach as in Lemma 5.2 to construct/induce an ℋ-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.
𝑑 is (weakly) complete wrt Symm ℋ 𝑑 .
Corollary 6.3. KB ℋ 𝑑 has the finite frame property 17 , and hence the finite model property.
The first author acknowledges financial support from the DSI-NRF Centre of Excellence in Mathematical and 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.
We return to the start of the while loop. (T 2 , 𝑈 2 ) consists of the unfinished nodes 3, 4 and 5, and the open branches B 3 2 and B 5 2 . 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 = B 3 2 , which is the only open branch of T 2 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. (T . 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 = B 10 6 . 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:
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 following is apparent in general. No branch of T is ever shrunk during the execution of construct-Tableau. Further, let B be a branch of the constructed tree. For all 𝑖 ∈ N, if the node 𝑛 was added to B during the 𝑖 𝑡ℎ iteration, then for every node 𝑛 ′ added to B in iteration 𝑗 ≤ 𝑖, we have 𝑐𝑜𝑛(𝑈 (𝑛 ′ )) ⊆ 𝑐𝑜𝑛(𝑈 (𝑛)).
We use König's Lemma [38] (see [36, p. 32]) to prove termination. Recall that König's Lemma states: Every infinite, finitely generated tree must contain at least one infinite branch. Where a tree is said to be finitely generated iff 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). 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 𝑥 ∈ 𝐵 𝑘 iff 𝑥 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 procedure 16 . 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 , ∅)𝛼}.
Proof. We can prove that the following is a loop invariant for the while loop performed by construct-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 iff 𝜙 is valid.
Proof. The forward implication follows from Lemma 5.5 and soundness.
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 B i 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 Condition (9) holds: 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 𝑗. Further, iteration 𝑗 must involve an application of 𝑝K𝐹 □ or 𝑝K𝐹 ♢ for B 𝑗−1 , and so the call to Reactivate