Four papers on pinning a modal logic down: Cheq has no finite axiom system, uncountably many congruential logics have no neighborhood frame, closure semantics reaches the least modal logic, and dynamic epistemic logic gets a cut-free calculus

Four papers posted between 28 September and 2 October 2026 put a modal logic through each of the three instruments used to pin one down — a finite axiom system, a sound semantics, a proof calculus — and two of the instruments give out. Krzysztof Aleksander Krawczyk proves that uncountably many congruential modal logics are Post complete and neighborhood-unsound: no neighborhood frame validates exactly their theorems, so the standard semantics for that family is unsound for them 1. Han Xiao proves that the intermediate logic Cheq is not finitely axiomatizable, closing a question that goes back to a 2003 paper of Johan van Benthem, Guram Bezhanishvili and Mai Gehrke 2. Yuki Nishimura builds closure semantics, a possible-world semantics that stays sound and strongly complete down to the least modal logic, the system whose modal operator carries no axiom or inference rule of its own 3. Clara Lerouvillois and Francesca Poggiolesi give dynamic epistemic logic a hypersequent calculus whose logical rules are invertible and whose cut rule is admissible 4.

Krawczyk's paper and Xiao's paper each settle a question that had stood open for years, and both went public on 30 September: Krawczyk's in The Review of Symbolic Logic, Xiao's on arXiv. The other two fill gaps. Nishimura supplies the semantics the weakest modal systems had lacked, and Lerouvillois and Poggiolesi supply the calculus dynamic epistemic logic had lacked. All four are new, none has been refereed, and none has attracted a citing work yet.

Each paper below was first published inside the 28 September – 2 October window, and each is one step from its arXiv identifier or DOI. The table states the question each one answers, what its support rests on, and where it fits.

Maximal Neighborhood Unsound Congruential Modal Logics appeared online on 30 September 2026 in The Review of Symbolic Logic, as an open-access article. Krzysztof Aleksander Krawczyk works at the Institute of Philosophy of the Jagiellonian University in Kraków, and the article runs to 17 pages. It was received on 23 November 2025, and the research was funded by the Polish National Science Centre under grant 2023/49/N/HS1/04070. The paper states that no AI was used at any stage of the work 6.

A modal logic here is any set of formulas that contains the tautologies and is closed under modus ponens and uniform substitution. It is congruential when it is also closed under the rule that replaces equivalents inside the modal operator, and the congruential modal logics form a complete lattice under inclusion whose coatoms are the Post complete ones — the logics with no proper consistent extension. Neighborhood frames supply their semantics: a frame is a set of worlds together with a function N that assigns to each world a set of subsets of worlds, and a formula of the form □φ holds at a world w exactly when the set of worlds satisfying φ is a member of N(w) 6. Every normal modal logic is validated by at least one one-element Kripke frame, so the whole normal family is Kripke-sound; the congruential family is where soundness can fail 6.

Krawczyk builds an uncountable family of finite modal algebras A_f, indexed by the bijections f from the middle part of a Boolean algebra onto its atoms. Proposition 4.8 shows that the varieties these algebras generate are pairwise distinct and all minimal. Theorem 4.11 then shows that no frame validates the logic attached to any of those varieties: a validating frame would have to sit inside the variety, and a transfinite argument rules that out. The fundamental theorem gathers the two: for every f the variety is minimal, distinct f give distinct varieties, and no frame whose algebra is a powerset algebra lies in the variety 6.

Because congruential modal logics are algebraizable and modal algebras are dual to neighborhood frames, the theorems transfer. Each of the resulting logics is Post complete and has no neighborhood frame that validates it, which is unsoundness rather than the milder incompleteness that a logic can have when some frame validates more than its theorems 6. Peter Fritz proved in 2016 that there are continuum many Post complete congruential modal logics but left open whether any of them could be neighborhood incomplete; Krawczyk answers that question with a yes and an explicit construction 6.

This is a refereed, open-access journal article, and the proof stands on its own: the construction is supplied in full, and the transfinite argument for Theorem 4.11 is worked out inside the paper rather than cited. What the paper takes from the literature is standard duality and the definition of Post completeness. The logics it produces use a single modal operator, which the paper notes is new for the unsoundness phenomenon: the earlier examples all needed two or more operators 6. Each of these logics has degree of incompleteness continuum, since the class of frames that validates it is empty and continuum many logics share that empty class 6. Two questions remain open on the author's own statement: whether the varieties can be made to satisfy other properties while keeping the unsoundness, and the exact number of Post complete congruential modal logics that are neighborhood complete 6.

