pith. sign in

arxiv: 2605.20841 · v1 · pith:VOWX3RNQnew · submitted 2026-05-20 · 🧮 math.LO

Intuitionism and computing with partial information

Hristo Ganchev , Paul Shafer , Theodore A. Slaman , Andrea Sorbi , Mariya I. Soskova This is my paper

Pith reviewed 2026-05-21 02:24 UTC · model grok-4.3

classification 🧮 math.LO
keywords Dyment latticeDyment-Muchnik latticeBrouwer algebraintuitionistic propositional calculusenumeration degreessplitting classweak law of excluded middle
0
0 comments X

The pith

Initial segments of the Dyment and Dyment-Muchnik lattices form Brouwer algebras modeling exactly the intuitionistic propositional calculus.

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

The paper proves that there are initial segments in both the Dyment lattice and the Dyment-Muchnik lattice of enumeration degrees. These segments can be turned into Brouwer algebras that capture precisely the intuitionistic propositional calculus. The construction for the Dyment-Muchnik lattice relies on building a splitting class of enumeration degrees. In contrast, the complete lattices satisfy the intuitionistic calculus together with the weak law of excluded middle. The authors further note that some downwards closed classes of enumeration degrees under enumeration reducibility do not serve as splitting classes.

Core claim

There exist initial segments of both the Dyment lattice and the Dyment-Muchnik lattice that yield Brouwer algebras modeling exactly the intuitionistic propositional calculus. For the Dyment-Muchnik lattice, this result is obtained by constructing a splitting class of enumeration degrees. The full Dyment lattice and the full Dyment-Muchnik lattice model the intuitionistic propositional calculus plus the weak law of excluded middle.

What carries the argument

The initial segment of the Dyment-Muchnik lattice constructed using a splitting class of enumeration degrees, which forms a Brouwer algebra for the intuitionistic propositional calculus.

If this is right

  • The full versions of both lattices model the intuitionistic propositional calculus plus the weak law of excluded middle.
  • Certain naturally definable classes of enumeration degrees that are downwards closed under enumeration reducibility do not form splitting classes.
  • Initial segments can be used to separate pure intuitionistic logic from additional logical principles in these degree structures.

Where Pith is reading between the lines

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

  • This approach may allow for the modeling of other propositional logics using different choices of initial segments in these lattices.
  • Connections between computation with partial information and algebraic models of intuitionism could lead to new ways of understanding intermediate logics.
  • Similar splitting class constructions might apply to other lattices in computability theory to isolate specific logical behaviors.

Load-bearing premise

A splitting class of enumeration degrees exists and can be used to produce the desired initial segment in the Dyment-Muchnik lattice.

What would settle it

Showing that no splitting class of enumeration degrees exists would prevent the construction for the Dyment-Muchnik lattice, or finding that the resulting algebra satisfies additional principles beyond the intuitionistic propositional calculus.

read the original abstract

There exist initial segments of both the Dyment lattice and the Dyment-Muchnik lattice that yield Brouwer algebras modeling exactly the intuitionistic propositional calculus. For the Dyment-Muchnik lattice, this result is obtained by constructing a splitting class of enumeration degrees. In contrast, the full Dyment lattice and the full Dyment-Muchnik lattice model the intuitionistic propositional calculus plus the weak law of excluded middle. We also observe that certain naturally definable classes of enumeration degrees, which are downwards closed under enumeration reducibility, fail to form splitting classes.

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. The paper claims that initial segments exist in both the Dyment lattice and the Dyment-Muchnik lattice of enumeration degrees that form Brouwer algebras modeling exactly the intuitionistic propositional calculus (IPC). For the Dyment-Muchnik lattice this is obtained via an explicit construction of a splitting class of enumeration degrees; the full lattices are shown to model IPC + WLEM, and certain naturally definable downwards-closed classes are shown not to be splitting classes.

Significance. If the constructions are correct, the results supply new, computability-theoretic models that separate IPC from WLEM inside concrete lattices of enumeration degrees. The splitting-class technique and the negative results on non-splitting classes both enlarge the set of available tools for building initial segments with prescribed logical properties.

major comments (2)
  1. [§5] §5 (Dyment-Muchnik construction): the argument that the chosen splitting class generates an initial segment whose Brouwer algebra validates exactly IPC (and not WLEM) rests on keeping certain pairs of degrees incomparable; the text does not supply an explicit verification that the splitting property does not force any such pair to become comparable, which is load-bearing for the separation from the full lattice.
  2. [Theorem 5.3] Theorem 5.3 and the preceding definition of the splitting class: it is asserted that the class is downwards closed under enumeration reducibility and splits, yet the proof sketch does not address whether the closure operation preserves the incomparabilities required to falsify WLEM instances in the generated algebra.
