pith. sign in

arxiv: 2606.31893 · v1 · pith:XLXX7WUSnew · submitted 2026-06-30 · 💻 cs.LO

Non-finite Axiomatizability of Generalized Medvedev Logics

Han Xiao (Tsinghua University) This is my paper

Pith reviewed 2026-07-01 02:13 UTC · model grok-4.3

classification 💻 cs.LO
keywords Medvedev logicintermediate logicsfinite axiomatizabilityKripke framestopless productsKC logicCheq logic
0
0 comments X

The pith

Every generalized Medvedev logic is not finitely axiomatizable.

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

The paper defines generalized Medvedev logics via topless finite products of rooted Kripke frames with a top. It first establishes that the version with the top intact characterizes exactly the logic KC. Building on the known non-finite axiomatizability of classical Medvedev logic, the work proves the same property for all generalized versions, including those containing Cheq as a sublogic. It further shows there are at least countably many distinct such logics and that none is the least among them.

Core claim

Generalized Medvedev logics are the intermediate logics of topless finite products of rooted Kripke frames with a top; every such logic is not finitely axiomatizable, and whenever Cheq is a sublogic the generalized Medvedev logic is not finitely axiomatizable over Cheq. The poset of these logics contains at least countably many elements and has no least element.

What carries the argument

Topless finite products of rooted Kripke frames with a top, which define the generalized Medvedev logics and allow reduction of non-axiomatizability results from the topless case.

If this is right

  • Non-finite axiomatizability holds for topless products of arbitrary finite chains.
  • Non-finite axiomatizability holds for topless products of arbitrary finite rooted frames with a top.
  • Any generalized Medvedev logic containing Cheq is not finitely axiomatizable over Cheq.
  • The collection of generalized Medvedev logics has at least countably many distinct members.
  • No generalized Medvedev logic is the smallest in the collection.

Where Pith is reading between the lines

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

  • The topless product construction may produce non-finitely axiomatizable logics in other families of intermediate logics beyond those studied here.
  • The absence of a least generalized Medvedev logic indicates that the poset of these logics is not a complete lattice in the usual sense.
  • Results about Cheq sublogics suggest a general method for transferring non-axiomatizability across related frame classes.

Load-bearing premise

The intermediate logic characterized by finite products of rooted Kripke frames with a top is exactly KC.

What would settle it

Exhibit a finite axiomatization, over intuitionistic logic, of any one generalized Medvedev logic obtained from topless products of finite rooted frames with a top.

Figures

Figures reproduced from arXiv: 2606.31893 by Han Xiao (Tsinghua University).