Open it if you work on algebraic modal logic, on neighborhood semantics, or on the incompleteness of modal systems. Read Section 3 for Fritz's two theorems and the exact shape of the open problem, then Section 4 up to Theorem 4.11 for the construction. The prerequisites are the duality between modal algebras and neighborhood frames, universal algebra at the level of varieties and ultrafilters, and enough comfort with transfinite induction to follow the key lemma.

Non-finite Axiomatizability and Undecidability of Cheq was first submitted to arXiv on 30 September 2026 under cs.LO and runs to 21 pages. Han Xiao is the sole author, at the Tsinghua–UvA Joint Research Center for Logic at Tsinghua University 2. The paper carries an explicit disclosure about machine assistance: the mathematical arguments were not generated with AI, the non-finite-axiomatizability proof is self-contained and predates the recent wave of machine proofs, and the undecidability theorem does use an AI-generated proof that Medvedev's logic is undecidable 7.

Cheq is the intermediate logic of chequered subsets. Its modal counterpart, the logic L∞, was introduced in 2003 by van Benthem, Guram Bezhanishvili and Mai Gehrke, and Tadeusz Litak later named the intermediate analogue Cheq. Cheq sits inside Medvedev's logic Med, the logic of finite problems, and it already had a small dossier: it has the disjunction property, it validates Scott's axiom, it fails the Kreisel–Putnam axiom, and it is not structurally complete 7. An intermediate logic is finitely axiomatizable when finitely many axiom schemata generate it by modus ponens and substitution; Cheq, the paper shows, is not.

Theorem 5.3 states that Cheq is not finitely axiomatizable 7. The question had a particular history: Fontaine showed in 2006 that Medvedev's logic is not even finitely axiomatizable over Cheq, Maksimova, Skvortsov and Shehtman had proved the same for Medvedev's logic itself, and Shatrov announced the Cheq result at a 2007 conference in Oxford without ever publishing it 7.

The second result is a reduction rather than a fresh undecidability proof. Theorem 6.1 states that for every formula φ, φ belongs to Med exactly when a translated formula C(φ) belongs to Cheq, where the translation uses a Friedman-style device. The construction reads Cheq frames as dual face posets of hypercubes and carves a simplex out of a hypercube, which is why Medvedev frames appear inside Cheq frames 7. The corollary is that if Medvedev's logic is undecidable then Cheq is undecidable too, so Cheq's undecidability now holds conditional on the undecidability of Medvedev's logic, which a separate 2026 preprint supplies 7.

This is a preprint that has not been peer-reviewed, and the support is proof-theoretic across 21 pages with no data. The non-finite-axiomatizability theorem stands on its own argument. The undecidability result rests on a premise from outside the paper, the undecidability of Medvedev's logic, so a reader who wants that conclusion unreduced will have to read the other preprint as well 7. The paper also locates Cheq in the modal logic of forcing: earlier work by the same author shows that, under an added set-theoretic assumption, the modal logic of c.c.c. forcing is contained in S4.FPFA, the least modal companion of Cheq 7.

Open it if you work on intermediate logics, on Medvedev's logic of finite problems, or on the modal logic of forcing. Read Section 3 first for the comparison of modal companions, then Section 4 for the reading of Cheq frames as hypercube face posets, then Theorem 5.3 and the reduction in Section 6. The prerequisites are intermediate and modal logic, the Gödel translation and modal companions, p-morphisms between finite posets, and enough combinatorics of hypercubes to follow the geometric argument.

Closure Semantics for Weak Modal Logics: Completeness and Representations was first submitted to arXiv on 1 October 2026 under math.LO, and runs to 26 pages. Yuki Nishimura is the sole author 3.

Weakening the requirements of normality produces a hierarchy of modal systems below the familiar ones. The classical modal logic E keeps only replacement of equivalents for the modal operator; the logic of necessitation N keeps only the generalization rule; at the bottom sits the least modal logic, in which no modal axiom or inference rule is imposed, so formulas containing the modal operator arise only through uniform substitution 8. A closure model assigns to each world w a set G(w) of modal formulas, called its generator, and interprets □φ as the claim that φ lies in cl(G(w)), where the closure operation cl carries no general requirement of extensivity, monotonicity or idempotence 8. Conditions on the sets cl(G(w)) then encode particular modal principles, so the same framework can host systems that differ in which axioms and rules they keep.

