pith. sign in

arxiv: 2605.29880 · v1 · pith:A4SWOZZXnew · submitted 2026-05-28 · 🧮 math.LO

Undecidability in Relevant Logic

S{\o}ren Brinck Knudstorp This is my paper

Pith reviewed 2026-06-28 23:55 UTC · model grok-4.3

classification 🧮 math.LO
keywords relevant logicundecidabilityWang tilingsemilattice semanticshypothetical syllogismpositive relevant logicR logicE logic
0
0 comments X

The pith

Every positive relevant logic from hypothetical syllogism axioms up to semilattice logic S is undecidable.

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

The paper proves undecidability for every positive relevant logic that extends the axioms of hypothetical syllogism, prefixing and suffixing while remaining inside the logic of the semilattice frame on finite subsets of the naturals. The proof works by reducing the Wang tiling problem on arbitrarily large finite isosceles right triangles to the question of formula validity in these logics. This directly shows that the semilattice relevant logic S itself is undecidable, overturning prior expectations, and supplies a fresh reduction proof for the undecidability of R, E and T. A reader cares because the result closes a long-open decision question for an entire interval of relevant logics by embedding a known undecidable geometric problem into the semantics.

Core claim

We prove undecidability for every positive relevant logic extending the system axiomatized by hypothetical syllogism, prefixing, and suffixing and contained in the logic of the semilattice frame (P_fin(N), ∪, ∅). This settles the longstanding decision problem for the semilattice relevant logic S in the negative, contrary to prevailing expectations of decidability. It also provides a new proof of Urquhart's (1984) undecidability theorem for R, E, and T, now by reduction from the Wang tiling problem for arbitrarily large finite isosceles right triangular regions of the plane.

What carries the argument

Reduction from the Wang tiling problem on finite isosceles right triangular regions of the plane to the validity problem in semilattice frame semantics.

If this is right

  • The semilattice relevant logic S is undecidable.
  • The logics R, E and T are undecidable, with a new proof via triangular tiling.
  • No decision procedure exists for any positive relevant logic strictly between the basic axioms and S.
  • Validity checking in these logics can encode the existence of tilings of arbitrary finite triangular regions.

Where Pith is reading between the lines

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

  • Similar tiling reductions may establish undecidability for other substructural logics whose semantics contain semilattice-like structures.
  • The boundary between decidable and undecidable relevant logics may be located by checking which frames can embed triangular tiling constraints.
  • Extending the result to logics with negation or to infinite regions could reveal further undecidability thresholds.

Load-bearing premise

The reduction correctly translates the existence of a tiling into non-validity of a corresponding formula without allowing the logic to decide the tiling question on its own.

What would settle it

An algorithm that decides validity for all formulas in the semilattice relevant logic S, or an explicit triangular region together with its encoded formula where the tiling exists but the formula is valid (or the converse).

Figures

Figures reproduced from arXiv: 2605.29880 by S{\o}ren Brinck Knudstorp.