minor comments (2)
  1. [Introduction] The notation for the Dyment lattice and Dyment-Muchnik lattice is introduced without a forward reference to the precise definitions in the literature; a single sentence recalling the standard definitions would improve readability.
  2. [final section] Several claims about 'naturally definable classes' in the final section would benefit from an explicit list or table of the classes considered and the reason each fails to split.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading of the manuscript and for highlighting the need for greater explicitness in the Dyment-Muchnik construction. We agree that the separation of IPC from WLEM in the initial segment relies on preserving specific incomparabilities, and that the current text leaves this verification somewhat implicit. We will revise §5 and the proof of Theorem 5.3 to supply the missing details while preserving the correctness of the constructions.

read point-by-point responses

  1. Referee: [§5] §5 (Dyment-Muchnik construction): the argument that the chosen splitting class generates an initial segment whose Brouwer algebra validates exactly IPC (and not WLEM) rests on keeping certain pairs of degrees incomparable; the text does not supply an explicit verification that the splitting property does not force any such pair to become comparable, which is load-bearing for the separation from the full lattice.

    Authors: We accept that an explicit verification is required. The splitting class is constructed so that the generators of the algebra remain pairwise incomparable by ensuring that any new degrees introduced by splitting are chosen below existing bounds without creating reductions between the critical pairs. In the revised manuscript we will add a lemma immediately after the definition of the splitting class that proves, for each pair a, b used to falsify a WLEM instance, that no enumeration reduction from a to b or b to a is introduced by the splitting operation. This will make the separation from the full lattice fully rigorous. revision: yes

  2. Referee: [Theorem 5.3] Theorem 5.3 and the preceding definition of the splitting class: it is asserted that the class is downwards closed under enumeration reducibility and splits, yet the proof sketch does not address whether the closure operation preserves the incomparabilities required to falsify WLEM instances in the generated algebra.

    Authors: We agree the proof sketch is too brief on this point. The downwards closure is taken only over degrees already compatible with the chosen incomparabilities; because the splitting is performed uniformly below each generator, no new comparability between the key pairs can arise. In the revision we will expand the proof of Theorem 5.3 with a short argument showing that if a and b are incomparable before closure, then any degree c ≤ a or c ≤ b introduced by closure remains incomparable to the other generator, thereby preserving the falsification of the relevant WLEM instance. revision: yes

Circularity Check

0 steps flagged

No circularity; construction is independent within enumeration degrees

full rationale

The paper establishes existence of initial segments via explicit construction of a splitting class of enumeration degrees for the Dyment-Muchnik lattice, while noting that the full lattices satisfy IPC + WLEM and that some downwards-closed classes fail to split. This is a direct mathematical construction in computability theory rather than any self-definitional loop, fitted prediction, or load-bearing self-citation chain. No equations or steps reduce the target Brouwer algebra property to the inputs by construction; the result remains falsifiable against external models of enumeration degrees and does not rely on renaming or smuggling prior ansatzes.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper is a pure mathematical result relying on standard background in computability theory; no free parameters, invented entities, or ad-hoc axioms are indicated in the abstract.

axioms (1)
  • standard math Standard properties of enumeration reducibility and the structure of the Dyment and Dyment-Muchnik lattices
    The abstract presupposes established facts about enumeration degrees and lattice constructions from prior literature in the field.

pith-pipeline@v0.9.0 · 5626 in / 1171 out tokens · 35724 ms · 2026-05-21T02:24:04.124097+00:00 · methodology

discussion (0)

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

Lean theorems connected to this paper

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

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

