Fusions of One-Variable First-Order Modal Logics

Dmitry Shkatov; Frank Wolter; Roman Kontchakov

REVIEW 2 major objections 3 minor 35 references

Fusions of One-Variable First-Order Modal Logics

T0 review · 2 major / 3 minor · reviewed 2026-08-02 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read This paper proves that Kripke completeness and decidability transfer under fusions of equality-free one-variable first-order modal logics, for local and global consequence and for both expanding and constant domain semantics — and that addi

desk verdict Positive fusion transfer theorems are solid and new; the advertised non-preservation results for fusion with equality are not proven—they target the semantic product logic instead. read the letter →

arxiv 2603.04512 v3 pith:FYXLF6TR submitted 2026-03-04 cs.LO

Roman Kontchakov , Dmitry Shkatov , Frank Wolter This is my paper · ORCID

classification cs.LO MSC 03B4503B25

keywords one-variablefirst-ordermodallogicfusionKripkecompletenessdecidabilitylocalandglobalconsequencefinitemodelpropertyequalitynon-rigidconstantssharedS5modality

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper asks which good properties survive when two one-variable first-order modal logics are fused — combined without mixing axioms. It proves that, as long as equality is absent, Kripke completeness and decidability transfer for both local and global consequence and under both expanding and constant domain semantics; the finite model property transfers only in the local case. It also shows that once equality is admitted together with non-rigid constants — equivalently, the ability to count up to one — all positive transfer collapses: the fusion can become undecidable, via an encoding of Diophantine equations. A complementary result views one-variable logics as propositional modal logics sharing an S5 modality and gives a sufficient condition for transfer of completeness and decidability in that setting. These results matter because one-variable modal logics are a tractable middle ground between propositional modal logic and full first-order modal logic, and fusion is a standard modular way to build combined logics.

What carries the argument

The central device is the cactus model construction, lifted to one-variable first-order logic through quasimodels. A quasistate is a finite set of types — Boolean-consistent sets of subformulas — closed under existential witnesses, so a single finite object stands for arbitrarily many domain elements. Surrogate predicates isolate the two components: each factor replaces the other's maximal modal subformulas by fresh atoms. The fusion proof grafts one component's quasimodels onto the other's at 'thorn' worlds, alternating between the two accessibility relations, until a limit cactus is built whose runs are coherent and saturated for both modalities. For the harder local consequence case, the

What would settle it

Check property (†) on a concrete formula with mixed nesting, for example φ = 2_1 2_2 p ∧ 2_2 2_1 2_2 q with adp(φ) = adp_1(φ), and compute adp(Θ_1(φ)) against max{0, adp(φ)−1} and against adp_2(Θ_1(φ)); a single mismatch is a counterexample to the unproved observation that underpins local decidability.

Watch

Extended reading notes

Core claim

The central assertion is Theorem A: for Kripke complete one-variable first-order modal logics without equality, fusing any two preserves Kripke completeness and decidability of both the local and global consequence relations, under both expanding-domain and constant-domain semantics. The proof uses the cactus model construction lifted through quasimodels: each factor contributes a tapered model, the two are grafted along alternating accessibility relations, and truth of all relevant subformulas is preserved in the limit. The paper further establishes Theorem B: once equality and non-rigid constants are present, the transfer fails — decidability and recursive axiomatisability are not preserve

Load-bearing premise

The local decidability transfer rests on property (†) in Section 3.2, stated as an observation without proof: projecting a formula through Θ_i lowers its alternating modal depth by exactly one; if that fails for some formula shape, the recursive enumeration of quasistates in Lemma 3.6 need not terminate.

Editorial extensions

If this is right

Any two Kripke complete, decidable one-variable modal logics without equality can be fused, and the fusion remains Kripke complete and decidable for both local and global consequence, under expanding or constant domains.
Global reasoning in such fusions cannot in general be supported by finite models: for every nontrivial fusion the global finite model property fails, even when both factors have it; only local consequence retains the finite model property.
Equality plus non-rigid constants is a genuine threshold: decidability and recursive axiomatisability are not preserved, with undecidability coming from Diophantine equations.
For fusions of propositional modal logics sharing an S5 modality, Kripke completeness and decidability transfer under the sufficient condition that the components admit E-homogeneous models; semicommutators and expanding products with S5 satisfy this condition.
Because one-variable first-order logic without equality embeds as S5, the proof gives a method for fusing any two modal logics that share an S5 fragment, not just the first-order examples.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

