=Paper=
{{Paper
|id=Vol-3717/paper1
|storemode=property
|title=Prefixed Tableaux and Decision Procedures for Many-Valued Modal Logics
|pdfUrl=https://ceur-ws.org/Vol-3717/paper1.pdf
|volume=Vol-3717
|authors=Guy Axelrod,Willem Conradie
|dblpUrl=https://dblp.org/rec/conf/paar/AxelrodC24
}}
==Prefixed Tableaux and Decision Procedures for Many-Valued Modal Logics==
https://ceur-ws.org/Vol-3717/paper1.pdf
Prefixed Tableaux and Decision Procedures for Many-Valued
Modal Logics
Guy Axelrod1,* , Willem Conradie1,2
1
University of the Witwatersrand, South Africa
2
National Institute for Theoretical and Computational Sciences (NITheCS), South Africa
Abstract
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.
Keywords
Many-Valued Modal Logic, Prefixed Tableaux, Completeness, Decidability, Finite Model Property
1. Introduction
Many-valued modal logics (MVML) generalize the Kripke semantics of standard modal logic1 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
PAAR’24: 9th Workshop on Practical Aspects of Automated Reasoning, July 2, 2024, Nancy, France
*
Corresponding author.
$ g.axelrod1@gmail.com (G. Axelrod); willem.conradie@wits.ac.za (W. Conradie)
0000-0002-1752-8069 (G. Axelrod); 0000-0001-9906-4132 (W. Conradie)
© 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
1
By ‘standard’ is meant all those logics studied in standard reference texts in modal logic such as [4, 5, 6]
CEUR
ceur-ws.org
Workshop ISSN 1613-0073
Proceedings
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ℋ 𝑑 .
2. Background
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.
Definition 2.1. 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 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 𝜙.
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
• 𝑉 (s, 𝛾) = 𝑉 (s, 𝛾) for every 𝛾 ∈ Φ ∪ 𝐻,
• 𝑉 (s, (𝜙 ∧ 𝜓)) = 𝑉 (s, 𝜙) ∧ 𝑉 (s, 𝜓),
• 𝑉 (s, (𝜙 ∨ 𝜓)) = 𝑉 (s, 𝜙) ∨ 𝑉 (s, 𝜓),
• 𝑉 (s, (𝜙 ⊃ 𝜓)) = 𝑉 (s, 𝜙) ⇒ 𝑉 (s, 𝜓),
⋀︁
• 𝑉 (s, □𝜙) = {𝑅(s, v) ⇒ 𝑉 (v, 𝜙) | v ∈ 𝑊 },
⋁︁
• 𝑉 (s, ♢𝜙) = {𝑅(s, v) ∧ 𝑉 (v, 𝜙) | v ∈ 𝑊 }.
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
2
We will often drop the ℋ and just speak of truth values.
3
In 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
differentiate between syntactic and semantic objects. This, in turn, allows us to differentiate 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.
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 (𝑊, 𝑅)
is 𝑑-symmetric iff 𝑑 ∧ 𝑅(s, v) = 𝑑 ∧ 𝑅(v, s) for every s, v ∈ 𝑊 . Letting Symmℋ 𝑑 denote the class of all
𝑑-symmetric ℋ-frames, we use KBℋ 𝑑 to denote4 Λ
Symm ℋ .
𝑑
3. Prefixed Tableaux
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.
4
The 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.
5
For 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 𝜙.
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.
𝒩
(𝜌)
𝒟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 denom-
inator(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 , . . . , 𝑆𝑛 }.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 𝑇 * .
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 branches7 .
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
6
Note that the identity operation on 𝒫(𝒫(𝑝𝑆𝐵𝐼)) is described by every rule.
7
The 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 𝑤𝑜𝑟𝑙𝑑𝑠(𝑋) := {𝑤𝑜𝑟𝑙𝑑(𝑥) | 𝑥 ∈ 𝑋}.
With prefixes in hand, we view branches of a tableau as describing an entire hypothetical satisfying model –
not 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ℋ .
𝑝𝒞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.
Furthermore, we use 𝜎 ′ as an abbreviation for 𝑐𝑜𝑛𝑠(𝒩 ) 8 .
𝑋; (𝑤, 𝜎)𝑇 (𝑎 ⊃ 𝑏) 𝑋; (𝑤, 𝜎)𝐹 (𝑎 ⊃ 𝑏) 𝑋; (𝑤, 𝜎)𝐹 (0 ⊃ 𝜙)
(𝑝⊥1 ) (𝑝⊥2 ) (𝑝⊥3 )
𝒩 ; (𝑤, ∅)⊥ 𝒩 ; (𝑤, ∅)⊥ 𝒩 ; (𝑤, ∅)⊥
Where 𝑎 ≰ 𝑏 Where 𝑎 ≤ 𝑏
𝑋; (𝑤, 𝜎)𝐹 (𝜙 ⊃ 1) 𝑋; (𝑤, 𝜎)𝑇 (𝑎 ⊃ 𝜙); (𝑤, 𝜎 ′ )𝑇 (𝜙 ⊃ 𝑏)
(𝑝⊥4 ) (𝑝⊥5 )
𝒩 ; (𝑤, ∅)⊥ 𝒩 ; (𝑤, ∅)⊥
Where 𝑎 ≰ 𝑏
Table 1
Closing rules
𝑋; (𝑤, 𝜎)𝐹 (𝑎 ⊃ 𝜙) 𝑋; (𝑤, 𝜎)𝐹 (𝜙 ⊃ 𝑎)
(𝑝𝐹 ≥) 𝒩 ; ... 𝒩; (𝑝𝐹 ≤) 𝒩 ; ... 𝒩;
(𝑤, 𝜎 ′ )𝑇 (𝜙 ⊃ 𝑡1 ) (𝑤, 𝜎 ′ )𝑇 (𝜙 ⊃ 𝑡𝑛 ) (𝑤, 𝜎 ′ )𝑇 (𝑢1 ⊃ 𝜙) (𝑤, 𝜎 ′ )𝑇 (𝑢𝑘 ⊃ 𝜙)
Where 𝑡1 , . . . , 𝑡𝑛 are all the maximal ℋ-truth values not Where 𝑢1 , . . . , 𝑢𝑘 are all the minimal ℋ-truth values not
above 𝑎, and 𝑎 ̸= 0. below 𝑎, and 𝑎 ̸= 1.
𝑋; (𝑤, 𝜎)𝑇 (𝑎 ⊃ 𝜙) 𝑋; (𝑤, 𝜎)𝑇 (𝜙 ⊃ 𝑎)
(𝑝𝑇 ≥) (𝑝𝑇 ≤)
𝒩 ; (𝑤, 𝜎 ′ )𝐹 (𝜙 ⊃ 𝑡𝑖 ) 𝒩 ; (𝑤, 𝜎 ′ )𝐹 (𝑢𝑖 ⊃ 𝜙)
Where 𝑡𝑖 is any maximal ℋ-truth value not above 𝑎, and Where 𝑢𝑖 is any minimal ℋ-truth value not below 𝑎, and
𝑎 ̸= 0. 𝑎 ̸= 1.
Table 2
Reversal rules
8
In 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 𝑎 ̸= 0.
𝑋; (𝑤, 𝜎)𝑇 ((𝜙 ∨ 𝜓) ⊃ 𝑎) 𝑋; (𝑤, 𝜎)𝐹 ((𝜙 ∨ 𝜓) ⊃ 𝑎)
(𝑝𝑇 ∨) (𝑝𝐹 ∨)
𝒩 ; (𝑤, 𝜎 ′ )𝑇 (𝜙 ⊃ 𝑎); (𝑤, 𝜎 ′ )𝑇 (𝜓 ⊃ 𝑎) 𝒩 ; (𝑤, 𝜎 ′ )𝐹 (𝜙 ⊃ 𝑎) 𝒩 ; (𝑤, 𝜎 ′ )𝐹 (𝜓 ⊃ 𝑎)
Where 𝑎 ̸= 1. Where 𝑎 ̸= 1.
𝑋; (𝑤, 𝜎)𝐹 (𝑎 ⊃ (𝜙 ⊃ 𝜓))
𝑋; (𝑤, 𝜎)𝑇 (𝑎 ⊃ (𝜙 ⊃ 𝜓))
𝒩; ... 𝒩;
(𝑝𝐹 ⊃) (𝑝𝑇 ⊃) 𝒩 ; 𝒩;
(𝑤, 𝜎 ′ )𝑇 (𝑡1 ⊃ 𝜙); (𝑤, 𝜎 ′ )𝑇 (𝑡𝑛 ⊃ 𝜙);
′ (𝑤, 𝜎 ′ )𝐹 (𝑡𝑖 ⊃ 𝜙) (𝑤, 𝜎 ′ )𝑇 (𝑡𝑖 ⊃ 𝜓)
(𝑤, 𝜎 )𝐹 (𝑡1 ⊃ 𝜓) (𝑤, 𝜎 ′ )𝐹 (𝑡𝑛 ⊃ 𝜓)
Where 𝑡𝑖 is any ℋ-truth value below 𝑎 except 0.
Where 𝑡1 , . . . , 𝑡𝑛 are all the ℋ-truth values below 𝑎 except
0.
Table 3
Propositional rules
𝑋; (𝑤, 𝜎)𝑇 (𝑎 ⊃ □𝜙) 𝑋; (𝑤, 𝜎)𝑇 (♢𝜙 ⊃ 𝑎)
(𝑝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.
Table 4
Modal rules
4. Soundness
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.
Lemma 4.1. 𝜌 preserves ℱ-satisfiability for each 𝜌 ∈ 𝑝𝒞Kℋ .
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 𝐼 ′ .
5. Completeness
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:
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 × 𝐻.
9
See [37], in which this is done in the context of prefixed systems for standard modal logics.
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).
Lemma 5.2. If 𝑆 ⊆ 𝑝𝑆𝐵𝐼 is downward saturated, then 𝑆 is satisfiable.
Proof. Suppose 𝑆 is downward saturated. Define the ℋ-frame (𝑊, 𝑅) where 𝑊 := 𝑤𝑜𝑟𝑙𝑑𝑠(𝑆) and for all
𝑤, 𝑣 ∈ 𝑊 , {︃
𝑅𝑆 (𝑤, 𝑣) if 𝑅𝑆 (𝑤, 𝑣) defined
𝑅(𝑤, 𝑣) :=
0 otherwise
It follows from Condition (1) of downward saturation that 𝑅 : 𝑊 2 → 𝐻 is a well-defined function. Now,
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 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 𝐼.
5.1. Decision Procedure
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
10
Such 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.
11
Note that there may be multiple such models with distinct valuations.
12
For 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).
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.
procedure isValid(𝜙) returns true or false
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
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 𝑈 (𝑛) = (𝑤, 𝜎)𝛽
8: for each open branch B of T𝑖 containing 𝑛 do
9: We now proceed to extend or fork B depending on the form of 𝑈 (𝑛).
10: 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 , 𝑝⊥2 , 𝑝⊥3 , 𝑝⊥4 or 𝑝⊥5 then
14: Extend B with a node labelled (𝑤, ∅)⊥.
15: Continue to the next iteration
16: else if 𝛽 is 𝐹 (𝑎 ⊃ 𝜙) where 𝑎 ∈ 𝐻 and 𝜙 is of the form
𝑝 (a propositional variable) or 𝜓 ∨ 𝜃 or ♢𝜓 then
17: for each 𝑡 ∈ 𝑚𝑎𝑥({𝑐 ∈ 𝐻 | 𝑎 ≰ 𝑐}) do
18: Create a node 𝑛′ , with 𝑈 (𝑛′ ) = (𝑤, 𝜎 ′ )𝑇 (𝜙 ⊃ 𝑡)
19: Add 𝑛′ as a child of 𝑙
20: end for
21: else if 𝛽 is 𝐹 (𝜙 ⊃ 𝑎) where 𝑎 ∈ 𝐻, 𝑎 ̸= 1 and 𝜙 is of the form
𝑝 (a propositional variable) or 𝜓 ∧ 𝜃 or 𝜓 ⊃ 𝜃 or □𝜓 then. . .
22: else if 𝛽 is 𝑇 (𝑎 ⊃ 𝜙) where 𝑎 ∈ 𝐻 and 𝜙 is of the form 𝜓 ∨ 𝜃 or ♢𝜓 then
23: for each 𝑡 ∈ 𝑚𝑎𝑥({𝑐 ∈ 𝐻 | 𝑎 ≰ 𝑐}) do
24: Create a new node 𝑛′ with 𝑈 (𝑛′ ) = (𝑤, 𝜎 ′ )𝐹 (𝜙 ⊃ 𝑡)
25: Extend B with 𝑛′
26: end for
27: else if 𝛽 is 𝑇 (𝜙 ⊃ 𝑎) where 𝑎 ∈ 𝐻 and 𝜙 is of the form 𝜓 ∧ 𝜃 or 𝜓 ⊃ 𝜃 or □𝜓 then. . .
28: else if 𝛽 is of the form 𝑇 (𝑎 ⊃ (𝜙 ∧ 𝜓)) for some truth value 𝑎 ̸= 0 then. . .
29: else if 𝛽 is of the form 𝐹 (𝑎 ⊃ (𝜙 ∧ 𝜓)) for some truth value 𝑎 ̸= 0 then. . .
30: else if 𝛽 is of the form 𝑇 ((𝜙 ∨ 𝜓) ⊃ 𝑎) for some truth value 𝑎 ̸= 1 then. . .
31: else if 𝛽 is of the form 𝐹 ((𝜙 ∨ 𝜓) ⊃ 𝑎) for some truth value 𝑎 ̸= 1 then. . .
32: else if 𝛽 is of the form 𝐹 (𝑎 ⊃ (𝜙 ⊃ 𝜓)) then
33: for each 𝑡 ∈ {𝑐 ∈ 𝐻 | 𝑐 ≤ 𝑎 and 𝑐 ̸= 0} do
34: Create nodes 𝑛′ and 𝑛′′ , with
𝑈 (𝑛′ ) = (𝑤, 𝜎 ′ )𝑇 (𝑡 ⊃ 𝜙) and 𝑈 (𝑛′′ ) = (𝑤, 𝜎 ′ )𝐹 (𝑡 ⊃ 𝜓)
35: Add 𝑛′ as a child of 𝑙 and 𝑛′′ as a child of 𝑛′
36: end for
37: else if 𝛽 is of the form 𝑇 (𝑎 ⊃ (𝜙 ⊃ 𝜓)) then
38: for each 𝑡 ∈ {𝑐 ∈ 𝐻 | 𝑐 ≤ 𝑎 and 𝑐 ̸= 0} do
39: Create nodes 𝑛′ and 𝑛′′ , with
𝑈 (𝑛′ ) = (𝑤, 𝜎 ′ )𝐹 (𝑡 ⊃ 𝜙) and 𝑈 (𝑛′′ ) = (𝑤, 𝜎 ′ )𝑇 (𝑡 ⊃ 𝜓)
40: if this is the first iteration of this for loop then
41: Add 𝑛′ and 𝑛′′ as children of 𝑙
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, 𝑈 )
Reactivate(𝑛)
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 ⊃ □𝑝 4 (𝑤0 , ∅)𝑇 ℎ ⊃ □𝑝
(︀ )︀ (︀ )︀
3 (𝑤0 , ∅)𝐹 1 ⊃ □♢𝑝 5 (𝑤0 , ∅)𝐹 ℎ ⊃ □♢𝑝
(︀ )︀ (︀ )︀ ..
6 (𝑤1 , {(𝑤0 , 𝑤1 , 1)})𝐹 1 ⊃ ♢𝑝 7 (𝑤1 , {(𝑤0 , 𝑤1 , ℎ)})𝐹 ℎ ⊃ ♢𝑝
.
(︀ )︀ (︀ )︀
8 (𝑤1 , {(𝑤0 , 𝑤1 , 1)})𝑇 1 ⊃ 𝑝 9 (𝑤1 , {(𝑤0 , 𝑤1 , ℎ)})𝑇 ℎ ⊃ 𝑝
(︀ )︀ ..
10 (𝑤1 , {(𝑤0 , 𝑤1 , 1)})𝑇 ♢𝑝 ⊃ ℎ
.
(︀ )︀
Figure 5.1: Labeled tree constructed during execution of constructTableau 𝐹 (1 ⊃ (□𝑝 ⊃ □♢𝑝))
Example 5.3. Assume ℋ = ℋ3 , and 𝜙 = □𝑝 ⊃ □♢𝑝. Then isValid(𝜙) returns false. Let us see why by
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
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 (T0 , 𝑈0 ) is set to the current state of (T, 𝑈 ).
The branch B01 containing only node 1 is a branch of T0 (Note, in this example we shall use B𝑖𝑗 to denote the
branch of tree T𝑖 with leaf node 𝑗). Node 1 is unfinished and clearly B01 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 = 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
(T, 𝑈 ).
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
B13 .
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.
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:
1
𝑤0 𝑤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 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).
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 𝑥 ∈ 𝐵𝑘 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 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 , ∅)𝛼}.
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 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
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
16
Not all such methods are equally efficient 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.
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ℋ = Λℱ . 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
finite. And since M𝑈 (B) is a counter model for 𝜙, we must have 𝜙 ∈/ Λℱ .
6. Tableau System for KBℋ
𝑑
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:
(𝑝KB𝐹 □𝑑 )
𝑋; (𝑤, 𝜎)𝐹 (𝑎 ⊃ □𝜙)
𝒩 ; (𝑣, 𝜎 ′ ∪ ... 𝒩 ; (𝑣, 𝜎 ′ ∪ ... 𝒩 ; (𝑣, 𝜎 ′ ∪ ... 𝒩 ; (𝑣, 𝜎 ′ ∪
𝑘1
{(𝑤, 𝑣, 𝑡1 ), (𝑣, 𝑤, 𝑡11 )}) {(𝑤, 𝑣, 𝑡1 ), (𝑣, 𝑤, 𝑡1 )}) {(𝑤, 𝑣, 𝑡𝑛 ), (𝑣, 𝑤, 𝑡1𝑛 )}) {(𝑤, 𝑣, 𝑡𝑛 ), (𝑣, 𝑤, 𝑡𝑘𝑛𝑛 )})
𝐹 (𝑎 ∧ 𝑡1 ⊃ 𝜙) 𝐹 (𝑎 ∧ 𝑡1 ⊃ 𝜙) 𝐹 (𝑎 ∧ 𝑡𝑛 ⊃ 𝜙) 𝐹 (𝑎 ∧ 𝑡𝑛 ⊃ 𝜙)
Where 𝑣 is any symbol of Σ that is not in 𝑤𝑜𝑟𝑙𝑑𝑠(𝒩 ), 𝑡1 , . . . , 𝑡𝑛 are all the ℋ-truth values s.t. 𝑎 ∧ 𝑡𝑖 ̸= 0, and for each 𝑖 ∈ {1, . . . , 𝑛},
{𝑡1𝑖 , . . . , 𝑡𝑘𝑖 𝑖 } = {𝑡 ∈ 𝐻 | 𝑑 ∧ 𝑡𝑖 = 𝑑 ∧ 𝑡}.
(𝑝KB𝐹 ♢𝑑 )
𝑋; (𝑤, 𝜎)𝐹 (♢𝜙 ⊃ 𝑎)
𝒩 ; (𝑣, 𝜎 ′ ∪ ... 𝒩 ; (𝑣, 𝜎 ′ ∪ ... 𝒩 ; (𝑣, 𝜎 ′ ∪ ... 𝒩 ; (𝑣, 𝜎 ′ ∪
{(𝑤, 𝑣, 𝑡1 ), (𝑣, 𝑤, 𝑡11 )}) {(𝑤, 𝑣, 𝑡1 ), (𝑣, 𝑤, 𝑡𝑘1 1 )}) {(𝑤, 𝑣, 𝑡𝑛 ), (𝑣, 𝑤, 𝑡1𝑛 )}) {(𝑤, 𝑣, 𝑡𝑛 ), (𝑣, 𝑤, 𝑡𝑘𝑛𝑛 )})
𝐹 (𝜙 ⊃ 𝑡1 ⇒ 𝑎) 𝐹 (𝜙 ⊃ 𝑡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𝑑 .
Proof. It suffices to show that each rule in 𝑝𝒞KBℋ ℋ ℋ
𝑑 preserves Symm𝑑 -satisfiability. Let 𝜌 ∈ 𝑝𝒞KB𝑑 and suppose
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.
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 ap-
plications 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ℋ 17
𝑑 has the finite frame property , and hence the finite model property.
Acknowledgments
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.
References
[1] M. Fitting, Many-valued modal logics, Fundamenta informaticae 15 (1991) 235–254.
17
In particular, KBℋ ℋ
𝑑 = Λℱ where ℱ is the class of all finite members of Symm𝑑 .
[2] M. Fitting, Many-Valued Modal Logics II, Fundamenta Informaticae 17 (1992) 55–73. URL: https://
content.iospress.com/articles/fundamenta-informaticae/fi17-1-2-05. doi:10.3233/FI-1992-171-205,
publisher: IOS Press.
[3] M. Fitting, Tableaus for many-valued modal logic, Studia Logica 55 (1995) 63–87. URL: https://doi.org/10.
1007/BF01053032. doi:10.1007/BF01053032.
[4] P. Blackburn, M. d. Rijke, Y. Venema, Modal Logic, Cambridge University Press, 2001.
[5] P. Blackburn, J. van Benthem, F. Wolter (Eds.), Handbook of Modal Logic, Elsevier, 2006.
[6] A. V. Chagrov, M. Zakharyaschev, Modal Logic, 1997.
[7] M. Fitting, How True It Is = Who Says It’s True, Studia Logica: An International Journal for Symbolic
Logic 91 (2009) 335–366. arXiv:40269042.
[8] M. Cerami, F. Esteva, Àngel García-Cerdaña, On the relationship between fuzzy description logics
and many-valued modal logics, International Journal of Approximate Reasoning 93 (2018) 372–394.
URL: https://www.sciencedirect.com/science/article/pii/S0888613X17306990. doi:https://doi.org/
10.1016/j.ijar.2017.11.006.
[9] F. Baader, I. Horrocks, U. Sattler, Description logics as ontology languages for the semantic web, in:
Mechanizing Mathematical Reasoning: Essays in Honor of Jörg H. Siekmann on the Occasion of His 60th
Birthday, Springer, 2005, pp. 228–248.
[10] W. Conradie, D. Della Monica, E. Muñoz-Velasco, G. Sciavicco, I. E. Stan, Fuzzy Halpern and Shoham’s
interval temporal logics, Fuzzy Sets and Systems (2022). URL: https://www.sciencedirect.com/science/
article/pii/S0165011422002068. doi:https://doi.org/10.1016/j.fss.2022.05.014.
[11] W. Conradie, A. Craig, A. Palmigiano, N. Wijnberg, Modelling competing theories, in: 2019 Conference
of the International Fuzzy Systems Association and the European Society for Fuzzy Logic and Technology
(EUSFLAT 2019), Atlantis Press, 2019/08. URL: https://doi.org/10.2991/eusflat-19.2019.100. doi:https:
//doi.org/10.2991/eusflat-19.2019.100.
[12] W. Conradie, A. Palmigiano, C. Robinson, A. Tzimoulis, N. Wijnberg, Modelling socio-political competi-
tion, Fuzzy Sets and Systems 407 (2021) 115–141.
[13] W. Conradie, S. Frittella, K. Manoorkar, S. Nazari, A. Palmigiano, A. Tzimoulis, N. M. Wijnberg, Rough
concepts, Information Sciences 561 (2021) 371–413.
[14] K. Segerberg, Some modal logics based on a three-valued logic, Theoria 33 (1967) 53–71. doi:10.1111/j.
1755-2567.1967.tb00610.x.
[15] S. K. Thomason, Possible worlds and many truth values, Studia Logica: An International Journal for
Symbolic Logic 37 (1978) 195–204. URL: http://www.jstor.org/stable/20014897.
[16] C. G. Morgan, Local and global operators and many-valued modal logics., Notre Dame Journal of Formal
Logic 20 (1979) 401–411.
[17] P. Ostermann, Many-valued modal propositional calculi, Mathematical Logic Quarterly 34 (1988) 343–354.
doi:10.1002/malq.19880340411.
[18] P. Ostermann, Many-valued modal logics: Uses and predicate calculus, Zeitschrift fur mathematische
Logik und Grundlagen der Mathematik 36 (1990) 367–376. doi:10.1002/malq.19900360411.
[19] C. D. Koutras, C. Nomikos, P. Peppas, Canonicity and Completeness Results for Many-Valued Modal
Logics, Journal of Applied Non-Classical Logics 12 (2002) 7–41. URL: https://www.tandfonline.com/doi/
abs/10.3166/jancl.12.7-41. doi:10.3166/jancl.12.7-41.
[20] G. Priest, Many-valued modal logics: A simple approach, The Review of Symbolic Logic 1 (2008) 190–203.
doi:10.1017/S1755020308080179.
[21] M. Fitting, Proof Methods for Modal and Intuitionistic Logics, Springer Netherlands, Dordrecht, 1983.
URL: http://link.springer.com/10.1007/978-94-017-2794-5. doi:10.1007/978-94-017-2794-5.
[22] W. Conradie, R. Monego, E. Muñoz Velasco, G. Sciavicco, I. E. Stan, A Sound and Complete Tableau
System for Fuzzy Halpern and Shoham’s Interval Temporal Logic, in: A. Artikis, F. Bruse, L. Hunsberger
(Eds.), 30th International Symposium on Temporal Representation and Reasoning (TIME 2023), volume
278 of Leibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl – Leibniz-Zentrum für
Informatik, Dagstuhl, Germany, 2023, pp. 9:1–9:14. URL: https://drops-dev.dagstuhl.de/entities/document/
10.4230/LIPIcs.TIME.2023.9. doi:10.4230/LIPIcs.TIME.2023.9.
[23] F. Bou, F. Esteva, L. Godo, Modal systems based on many-valued logics., in: EUSFLAT Conf.(1), 2007, pp.
177–182.
[24] F. Bou, F. Esteva, L. Godo, R. O. Rodríguez, On the minimum many-valued modal logic over a finite
residuated lattice, Journal of Logic and computation 21 (2011) 739–790.
[25] A. Vidal, On transitive modal many-valued logics, Fuzzy Sets Syst. 407 (2021) 97–114. URL: https:
//doi.org/10.1016/j.fss.2020.01.011. doi:10.1016/j.fss.2020.01.011.
[26] A. Vidal, Undecidability and non-axiomatizability of modal many-valued logics, The Journal of Symbolic
Logic 87 (2022) 1576–1605. doi:10.1017/jsl.2022.32.
[27] M. Takano, Subformula property in many-valued modal logics, The Journal of Symbolic Logic 59 (1994)
1263–1273.
[28] C. G. Fermüller, H. Langsteiner, Tableaux for finite-valued logics with arbitrary distribution modalities,
in: Automated Reasoning with Analytic Tableaux and Related Methods, Springer Berlin Heidelberg, 1998,
pp. 156–171.
[29] J. Sakalauskaiṫe, Tableaus with invertible rules for many-valued modal propositional logics, Lithuanian
Mathematical Journal 42 (2002) 191–203.
[30] R. Hahnle, Automated Deduction in Multiple-valued Logics, Oxford University Press, 1994. URL: https:
//doi.org/10.1093/oso/9780198539896.001.0001. doi:10.1093/oso/9780198539896.001.0001.
[31] M. D’Agostino, D. M. Gabbay, R. Hähnle, J. Posegga (Eds.), Handbook of Tableau Methods, Springer
Netherlands, Dordrecht, 1999. URL: http://link.springer.com/10.1007/978-94-017-1754-0. doi:10.1007/
978-94-017-1754-0.
[32] N. Bezhanishvili, D. de Jongh, Intuitionistic logic, 2006. URL: https://eprints.illc.uva.nl/id/eprint/200,
Lecture Notes.
[33] H. Rasiowa, R. Sikorski, The Mathematics of Metamathematics, Polish Scientific Publ., 1968.
[34] C. Britz, W. Conradie, W. Morton, Correspondence theory for many-valued modal logic, arXiv preprint
arXiv:2401.07894 (2024).
[35] E. W. Beth, The Foundations of Mathematics, North-Holland, Amsterdam, 1959.
[36] R. M. Smullyan, First-Order Logic, Springer, Berlin, Heidelberg, 1968. doi:10.1007/
978-3-642-86718-7.
[37] M. Fitting, Modal proof theory, in: P. Blackburn, J. Van Benthem, F. Wolter (Eds.), Studies in Logic and
Practical Reasoning, volume 3 of Handbook of Modal Logic, Elsevier, 2007, pp. 85–138. doi:10.1016/
S1570-2464(07)80005-X.
[38] D. König, Über eine schlussweise aus dem endlichen ins unendliche, Acta Sci. Math.(Szeged) 3 (1927)
121–130.