The paper proves soundness for every subset of the principle list {E, G, M, C, N, K} (Theorem 3.3), strong completeness for every subset of {M, C, N, K} (Theorem 3.12), and then strong completeness for the full list including E and G (Theorem 3.20), so that semantic consequence from an arbitrary set of assumptions coincides with derivability 8. The least modal logic thus receives a possible-world semantics that imposes no condition on the modal operator at all. Theorem 3.13 gives the finite model property, and Corollary 3.14 makes the systems decidable, in fact primitive recursive 8.

A second half compares closure models with three existing frameworks by model-to-model translation. Theorems 4.10, 4.19 and 4.30 give truth-preserving translations in both directions between closure models and neighborhood models, FMT models, and Kripke models, and Corollary 4.31 records that Kripke models and the Kripke-representable closure models define the same logic 8. The condition a closure model has to satisfy for the Kripke translation is stronger than the condition matching the usual axiomatization of the modal logic K, even though the two conditions determine the same logic 8.

A preprint that has not been peer-reviewed. The support is proof-theoretic and model-theoretic across 26 pages, with no data. The construction adapts closure semantics that Kogure and Kurahashi developed for non-normal provability logics, lifted out of its arithmetical setting and given no closure requirements on cl 8. It differs from the non-deterministic semantics that Grätz gave for the least modal logic and that Omori and Skurt later developed, because those work from generalized truth values and give up possible worlds, while closure semantics keeps worlds and so can be compared to the other world-based frameworks 8.

Open it if you work on non-normal modal logic, on neighborhood semantics, or on completeness for very weak systems. Read Section 1.1 first, for where this sits against earlier minimal systems and against non-deterministic semantics, then Section 3 for the completeness construction, then Section 4 for the translations. The prerequisites are normal modal logic, neighborhood frames, and enough familiarity with canonical-model arguments to follow a Lindenbaum-style adaptation.

Dynamic Proof Theory for Dynamic Epistemic Logic was first submitted to arXiv on 29 September 2026 under cs.LO, and runs to 30 pages. Clara Lerouvillois is at IRIT (CNRS, INP, University of Toulouse) and at the IHPST (CNRS, University Paris 1 Panthéon-Sorbonne); Francesca Poggiolesi is at the IHPST 9.

Static epistemic logic represents what agents know at a moment and abstracts away from how knowledge is acquired or lost. Dynamic epistemic logic adds that dimension: action models turn announcements, private communications and other epistemic events into objects of the language, and validity is judged in the model that results after an event. The semantics is well established, and the paper notes that proof-theoretic treatments have been scarce; the one earlier treatment with an S5 base, it says, was not inherently dynamic 9. The paper's objects are dynamic hypersequents, which carry several sequents at once together with an agent index and an event store, so a single structure can represent a sequence of epistemic events 9.

The calculus, written IDHS_DEL, has logical rules that are provably invertible and structural rules of weakening, contraction and merge that are admissible, and Theorem 13 establishes that the cut rule is admissible as well 9. Theorem 9 gives soundness and Theorem 11 completeness with respect to dynamic epistemic logic, so a formula is valid exactly when the calculus derives it 9. The authors state that this is the only proof-theoretic calculus for dynamic epistemic logic that is both grounded in a classical S5 framework and inherently dynamic 4.

A preprint that has not been peer-reviewed; 30 pages, all proof-theoretic, no data. Cut admissibility is proved rather than assumed, and it is the property that lets the calculus serve as a procedure for deciding derivability and not only as a checkpoint on derivations that are already written down 9. The construction is tied to a classical S5 epistemic base, and the paper makes no claim for weaker epistemic bases 9.

Open it if you work on proof theory for modal or epistemic logic, on action models, or on cut elimination. Read Section 2 for the dynamic hypersequent apparatus with its agent index and event store, the section that establishes invertibility and the structural rules, and Section 7 for the cut-elimination proof. The prerequisites are sequent and hypersequent calculi, epistemic logic over S5, and the action-model semantics of dynamic epistemic logic.

The four results put the same question to four instruments. Xiao's theorem removes the finite axiom system from Cheq. Krawczyk's removes the neighborhood frame from an uncountable family of congruential logics, and it removes it in the strong sense, since no frame validates those logics at all 1. Nishimura builds a semantics that reaches the systems too weak to have had one, and Lerouvillois and Poggiolesi build a calculus for a logic that until now had only a semantics 34. Read together, the four run across the same stretch of the field: from normal modal logic down to the least modal logic, and from static epistemic logic to its dynamic extensions.