Editorial inference: the paper's boundary suggests that the expressive ability to count up to one is what makes fusion unsafe; one could test whether one-variable logics with genuine counting quantifiers beyond one fail even more badly, perhaps by a similar Diophantine encoding.
Editorial inference: the E-homogeneous model condition is a reusable design pattern — any propositional modal logic that can be inflated so every formula occurs either nowhere or κ times inside each equivalence class can be fused safely; one could try verifying the condition for logics beyond semicommutators, such as graded modal logics.
Editorial inference: the sketched adaptation to monodic fragments over the two-variable fragment with counting suggests that decidability collapses once equality-rich base fragments are combined with modal layers; a full proof for the two-variable-with-counting monodic case would extend Theorem 4.6 beyond the sketch.
Editorial inference: the global finite model property failure for all nontrivial fusions means automated reasoning should target local consequence or develop non-finite bounded structures rather than expect small finite countermodels for global reasoning.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Here's the take: the positive half of this paper is genuinely new and looks correct; the negative half, as presented in the abstract and Theorem B, is not established by the body. The body proves that the semantically defined logic Log^=cd(D⊗Dfin) is undecidable, not that the syntactic fusion L1⊗L2 of two decidable logics is undecidable. Those are different objects.

On the positive side, the equality-free transfer theorems—completeness and decidability for local and global consequence, expanding and constant domains—are the first systematic treatment for one-variable first-order modal logics. The quasimodel/cactus construction is a real technical piece of work. The shared-S5 theorem (Theorem C) is also new and gives a clean sufficient condition, with the semicommutator applications. The Diophantine encoding itself is clever and shows something interesting about the product logic—but it lands on the wrong target.

The central issue is the gap between the abstract's claim and what is proven. For the syntactic fusion, you need to show either that the fusion is undecidable or that it is incomplete. Undecidability of the larger Log^=(C1⊗C2) doesn't imply undecidability of the subset L1⊗L2, and validity of ¬φ on the product doesn't imply derivability in the fusion without completeness. The paper needs to either prove those implications for these particular logics or restate the negative results honestly as non-preservation for the frame-class logic. This is not a cosmetic fix; it changes the main contribution.

A smaller concern: property (†) in Section 3.2 is stated as an observation, but the termination of the recursive enumeration for local decidability depends on it. It is plausible, but it should be proved rather than left to the reader. Some other proof details are compressed, consistent with the preliminary-report label.

Who benefits: modal logicians and description-logic people interested in combinations. The positive theorems deserve a place in the literature. The negative claims, as stated, would be a major result if proven for the fusion; right now they are overreach.

Recommendation: send to peer review, but the referee should require the authors to fix the negative statements. If they cannot, the paper can still be salvaged as a positive-transfer paper with a cautionary note about the semantic product.

Referee Report

2 major / 3 minor

Summary. This paper investigates preservation of Kripke completeness and decidability under fusions of one-variable first-order modal logics. In §3 the authors prove a positive transfer theorem for the equality-free case: if L1 and L2 are Kripke complete one-variable modal logics for frame classes C1, C2 closed under disjoint unions, then their fusion L1⊗L2 is Kripke complete for C1⊗C2 and decidable, for local and global consequence and expanding/constant domain semantics (Theorem 3.1, Lemmas 3.2 and 3.6). They also show the finite model property transfers only for local consequence (Theorems 3.5 and 3.10). In §4 they prove undecidability of the semantic product logic Log^=d(C1⊗C2) in several settings with equality and non-rigid constants, via encodings of Diophantine equations and Minsky machines, and state that this gives non-preservation for fusions with equality. §5 gives a sufficient condition for transfer in propositional fusions sharing an S5 modality using E-homogeneous models.

