Strong Completeness of Provability Logic for Uncountable Languages
Pith reviewed 2026-05-16 05:57 UTC · model grok-4.3
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.
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
- 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.
Referee Report
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)
- [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.
- [λ-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)
- [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.
- [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
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
-
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
-
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
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
axioms (1)
- standard math Erdős-Rado partition theorem
invented entities (2)
-
λ-bouquet spaces
no independent evidence
-
ultralinear λ-bouquet spaces
no independent evidence
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.