pith. sign in

arxiv: 2604.18403 · v1 · submitted 2026-04-20 · 💻 cs.LO · math.LO

Nested Sequents for Horn-Characterizable Quantified Modal Logics with Equality via Reachability Rules

Tim S. Lyon , Eugenio Orlandelli This is my paper

Pith reviewed 2026-05-10 03:19 UTC · model grok-4.3

classification 💻 cs.LO math.LO
keywords nested sequentsquantified modal logicsreachability rulessemi-Thue systemsHorn conditionsinner domainsouter domainscut-elimination
0
0 comments X

The pith

Cut-free nested sequent systems with signatures and reachability rules provide sound and complete proof systems for quantified modal logics featuring both inner and outer domains.

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

This paper develops the first cut-free nested sequent calculi for quantified modal logics whose semantics rely on models that assign both an inner domain and an outer domain to each world. The systems extend ordinary nested sequents by adding signatures as multisets of terms and introduce reachability rules that rely on semi-Thue systems to move formulas or terms along paths in the sequent structure. These parameterized rules enforce a range of domain conditions such as increasing, decreasing, constant, or empty domains together with frame properties including seriality and general path conditions. A reader would care because the calculi come with proofs of admissible structural rules, rule invertibility, and syntactic cut-elimination, while also showing that the ordinary universal quantifier rule already captures constant outer domains.

Core claim

The authors show that nested sequents augmented with term signatures and reachability rules parameterized by semi-Thue systems yield sound and complete cut-free systems for Horn-characterizable quantified modal logics with equality. The models interpret formulas over relational structures that give each world both an inner domain of existing objects and an outer domain of possible objects, and the reachability rules propagate or consume terms and formulas along grammar-generated paths to enforce the required monotonicity and path conditions.

What carries the argument

Reachability rules parameterized by semi-Thue systems, which propagate or consume formulae or terms along paths within nested sequents that are encoded as strings generated by the grammar.

If this is right

  • Structural rules such as weakening, contraction, and exchange are admissible in the systems.
  • Every rule is invertible.
  • A syntactic cut-elimination theorem holds.
  • The standard universal quantifier rule subsumes the Extended Barcan Rule and forces constant outer domains.
  • The systems cover logics with increasing, decreasing, constant, and empty domains as well as seriality and path conditions.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The grammar parameterization may extend to logics whose conditions lie outside the Horn fragment by suitable choice of semi-Thue systems.
  • The use of signatures opens a route to uniform treatment of equality and term existence in other sequent-style calculi for modal logics.
  • Proof-search procedures built on these rules could support automated reasoning tools for quantified modal statements with domain restrictions.
  • Similar reachability mechanisms might connect nested sequents to hypersequent or display systems for the same class of logics.

Load-bearing premise

That reachability rules based on semi-Thue systems can encode every Horn-characterizable frame condition and domain property while keeping the systems cut-free and complete.

What would settle it

A Horn condition on frames or domains for which no semi-Thue system yields a sound and complete nested sequent system under the given semantics with inner and outer domains.

Figures

Figures reproduced from arXiv: 2604.18403 by Eugenio Orlandelli, Tim S. Lyon.