Significance. The equality-free positive theorem is a substantial result: it extends the classical fusion-transfer theorems to a first-order fragment, using a careful cactus/quasimodel construction. If the property (†) in §3.2 is proved, the decidability part is convincing. The non-preservation results in §4 are interesting as statements about product frame classes, but as written they do not establish the abstract's claim about fusions of logics. The §5 sufficient condition for S5-sharing fusions is a useful contribution and addresses a real problem. Overall, the paper contains valuable ideas but needs substantial revision of the negative claims.

major comments (2)

[§4 (Theorem 4.1, Corollary 4.2), Abstract] The abstract and Theorem B state that Kripke completeness and decidability are not preserved for fusions with equality. The formal results in Section 4, however, concern Log^=d(C1⊗C2), the set of formulas valid on the product frame class, not the syntactic fusion L1⊗L2 defined in §2. For Kripke complete components one always has L1⊗L2 ⊆ Log^=d(C1⊗C2); undecidability of the superset does not imply undecidability of the fusion, and non-recursive enumerability of the superset does not imply non-recursive enumerability of the subset. Corollary 4.2 states the conclusion for the mapping (Log^=d C1, Log^=d C2) ↦ Log^=d(C1⊗C2), which is not the fusion operation. Moreover, Log^=d(C1⊗C2) is Kripke complete by definition, so the claimed non-preservation of Kripke completeness does not follow from it either. Please either prove the non-preservation for the syntactic fusion or re-state the negative r
[§3.2, property (†)] The decidability of local consequence in Theorem 3.1 rests on the recursion in Lemma 3.6: membership in QQQ_i(ϕ) is decided by applying Lemma 3.6 to the Θ_i(ϕ)-quasistate realisations, and this requires adp(Θ_i(Φ)) = max{0,adp(Φ)-1} and adp(Θ_i(Φ)) = adp_{3-i}(Θ_i(Φ)). This is stated as 'Observe that' and no proof is supplied. It is load-bearing: if it fails for some formula shapes, the local decidability transfer collapses. Please give a formal proof of (†) and of the well-foundedness of the recursion, or show that the alternation-depth measure is well-defined.

minor comments (3)

[§5, Lemma 5.3] The proof omits the (i)⇒(iii) direction as 'similar to the one-variable case'. Since this implication is essential for completeness/decidability in Theorem 5.2, please spell out the construction of QQQ or give a precise pointer to the corresponding part of Lemma 3.2.
[§4, Theorem 4.6] Theorem 4.6 is stated as a theorem but only an informal sketch is given after it. Either provide the full reduction or explicitly label the statement as a conjecture/sketch.
[§3.2, Lemma 3.6] The notation '2≤md_i(ϕ)_i' in item (L3) is used without prior definition; please define the iterated box notation used here.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: the positive transfer proofs construct models from component completeness/decidability; the only explicitly flagged self-reference in QQQ_i(φ) is resolved by alternation-depth induction. The Section 4 semantic-vs-syntactic mismatch is a correctness/scope concern, not a circular reduction.

full rationale

Walking the derivation chain: Theorem A is proved via Lemma 3.2 (global consequence) and Lemma 3.6/Claim 3.9 (local consequence). Both lemmas are constructive and use only soundness of the fusion and Kripke completeness/decidability of the component logics Li for Ci, building the witnessing model on C1⊗C2 by grafting quasimodels/cacti. No step assumes that L1⊗L2 is already complete or decidable. The only place the paper itself raises circularity is the paragraph after Lemma 3.6: "while the definition of QQQ_i(ϕ) refers to ⊢ L1⊗L2 and thus may appear circular, by property (†), the Θ_i(ϕ)-formulas have smaller alternation depth, and so we can apply the criterion in Lemma 3.6 recursively... This recursion terminates as we eventually reach formulas of alternation depth 0, which, by definition, belong to either L_1 or L_2, where, by assumption, the consequence relation is decidable." That is a well-founded internal recursion on alternation depth, not a circular dependence on the target theorem; even if property (†) were unproved, that would be a correctness issue, not circularity. The cited quasimodel/cactus techniques ([16],[24]) are re-proved in the body, so they are not load-bearing self-citations; the decidable equality logics used in Section 4 are due to Hampson and Kurucz, not the present authors. The substantive caveat is in Section 4/Corollary 4.2: the undecidability theorem concerns Log=(C1⊗C2), the logic of the product frame class, whereas the fusion defined in §2 is the smallest syntactic logic containing L1∪L2. Since L1⊗L2 ⊆ Log=(C1⊗C2), undecidability of the larger set does not by itself establish undecidability of the syntactic fusion without the completeness transfer that is under investigation. This is a target-mismatch/correctness concern about the negative claims, not an equation reducing to itself or a fitted parameter renamed as a prediction. No circular step is therefore exhibited, and the circularity score is low.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

