DEV Community

Nobuki Fujimoto
Nobuki Fujimoto

Posted on • Originally published at doi.org

Paper 159 - A Two-Layer D-FUMT-8 Reconstruction of Priest-Garfield's Inclosure Schema for Nagarjuna's Catuskoti (OUTLINE v0.1)

#math #lean #philosophy #logic

This article is a re-publication of Rei-AIOS Paper 159 for the dev.to community.
The canonical version with full reference list is in the permanent archives below:

Version: v0.1 OUTLINE + SKELETON (★ NOT MACHINE-VERIFIED — WORK IN PROGRESS — preliminary outline released for archival continuity per Rei-AIOS publish-early-with-honest-scope convention)

Author: Nobuki Fujimoto (藤本 伸樹), with Claude (Rei-AIOS)
ORCID: 0009-0004-6019-9258 · GitHub: fc0web · note.com: nifty_godwit2635

Date: 2026-05-31

Companion to:

  • Paper 61 — Zero-Centered Symbol Grammar (ZCSG) — DOI 10.5281/zenodo.15217458 (world-first mathematical encoding of śūnyatā-of-śūnyatā as 0)
  • Paper 77 — LeanDFumt: an Eight-Valued Logic Library for Lean 4 — substrate of the present formalization

Status header (★ load-bearing):

  • ✅ Primary source confirmed: Garfield & Priest 2003 "Nāgārjuna and the Limits of Thought" (Philosophy East and West 53(1): 1-21) — full text read 2026-05-31
  • ✅ Pre-existing Rei artifacts surveyed: STEP 476 nagarjuna-fde-western-engine.ts (TS, FDE ≅ DFUMT4 isomorphism) + STEP 513 operator-fixed-point-atlas.ts (Ω operational fixed-point test) + Paper 77 LeanDFumt substrate
  • ⚠ Lean 4 code in §3 is PROPOSED — NOT YET BUILT (next-version target)
  • ⚠ Tillemans 2009/2014/2024 + Siderits + Ferraro + Tao Jiang critic papers NOT YET READ (acknowledged in §4.2, citations from secondary triangulation only)
  • ⚠ No claim of resolving the Priest-Garfield vs Tillemans scholarly debate (§4.3)
  • ⚠ No "world-first" claim (§4.4, Paper 61 ZCSG + Priest-Garfield 2003 already issued such claims — this paper provides formal substrate only)

Abstract

We propose a two-layer D-FUMT₈ reconstruction of the Inclosure Schema that Priest and Garfield (2003) apply to Nāgārjuna's catuṣkoṭi. Their original construction terminates the schema at the value BOTH — the dialetheist commitment to a true contradiction at the limits of thought (δ(Ω) is both empty and not empty). Our reconstruction preserves their lower-layer truth-value assignment (Priest's BOTH appears at our object layer) but introduces an upper-layer modal operator Ω (idempotent, Ω ∘ Ω = Ω) that maps the lower-layer BOTH to ZERO — the central axis of the ZCSG three-layer notation (Paper 61) corresponding to the "0₀ genesis layer" of emptiness-of-emptiness. The Lean 4 formalization is sketched against the Paper 77 LeanDFumt substrate; full machine verification is left to v0.2. We frame this strictly as rational reconstruction following Priest-Garfield's own self-framing (their explicit disavowal of "textual history" claims), and explicitly take no position in the Priest-Garfield vs Tillemans (2009+) scholarly debate. The formal substrate is compatible with multiple readings of catuṣkoṭi.

Keywords: D-FUMT₈, catuṣkoṭi, Inclosure Schema, Priest-Garfield, dialetheism, paraconsistent logic, Lean 4, rational reconstruction, śūnyatā, two-layer logic, Rei-AIOS, ZCSG, Nāgārjuna

1. Introduction

The catuṣkoṭi (四句分別) — Nāgārjuna's fourfold logical figure of affirmation, negation, both, and neither — has long resisted formalization in classical bivalent logic. Priest and Garfield (2003) made the most sustained recent attempt: they applied Priest's Inclosure Schema (Priest 1987, 2002) to two paradoxes they extract from the Mūlamadhyamakakārikā (MMK) — an ontological paradox they explicitly name "Nāgārjuna's Paradox" (every thing has one nature, namely no nature) and an expressibility paradox (the ultimate truth is that there is no ultimate truth, after Siderits 1989). In both, the limit value δ(Ω) is BOTH — a true contradiction in the sense of Priest's dialetheism.