The same week carried three further results on that stretch. Martín Figallo, Jonathan Sarmiento and Luis Pezzini give a sequent calculus for the minimal tense logic K_t and prove it sound and complete against tense Boolean algebras, adapting the Lindenbaum–Tarski construction to Kashima's nested sequents 10. Yanjun Li and Rujing Wang publish in the Journal of Philosophical Logic an axiomatization for public announcement logic with iterated updates, which extends the dynamic-epistemic line of the third featured paper into a journal setting 11. Thorsten Engesser and Agata Ciabattoni build a doxastic deontic logic out of a classically reducible fragment of Chellas's minimal deontic logic combined with multi-agent KD45; satisfiability in their deontic fragment is NP-complete, and optimal decision making under weighted norms reduces to weighted partial MaxSAT in polynomial time 12.

The model-companion question also returned this week, in a different setting. Özlem Beyarslan and Piotr Kowalski show that adjoining an automorphism to a bounded PAC field of characteristic zero, with the absolute Galois group free profinite or free pro-p of finite rank, yields a theory with no model companion, and that adding a second commuting automorphism to any completion of ACFA has no model companion either 13.

Every count below was read on 4 October 2026.

None of the four featured papers has a citing work on any route that answered. OpenAlex returns a cited-by count of zero for each of them 14. DataCite, the registration agency for arXiv's DOIs, also returns zero for the three preprints 15. Google Scholar lists one record for each title and shows no cited-by link for any of them, which is how its result page looks when a record has attracted none 16. The Semantic Scholar graph endpoint answered for all four in a single batch request: zero citations each, against reference counts of 37 for the Cheq paper, 15 for closure semantics, 14 for the tense-logic paper and 11 for dynamic proof theory 17. Crossref does not index arXiv DOIs, so it returns nothing for the three preprints; for Krawczyk's journal article it records zero citing works and 32 references 18.

A zero in the week of posting can reflect indexing lag as easily as it reflects the absence of interest. The three preprints were submitted between 29 September and 1 October, and the Krawczyk article, although received in November 2025, was published online on 30 September. Nothing in these numbers separates a result nobody will build on from one that has not yet been read.

Where the numbers do say something is in the literature these papers attach to. Krawczyk's article lands in a line that runs from Kit Fine's 1974 incomplete logic containing S4, with 132 citing works, and Wim Blok's 1980 study of the lattice of modal logics, with 98, to Kosta Došen's 1989 duality paper between modal algebras and neighborhood frames, with 52 192021. The closest antecedent in the same family is Lloyd Humberstone's 2016 note on extending congruential modal logics, which carries three citing works, and Fritz's own 2016 paper on Post completeness in congruential modal logics has no DOI and no OpenAlex record, so its citations are not readable through these routes 22. On the dynamic side, the anchor is still Baltag, Moss and Solecki's logic of public announcements, which shows 607 citing works for its 2016 reprint, with 5 to 7 added in each of the last three years 23. The undecidability result that Xiao's corollary depends on comes from 2026 preprints that still read zero 24.

For a reader deciding what to read, the useful signal this week is structural rather than bibliometric. Two of the four papers close questions that had been open for years — one from 2003, one from 2016 — and both are the kind of result that other authors can start from immediately, because each supplies a construction rather than a survey.

If you work on algebraic modal logic or neighborhood semantics, read Krawczyk first. It is the refereed paper of the four, the construction is explicit, and Theorem 4.11 is the step worth checking against the duality you already use.

If you work on intermediate logics or the modal logic of forcing, read Xiao first. The non-finite-axiomatizability proof is self-contained and the geometric reading of Cheq frames as hypercube face posets is the part most likely to transfer to another logic.

If you care about missing semantics for very weak systems, read Nishimura first. Section 4 is the part to check, because the translations decide whether closure models are a new framework or a restatement of neighborhood models.

If your work is in epistemic logic or in proof theory, read Lerouvillois and Poggiolesi first. Section 7 carries the cut-elimination proof, and the question to keep in view is how much of the argument depends on the S5 base.

One question cuts across all four: which of these logics can be given a finite presentation of the kind it needs, and what does the answer cost? Cheq has no finite axiom system, Krawczyk's logics have no frames, closure semantics buys completeness for weak systems at the price of a closure operation with no general laws, and the dynamic hypersequent calculus buys cut admissibility at the price of carrying an event store through every rule.