The paper relies on standard background results (S5 translation, decidability of specific logics, undecidability of Diophantine equations and Minsky machines) and established proof techniques (cactus/quasimodels). No new entities are postulated. The hypotheses of Theorem 3.1 (frame classes closed under disjoint unions) are explicit assumptions, not hidden axioms.

assumptions (5)

standard math The one-variable fragment of first-order logic without equality is equivalent to propositional modal logic S5 (Wajsberg).
Used in Lemma 2.1 and Section 5 to translate one-variable formulas into propositional formulas with a shared S5 modality.
domain assumption Log=cd D and Log=cd Dfin are decidable (Hampson 2018).
The undecidability counterexample in Theorem 4.1 depends on these known decidability results for the inequality modal logic over D and finite D.
standard math Solving Diophantine equations (polynomial equations with positive integer coefficients) is undecidable (Davis).
Theorem 4.1 reduces satisfiability in Log=cd(D⊗Dfin) to solving Diophantine equations.
standard math The halting problem for two-counter Minsky machines is undecidable.
Theorem 4.3 reduces global consequence to Minsky machine halting.
domain assumption The cactus model construction (Goranko & Passy) and quasimodel technique (Kurucz et al.) are sound for one-variable modal logics.
The positive transfer proof of Theorem 3.1 is built on these constructions; the paper does not reprove their soundness.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Fusions of One-Variable First-Order Modal Logics." pith.science (2026). https://pith.science/paper/FYXLF6TR

@misc{pith2026260304512,
  author       = {Pith},
  title        = {Pith review of: Fusions of One-Variable First-Order Modal Logics},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/FYXLF6TR}},
  note         = {Machine review of arXiv:2603.04512}
}

read the original abstract

We investigate preservation results for the independent fusion of one-variable first-order modal logics. We show that, without equality, Kripke completeness and decidability of global and local consequence relations are preserved, under both expanding and constant domain semantics. By contrast, Kripke completeness and decidability are not preserved for fusions with equality and non-rigid constants (or, equivalently, counting up to one), again for the global and local consequence and under both expanding and constant domain semantics. This result is shown by encoding Diophantine equations. Even without equality, the finite model property is preserved only in the local case. Finally, we view fusions of one-variable modal logics as fusions of propositional modal logics sharing an S5 modality and provide a general sufficient condition for transfer of Kripke completeness and decidability (but not of finite model property).

Figures

Figures reproduced from arXiv: 2603.04512 by the authors.

**Figure 2.** a) Formula card(I,P). b) Equation e of the form y = z1 ×z2 with z1 = 3 and z2 = 2. If e is of the form y = z1+z2, then we introduce two unary predicates Q e 1 and Q e 2 and, for both i = 1,2, add formula card(Izi ,Q e i ), which ensures |Pzi |wi = |Q e i |wi at the world wi ∈ W marked with Izi . Next, we state that Q e 1 and Q e 2 are disjoint at all worlds w ∈ W and empty at worlds w ∈ W where the respective Izi do… view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

35 extracted references · 12 canonical work pages

[1]

Decidability in First-Order Modal Logic with Non-Rigid Constants and Definite Descriptions

Alessandro Artale, Christopher Hampson, Roman Kontchakov, Andrea Mazzullo & Frank Wolter (2025): Decidability in First-Order Modal Logic with Non-Rigid Constants and Definite Descriptions.CoRR abs/2509.08165, doi:10.48550/arXiv.2509.08165. arXiv:2509.08165