Figure 1
Figure 1. Figure 1: Axiom System HQ◦ =.K for Q ◦ =.K. Remark 2.6. Observe that if M, w, σ ⊩ Et, then σ(t) ∈ Dw, that is, if the existence predicate holds of a term t at a world w, then its interpretation is in the inner domain of w. We say that a model M = ⟨W, R, U, D, I⟩ is connected iff for any two worlds w, u ∈ W there exists a (potentially undirected) R-path connecting w to u. The following proposition will be useful in t… view at source ↗
Figure 2
Figure 2. Figure 2: Additional frame/domain conditions and their corresponding axioms. We note [PITH_FULL_IMAGE:figures/full_fig_p008_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: The nested system NQ◦ =.K(C) with C a set of frame conditions. Frame Conditions in C Corresponding Additional Side Conditions for dp ID ∈ C, but DD ̸∈ C †3 (C) := “w L⇝ u with L := LS4∪S(G)(R).” DD ∈ C, but ID ̸∈ C †3 (C) := “w L⇝ u with L := LS4∪S(G)(R¯).” ID, DD ∈ C †3 (C) := “w L⇝ u with L := LS5(G)(R).” [PITH_FULL_IMAGE:figures/full_fig_p013_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: The side condition †3 (C) for dp. one bottom-up introduce any term to a component of a nested sequent; this corresponds to the fact that all terms are interpreted in all domains of a model satisfying classical domains. Note that the ∀ and nd rules are subject to a freshness condition, that is, the variable y must be fresh in any application of the rule, i.e., y cannot occur free in the conclusion of a rule… view at source ↗
Figure 5
Figure 5. Figure 5: A diagram depicting which (hp-)admissibility (and hp-invertibility) results are [PITH_FULL_IMAGE:figures/full_fig_p018_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Height-preserving admissible rules in NQ◦ =.K(C). The shift rule sft(C) is a novel contribution of this paper and is interesting as it uniformly captures reasoning with generalized path conditions in a single rule.3 This is advantageous as it does not require one to introduce a special structural rule for each individual generalized path condition, as is the approach in other settings [4, 27] and which req… view at source ↗
read the original abstract

We introduce cut-free nested sequent systems for a broad class of quantified modal logics (QMLs). The QMLs we consider are semantically defined using relational models that assign both an inner and outer domain to each world. This rich model structure enables the specification of various QMLs by enforcing different frame conditions, including increasing, decreasing, constant, and empty domains, as well as general path conditions and seriality. We extend the usual notion of nested sequent to include signatures, i.e., multisets of terms, which let us naturally define rules capturing the aforementioned domain conditions. A distinctive feature of our nested sequent systems is the use of reachability rules--inference rules parameterized by formal grammars (viz., semi-Thue systems). These rules operate by propagating or consuming formulae or terms along certain paths within a nested sequent, where paths are encoded as strings generated by a parameterizing grammar. This paper is the first to provide sound and complete nested systems for QMLs semantically characterized by models using both inner and outer domains. We analyze the proof-theoretic properties of these systems, identify a number of admissible structural rules, establish the invertibility of all rules, and prove a non-trivial syntactic cut-elimination theorem. We also observe that the standard universal quantifier rule used in nested systems subsumes the Extended Barcan Rule, which forces nested systems to capture QMLs with constant outer domains.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The manuscript introduces cut-free nested sequent systems for quantified modal logics (QMLs) semantically characterized by relational models with both inner and outer domains. Signatures (multisets of terms) are added to nested sequents to capture domain conditions (increasing, decreasing, constant, empty), while reachability rules parameterized by semi-Thue systems propagate formulae and terms along grammar-generated paths to handle Horn-characterizable frame conditions such as seriality and general path conditions. The systems are claimed to be sound and complete for this class, with admissible structural rules, invertible rules, and a syntactic cut-elimination theorem; the paper asserts it is the first to provide such nested systems for inner/outer domain semantics and notes that the standard universal quantifier rule subsumes the Extended Barcan Rule.

Significance. If the soundness, completeness, and cut-elimination results hold, the work offers a uniform and modular proof-theoretic treatment of a wide range of QMLs with varying domain and frame properties, extending nested sequent methodology in a novel way via grammar-parameterized reachability rules. This is a clear strength for the field, as it avoids ad-hoc rules for each logic while preserving cut-freeness. The syntactic cut-elimination theorem and the observation on the universal quantifier rule are particularly valuable contributions that could support further developments in automated reasoning for quantified modal logics.

minor comments (2)
  1. The introduction would benefit from a short comparison (perhaps in a table) with prior nested sequent systems for QMLs to more explicitly highlight the novelty of signatures and reachability rules.
  2. A brief reminder or reference to the definition of Horn conditions and semi-Thue systems in the preliminaries section would help readers from outside formal language theory.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive and accurate summary of our manuscript, as well as for recommending minor revision. The referee correctly identifies the core contributions: the first cut-free nested sequent systems for Horn-characterizable QMLs with inner/outer domains and equality, using signatures and grammar-parameterized reachability rules, along with the syntactic cut-elimination result and the observation on the universal quantifier rule subsuming the Extended Barcan Rule.

Circularity Check

0 steps flagged

No significant circularity in derivation chain

full rationale

The paper constructs its nested sequent systems directly from standard relational semantics using inner and outer domains, extending nested sequents with signatures and reachability rules parameterized by semi-Thue systems to capture domain conditions and Horn frame properties. All core results on soundness, completeness, cut-elimination, admissibility, and invertibility are established syntactically from the rule definitions and semantic correspondence without reducing any prediction or theorem to a fitted parameter, self-referential definition, or load-bearing self-citation. The universal quantifier rule subsuming the Extended Barcan Rule is derived from the system design rather than assumed. The derivation remains self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claims rest on standard definitions of relational models with inner and outer domains plus the assumption that frame conditions are Horn-characterizable; no free parameters or invented entities are introduced beyond the new rule mechanisms.

axioms (2)
  • domain assumption Relational models assign inner and outer domains to each world
    This is the semantic foundation stated in the abstract for defining the class of QMLs.
  • domain assumption Frame conditions are Horn-characterizable
    The logics considered are restricted to those whose conditions can be captured via the reachability rules.

pith-pipeline@v0.9.0 · 5560 in / 1359 out tokens · 52583 ms · 2026-05-10T03:19:44.357914+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

41 extracted references · 18 canonical work pages

  1. [1]

    The method of hypersequents in the proof theory of propositional non- classical logics

    Arnon Avron. The method of hypersequents in the proof theory of propositional non- classical logics. In Wilfrid Hodges, Martin Hyland, Charles Steinhorn, and John Truss, 28 editors,Logic: From Foundations to Applications: European Logic Colloquium, page 1–32. Clarendon Press, USA, 1996. ISBN 0198538626

    1996

  2. [2]

    Nuel D. Belnap. Display logic.Journal of Philosophical Logic, 11:375–417, 1982. URL https://doi.org/10.1007/BF00284976

    work page doi:10.1007/bf00284976 1982

  3. [3]

    First-order modal logic

    Torben Bra¨ uner and Silvio Ghilardi. First-order modal logic. In Patrick Blackburn, Jo- han Van Benthem, and Frank Wolter, editors,Handbook of Modal Logic, volume 3 ofStudies in Logic and Practical Reasoning, pages 549–620. Elsevier, 2007. doi: https://doi.org/10.1016/S1570-2464(07)80012-7

    work page doi:10.1016/s1570-2464(07)80012-7 2007

  4. [4]

    Deep sequent systems for modal logic.Archive for Math- ematical Logic, 48(6):551–577, 2009

    Kai Br¨ unnler. Deep sequent systems for modal logic.Archive for Mathematical Logic, 48(6):551–577, 2009. doi: 10.1007/s00153-009-0137-3

    work page doi:10.1007/s00153-009-0137-3 2009

  5. [5]

    Robert A. Bull. Cut elimination for propositional dynamic logic without *.Mathematical Logic Quarterly, 38(1):85–100, 1992. doi: 10.1002/malq.19920380107

    work page doi:10.1002/malq.19920380107 1992

  6. [6]

    Lyon, Revantha Ramanayake, and Alwen Tiu

    Agata Ciabattoni, Tim S. Lyon, Revantha Ramanayake, and Alwen Tiu. Display to labeled proofs and back again for tense logics.ACM Transactions on Computational Logic, 22(3):1–31, 2021. doi: https://doi.org/10.1145/3460492

    work page doi:10.1145/3460492 2021

  7. [7]

    A unified completeness theorem for quantified modal logics.The Journal of Symbolic Logic, 67(4):1483–1510, 2002

    Giovanna Corsi. A unified completeness theorem for quantified modal logics.The Journal of Symbolic Logic, 67(4):1483–1510, 2002. ISSN 00224812

    2002

  8. [8]

    Tableau methods of proof for modal logics.Notre Dame Journal of Formal Logic, 13(2):237–247, 1972

    Melvin Fitting. Tableau methods of proof for modal logics.Notre Dame Journal of Formal Logic, 13(2):237–247, 1972

    1972

  9. [9]

    Nested sequents for intuitionistic logics.Notre Dame Journal of Formal Logic, 55(1):41–61, 2014

    Melvin Fitting. Nested sequents for intuitionistic logics.Notre Dame Journal of Formal Logic, 55(1):41–61, 2014

    2014

  10. [10]

    Modal interpolation via nested sequents,

    Melvin Fitting and Roman Kuznets. Modal interpolation via nested sequents.Annals of pure and applied logic, 166(3):274–305, 2015. doi: 10.1016/j.apal.2014.11.002

    work page doi:10.1016/j.apal.2014.11.002 2015

  11. [11]

    Mendelsohn.First-Order Modal Logic, 2nd edition

    Melvin Chris Fitting and Richard L. Mendelsohn.First-Order Modal Logic, 2nd edition. Cham: Springer, 2023

    2023

  12. [12]

    Untersuchungen ¨ uber das logische schließen

    Gerhard Gentzen. Untersuchungen ¨ uber das logische schließen. i.Mathematische Zeitschrift, 39(1):176–210, 1935

    1935

  13. [13]

    Untersuchungen ¨ uber das logische schließen

    Gerhard Gentzen. Untersuchungen ¨ uber das logische schließen. ii.Mathematische Zeitschrift, 39(1):405–431, 1935

    1935

  14. [14]

    Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents

    Rajeev Gor´ e, Linda Postniece, and Alwen Tiu. Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents. In Carlos Areces and Robert Goldblatt, editors,Advances in Modal Logic 7, pages 43–66. College Publications, London, 2008

    2008

  15. [15]

    On the correspondence between display postulates and deep inference in nested sequent calculi for tense logics.Logical Methods in Computer Science, 7(2), 2011

    Rajeev Gor´ e, Linda Postniece, and Alwen Tiu. On the correspondence between display postulates and deep inference in nested sequent calculi for tense logics.Logical Methods in Computer Science, 7(2), 2011. doi: 10.2168/LMCS-7(2:8)2011. 29

    work page doi:10.2168/lmcs-7(2:8)2011 2011

  16. [16]

    Tree-sequent methods for subintuitionistic predicate logics

    Ryo Ishigaki and Kentaro Kikuchi. Tree-sequent methods for subintuitionistic predicate logics. In Nicola Olivetti, editor,Automated Reasoning with Analytic Tableaux and Related Methods, volume 4548 ofLecture Notes in Computer Science, pages 149–164. Springer, Berlin, Heidelberg, 2007

    2007

  17. [17]

    Cut-free sequent calculi for some tense logics.Studia Logica, 53(1): 119–135, 1994

    Ryo Kashima. Cut-free sequent calculi for some tense logics.Studia Logica, 53(1): 119–135, 1994

    1994

  18. [18]

    Saul A. Kripke. A completeness theorem in modal logic.Journal of Symbolic Logic, 24 (1):1–14, 1959. doi: 10.2307/2964568

    work page doi:10.2307/2964568 1959

  19. [19]

    Proof theoretic methodology for propositional dynamic logic

    Daniel Leivant. Proof theoretic methodology for propositional dynamic logic. In J. D´ ıaz and I. Ramos, editors,Formalization of Programming Concepts, pages 356–373. Springer, Berlin, Heidelberg, 1981

    1981

  20. [20]

    Springer International Publishing, Cham, 2024

    Bj¨ orn Lellmann and Francesca Poggiolesi. Nested sequents or tree-hypersequents—a survey. In Yale Weiss and Romina Birman, editors,Saul Kripke on Modal Logic, pages 243–301. Springer International Publishing, Cham, 2024. ISBN 978-3-031-57635-5. doi: 10.1007/978-3-031-57635-5 11

    work page doi:10.1007/978-3-031-57635-5 2024

  21. [21]

    On the Correspondence between Nested Calculi and Semantic Systems for Intuitionistic Logics.Journal of Logic and Computation, 31(1):213–265, 12 2020

    Tim Lyon. On the Correspondence between Nested Calculi and Semantic Systems for Intuitionistic Logics.Journal of Logic and Computation, 31(1):213–265, 12 2020. ISSN 0955-792X. doi: 10.1093/logcom/exaa078

    work page doi:10.1093/logcom/exaa078 2020

  22. [22]

    Lyon.Refining Labelled Systems for Modal and Constructive Logics with Appli- cations

    Tim S. Lyon.Refining Labelled Systems for Modal and Constructive Logics with Appli- cations. PhD thesis, Technische Universit¨ at Wien, 2021

    2021

  23. [23]

    Tim S. Lyon. Nested sequents for intermediate logics: The case of G¨ odel- Dummett logics.Journal of Applied Non-Classical Logics, 33(2):121–164, 2023. doi: 10.1080/11663081.2023.2233346

    work page doi:10.1080/11663081.2023.2233346 2023

  24. [24]

    Tim S. Lyon. Unifying sequent systems for G¨ odel-L¨ ob provability logic via syntactic transformations. In J¨ org Endrullis and Sylvain Schmitz, editors,33rd EACSL An- nual Conference on Computer Science Logic (CSL 2025), volume 326 ofLeibniz In- ternational Proceedings in Informatics (LIPIcs), pages 42:1–42:23. Schloss Dagstuhl – Leibniz-Zentrum f¨ ur I...

    2025

  25. [25]

    Lyon and Luc´ ıa G´ omez ´Alvarez

    Tim S. Lyon and Luc´ ıa G´ omez ´Alvarez. Automating reasoning with standpoint logic via nested sequents. InProceedings of the 19th International Conference on Principles of Knowledge Representation and Reasoning, pages 257–266, 8 2022. doi: 10.24963/kr.2022/26

    work page doi:10.24963/kr.2022/26 2022

  26. [26]

    Lyon and Jonas Karge

    Tim S. Lyon and Jonas Karge. Constructive interpolation and concept-based beth definability for description logics via sequents. InProceedings of the Thirty-Third In- ternational Joint Conference on Artificial Intelligence (IJCAI 2024), pages 3484–3492. ijcai.org, 2024. URLhttps://www.ijcai.org/proceedings/2024/386. 30

    2024

  27. [27]

    Das and S

    Tim S. Lyon and Eugenio Orlandelli. Nested sequents for quantified modal logics. In Automated Reasoning with Analytic Tableaux and Related Methods: 32nd International Conference (TABLEAUX 2023), Proceedings, page 449–467, Berlin, Heidelberg, 2023. Springer-Verlag. ISBN 978-3-031-43512-6. doi: 10.1007/978-3-031-43513-3 24

    work page doi:10.1007/978-3-031-43513-3 2023

  28. [28]

    Lyon and Piotr Ostropolski-Nalewaja

    Tim S. Lyon and Piotr Ostropolski-Nalewaja. Foundations for an abstract proof theory in the context of horn rules, 2023. URLhttps://arxiv.org/abs/2304.05697

    work page arXiv 2023

  29. [29]

    Lyon, Alwen Tiu, Rajeev Gor´ e, and Ranald Clouston

    Tim S. Lyon, Alwen Tiu, Rajeev Gor´ e, and Ranald Clouston. Syntactic interpolation for tense logics and bi-intuitionistic logic via nested sequents. In Maribel Fern´ andez and Anca Muscholl, editors,28th EACSL Annual Conference on Computer Science Logic (CSL 2020), volume 152 ofLIPIcs, pages 28:1–28:16. Schloss Dagstuhl – Leibniz- Zentrum f¨ ur Informati...

    2020

  30. [30]

    Lyon, Agata Ciabattoni, Didier Galmiche, Marianna Girlando, Dominique Larchey-Wendling, Daniel M´ ery, Nicola Olivetti, and Revantha Ramanayake

    Tim S. Lyon, Agata Ciabattoni, Didier Galmiche, Marianna Girlando, Dominique Larchey-Wendling, Daniel M´ ery, Nicola Olivetti, and Revantha Ramanayake. Inter- nal and external calculi: Ordering the jungle without being lost in translations, 2025. URLhttps://arxiv.org/abs/2312.03426

    work page arXiv 2025

  31. [31]

    Lyon, Ian Shillito, and Alwen Tiu

    Tim S. Lyon, Ian Shillito, and Alwen Tiu. Taking bi-intuitionistic logic first-order: A proof-theoretic investigation via polytree sequents. In J¨ org Endrullis and Sylvain Schmitz, editors,33rd EACSL Annual Conference on Computer Science Logic (CSL 2025), volume 326 ofLeibniz International Proceedings in Informatics (LIPIcs), pages 41:1–41:23. Schloss Da...

    2025

  32. [32]

    Cambridge University Press, 2011

    Sara Negri and Jan Von Plato.Proof analysis: a contribution to Hilbert’s last problem. Cambridge University Press, 2011

    2011

  33. [33]

    Labelled calculi for quantified modal logics with definite descriptions.Journal of Logic and Computation, 31:923–946, 2021

    Eugenio Orlandelli. Labelled calculi for quantified modal logics with definite descriptions.Journal of Logic and Computation, 31:923–946, 2021. URL https://doi.org/10.1093/logcom/exab018

    work page doi:10.1093/logcom/exab018 2021

  34. [34]

    Quantified modal logics: One approach to rule (al- most) them all!Journal of Philosophical Logic, 53:959–996, 2024

    Eugenio Orlandelli. Quantified modal logics: One approach to rule (al- most) them all!Journal of Philosophical Logic, 53:959–996, 2024. URL https://doi.org/10.1007/s10992-024-09754-7

    work page doi:10.1007/s10992-024-09754-7 2024

  35. [35]

    The method of tree-hypersequents for modal proposi- tional logic

    Francesca Poggiolesi. The method of tree-hypersequents for modal propositional logic. In David Makinson, Jacek Malinowski, and Heinrich Wansing, editors,Towards Math- ematical Philosophy, volume 28 ofTrends in logic, pages 31–51. Springer, 2009. doi: 10.1007/978-1-4020-9084-4 3

    work page doi:10.1007/978-1-4020-9084-4 2009

  36. [36]

    Recursive unsolvability of a problem of Thue.The Journal of Symbolic Logic, 12(1):1–11, 1947

    Emil L Post. Recursive unsolvability of a problem of Thue.The Journal of Symbolic Logic, 12(1):1–11, 1947

    1947

  37. [37]

    PhD thesis, University of Edinburgh

    Alex K Simpson.The Proof Theory and Semantics of Intuitionistic Modal Logic. PhD thesis, University of Edinburgh. College of Science and Engineering. School of Informat- ics, 1994. 31

    1994

  38. [38]

    Rasiowa-Sikorski lemma and Kripke completeness of predicate and infinitary modal logics

    Yoshihito Tanaka and Hiroakira Ono. Rasiowa-Sikorski lemma and Kripke completeness of predicate and infinitary modal logics. In Marcus Kracht, Maarten de Rijke, Heinrich Wansing, and Michael Zakharyaschev, editors,Advances in Modal Logic, pages 419–437. CSLI Publications, 1998

    1998

  39. [39]

    A hypersequent system for G¨ odel-Dummett logic with non-constant do- mains

    Alwen Tiu. A hypersequent system for G¨ odel-Dummett logic with non-constant do- mains. In Kai Br¨ unnler and George Metcalfe, editors,Automated Reasoning with Ana- lytic Tableaux and Related Methods, pages 248–262. Springer Berlin Heidelberg, Berlin, Heidelberg, 2011. ISBN 978-3-642-22119-4

    2011

  40. [40]

    Grammar logics in nested sequent calculus: Proof theory and decision procedures

    Alwen Tiu, Egor Ianovski, and Rajeev Gor´ e. Grammar logics in nested sequent calculus: Proof theory and decision procedures. In Thomas Bolander, Torben Bra¨ uner, Silvio Ghilardi, and Lawrence S. Moss, editors,Advances in Modal Logic 9, pages 516–537. College Publications, 2012

    2012

  41. [41]

    Springer Science & Business Media, 2000

    Luca Vigan` o.Labelled Non-Classical Logics. Springer Science & Business Media, 2000. §A. Proofs for Section 3 Theorem3.14.IfNQ ◦ =.K(C)⊢ G, thenGis valid w.r.t. the class of framesF(C). Proof.Additional cases for the soundness theorem are provided below: ∀. Suppose thatH=G{Γ,∀xφ} w is invalid. By assumption, there exists a model Mbased on a frame inF(C),...

    2000