Figure 1
Figure 1. Figure 1: The lower staircase for O(3); its construction relies on (h) and (p) [PITH_FULL_IMAGE:figures/full_fig_p010_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: The upper staircase for O(3), constructed via (s). Finally, the octant O(3) is constructed from the upper staircase by means of (p) (x · y) · z ⊆ x · (y · z), as in [PITH_FULL_IMAGE:figures/full_fig_p011_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: The octant O(3), constructed recursively from the upper staircase via (p): first the dashed , then the dotted . Remark 3.3 (Sources of (un)decidability). This highlights the role of Hypo￾thetical syllogism, Prefixing and Suffixing in driving undecidability. In com￾parison, recall that omitting Hypothetical syllogism from TWJ+ gives the de￾cidable logic TW+. This reflects a more general phenomenon: its (Hyp… view at source ↗
Figure 4
Figure 4. Figure 4: Extending the lower staircase to the upper staircase through (s) (a · b) · c ⊆ b · (a · c). Part III. To generate the full octant O(k), we need points gi,j for all 0 ≤ i ≤ j ≤ k with xi+1 · gi,j ∋ gi+1,j and gi,j · yj+1 ∋ gi,j+1. (4) We obtain these points recursively. The base case is the upper staircase, where (4) already holds. For the inductive step, suppose xi+1 · gi,j ∋ gi+1,j and gi+1,j · yj+1 ∋ gi+… view at source ↗
Figure 5
Figure 5. Figure 5: Generating the octant O(k) from the upper staircase through (p) (a · b) · c ⊆ a · (b · c). Part IV. Having identified the octant within the refuting model, we define a tiling τ : O(k) → W by (m, n) 7→ t ∈ W such that gm,n ⊩ t. We show that τ is well-defined and satisfies the tiling conditions. For well-definedness, we first verify that each octant point gm,n satisfies at most one tile formula t for t ∈ W. … view at source ↗
read the original abstract

We prove undecidability for every positive relevant logic extending the system axiomatized by hypothetical syllogism, prefixing, and suffixing and contained in the logic of the semilattice frame $(P_{\mathrm{fin}}(\mathbb{N}), \cup, \varnothing)$. This settles the longstanding decision problem for the semilattice relevant logic S in the negative, contrary to prevailing expectations of decidability. It also provides a new proof of Urquhart's (1984) undecidability theorem for R, E, and T, now by reduction from the Wang tiling problem for arbitrarily large finite isosceles right triangular regions of the plane.

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

Summary. The manuscript proves undecidability for every positive relevant logic extending the axiomatization consisting of hypothetical syllogism, prefixing, and suffixing and contained in the semilattice logic S, interpreted over the frame (P_fin(N), ∪, ∅). The central argument is a reduction from the undecidability of the Wang tiling problem restricted to arbitrarily large finite isosceles right triangular regions of the plane; this yields a negative resolution of the decision problem for S and supplies an alternative proof of Urquhart’s 1984 undecidability theorems for R, E, and T.

Significance. If the reduction is faithful, the result is significant: it resolves a longstanding open question for the semilattice logic S (previously expected to be decidable) and furnishes a new, tiling-based proof for the undecidability of the stronger systems R, E, and T. The technique is standard in the field and directly extends cited prior work of Urquhart.

minor comments (1)
  1. The abstract states that the result is 'contrary to prevailing expectations of decidability' for S; a single sentence indicating the source of those expectations (e.g., a citation or prior conjecture) would help readers situate the claim.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment and recommendation to accept the manuscript. The report accurately summarizes the main results.

Circularity Check

0 steps flagged

No significant circularity; reduction to external undecidability result

full rationale

The paper establishes undecidability of the target relevant logics by explicit reduction from the Wang tiling problem on finite isosceles right triangles, an independently known undecidable problem. This is an external benchmark, not a self-referential definition, fitted parameter, or self-citation chain. The construction embeds tiling constraints into the semilattice frame semantics without deriving the undecidability from the logics' own axioms or prior results by the same author. No step matches the enumerated circularity patterns; the central claim remains independent of its own outputs.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The proof rests on standard properties of relevant logic axioms and the semilattice frame together with the known undecidability of a tiling problem; no free parameters or new entities are introduced in the abstract.

axioms (2)
  • domain assumption The semilattice frame (P_fin(N), ∪, ∅) validates exactly the target relevant logics
    Stated in the abstract as the upper bound containing the logics under consideration.
  • standard math Wang tiling is undecidable for arbitrarily large finite isosceles right triangular regions
    Used as the source problem for the reduction; treated as an established fact.

pith-pipeline@v0.9.1-grok · 5628 in / 1416 out tokens · 37244 ms · 2026-06-28T23:55:54.907703+00:00 · methodology

discussion (0)

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

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Possibly Relevant Translations

    math.LO 2026-06 unverdicted novelty 6.0

    Translations from relevant logics to normal modal logics are developed to explore their structural connections.

Reference graph

Works this paper leans on

13 extracted references · cited by 1 Pith paper

  1. [1]

    ,Diamonds and dominoes: Impossibility results for associative modal logics, 2025, Preprint

    2025

  2. [2]

    ,Possibly relevant translations,Advances in modal logic, aiml 2026, 2026

    2026

  3. [3]

    [18]Saul A

    ,R is incomplete for sets, Unpublished manuscript, in preparation. [18]Saul A. Kripke,The problem of entailment,The Journal of Symbolic Logic, vol. 24 (1959), no. 4, p. 324, Abstract. [19]L. Lipshitz,The undecidability of the word problems for projective geometries and modular lattices,Transactions of the American Mathematical Society, vol. 193 (1974), pp...

    1959

  4. [4]

    [24]Alasdair Urquhart,Semantics for relevant logics,The Journal of Symbolic Logic, vol

    ,Relevant logics: Implication, modality, quantification, Cambridge Univer- sity Press, 2026. [24]Alasdair Urquhart,Semantics for relevant logics,The Journal of Symbolic Logic, vol. 37 (1972), pp. 159 – 169

    2026

  5. [5]

    thesis, University of Pittsburgh, 1973

    ,The semantics of entailment,Ph.D. thesis, University of Pittsburgh, 1973

    1973

  6. [6]

    49 (1984), no

    ,The undecidability of entailment and relevant implication,The Journal of Symbolic Logic, vol. 49 (1984), no. 4, pp. 1059–1073

    1984

  7. [7]

    64 (1999), no

    ,The complexity of decision procedures in relevance logic II,The Journal of Symbolic Logic, vol. 64 (1999), no. 4, pp. 1774–1802

    1999

  8. [8]

    13 (2016)

    ,Relevance logic: Problems open and closed,The Australasian Journal of Logic, vol. 13 (2016)

    2016

  9. [9]

    20 (2023), no

    ,The geometry of relevant implication II,The Australasian Journal of Logic, vol. 20 (2023), no. 1, pp. 88–94. [30]John von Neumann,Continuous geometry, Princeton University Press, Princeton, New Jersey, 1960. [31]Hao Wang,Proving theorems by pattern recognition — II,The Bell System Technical Journal, vol. 40 (1961), no. 1, pp. 1–41

    2023

  10. [10]

    ,Dominoes and the∀∃∀case of the decision problem,Mathematical theory of automata, 1963, pp. 23–55. [33]Yale Weiss,A note on the relevance of semilattice relevance logic,Australasian Journal of Logic, vol. 16 (2019), no. 6, pp. 177–185

    1963

  11. [11]

    109 (2021), pp

    ,A characteristic frame for positive intuitionistic and relevance logic,Studia Logica, vol. 109 (2021), pp. 687–699

    2021

  12. [12]

    109 (2021), pp

    ,A conservative negation extension of positive semilattice logic without the finite model property,Studia Logica, vol. 109 (2021), pp. 125–136

    2021

  13. [13]

    15 (2021), pp

    ,A reinterpretation of the semilattice semantics with applications,Logica Uni- versalis, vol. 15 (2021), pp. 171–191. 27 [37]Yale WeissandShawn Standefer,Constructivism and relevance,Erkenntnis, (forthcoming). ILLC & PHILOSOPHY UNIVERSITY OF AMSTERDAM AMSTERDAM, THE NETHERLANDS E-mail: s.b.knudstorp@uva.nl URL: https://knudstorp.github.io/

    2021