work page Pith review arXiv doi:10.48550/arxiv.2509.08165 2025
[2]

Comput.204(10), pp

Franz Baader, Silvio Ghilardi & Cesare Tinelli (2006):A new combination procedure for the word prob- lem that generalizes fusion decidability results in modal logics.Inf. Comput.204(10), pp. 1413–1452, doi:10.1016/J.IC.2005.05.009

work page doi:10.1016/j.ic.2005.05.009 2006
[3]

Cambridge University Press

Franz Baader, Ian Horrocks, Carsten Lutz & Ulrike Sattler (2017):An Introduction to Description Logic. Cambridge University Press. R. Kontchakov, D. Shkatov & F. Wolter23

2017
[4]

Franz Baader, Carsten Lutz, Holger Sturm & Frank Wolter (2002):Fusions of Description Logics and Ab- stract Description Systems.J. Artif. Intell. Res.16, pp. 1–58, doi:10.1613/JAIR.919

work page doi:10.1613/jair.919 2002
[5]

To appear

Guram Bezhanishvili & Mher Khan (2026):The Monadic Grzegorczyk Logic.Annals of Pure and Applied Logic. To appear

2026
[6]

Fredrik Dahlqvist & Dirk Pattinson (2011):On the Fusion of Coalgebraic Logics. In:Proc. of the 4th Int. Conf. on Algebra and Coalgebra in Computer Science (CALCO 2011),Lecture Notes in Computer Science 6859, Springer, pp. 161–175, doi:10.1007/978-3-642-22944-2_12

work page doi:10.1007/978-3-642-22944-2_12 2011
[7]

In Jon Barwise, editor:Handbook of Mathematical Logic, North-Holland, Amsterdam, pp

Martin Davis (1977):Unsolvable Problems. In Jon Barwise, editor:Handbook of Mathematical Logic, North-Holland, Amsterdam, pp. 567–594

1977
[8]

147–156, doi:10.1023/A:1021352309671

Anatoli Degtyarev, Michael Fisher & Alexei Lisitsa (2002):Equality and Monodic First-Order Temporal Logic.Stud Logica72(2), pp. 147–156, doi:10.1023/A:1021352309671

work page doi:10.1023/a:1021352309671 2002

Show all 35 references

[9]

Kit Fine & Gerhard Schurz (1996):Transfer Theorems for Multimodal Logics. In B. Jack Copeland, editor: Logic and Reality: Essays on the Legacy of Arthur Prior, Oxford University Press, pp. 169–213

1996
[10]

Gabbay (2003):Fibred Semantics and the Weaving of Logics

Dov M. Gabbay (2003):Fibred Semantics and the Weaving of Logics. In D. M. Gabbay & F. Guenthner, editors:Handbook of Philosophical Logic, 10, Kluwer, pp. 1–76

2003
[11]

Gabbay & Valentin B

Dov M. Gabbay & Valentin B. Shehtman (1998):Products of Modal Logics, Part 1.Log. J. IGPL6(1), pp. 73–146, doi:10.1093/JIGPAL/6.1.73

1998 doi
[12]

Pure Appl

David Gabelaia, Agi Kurucz, Frank Wolter & Michael Zakharyaschev (2006):Non-primitive recursive de- cidability of products of modal logics with expanding domains.Ann. Pure Appl. Log.142(1-3), pp. 245–268, doi:10.1016/J.APAL.2006.01.001

2006 doi
[13]

Silvio Ghilardi, Enrica Nicolini & Daniele Zucchelli (2008):A comprehensive combination framework.ACM Trans. Comput. Log.9(2), pp. 8:1–8:54, doi:10.1145/1342991.1342992

2008
[14]

Silvio Ghilardi & Luigi Santocanale (2003):Algebraic and Model Theoretic Techniques for Fusion Decid- ability in Modal Logics. In:Proc. of the 10th Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2003),Lecture Notes in Computer Science2850, Sp...

2003 doi
[15]

Center for the Study of Language and Information