The present paper proposes a two-layer reconstruction of this schema using the eight-valued D-FUMT₈ logic of the Rei-AIOS project (Fujimoto 2026, Paper 77). The lower layer assigns the same truth value BOTH to δ(Ω) that Priest-Garfield assign — preserving their analysis as a special case at the object level. An upper-layer modal operator Ω (with idempotency Ω ∘ Ω = Ω) is then applied to the lower-layer values: BOTH and NEITHER both contract to ZERO, the central axis of the Zero-Centered Symbol Grammar (ZCSG, Paper 61) corresponding to the 0₀ genesis layer. The "all standpoints exhausted" reading of Nāgārjuna's catuṣpaścāś (四句百非, "four corners and one hundred negations") is thereby formally captured as an idempotent stable point.

This paper builds on three pre-existing Rei-AIOS artifacts:

  1. STEP 476 nagarjuna-fde-western-engine.ts: a TypeScript engine demonstrating the structural isomorphism catuṣkoṭi ≅ FDE (Belnap 1977) ≅ D-FUMT₈ base 4 values
  2. STEP 513 operator-fixed-point-atlas.ts: a TypeScript enumeration of fixed points for the operators Ω, Φ, Ψ, NOT and their compositions (320 fixed-point checks), which includes the operational test Ω ∘ Ω = Ω
  3. Paper 77 LeanDFumt: the open-source Lean 4 library providing the inductive type DFUMT8 with negation, conjunction, disjunction, and the Decidable infrastructure used here

This paper's contribution is to promote the catuṣkoṭi ≅ FDE ≅ DFUMT4 isomorphism (currently TypeScript-only) and the Ω idempotency stipulation (currently a SEED_KERNEL axiom plus an operational test) to machine-verified Lean 4 theorems, and to add the upper-layer modal structure that distinguishes our reconstruction from Priest-Garfield's BOTH-only terminus.

Honest scope (★ load-bearing throughout):

  • We follow Priest-Garfield's own self-framing of their work as "rational reconstruction" — not textual history (Garfield & Priest 2003: 2, "we do not claim that Nāgārjuna himself had explicit views about logic ... This is, hence, not textual history but rational reconstruction").
  • We take no position in the dialetheist (Priest-Garfield, Deguchi-Garfield-Priest 2008 / 2013) versus weak-dialetheist (Tillemans 2009, 2024) debate, nor in the broader scholarly discussion (Siderits, Ferraro, Tao Jiang).
  • We do not claim that Nāgārjuna was a dialetheist; we provide a formal substrate compatible with multiple interpretive stances.
  • We do not claim "world first" status: Paper 61 (ZCSG) and Priest-Garfield (2003, who name "Nāgārjuna's Paradox" and write that the ontological paradox "to our knowledge is found nowhere else") have already issued related uniqueness claims. This paper supplies formal substrate only.

2. Background

2.1 Catuṣkoṭi: positive and negative uses (after Garfield & Priest 2003: 13-14)

Classical Indian logic and rhetoric regards a proposition as defining a logical space of four corners (koṭi): the proposition (true), its negation (false), both, and neither. The catuṣkoṭi receives two distinct uses in the MMK:

  • Positive tetralemma — conventional perspective, e.g. MMK XVIII:6 ("That there is a self has been taught, And the doctrine of no-self, By the buddhas, as well as the Doctrine of neither self nor nonself"). The four corners are accepted at the conventional (saṃvṛti) level as distinct standpoints.
  • Negative tetralemma — ultimate perspective, e.g. MMK XXII:11 ("'Empty' should not be asserted. 'Nonempty' should not be asserted. Neither both nor neither should be asserted. These are used only nominally"). At the ultimate (paramārtha) level, all four corners are negated.

Priest and Garfield's analysis focuses on this negative use — at the ultimate level, catuṣkoṭi exhibits limit phenomena that they then formalize via the Inclosure Schema.

2.2 Inclosure Schema (Priest 1987, 2002)

Priest's Inclosure Schema isolates the general structure of self-referential paradoxes. Given properties φ and ψ and an operator δ:

