arxiv: 2605.07438 · v1 · submitted 2026-05-08 · 🧮 math.LO

Recognition: 1 theorem link

· Lean Theorem

Bounded depth in Hilbert algebras

Luca Carai, Miriam Kurtzhals, Tommaso Moraschini

Pith reviewed 2026-05-11 01:53 UTC · model grok-4.3

classification 🧮 math.LO

keywords Hilbert algebrasbounded depthequational classesHeyting algebrasimplicative subreductsvarietiesalgebraic logic

0 comments

The pith

Hilbert algebras of depth at most n form an equational class.

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

Hilbert algebras consist of the implication operation extracted from Heyting algebras. The paper proves that for any fixed natural number n, membership in the class of Hilbert algebras with depth at most n is equivalent to satisfying one equation in the language of implication alone. This transfers a known equational description of bounded depth from the richer Heyting signature to the simpler Hilbert signature. A reader cares because the result shows the property remains algebraically simple even after discarding the lattice structure, allowing direct equational reasoning about these algebras.

Core claim

For each natural number n there is an equation in the language of Hilbert algebras such that a Hilbert algebra satisfies the equation precisely when it has depth at most n. The equation is obtained by adapting the corresponding equation already known to work for Heyting algebras.

What carries the argument

The equational condition obtained by restricting the bounded-depth equation from Heyting algebras to the implicative subreduct.

If this is right

The class of Hilbert algebras of depth at most n is closed under subalgebras, homomorphic images, and direct products.
Bounded depth becomes expressible without any reference to meet, join, or the lattice order.
Each such class is a variety and therefore admits a free algebra on any set of generators.
The equational theory of these varieties can be studied directly in the implication signature.

Where Pith is reading between the lines

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

The same transfer technique may apply to other invariants such as width or height that are already equational in Heyting algebras.
One can now ask whether the free Hilbert algebras of bounded depth coincide with the implication reducts of the corresponding free Heyting algebras.
The result opens the possibility of classifying subvarieties of Hilbert algebras by their depth bounds in a uniform way.

Load-bearing premise

The depth of a Heyting algebra, when measured only by chains visible through the implication operation, matches the depth in the original algebra.

What would settle it

Exhibit a Hilbert algebra that has depth greater than n yet satisfies the candidate equation, or a Hilbert algebra of depth at most n that fails the equation.

read the original abstract

Hilbert algebras are the implicative subreducts of Heyting algebras. It is shown that having depth at most n is an equational condition in Hilbert algebras. This generalizes an analogous well-known result in the setting of Heyting algebras.

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.

Desk Editor's Note private letter to a colleague

The paper translates the known equational axioms for bounded depth from Heyting algebras into the implicative signature and verifies they work for Hilbert algebras.

read the letter

The core result is that depth at most n is equationally definable in Hilbert algebras using only implication and the top element. They rewrite the Heyting equations by expressing the lattice operations through implications and then check directly that the new equations hold exactly when all chains are short enough. This works because every Hilbert algebra is the implicative reduct of some Heyting algebra and the order is the same in both, so the chain condition carries over without extra assumptions. The explicit translation and verification are the useful parts; they turn an abstract transfer into something concrete that can be used in calculations. The argument looks solid on its own terms and avoids circularity by building the equations from the known Heyting case rather than assuming the conclusion. The main limitation is that the work stays narrow: it is a direct generalization rather than a new technique or a broader reorganization of the theory. No major gaps appear in the logic, but the payoff is mostly filling this one small slot in the literature. Readers who already work with subreducts of Heyting algebras or equational classes in algebraic logic will get the most out of it; others can skip it. I would send this to peer review. It is a modest, self-contained note that is worth checking and archiving even if it will not shift the larger field.

Referee Report

0 major / 2 minor