Robert Goldblatt (1987):Logics of time and computation. Center for the Study of Language and Information

1987
[16]

Valentin Goranko & Solomon Passy (1992):Using the Universal Modality: Gains and Questions.J. Log. Comput.2(1), pp. 5–30, doi:10.1093/LOGCOM/2.1.5

1992 doi
[17]

Christopher Hampson (2016):Two-dimensional modal logics with difference relations. Ph.D. thesis, King’s College London, UK. Available athttps://kclpure.kcl.ac.uk/portal/en/studentTheses/ two-dimensional-modal-logics-with-difference-relations/

2016
[18]

In: Proc

Christopher Hampson (2018):The Bimodal Logic of Commuting Difference Operators Is Decidable. In: Proc. of the 12th Conf.ón Advances in Modal Logic (AiML 2018), College Publications, pp. 311–326. Avail- able athttp://www.aiml.net/volumes/volume12/Hampson.pdf

2018
[19]

Christopher Hampson & Agi Kurucz (2015):Undecidable Propositional Bimodal Logics and One-Variable First-Order Linear Temporal Logics with Counting.ACM Trans. Comput. Log.16(3), pp. 27:1–27:36, doi:10.1145/2757285

2015 doi
[20]

Marcus Kracht & Frank Wolter (1991):Properties of Independently Axiomatizable Bimodal Logics.J. Symb. Log.56(4), pp. 1469–1485, doi:10.2307/2275487

1991 doi
[21]

Marcus Kracht & Frank Wolter (1999):Normal Monomodal Logics Can Simulate All Others.J. Symb. Log. 64(1), pp. 99–138, doi:10.2307/2586754

1999 doi
[22]

In Patrick Blackburn, Johan van Benthem & Frank Wolter, editors:Handbook of Modal Logic, Elsevier, pp

Agi Kurucz (2007):Combining Modal Logics. In Patrick Blackburn, Johan van Benthem & Frank Wolter, editors:Handbook of Modal Logic, Elsevier, pp. 869–924

2007
[23]

Methods Comput

Agi Kurucz, Frank Wolter & Michael Zakharyaschev (2025):Deciding the Existence of Interpolants and Def- initions in First-Order Modal Logic.Log. Methods Comput. Sci.21(4), doi:10.46298/LMCS-21(4:6)2025. 24Fusions of One-Variable First-Order Modal Logics

2025 doi
[24]

Gabbay (2003):Many-Dimensional Modal Logics: Theory and Applications.Studies in Logic and the Foundations of Mathematics148, North Holland, Amsterdam

Agi Kurucz, Frank Wolter, Michael Zakharyaschev & Dov M. Gabbay (2003):Many-Dimensional Modal Logics: Theory and Applications.Studies in Logic and the Foundations of Mathematics148, North Holland, Amsterdam

2003
[25]

Minsky (1967):Finite and Infinite Machines

M. Minsky (1967):Finite and Infinite Machines. Prentice-Hall

1967
[26]

Ian Pratt-Hartmann (2005):Complexity of the Two-Variable Fragment with Counting Quantifiers.J. Log. Lang. Inf.14(3), pp. 369–395, doi:10.1007/S10849-005-5791-1

2005 doi
[27]

Maarten de Rijke (1992):The Modal Logic of Inequality.J. Symb. Log.57(2), pp. 566–584, doi:10.2307/2275293

1992 doi
[28]

In: Proc

Valentin Shehtman & Dmitry Shkatov (2019):On one-variable fragments of modal predicate logics. In: Proc. of SYSMICS 2019, ILLC, University of Amsterdam, pp. 129–132

2019
[29]

Mathematics108(2), pp

Valentin Shehtman & Dmitry Shkatov (2023):Semiproducts, Products, and Modal Predicate Logics: Some Examples.Doklady. Mathematics108(2), pp. 411–418

2023
[30]

Advances in Modal Logic 2024, Short Papers, pp

Valentin Shehtman & Dmitry Shkatov (2024):Fusions of Canonical Predicate Modal Logics Are Canonical. Advances in Modal Logic 2024, Short Papers, pp. 51–56