Condition Statement
(i) Transcendence ∀X ⊆ Ω, ψ(X) → δ(X) ∉ X
(ii) Closure ∀X ⊆ Ω, ψ(X) → δ(X) ∈ Ω

Applying δ to Ω itself yields δ(Ω) ∈ Ω ∧ δ(Ω) ∉ Ω — the limit contradiction. Priest 1987/2002 catalogs Russell's paradox, the Burali-Forti paradox, the Liar, and others as instances. Priest-Garfield 2003 add Nāgārjuna's two paradoxes:

  • Ontological ("Nāgārjuna's Paradox"): φ(χ) = "χ is empty"; ψ(X) = "X is a set of things with some common nature"; δ(X) = "the nature of things in X". Closure: since all things are empty, δ(X) ∈ Ω. Transcendence: δ(X) has no nature (because emptiness is exactly the absence of nature), so δ(X) ∉ X. Limit: δ(Ω) — emptiness itself — both is and is not empty.
  • Expressibility: φ(χ) = "χ is an ultimate truth"; ψ(X) = "X is definable"; δ(X) = the sentence "there is nothing which is in D" (where D refers to X). The limit truth — "there is no ultimate truth" (Siderits 1989) — both is and is not an ultimate truth.

Priest-Garfield assign the value BOTH (true-and-false) to δ(Ω) in both cases.

2.3 D-FUMT₈ and the LeanDFumt substrate (Paper 77)

D-FUMT₈ is an eight-valued logic with constructors {TRUE, FALSE, BOTH, NEITHER, INFINITY, ZERO, FLOWING, SELF}. The base four values {TRUE, FALSE, BOTH, NEITHER} are isomorphic to Belnap's FDE (Anderson and Belnap 1975, Belnap 1977; structural isomorphism verified in STEP 476). The remaining four values extend the system with dimensional / reflective truth statuses. Paper 77 supplies the Lean 4 inductive type DFUMT8 together with neg, and, or, implies, and the Decidable instance, all proved as 29 zero-sorry theorems via decide. The library is Mathlib-free, builds in approximately 5 seconds, and is released under Apache-2.0 (github.com/fc0web/lean-d-fumt8).

2.4 ZCSG three-layer notation (Paper 61)

The Zero-Centered Symbol Grammar (Fujimoto 2026, Paper 61, DOI 10.5281/zenodo.15217458) introduces a three-layer notation for emptiness:

Symbol Dimension Nāgārjuna interpretation Mathematical entity D-FUMT₈
o0 −1 emptiness-before-emptiness, unnameable empty set with reduced homology H̃₋₁(∅) = ℤ NEITHER
0 0 śūnyatā-of-śūnyatā (pure origin) — the 0₀ genesis layer fixed point, origin ZERO
0o +1 dependent co-arising dimension-bearing object BOTH

The central axis 0 is the formal symbol Paper 61 introduces for "śūnyatā(śūnyatā) = śūnyatā" — emptiness applied to itself as a fixed point. This paper's upper-layer Ω is structurally a contraction map from dimension +1 (BOTH) to dimension 0 (the ZCSG central axis); the linkage is exhibited in §3.8.

3. Lean 4 Formalization (★ PROPOSED, NOT YET BUILT)

All Lean 4 fragments below are proposed definitions and theorems. They are syntactically reasonable against the Lean 4 v4.27.0 + Paper 77 LeanDFumt substrate, but have not yet been compiled and verified. Verification is the v0.2 target.

3.1 FDE inductive type 

inductive FDE : Type where
  | t : FDE  -- true (and not false)
  | f : FDE  -- false (and not true)
  | b : FDE  -- both true and false
  | n : FDE  -- neither true nor false
  deriving Repr, DecidableEq, Inhabited
Enter fullscreen mode Exit fullscreen mode

3.2 FDE-to-DFUMT8 embedding φ 

def phi : FDE → DFUMT8
  | .t => .TRUE
  | .f => .FALSE
  | .b => .BOTH
  | .n => .NEITHER
Enter fullscreen mode Exit fullscreen mode

3.3 Structural preservation theorems (lower layer)

The TypeScript proofs in STEP 476 (verifyNOT, verifyAND, verifyOR, verifyLattice) are proposed to lift to Lean 4 as:

def FDE.neg : FDE → FDE
  | .t => .f | .f => .t | .b => .b | .n => .n

