pith. sign in

arxiv: 2602.09470 · v2 · pith:6PSNABKWnew · submitted 2026-02-10 · 🧮 math.LO

Strong Completeness of Provability Logic for Uncountable Languages

Pith reviewed 2026-05-16 05:57 UTC · model grok-4.3

classification 🧮 math.LO
keywords provability logicGLstrong completenessmodal logictopological semanticsIcard topologybouquet spacespartition theorem
0
0 comments X

The pith

Provability logic GL fails strong completeness for modal languages of cardinality (2^|λ| + ℵ₀)^+ on ordinals with generalized Icard topologies.

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

The paper establishes that for any ordinal λ greater than zero, in modal languages whose size reaches (2 to the power of the cardinality of λ plus aleph null) to the plus, there is a set of formulas consistent with the provability logic GL that nevertheless has no satisfying model when the models are based on ordinals equipped with the generalized Icard topology I_λ or the topology τ_c plus λ. This result is obtained via the Erdős–Rado partition theorem and highlights a breakdown of strong completeness for sufficiently large uncountable languages under these particular topological semantics. To counter this, the authors introduce λ-bouquet spaces, which restore strong completeness for GL in languages of size exactly λ, and ultralinear λ-bouquet spaces that do the same for the logic GL.3.

Core claim

For an ordinal λ > 0 there exists a GL-consistent set of formulas in a language of cardinality (2^|λ| + ℵ₀)^+ having neither a (Θ, I_λ)-model nor a (Θ, τ_c + λ)-model. The λ-bouquet spaces and ultralinear λ-bouquet spaces yield strong completeness of GL and GL.3 respectively for languages of cardinality λ.

What carries the argument

The generalized Icard topologies on ordinals together with the newly defined λ-bouquet spaces, which serve both to exhibit the failure of strong completeness at large cardinalities via partition properties and to establish positive completeness results at cardinality λ.

If this is right

  • Strong completeness for GL holds relative to λ-bouquet spaces whenever the language has cardinality λ.
  • Strong completeness for GL.3 holds relative to ultralinear λ-bouquet spaces for languages of cardinality λ.
  • The negative result shows that ordinal models with Icard-type topologies cannot validate strong completeness beyond a specific uncountable threshold.
  • The use of the Erdős–Rado theorem indicates that combinatorial partition properties are key to constructing the inconsistent model sets.

Where Pith is reading between the lines

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

  • The result suggests that alternative classes of topological spaces may be needed to recover strong completeness for provability logic in languages larger than λ.
  • Similar constructions could be explored for other modal logics such as those extending GL.
  • One might investigate whether the bouquet space approach generalizes to provide completeness at higher cardinalities with modified definitions.

Load-bearing premise

That models on ordinals equipped with the generalized Icard topologies I_λ and τ_c + λ are the appropriate semantics against which to test strong completeness of GL.

What would settle it

Finding a specific model on an ordinal Θ with the I_λ topology that satisfies all formulas in the constructed GL-consistent set for a language of cardinality (2^|λ| + ℵ₀)^+ would show that the failure of strong completeness does not hold.

read the original abstract

For an ordinal $\lambda>0$, we use the Erd\H{o}s--Rado partition theorem to prove the failure of strong completeness of $\mathsf{GL}$ for modal languages of cardinality $(2^{|\lambda|+\aleph_0})^{+}$ with respect to models on ordinals equipped with the generalized Icard topologies $\mathcal{I}_{\lambda}$ and ${\tau_{c}}_{+\lambda}$. Specifically, we show that for such languages there exists a $\mathsf{GL}$-consistent set of formulas having neither $(\Theta, \mathcal{I}_{\lambda})$-model nor $(\Theta, {\tau_{c}}_{+\lambda})$-model. We also introduce two kinds of natural classes of topological spaces, called \emph{ $\lambda$-bouquet spaces} and \emph{ultralinear $\lambda$-bouquet spaces}, and prove that they yield strong completeness of $\mathsf{GL}$ and $\mathsf{GL}.3$ respectively for languages of cardinality $\lambda$.

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

2 major / 2 minor

Summary. For an ordinal λ > 0, the paper uses the Erdős-Rado partition theorem to show that GL fails to be strongly complete for modal languages of cardinality (2^|λ| + ℵ₀)^+ with respect to models on ordinals equipped with the generalized Icard topologies I_λ and τ_c +λ: there exists a GL-consistent set Σ with neither (Θ, I_λ)-model nor (Θ, τ_c +λ)-model. The paper also defines λ-bouquet spaces and ultralinear λ-bouquet spaces and proves that these yield strong completeness of GL and GL.3 respectively for languages of cardinality λ.