2024
[31]

Thomason (1980):Independent Propositional Modal Logics.Studia Logica39, pp

Stephen K. Thomason (1980):Independent Propositional Modal Logics.Studia Logica39, pp. 143–144, doi:10.1007/BF00370317

1980 doi
[32]

Wajsberg (1933):Ein erweiterter Klassenkalkül.Monatshefte für Mathematik und Physik40, pp

M. Wajsberg (1933):Ein erweiterter Klassenkalkül.Monatshefte für Mathematik und Physik40, pp. 113– 126

1933
[33]

Frank Wolter (1996):Fusions of Modal Logics Revisited. In:Proc. of the 1st Workshop on Advances in Modal Logic (AiML 1996), CSLI Publications, pp. 361–379

1996
[34]

In Ernest Sosa, editor:The Philosophy of Nicholas Rescher, D

Georg Henrik von Wright (1979):A Modal Logic of Place. In Ernest Sosa, editor:The Philosophy of Nicholas Rescher, D. Reidel, Dordrecht, pp. 65–73

1979
[35]

Alberto Zanardo, Amílcar Sernadas & Cristina Sernadas (2001):Fibring: Completeness Preservation.J. Symb. Log.66(1), pp. 414–439, doi:10.2307/2694931

2001 doi

Pith tools

Reviewed August 2, 2026 · model on record in the stance chip above.

[1] [1]

Decidability in First-Order Modal Logic with Non-Rigid Constants and Definite Descriptions

Alessandro Artale, Christopher Hampson, Roman Kontchakov, Andrea Mazzullo & Frank Wolter (2025): Decidability in First-Order Modal Logic with Non-Rigid Constants and Definite Descriptions.CoRR abs/2509.08165, doi:10.48550/arXiv.2509.08165. arXiv:2509.08165

work page Pith review arXiv doi:10.48550/arxiv.2509.08165 2025

[2] [2]

Comput.204(10), pp

Franz Baader, Silvio Ghilardi & Cesare Tinelli (2006):A new combination procedure for the word prob- lem that generalizes fusion decidability results in modal logics.Inf. Comput.204(10), pp. 1413–1452, doi:10.1016/J.IC.2005.05.009

work page doi:10.1016/j.ic.2005.05.009 2006

[3] [3]

Cambridge University Press

Franz Baader, Ian Horrocks, Carsten Lutz & Ulrike Sattler (2017):An Introduction to Description Logic. Cambridge University Press. R. Kontchakov, D. Shkatov & F. Wolter23

2017

[4] [4]

Franz Baader, Carsten Lutz, Holger Sturm & Frank Wolter (2002):Fusions of Description Logics and Ab- stract Description Systems.J. Artif. Intell. Res.16, pp. 1–58, doi:10.1613/JAIR.919

work page doi:10.1613/jair.919 2002

[5] [5]

To appear

Guram Bezhanishvili & Mher Khan (2026):The Monadic Grzegorczyk Logic.Annals of Pure and Applied Logic. To appear

2026

[6] [6]

Fredrik Dahlqvist & Dirk Pattinson (2011):On the Fusion of Coalgebraic Logics. In:Proc. of the 4th Int. Conf. on Algebra and Coalgebra in Computer Science (CALCO 2011),Lecture Notes in Computer Science 6859, Springer, pp. 161–175, doi:10.1007/978-3-642-22944-2_12

work page doi:10.1007/978-3-642-22944-2_12 2011

[7] [7]

In Jon Barwise, editor:Handbook of Mathematical Logic, North-Holland, Amsterdam, pp

Martin Davis (1977):Unsolvable Problems. In Jon Barwise, editor:Handbook of Mathematical Logic, North-Holland, Amsterdam, pp. 567–594

1977

[8] [8]

147–156, doi:10.1023/A:1021352309671

Anatoli Degtyarev, Michael Fisher & Alexei Lisitsa (2002):Equality and Monodic First-Order Temporal Logic.Stud Logica72(2), pp. 147–156, doi:10.1023/A:1021352309671

work page doi:10.1023/a:1021352309671 2002