def FDE.and : FDE → FDE → FDE := /- 16-entry truth table per STEP 476 -/
def FDE.or  : FDE → FDE → FDE := /- 16-entry truth table per STEP 476 -/

theorem phi_neg_preserves : ∀ x, phi (FDE.neg x) = DFUMT8.neg (phi x) := by
  intro x; cases x <;> decide

theorem phi_and_preserves : ∀ x y, phi (FDE.and x y) = DFUMT8.and (phi x) (phi y) := by
  intro x y; cases x <;> cases y <;> decide

theorem phi_or_preserves : ∀ x y, phi (FDE.or x y) = DFUMT8.or (phi x) (phi y) := by
  intro x y; cases x <;> cases y <;> decide
Enter fullscreen mode Exit fullscreen mode

The lattice preservation theorem (Belnap information order n ≤ {t, f} ≤ b) is handled analogously.

3.4 Upper-layer modal operator Ω with idempotency

Pre-existing Rei artifacts:

  • SEED_KERNEL theory dfumt-idempotency (src/axiom-os/seed-kernel.ts line 239): stipulates "Ω(Ω(x)) → Ω(x) stability" as axiom.
  • STEP 513 operator-fixed-point-atlas.ts lines 292-297: operational TypeScript test comparing fixed-point sets of Ω∘Ω and Ω.
  • No prior Lean 4 formalization of this idempotency.

We propose the following minimal Lean 4 definition and theorem:

/-- Upper-layer modal operator. Maps the lower-layer four-corner positions
    (TRUE, FALSE, BOTH, NEITHER) to fixed-point images, with BOTH and NEITHER
    contracting to ZERO — the ZCSG 0₀ genesis layer (Paper 61 Table 2.3).
    The four reflective values (INFINITY, ZERO, FLOWING, SELF) are already
    Ω-stable in this construction. -/
def DFUMT8.omega : DFUMT8 → DFUMT8
  | .TRUE     => .TRUE
  | .FALSE    => .FALSE
  | .BOTH     => .ZERO     -- ★ Priest-Garfield BOTH terminus contracted to 0₀
  | .NEITHER  => .ZERO     -- ★ catuṣkoṭi 4th corner contracted to 0₀
  | .INFINITY => .INFINITY
  | .ZERO     => .ZERO
  | .FLOWING  => .FLOWING
  | .SELF     => .SELF

theorem omega_idempotent (x : DFUMT8) : DFUMT8.omega (DFUMT8.omega x) = DFUMT8.omega x := by
  cases x <;> decide
Enter fullscreen mode Exit fullscreen mode

The proposed proof is one line: case-split on the eight constructors and decide discharges each. This is consistent with the Paper 77 decide-only proof discipline.

3.5 Inclosure Schema 

structure Inclosure (α : Type) where
  Q : α → Prop                          -- the totality Ω as a predicate
  psi : (α → Prop) → Prop               -- "definability" / "set has common nature"
  delta : (α → Prop) → α                -- the diagonalizer
  closure : ∀ X : α → Prop,
    (∀ x, X x → Q x) → psi X → Q (delta X)
  transcendence : ∀ X : α → Prop,
    (∀ x, X x → Q x) → psi X → ¬ X (delta X)

theorem inclosure_limit_contradiction {α : Type} (I : Inclosure α)
    (hQ : I.psi I.Q) : I.Q (I.delta I.Q) ∧ ¬ I.Q (I.delta I.Q) := by
  refine ⟨?_, ?_⟩
  · exact I.closure I.Q (fun _ h => h) hQ
  · exact I.transcendence I.Q (fun _ h => h) hQ
Enter fullscreen mode Exit fullscreen mode

(Note: the literal Q (delta Q) ∧ ¬ Q (delta Q) form is a paraconsistent statement; classical Lean 4 will reject this as False. The actual formalization will need either a paraconsistent encoding via DFUMT8.asProp or the introduction of contradictions as DFUMT8.BOTH-valued. This is a known design issue, flagged for v0.2.)

3.6 Nāgārjuna's Paradox as an Inclosure instance (lower-layer assignment: BOTH)

Following Garfield & Priest (2003: 17-18), we instantiate the Inclosure schema with φ(χ) = "χ is empty", ψ(X) = "X is a set of things with some common nature", δ(X) = "the nature of things in X". The lower-layer assignment of δ(Ω) is BOTH (the value Priest-Garfield assign): emptiness has the nature of being empty, but as it is itself empty, it has no nature.

