pith. sign in

arxiv: 2409.10418 · v1 · submitted 2024-09-16 · 🧮 math.LO

Hyperformalism for Bunched Natural Deduction Systems

Shay Allen Logan , Blane Worley This is my paper

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

classification 🧮 math.LO
keywords hyperformalismbunched natural deductionrelevant logic Bsubstitutionsintensional contentproofsnatural deduction systems
0
0 comments X

The pith

The relevant logic B exhibits a powerful hyperformalism for bunched natural deduction systems after limited tweaks, extending also to proofs.

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

Hyperformal logics are those closed under substitution classes broader than uniform substitutions. The paper examines a strong form of this property for bunched natural deduction systems that tracks essentially all possible intensional content. It shows that the relevant logic B achieves this form after a few tweaks. The work further extends hyperformalism to cover the proofs themselves in addition to the statements proved. A sympathetic reader would care because the results indicate that the range of logics supporting hyperformalism is wider than prior work suggested.

Core claim

Logics closed under classes of substitutions broader than the class of uniform substitutions are known as hyperformal logics. The paper demonstrates that after a few tweaks the well-known relevant logic B exhibits a very powerful form of hyperformalism for bunched natural deduction systems that tracks essentially all the intensional content that can possibly be tracked. It further demonstrates that hyperformalism can be extended to accommodate not just what is proved in a given logic but the proofs themselves.

What carries the argument

Hyperformalism, the closure under broader classes of substitutions than uniform ones, applied to bunched natural deduction systems and extended to proofs.

Load-bearing premise

The relevant logic B can be modified in limited ways while preserving its core properties and achieving the full intensional tracking in bunched natural deduction.

What would settle it

A concrete substitution class broader than uniform substitutions under which the tweaked B fails to remain closed, or a specific bunched natural deduction whose intensional content cannot be tracked.

read the original abstract

Logics closed under classes of substitutions broader than class of uniform substitutions are known as hyperformal logics. This paper extends known results about hyperformal logics in two ways. First: we examine a very powerful form of hyperformalism that tracks, for bunched natural deduction systems, essentially all the intensional content that can possibly be tracked. We demonstrate that, after a few tweaks, the well-known relevant logic $\mathbf{B}$ exhibits this form of hyperformalism. Second: we demonstrate that not only can hyperformalism be extended along these lines, it can also be extended to accommodate not just what is proved in a given logic but the proofs themselves. Altogether, the paper demonstrates that the space of possibilities for the study of hyperformalism is much larger than might have been expected.

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 / 3 minor

Summary. The paper defines hyperformal logics as those closed under substitutions broader than uniform substitution. It extends prior results by defining a strong form of hyperformalism for bunched natural deduction systems that tracks essentially all intensional content, demonstrates that the relevant logic B satisfies this form after limited modifications, and shows that the same framework can be extended to track proofs themselves rather than only theorems.

Significance. If the constructions hold, the work enlarges the known space of hyperformal logics by providing explicit demonstrations for bunched ND systems and for proof-tracking, with B serving as a concrete example that preserves its core relevance properties under the described tweaks. The paper supplies direct constructions rather than derivations from unstated assumptions.

minor comments (3)
  1. The abstract refers to 'a few tweaks' to B; the manuscript should include an explicit list or table of these modifications and a verification that they preserve the relevance properties of B (e.g., no introduction of irrelevant implications).
  2. Notation for bunched natural deduction and the hyperformal substitution classes should be introduced with a short glossary or reference to standard definitions to aid readers unfamiliar with the bunched-logic literature.
  3. The extension to proof-tracking is described at a high level; a small worked example showing how a specific proof is tracked under the hyperformal substitution would strengthen the second claim.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment of the manuscript, including the summary of our results on hyperformalism for bunched natural deduction systems and the extension to proof-tracking, as well as the recommendation for minor revision. No specific major comments appear in the report.

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper presents explicit formal constructions demonstrating that (after limited tweaks) relevant logic B satisfies a strong form of hyperformalism for bunched natural deduction, plus an extension to track proofs themselves. These are direct demonstrations in a mathematical logic context, with no reduction of claims to fitted parameters, self-definitional loops, or load-bearing self-citations. The derivation chain is self-contained against external benchmarks in proof theory.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract provides no details on free parameters, axioms, or invented entities used in the demonstrations.