Figure 1
Figure 1. Figure 1: Medvedev frames. Lemma 2.4 (Maksimova, Skvortsov, & Shehtman; cf. [11, Lemma 4]). If F is a finite rooted frame with a top, then F is a Med-frame [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: The Chinese lanterns Ls,n (left) and L ′ s,n,m (right). We define the n-th suspension of a poset T inductively by T (0) ∶= T and T (n) ∶= T⊕(D × n). The following lemma appears as [11, Corollary 4]; a proof can also be found in [4, Claim 9]. Lemma 4.3 (Maksimova, Skvortsov, & Shehtman). Let F be a finite rooted frame with a top. Then for every n ≥ 0, the n-th suspension F (n) is a p-morphic image of some M… view at source ↗
Figure 3
Figure 3. Figure 3: The bowtie W. Lemma 5.1 (Bowtie Lemma). If F is any finite rooted frame, then F⊕W is a p-morphic image of some Vn, that is, the n-fold product of the two-fork. The Bowtie Lemma clarifies structural properties of Cheq-frames and therefore provides a useful tool for the analysis of Cheq-frame structures [PITH_FULL_IMAGE:figures/full_fig_p008_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: The members of the family {N(i) ∶ i ∈ ω}. Theorem 5.4. There are at least countably many pairwise distinct generalized Medvedev logics. Proof. We construct a family {N(i) ∶ i ∈ ω} of finite rooted frames with its top. We begin by set￾ting N(1) = C(3). By Theorem 4.1, we have TLPN(1) = Med. Next, define N(2) = ⟨N2,R2⟩ by N2 = {r2,1,2,3,4,t2} and R2 = {(r2,x) ∶ x ∈ N2} ∪ {(x,t2) ∶ x ∈ N2} ∪ {(x,x) ∶ x ∈ N2}.… view at source ↗
Figure 5
Figure 5. Figure 5: A schematic “geography” of generalized Medvedev logics. The red region indicates general [PITH_FULL_IMAGE:figures/full_fig_p010_5.png] view at source ↗
read the original abstract

We introduce a generalized form of Medvedev logics obtained by removing the greatest element from finite products of rooted Kripke frames with a top. We show that, before removing the top, the intermediate logic characterized by such finite products is exactly KC. Classical Medvedev logic is characterized by topless products of 2-chains, and a theorem of Maksimova, Skvortsov and Shehtman establishes that it is not finitely axiomatizable. Motivated by this result, Nick Bezhanishvili conjectured that non-finite axiomatizability extends to topless products of arbitrary finite chains and, more generally, to topless products of finite rooted frames with a top. We prove that every such generalized Medvedev logic is not finitely axiomatizable, thereby settling both conjectures in the affirmative. In 2003, van Benthem, Guram Bezhanishvili, and Gehrke introduced Cheq, the logic of chequered sets, and we show that whenever Cheq is a sublogic of a generalized Medvedev logic, the latter is not finitely axiomatizable over Cheq. Finally, we investigate the order structure of generalized Medvedev logics. We prove that there are at least countably many distinct generalized Medvedev logics and that no least such logic exists. These results extend the classical theory of Medvedev logic and clarify the behaviour of intermediate logics generated by topless product constructions.

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 paper introduces generalized Medvedev logics as the intermediate logics of topless finite products of rooted Kripke frames with a top. It first proves that the logic characterized by the corresponding frames with top is exactly KC. It then shows that every such generalized Medvedev logic is not finitely axiomatizable, by reduction to the Maksimova-Skvortsov-Shehtman theorem on classical Medvedev logic (the case of topless products of 2-chains). The paper also proves that if Cheq is a sublogic of a generalized Medvedev logic then the latter is not finitely axiomatizable over Cheq, and establishes that there are at least countably many distinct generalized Medvedev logics with no least element under inclusion.

Significance. If the central reductions hold, the results confirm both of Nick Bezhanishvili's conjectures on non-finite axiomatizability for topless products of arbitrary finite chains and of finite rooted frames with top. The work extends the classical Medvedev theory by handling the topless case via an explicit proof that the topped version yields KC, and by relating the new logics to Cheq. The lattice-theoretic results on the order structure of these logics add to the understanding of intermediate logics generated by product constructions.

minor comments (2)
  1. The abstract and §1 could more explicitly flag that the KC characterization (used for the reduction) is proved inside the paper rather than assumed, to make the logical flow clearer to readers familiar only with the classical Medvedev case.
  2. Notation for the product constructions (e.g., the distinction between topped and topless frames) is introduced in §2 but could benefit from a small diagram or table summarizing the frame classes and their logics.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive summary, significance assessment, and recommendation to accept. The report accurately captures the main results on non-finite axiomatizability, the relation to Cheq, and the lattice-theoretic properties of generalized Medvedev logics.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The derivation proves internally that finite products of rooted frames with top characterize exactly KC, then reduces topless non-finite-axiomatizability to the external Maksimova-Skvortsov-Shehtman theorem on classical Medvedev logic and to the van Benthem et al. Cheq result. No step equates a claimed prediction or theorem to a fitted input, self-citation, or ansatz by construction; all load-bearing reductions cite independent prior results or the paper's own explicit proofs. This is the normal case of a self-contained argument against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The paper rests on standard Kripke semantics for intermediate logics and on the prior characterization that finite products with top yield KC; no new free parameters or invented entities are introduced.

axioms (2)
  • standard math Kripke frame semantics correctly characterizes intermediate logics
    Invoked throughout the abstract for defining the logics via products of frames.
  • domain assumption Finite products of rooted frames with top characterize exactly KC
    Used to reduce the topless case to known non-axiomatizability results.

pith-pipeline@v0.9.1-grok · 5782 in / 1266 out tokens · 30641 ms · 2026-07-01T02:13:13.840024+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

15 extracted references · 8 canonical work pages · 1 internal anchor

  1. [1]

    Studia Logica 75(3), pp

    Johan van Benthem, Guram Bezhanishvili & Mai Gehrke (2003): Euclidean Hierarchy in Modal Logic . Studia Logica 75(3), pp. 327–344, doi:10.1023/B:STUD.0000009564.00287.16

    work page doi:10.1023/b:stud.0000009564.00287.16 2003

  2. [2]

    In: V .A

    Guram Bezhanishvili & Nick Bezhanishvili (2022): Jankov formulas and axiomatization techniques for inter- mediate logics. In: V .A. Y ankov on Non-Classical Logics, History and Philosophy of Mathematics, Springer, pp. 71–124, doi:10.1007/978-3-031-06843-0_4

    work page doi:10.1007/978-3-031-06843-0_4 2022

  3. [3]

    Gaëlle Fontaine (2006): ML is not finitely axiomatizable over Cheq. In Guido Governatori, Ian Hodkinson & Yde Venema, editors: Advances in Modal Logic, 6th Conference, AiML 2006 on 25-28 September, 2006 , College Publications, Noosa, Queensland, Australia, pp. 139–146. Available at https://dblp.org/rec/ conf/aiml/Fontaine06

    2006

  4. [4]

    Master’s thesis, Universiteit van Amsterdam

    Gaëlle Fontaine (2007): Axiomatization of ML and Cheq. Master’s thesis, Universiteit van Amsterdam. Available at https://eprints.illc.uva.nl/771/

    2007

  5. [5]

    In David Fernández-Duque, Alessandra Palmigiano & Sophie Pinchinat, editors: Advances in Modal Logic, H

    Gianluca Grilletti (2022): Medvedev logic is the logic of finite distributive lattices without top element . In David Fernández-Duque, Alessandra Palmigiano & Sophie Pinchinat, editors: Advances in Modal Logic, H. Xiao 781 14th Conference, AiML 2022 on 22-25 August, 2022 , College Publications, Rennes, Brittany, France, pp. 451–466. Available at https://d...

    2022

  6. [6]

    Israel Journal of Mathematics 207(2), pp

    Joel David Hamkins, George Leibman & Benedikt Löwe (2015): Structural connections between a forcing class and its modal logic. Israel Journal of Mathematics 207(2), pp. 617–651, doi:10.1007/s11856-015-1185-

    work page doi:10.1007/s11856-015-1185- 2015

  7. [7]

    Available at https://link.springer.com/article/10.1007/s11856-015-1185-5

    work page doi:10.1007/s11856-015-1185-5

  8. [8]

    Transactions of the American Mathematical Society 360(4), pp

    Joel David Hamkins & Benedikt Löwe (2008): The modal logic of forcing . Transactions of the American Mathematical Society 360(4), pp. 1793–1817, doi:10.1090/S0002-9947-07-04297-3

    work page doi:10.1090/s0002-9947-07-04297-3 2008

  9. [9]

    Mathematische Zeitschrift 35, pp

    Andrey Nikolaevich Kolmogorov (1932): Zur Deutung der intuitionistischen Logik . Mathematische Zeitschrift 35, pp. 58–65, doi:10.1007/BF01186549

    work page doi:10.1007/bf01186549 1932

  10. [10]

    Some notes on the superintuitionistic logic of chequered subsets of $\mathbb{R}^\infty$

    Tadeusz Litak (2004): Some notes on the superintuitionistic logic of chequered subsets of R∞. Bulletin of the Section of Logic 33(2), pp. 81–86, doi:10.48550/arXiv.1808.06393

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.1808.06393 2004

  11. [11]

    Benedikt Löwe & Han Xiao (2025): Modal and intermediate logics of spiked Boolean algebras . In Cyr- iac Aiswarya, Prabal Kumar Sen & Shashi Mohan Srivastava, editors: Logic and Its Applications, 11th Indian Conference, ICLA 2025 on 3-5 February, 2025 , Springer-Verlag, Kolkata, India, pp. 164–175, doi:10.1007/978-3-031-89610-1_12

    work page doi:10.1007/978-3-031-89610-1_12 2025

  12. [12]

    Doklady Akademii Nauk SSSR 245(5), pp

    Larisa Lvovna Maksimova, Dmitry Pavlovich Skvortsov & Valentin Borisovich Shehtman (1979): Impos- sibility of finite axiomatization of Medvedev’s logic of finite problems . Doklady Akademii Nauk SSSR 245(5), pp. 1051–1054. Available at https://www.mathnet.ru/eng/dan42643. English translation: Soviet Mathematics Doklady 20 (1979), 394-398

    1979

  13. [13]

    Doklady Akademii Nauk SSSR 142(5), pp

    Yuri Tikhonovich Medvedev (1962): Finitive problems. Doklady Akademii Nauk SSSR 142(5), pp. 1015–

    1962

  14. [14]

    English translation: Soviet Mathematics Doklady 3 (1962), 227-230

    Available at https://www.mathnet.ru/eng/dan26117. English translation: Soviet Mathematics Doklady 3 (1962), 227-230

    1962

  15. [15]

    Han Xiao (2024): Modal logics and intermediate logics motivated by an open problem on c.c.c. forcing . Ph.D. thesis, Universität Hamburg. Available athttps://ediss.sub.uni-hamburg.de/handle/ediss/ 11363

    2024