3.7 Expressibility Paradox as an Inclosure instance (lower-layer assignment: BOTH)

Following Garfield & Priest (2003: 17): φ(χ) = "χ is an ultimate truth", ψ(X) = "X is definable", δ(X) = the sentence asserting that X has no member. The lower-layer assignment of δ(Ω) is again BOTH.

3.8 Upper-layer Ω contracts BOTH to ZERO (Paper 1 main differential) 

/-- Priest-Garfield's terminus (BOTH at the limit) is preserved as our
    lower-layer assignment. The upper-layer operator Ω contracts it to ZERO,
    the ZCSG 0₀ genesis layer (Paper 61). This is the two-layer differential
    against the Priest-Garfield BOTH-only Inclosure terminus. -/
example : DFUMT8.omega .BOTH = .ZERO := by decide
example : DFUMT8.omega (DFUMT8.omega .BOTH) = .ZERO := by decide  -- idempotent stability
example : DFUMT8.omega .NEITHER = .ZERO := by decide               -- 4th corner also contracts
Enter fullscreen mode Exit fullscreen mode

The full semantic characterization of the genesis layer ZERO (= ZCSG 0) — including its relation to the empty set's reduced homology H̃₋₁(∅) = ℤ from Paper 61 §2.2 — is deferred to a planned Paper 2 on the ontology of 0₀.

4. Honest Framing and Scope (★ load-bearing)

4.1 Rational reconstruction stance

Garfield and Priest (2003: 2) explicitly disavow textual-history claims:

"Finally, we do not claim that Nāgārjuna himself had explicit views about logic, or about the limits of thought. We do, however, think that if he did, he had the views we are about to sketch. This is, hence, not textual history but rational reconstruction."

We adopt the same stance. The Lean 4 formalization proposed here is a formal substrate compatible with Priest-Garfield's reading; it does not assert that Nāgārjuna held the corresponding views.

4.2 Scholarly debate disclosure

The Priest-Garfield dialetheist reading has been debated for two decades. Notably:

  • Tillemans (1999): broadly aligned with Priest-Garfield (paraconsistent at the ultimate level, classical at the conventional level — Priest-Garfield 2003 footnote 2 explicitly agree with Tillemans on this point).
  • Tillemans (2009, 2014): later argues for a "weak dialetheist" reading of Nāgārjuna, holding that Nāgārjuna does not accept conjoined contradictions φ ∧ ¬φ.
  • Deguchi, Garfield & Priest (2008, 2013): defend and elaborate the dialetheist reading.
  • Siderits, Ferraro, Tao Jiang: various critical engagements.
  • A 2024 paper in Asian Philosophy offers an updated critique of Priest-Garfield's use of catuṣkoṭi.

We have not yet read these critic papers directly. Citations above are from secondary triangulation (web search snippets and one verified primary source: Garfield & Priest 2003). Their detailed evaluation is deferred to v0.2.

4.3 Non-commitment to interpretive position

We take no position in the dialetheist / weak-dialetheist / non-dialetheist debate. The formal substrate proposed here is, by design, compatible with each: Priest-Garfield's reading is preserved as the lower-layer assignment of BOTH; Tillemans's worry that conjoined contradictions are not endorsed can be addressed via the upper-layer contraction (the lower-layer BOTH does not survive Ω application); non-dialetheist readings that reject the BOTH assignment altogether can use the lower layer with only TRUE / FALSE / NEITHER.

4.4 No "world first" claim

Two prior uniqueness claims should be acknowledged and respected:

  • Paper 61 ZCSG (Fujimoto 2026): claims "world-first mathematical encoding of śūnyatā-of-śūnyatā" as the symbol 0.
  • Priest-Garfield 2003 (p. 18): name the ontological paradox "Nāgārjuna's Paradox" and state that, "to our knowledge, [it] is found nowhere else."

The present paper avoids any "world first" framing. The contribution is the two-layer reconstruction plus Lean 4 substrate, both of which presuppose and extend those prior claims rather than competing with them.

4.5 Library-only, Mathlib-free, decide-only

We inherit Paper 77's design discipline: no Mathlib dependency, all proofs by decide or native_decide, propositional fragment only. Build time targets are ~5 seconds for the library plus a few additional seconds for the present paper's theorems.