pith-pipeline@v0.9.0 · 5655 in / 879 out tokens · 29805 ms · 2026-05-23T20:57:09.042177+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

19 extracted references · 19 canonical work pages

  1. [1]

    Alan Ross Anderson and Nuel D. Belnap. Entailment: The Logic of Relevance and Neccessity, V ol. I . Princeton University Press, 1975

    work page 1975

  2. [2]

    R. B. Angell. Three systems of first degree entailment. Journal of Symbolic Logic, 42(1):147, 1977

    work page 1977

  3. [3]

    R. B. Angell. Deducibility, entailment and analytic con tainment. In J. Norman and R. Sylvan, editors, Di- rections in Relevant Logic , Reason and Argument, pages 119–143. Kluwer Academic Publi shers, Boston, MA, 1989

    work page 1989

  4. [4]

    Nuel D. Belnap. Entailment and relevance. The Journal of Symbolic Logic , 25(2):144–146, 1960

    work page 1960

  5. [5]

    F. Berto. Topics of Thought. Oxford University Press, Oxford, 2022

    work page 2022

  6. [6]

    Ross T. Brady. Depth relevance of some paraconsistent lo gics. Studia Logica: An International Journal for Symbolic Logic, 43(1/2):63–73, 1984

    work page 1984

  7. [7]

    Topic tra nsparency and variable sharing in weak rele- vant logics

    Thomas Macaulay Ferguson and Shay Allen Logan. Topic tra nsparency and variable sharing in weak rele- vant logics. Erkenntnis, pages 1–28, 2023

    work page 2023

  8. [8]

    K. Fine. Angellic content. Journal of Philosophical Logic, 45(2):199–226, 2016

    work page 2016

  9. [9]

    Strong depth relevance

    Shay Allen Logan. Strong depth relevance. The Australasian Journal of Logic , 18(6):645–656, 2021. 5Reminder: we’re assuming that x, y, and w are all reduced and that xw and yw have the same reduction. It’s only in that context that none of these cases are possible. 22 SHA Y ALLEN LOGAN AND BLAINE WORLEY

    work page 2021

  10. [10]

    Depth relevance and hyperformalism

    Shay Allen Logan. Depth relevance and hyperformalism. Journal of Philosophical Logic , 51(4):721–737, 2022

    work page 2022

  11. [11]

    Correction to: Depth relevance and hy performalism

    Shay Allen Logan. Correction to: Depth relevance and hy performalism. Journal of Philosophical Logic , 52(4):1235–1235, 2023

    work page 2023

  12. [12]

    Relevance Logic

    Shay Allen Logan. Relevance Logic. Cambridge University Press, 2024

    work page 2024

  13. [13]

    Relevant Logic: A Philosophical Examination of Inference

    Stephen Read. Relevant Logic: A Philosophical Examination of Inference . Wiley-Blackwell, Oxford, 1988

    work page 1988

  14. [14]

    G. Restall. An Introduction to Substructural Logics . Routledge, New Y ork, 2000

    work page 2000

  15. [15]

    M´ endez

    Gemma Robles and Jos´ e M. M´ endez. Generalizing the depth relevance condition: Deep relevant logics not included in R-mingle. Notre Dame Journal of F ormal Logic, 55(1):107–127, 2014

    work page 2014

  16. [16]

    Meyer, and Ros s T

    Richard Routley, V al Plumwood, Robert K. Meyer, and Ros s T. Brady. Relevant Logics and Their Rivals . Ridgeview, 1982

    work page 1982

  17. [17]

    Lecture notes on the lambda calculus, 2 013

    Peter Selinger. Lecture notes on the lambda calculus, 2 013

    work page

  18. [18]

    Proof invariance

    Blane Worley. Proof invariance. Australasian Journal of Logic, forthcoming

    work page

  19. [19]

    S. Y ablo. Aboutness. Princeton University Press, Princeton, 2014. Email address: salogan@ksu.edu Email address: bdworley@ucdavis.edu

    work page 2014