23 extracted references · 23 canonical work pages

  1. [1]

    Balbes and P

    R. Balbes and P. Dwinger.Distributive Lattices. University of Missouri Press, Columbia, Missouri, 1974

    work page 1974

  2. [2]

    Chagrov and A

    M. Chagrov and A. Zakharyashev.Modal Logic. Clarendon Press, Oxford, 1997

    work page 1997

  3. [3]

    S. B. Cooper.Computability Theory. Chapman & Hall/CRC Mathematics, Boca Raton, London, New York, Washington, DC, 2003

    work page 2003

  4. [4]

    de Jongh and A.S

    D.H.J. de Jongh and A.S. Troelstra. On the connection of partially ordered sets with some pseudo-Boolean algebras.Indag. Math., 28:317–329, 1966

    work page 1966

  5. [5]

    E. Z. Dyment. Certain properties of the Medvedev lattice.Mathematics of the USSR Sbornik, 30:321–340, 1976. English Translation

    work page 1976

  6. [6]

    D. M. Gabbay.Semantical Investigations In Heyting’s Intuitionistic Logic. Number 148 in Synthese Library. Springer-Science+Business Media, B.V., Dordrecht, 1981

    work page 1981

  7. [7]

    V. A. Jankov. The calculus of the weak law of excluded middle.Math. USSR Izvestija, 2:997–1004, 1968

    work page 1968

  8. [8]

    I. Sh. Kalimullin. Definability of the jump operator in the enumeration degrees.J. Math. Log., 3(2):257–267, 2003

    work page 2003

  9. [9]

    R. Kuyper. Natural factors of the Muchnik lattice capturing IPC.Ann. Pure Appl. Logic, 164(10):1025–1036, 2013

    work page 2013

  10. [10]

    R. Kuyper. Natural factors of the Medvedev lattice capturing IPC.Arch. Math. Logic, 53(7):865–879, 2014

    work page 2014

  11. [11]

    A. H. Lachlan and R. Lebeuf. Countable initial segments of the degrees.J. Symbolic Logic, 41:289–300, 1976

    work page 1976

  12. [12]

    McEvoy.The Structure of the Enumeration Degrees

    K. McEvoy.The Structure of the Enumeration Degrees. PhD thesis, School of Mathematics, University of Leeds, 1984

    work page 1984

  13. [13]

    Y. T. Medevdev. Degrees of difficulty of the mass problems.Dokl. Nauk. SSSR, 104(4):501–504, 1955

    work page 1955

  14. [14]

    A. A. Muchnik. On strong and weak reducibility of algorithmic problems.Sibirskii Matematicheskii Zhurnal, 4:1328–1341, 1963. Russian. INTUITIONISM AND COMPUTING WITH PARTIAL INFORMATION 27

    work page 1963

  15. [15]

    J. Myhill. A note on degrees of partial functions.Proc. Amer. Math. Soc., 12:519–521, 1961

    work page 1961

  16. [16]

    Rasiowa and R

    H. Rasiowa and R. Sikorski.The Mathematics of Metamathematics. Panstowe Wydawnictwo Naukowe, Warszawa, 1963

    work page 1963

  17. [17]

    Rogers, Jr.Theory of Recursive Functions and Effective Computability

    H. Rogers, Jr.Theory of Recursive Functions and Effective Computability. McGraw-Hill, New York, 1967

    work page 1967

  18. [18]

    E. Z. Skvortsova. Faithful interpretation of the intuitionistic propositional calculus by an initial segment of the Medvedev lattice.Sib. Math. J., 29(1):133–139, 1988

    work page 1988

  19. [19]

    R. I. Soare.Recursively Enumerable Sets and Degrees. Perspectives in Mathematical Logic, Omega Series. Springer-Verlag, Heidelberg, 1987

    work page 1987

  20. [20]

    A. Sorbi. Some remarks on the algebraic structure of the Medvedev lattice.J. Symbolic Logic, 55(2):831–853, 1990

    work page 1990

  21. [21]

    A. Sorbi. Embedding Brouwer algebras in the Medvedev lattice.Notre Dame J. Formal Logic, 32(2):266–275, 1991

    work page 1991

  22. [22]

    A. Sorbi. The Medvedev lattice of degrees of difficulty. In S. B. Cooper, T. A. Slaman, and S. S. Wainer, editors, Computability, Enumerability, Unsolvability - Directions in Recursion Theory, London Mathematical Society Lecture Notes Series, pages 289–312. Cambridge University Press, New York, 1996

    work page 1996

  23. [23]

    Sorbi and S

    A. Sorbi and S. Terwijn. Intuitionistic logic and Muchnik degrees.Algebra Universalis, 67(2):175–188, 2012. Department of Mathematical Logic, Faculty of Mathematics and Computer Science, Sofia University, Sofia Email address:ganchev@fmi.uni-sofia.bg School of Mathematics, University of Leeds, Leeds, LS2 9JT, United Kingdom Email address:p.e.shafer@leeds.a...

    work page 2012