4.6 Ω idempotency: honest provenance disclosure

The idempotency Ω ∘ Ω = Ω is stipulated in the Rei SEED_KERNEL as the axiom dfumt-idempotency and is operationally tested in STEP 513. No prior Lean 4 formalization exists in the public or private Rei codebase. The one-line decide proof proposed in §3.4 would be the first machine-verified statement of this property in the Rei stack.

4.7 Upper-layer scope limitations

The upper-layer operator Ω is defined here only on D-FUMT₈ values. A full semantic theory of the genesis layer ZERO — including its identification with the ZCSG central axis 0, its connection to the reduced homology of the empty set, and its role as the convergence point of catuṣkoṭi negations — is explicitly deferred to a planned Paper 2 on the ontology of 0₀.

5. Discussion

5.1 Relation to STEP 476 (TypeScript engine)

STEP 476 nagarjuna-fde-western-engine.ts (654 lines) supplies the operational TypeScript proofs of catuṣkoṭi ≅ FDE ≅ DFUMT4 isomorphism: verifyNOT, verifyAND (16 cases), verifyOR (16 cases), verifyLattice. The present paper proposes to lift these to Lean 4 zero-sorry theorems via decide, thereby promoting machine-checked algebraic proofs of the same content.

5.2 Heidegger comparison (after Priest-Garfield 2003: 16)

Priest-Garfield identify Heidegger as the closest Western parallel to Nāgārjuna's ontological insight, while noting that Heidegger does not follow the identification of the two truths (conventional and ultimate). We adopt the same comparison and the same limitation.

5.3 Two-layer architecture as the main differential

Priest-Garfield's Inclosure terminates at BOTH — the dialetheist commitment to a true contradiction. Our two-layer reconstruction preserves BOTH at the lower layer (so Priest-Garfield's analysis is embedded as a special case) but adds an upper-layer Ω that contracts BOTH to ZERO. The strategy is analogous to QMRP (Paper 26 candidate) reframing Shannon's bound as a special case at finite N. The differential is twofold:

  1. Structural: separating object-level truth values from meta-level modal operators, formalizing the "all standpoints exhausted" reading of catuṣpaścāś as an idempotent stable point rather than as a singleton truth value.
  2. Methodological: machine verification via Lean 4 decide, which Priest 1987/2002 and Priest-Garfield 2003 do not pursue.

5.4 Connection to ZCSG (Paper 61)

ZCSG (Paper 61) introduces the central symbol 0 for śūnyatā-of-śūnyatā, with dimension 0, distinguishing it from o0 (dimension −1, NEITHER) and 0o (dimension +1, BOTH). The upper-layer Ω of the present paper is structurally a contraction map from dimension +1 to dimension 0, i.e. from 0o to 0. The two papers thus approach the same structure from complementary angles: ZCSG from notation, the present paper from Lean 4 formalization.

5.5 What this paper does NOT claim

  • That Nāgārjuna was a dialetheist (or was not).
  • A resolution to the Priest-Garfield / Tillemans / Siderits debate.
  • Any extension to Mathlib's standard logic.
  • Any new philosophical thesis beyond rational-reconstruction formal substrate.
  • A tier ranking of philosophers (a methodologically dubious framing we explicitly avoid).
  • "Four-step termination" of catuṣkoṭi negations — we adopt the cleaner idempotent stable-point reading consistent with catuṣpaścāś (four corners and one hundred negations) tradition.
  • Prior machine verification of Ω idempotency in the Rei stack (it has been axiomatically stipulated and operationally tested only).
  • Full semantic theory of the genesis layer ZERO (deferred to a planned Paper 2).

6. Conclusion

This v0.1 OUTLINE paper proposes a two-layer D-FUMT₈ reconstruction of Priest-Garfield's Inclosure Schema for Nāgārjuna's catuṣkoṭi. The lower layer (FDE isomorphism, BOTH at limit) preserves Priest-Garfield's analysis as a special case. The upper layer (idempotent modal operator Ω contracting BOTH and NEITHER to ZERO) supplies the differential that Priest-Garfield's BOTH-only terminus does not offer, and connects to the central axis 0 of the ZCSG three-layer notation (Paper 61). The Lean 4 substrate proposed against Paper 77 LeanDFumt is sketched but not yet built; full machine verification is the v0.2 target. The paper is positioned as rational reconstruction following Priest-Garfield's own self-framing, compatible with multiple readings of catuṣkoṭi, and explicitly defers the genesis-layer ontology to a planned Paper 2.