Summary. The paper claims that the class of Hilbert algebras of depth at most n is equationally definable in the signature {→, 1}. Hilbert algebras are the implicative subreducts of Heyting algebras; depth is defined via the order a ≤ b ⇔ a → b = 1, which coincides with the order in the Heyting completion. The proof proceeds by rewriting the known equational axioms for bounded depth in Heyting algebras using only implicative operations and verifying directly that the resulting equations hold precisely when all chains have length ≤ n.

Significance. If the result holds, it supplies a useful equational characterization of bounded-depth Hilbert algebras, generalizing the corresponding fact for Heyting algebras and enabling the study of the associated varieties in the implicative signature alone. The manuscript's explicit translation of the axioms together with the direct verification that they characterize the depth condition are strengths that secure the transfer without additional assumptions or circularity.

minor comments (2)

[Abstract] The abstract is terse and does not indicate the method of proof (explicit translation of axioms); a single sentence summarizing the approach would improve accessibility.
[Introduction] The introduction would benefit from a brief, explicit citation to the well-known equational characterization of bounded depth in Heyting algebras before the translation is presented.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive assessment of our manuscript, including the recognition that the explicit translation of axioms and direct verification constitute strengths of the work. The recommendation for minor revision is noted.

Circularity Check

0 steps flagged

No significant circularity; derivation is self-contained via explicit translation and verification

full rationale

The paper defines depth in Hilbert algebras via the implicative order (a ≤ b iff a → b = 1) and shows it is equational by supplying an explicit translation of the bounded-depth axioms from the Heyting case into the {→, 1} signature, followed by direct verification that these equations hold precisely when all chains have length ≤ n. This construction secures the transfer without reducing to a fit, self-definition, or load-bearing self-citation; the generalization rests on the algebraic reduct property and the supplied equational rewriting rather than on prior results by construction. No step matches any enumerated circularity pattern.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The claim rests on the standard definition of Hilbert algebras as implicative subreducts and on the transfer of the depth notion from Heyting algebras; no free parameters or new entities are introduced in the abstract.

axioms (1)

domain assumption Hilbert algebras are the implicative subreducts of Heyting algebras
Foundational definition stated in the abstract.

pith-pipeline@v0.9.0 · 5317 in / 1002 out tokens · 44388 ms · 2026-05-11T01:53:52.330356+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/LogicAsFunctionalEquation.lean reality_from_one_distinction unclear
We say that a Hilbert algebra A has depth ⩽n ... iff A⊨d n ≈ 1

Reference graph

Works this paper leans on

8 extracted references · 8 canonical work pages

[1]

Burris and H

S. Burris and H. P. Sankappanavar.A Course in Universal Algebra. The millennium edition, available online, 2012

work page 2012
[2]

Bu¸ sneag

D. Bu¸ sneag. A note on deductive systems of a Hilbert algebra.Kobe Journal of Mathematics, 2(1):29–35, 1985

work page 1985
[3]

S. A. Celani and R. Jansana. On the free implicative semilattice extension of a Hilbert algebra.Mathe- matical Logic Quarterly, 58(3):188–207, 2012

work page 2012
[4]

Chagrov and M

A. Chagrov and M. Zakharyaschev.Modal Logic, volume 35 ofOxford Logic Guides. Oxford University Press, 1997

work page 1997
[5]

Diego.Sobre ´ algebras de Hilbert, volume 12 ofNotas de L´ ogica Matem´ atica

A. Diego.Sobre ´ algebras de Hilbert, volume 12 ofNotas de L´ ogica Matem´ atica. Universidad Nacional del Sur, Bah´ ıa Blanca (Argentina), 1965

work page 1965
[6]

L. Henkin. An algebraic characterization of quantifiers.Fundamenta Mathematicae, 37:63–74, 1950

work page 1950
[7]

A. Horn. The separation theorem of intuitionist propositional logic.The Journal of Symbolic Logic, 27:391–399, 1962

work page 1962
[8]

K¨ ohler

P. K¨ ohler. Brouwerian semilattices.Transactions of the American Mathematical Society, 268:103–126, 1981

work page 1981