Significance. The negative result, if the chosen topologies are accepted as representative, demonstrates a concrete size threshold beyond which strong completeness fails in these ordinal semantics, leveraging the Erdős-Rado theorem in a load-bearing way. The positive results supply new, explicitly constructed classes of spaces in which strong completeness holds for languages of size λ, including for the stronger logic GL.3 in the ultralinear case. These constructions are a clear strength.

major comments (2)
  1. [Abstract / negative-result section] Abstract and the section proving the negative result: the non-existence of models is shown only for the specific families (Θ, I_λ) and (Θ, τ_c +λ); the manuscript does not establish that every reasonable ordinal topology would likewise lack a model for the constructed Σ, so the claim of failure of strong completeness remains local to these two topologies rather than a general obstruction.
  2. [λ-bouquet spaces section] Section introducing λ-bouquet spaces: the completeness proof for GL on λ-bouquet spaces (and for GL.3 on the ultralinear variant) is tied to the particular definition of these spaces; without a comparison showing that these spaces are natural or exhaustive among reasonable alternatives, the positive result is narrower than the negative claim suggests.
minor comments (2)
  1. [Preliminaries] Notation for the topologies I_λ and τ_c +λ should be introduced with a brief reminder of their relation to the standard Icard topology before the main theorems.
  2. [Negative-result section] The statement of the Erdős-Rado application in the negative result would benefit from an explicit citation of the precise partition relation used.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading of our manuscript and the detailed comments. We respond to each major comment below, clarifying the intended scope of the results.

read point-by-point responses
  1. Referee: [Abstract / negative-result section] Abstract and the section proving the negative result: the non-existence of models is shown only for the specific families (Θ, I_λ) and (Θ, τ_c +λ); the manuscript does not establish that every reasonable ordinal topology would likewise lack a model for the constructed Σ, so the claim of failure of strong completeness remains local to these two topologies rather than a general obstruction.

    Authors: The manuscript explicitly limits the negative result to the generalized Icard topologies I_λ and τ_c +λ, as stated in the abstract and the relevant section. We use the Erdős-Rado theorem to construct a GL-consistent set Σ with no models on ordinals under these specific topologies for languages of the given cardinality. We do not claim or prove a general failure for arbitrary ordinal topologies; the result is presented as local to these two families. This matches the paper's claims without overstatement. revision: no

  2. Referee: [λ-bouquet spaces section] Section introducing λ-bouquet spaces: the completeness proof for GL on λ-bouquet spaces (and for GL.3 on the ultralinear variant) is tied to the particular definition of these spaces; without a comparison showing that these spaces are natural or exhaustive among reasonable alternatives, the positive result is narrower than the negative claim suggests.

    Authors: The λ-bouquet spaces and ultralinear λ-bouquet spaces are introduced as explicitly constructed natural classes in the ordinal setting, for which we prove strong completeness of GL and GL.3 respectively on languages of size λ. The results are tied to these definitions by design, providing concrete positive counterparts to the negative findings. We do not assert that the classes are exhaustive among all alternatives. To address the request for comparison, we can add a short clarifying paragraph on their motivation and relation to ordinal topologies in a revised version. revision: partial

Circularity Check

0 steps flagged

No circularity: external theorem and explicit new constructions keep derivation independent

full rationale

The negative result applies the external Erdős-Rado theorem to construct a GL-consistent set of formulas with no model in the explicitly defined generalized Icard topologies I_λ and τ_c +λ. The positive results define λ-bouquet spaces and ultralinear λ-bouquet spaces from scratch and prove strong completeness directly for languages of size λ inside those classes. No equation or claim reduces by construction to a fitted input, self-citation chain, or renamed prior result; all load-bearing steps rest on the cited partition theorem or on the paper's own definitions and proofs.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 2 invented entities

The central claims rest on the Erdős-Rado partition theorem as a standard tool and on the newly postulated λ-bouquet spaces whose properties are defined within the paper.

axioms (1)
  • standard math Erdős-Rado partition theorem
    Invoked to establish the non-existence of models for large languages on the given topologies.
invented entities (2)
  • λ-bouquet spaces no independent evidence
    purpose: Topological spaces that yield strong completeness of GL for languages of cardinality λ
    Newly introduced class of spaces whose definition and properties are supplied by the paper.
  • ultralinear λ-bouquet spaces no independent evidence
    purpose: Topological spaces that yield strong completeness of GL.3 for languages of cardinality λ
    Variant of the bouquet spaces introduced for the stronger logic GL.3.

pith-pipeline@v0.9.0 · 5475 in / 1382 out tokens · 58092 ms · 2026-05-16T05:57:44.527062+00:00 · methodology

discussion (0)

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