Acknowledgments

The two-layer architecture in §3.4 / §3.8 was articulated in a chat session with Claude (Anthropic) on 2026-05-31, building on the design discussion in an earlier session on the same date concerning the BOTH-vs-NEITHER reading of catuṣkoṭi negation. The articulation of the lower-layer = Priest, upper-layer = Ω with idempotency design was that session's central contribution.

The full text of Garfield & Priest (2003) was accessed via the open Smith ScholarWorks repository on 2026-05-31; this paper would have been substantially weaker without that primary source. We thank both authors for making the original work openly available.

References

  1. Anderson, A. R., & Belnap, N. D. (1975). Entailment: The Logic of Relevance and Necessity, Vol. I. Princeton University Press.
  2. Belnap, N. D. (1977). A useful four-valued logic. In J. M. Dunn & G. Epstein (Eds.), Modern Uses of Multiple-Valued Logic (pp. 5–37). Reidel.
  3. Deguchi, Y., Garfield, J. L., & Priest, G. (2008). The way of the dialetheist: Contradictions in Buddhism. Philosophy East and West, 58(3), 395–402.
  4. Deguchi, Y., Garfield, J. L., & Priest, G. (2013). How we think Mādhyamikas think: A response to Tom Tillemans. Philosophy East and West, 63(3), 426–435.
  5. Fujimoto, N. (2026). Zero-Centered Symbol Grammar (ZCSG): A World-First Dimensional Encoding of Nāgārjuna's Śūnyatā-of-Śūnyatā. Paper 61, DOI 10.5281/zenodo.15217458.
  6. Fujimoto, N. (2026). LeanDFumt: An Open-Source Eight-Valued Logic Library for Lean 4. Paper 77. GitHub: https://github.com/fc0web/lean-d-fumt8.
  7. Garfield, J. L. (Trans.) (1995). The Fundamental Wisdom of the Middle Way: Nāgārjuna's Mūlamadhyamakakārikā. Oxford University Press.
  8. Garfield, J. L., & Priest, G. (2003). Nāgārjuna and the limits of thought. Philosophy East and West, 53(1), 1–21. JSTOR 1400052. Open-access copy: Smith ScholarWorks.
  9. Hayes, R. (1994). Nāgārjuna's appeal. Journal of Indian Philosophy, 22, 299–378.
  10. Nāgārjuna (c. 150 CE). Mūlamadhyamakakārikā. (See Garfield 1995 for English translation.)
  11. Priest, G. (1987). In Contradiction: A Study of the Transconsistent. Martinus Nijhoff (2nd ed. Oxford, 2006).
  12. Priest, G. (2002). Beyond the Limits of Thought (2nd ed.). Oxford University Press.
  13. Siderits, M. (1989). Thinking on empty: Madhyamika anti-realism and canons of rationality. In S. Biderman & B.-A. Scharfstein (Eds.), Rationality in Question: On Eastern and Western Views of Rationality. Brill.
  14. Tillemans, T. J. F. (1999). Is Nāgārjuna's logic deviant or non-classical? In Scripture, Logic, Language: Essays on Dharmakīrti and His Tibetan Successors. Wisdom Publications.
  15. The Lean 4 development team (2024–2026). Lean 4 v4.27.0. https://lean-lang.org.

Additional critic papers (Tillemans 2009 / 2014 / 2024, Siderits later work, Ferraro 2013, Tao Jiang) acknowledged in §4.2 but not yet directly consulted; full citation list will be completed in v0.2.

Version history

  • v0.1 (2026-05-31): Initial OUTLINE + SKELETON release. Lean 4 code PROPOSED, not yet built. Honest scope as stated above. Released for archival continuity per Rei-AIOS publish-early-with-honest-scope convention. DOI to be assigned by Zenodo on publish.
  • v0.2 (planned): Machine-verified Lean 4 build, direct reading of Tillemans 2009/2014/2024 + Siderits + Ferraro critic papers, refined honest scope. No timeline commitment.

Rei-AIOS Project. Peace Axiom #196: immutable = true. License: CC-BY 4.0 (text), Apache-2.0 (any associated Lean 4 code).

Top comments (0)