pith. sign in

arxiv: 2605.12548 · v1 · pith:SW32MZ2Gnew · submitted 2026-05-10 · 💻 cs.LO

Cubical Type Theoretic Navya-Ny\=aya

Mrityunjoy Panday , Sudipta Ghosh This is my paper

Pith reviewed 2026-05-14 21:44 UTC · model grok-4.3

classification 💻 cs.LO
keywords Navya-Nyayacubical type theoryformalizationabhavatadatmyaavacchedakaIndian logictype theory
0
0 comments X

The pith

Cubical type theory encodes Navya-Nyaya's core structures without losing dependent delimitation or non-extensional identity.

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

The paper claims that formalizations of Navya-Nyaya in first-order logic, higher-order logic, and Martin-Löf type theory each lose load-bearing features such as dependent delimitation, typed absence, non-extensional identity, and unbounded relational depth. It shows that cubical type theory succeeds natively by supplying encodings for seven core constructs together with the qualifier-qualificand structure, a stratified-universe foundation for the padartha system, and proofs of four internal signature theorems. A sympathetic reader would care because the encoding preserves the original meaning of the philosophical texts while making their logical relations formally verifiable.

Core claim

We give CTT encodings for seven core constructs (sambandha, avacchedaka, abhava, vyapti, tadatmya, higher relations, paryapti) plus the qualifier-qualificand structure. We develop a stratified-universe foundation for the padartha system and prove four signature theorems internal to the encoding (involution of abhava, kevalanvayi irreducibility, coextension without identity, no h-set collapse) together with six metatheoretic results including soundness, conservativity, and faithfulness.

What carries the argument

The CTT encoding of the qualifier-qualificand structure and abhava, which uses De Morgan cubical operations to model dependent delimitation and relations at arbitrary depth.

Load-bearing premise

The load-bearing structures of Navya-Nyaya can be faithfully captured by the native features of cubical type theory without introducing new postulates that alter the original meaning.

What would settle it

A counterexample would be a core Navya-Nyaya construct or Tattvacintamani passage that cannot be encoded without additional postulates or that violates one of the four signature theorems when interpreted inside the cubical encoding.

read the original abstract

We present a formalization of the technical language of Navya-Nyaya - the "New Logic" school of late-classical Indian philosophy - in CCHM De Morgan cubical type theory (CTT). Previous formalization attempts in first-order logic (Matilal), higher-order logic (Ganeri), and Martin-Lof type theory (Bhattacharyya) each lose load-bearing structure: dependent delimitation (avacchedaka), typed absence (abhava), non-extensional identity (tadatmya), or unbounded relational depth (parampara-sambandha). We argue that CTT closes this gap natively. We give CTT encodings for seven core constructs (sambandha, avacchedaka, abhava, vyapti, tadatmya, higher relations, paryapti) plus the qualifier-qualificand structure; develop a stratified-universe foundation for the padartha system; and prove four signature theorems internal to the encoding (involution of abhava, kevalanvayi irreducibility, coextension without identity, no h-set collapse) and six metatheoretic results (soundness, conservativity, faithfulness, distinction preservation, decidability, commentarial conservativity). We close with worked encodings of fifteen Tattvacintamani passages, comparison with prior formalizations, an implementation sketch in Cubical Agda, and five distinguishing predictions - including a novel argument from Navya-Nyaya's involutive-negation doctrine for the necessity of De Morgan over Cartesian cubical foundations.

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 presents a formalization of the technical language of Navya-Nyaya in CCHM De Morgan cubical type theory (CTT). It provides CTT encodings for seven core constructs including sambandha, avacchedaka, abhava, vyapti, tadatmya, higher relations, and paryapti, along with the qualifier-qualificand structure. A stratified-universe foundation for the padartha system is developed. Four signature theorems are proved internally to the encoding: involution of abhava, kevalanvayi irreducibility, coextension without identity, and no h-set collapse. Six metatheoretic results are established: soundness, conservativity, faithfulness, distinction preservation, decidability, and commentarial conservativity. The manuscript includes worked encodings of fifteen passages from the Tattvacintamani, a comparison with prior formalizations, an implementation sketch in Cubical Agda, and five distinguishing predictions.

Significance. If the encodings faithfully capture the load-bearing structures of Navya-Nyaya without introducing altering postulates, this work represents a significant advance in applying modern type theory to classical Indian philosophy. The use of native CTT features for dependent delimitation and non-extensional identity addresses gaps in previous formalizations in FOL, HOL, and MLTT. The internal proofs of the signature theorems and metatheoretic properties lend credibility to the claims. The inclusion of concrete encodings, implementation sketch, and testable predictions strengthens the contribution and provides a basis for further research in both fields.

minor comments (3)
  1. [Abstract] The abstract lists six metatheoretic results (soundness, conservativity, etc.) without brief definitions or examples; a short parenthetical gloss in the abstract or introduction would aid accessibility for readers outside type theory.
  2. [Implementation sketch] The implementation sketch in Cubical Agda is mentioned but lacks even one short code fragment (e.g., the encoding of abhava as an involutive negation); adding a minimal illustrative snippet would make the claim of native capture more concrete.
  3. Ensure the bibliography contains complete entries for the cited prior formalizations (Matilal, Ganeri, Bhattacharyya) and any CTT references used in the metatheoretic arguments.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the careful and positive evaluation of our manuscript. The recognition of the contribution in applying CTT to Navya-Nyāya, the assessment of the encodings and metatheoretic results, and the recommendation for minor revision are appreciated. No specific major comments were provided in the report.

Circularity Check

0 steps flagged

No significant circularity; derivations are self-contained in native CTT

full rationale

The paper encodes seven Navya-Nyaya constructs directly in CCHM De Morgan cubical type theory and proves its four signature theorems (involution of abhava, kevalanvayi irreducibility, coextension without identity, no h-set collapse) plus six metatheoretic results internally from the native path, interval, and De Morgan structure. No parameter is fitted to data and then relabeled a prediction; no self-citation chain is invoked to justify the central encoding or to forbid alternatives; the qualifier-qualificand structure and stratified universes are introduced explicitly rather than smuggled via prior work by the same authors. The five distinguishing predictions are derived consequences of the involutive-negation encoding rather than inputs renamed as outputs. The argument therefore reduces to standard CTT axioms plus the explicit translation, with no definitional collapse or load-bearing self-reference.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The formalization rests on the background axioms of CCHM De Morgan cubical type theory and the interpretive mapping of Navya-Nyaya terms; no new free parameters or invented entities are introduced beyond the type theory itself.

axioms (1)
  • standard math Axioms and rules of CCHM De Morgan cubical type theory
    The encodings and proofs are developed inside this type theory as stated in the abstract.

pith-pipeline@v0.9.0 · 5584 in / 1129 out tokens · 45780 ms · 2026-05-14T21:44:28.310326+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

35 extracted references · 35 canonical work pages

  1. [1]

    Angiuli, C., Brunerie, G., Coquand, T., Harper, R., Hou (Favonia), K.-B., Licata, D. (2017). Cartesian Cubical Type Theory. Preprint

    work page 2017

  2. [2]

    et al.agda/cubical: A standard library for Cubical Agda.https://github

    Mörtberg, A. et al.agda/cubical: A standard library for Cubical Agda.https://github. com/agda/cubical

    work page

  3. [3]

    grahawithD¯ ıpik¯ a

    Annambhat.t.a.Tarkasam. grahawithD¯ ıpik¯ a. Various editions

    work page

  4. [4]

    Awodey, S. (2018). A cubical model of homotopy type theory.Annals of Pure and Applied Logic169(12): 1270–1294

    work page 2018

  5. [5]

    Bhatt, G. P. (1989).Navya-Ny¯ aya Theory of Verbal Cognition. Eastern Book Linkers

    work page 1989

  6. [6]

    (1990).Gad¯ adhara’s Theory of Objectivity

    Bhattacharyya, S. (1990).Gad¯ adhara’s Theory of Objectivity. ICPR

    work page 1990

  7. [7]

    (1996).Doubt, Belief and Knowledge

    Bhattacharyya, S. (1996).Doubt, Belief and Knowledge. ICPR

    work page 1996

  8. [8]

    (2007).Sabdapramana: Word and Knowledge

    Bilimoria, P. (2007).Sabdapramana: Word and Knowledge. Springer

    work page 2007

  9. [9]

    Cohen, C., Coquand, T., Huber, S., Mörtberg, A. (2018). Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom.TYPES 2015, LIPIcs 69

    work page 2018

  10. [10]

    Various editions

    Gad¯ adhara Bhat.t.¯ ac¯ arya.Vyutpattiv¯ ada;Śaktiv¯ ada. Various editions

    work page

  11. [11]

    (1999).Semantic Powers

    Ganeri, J. (1999).Semantic Powers. Oxford University Press

    work page 1999

  12. [12]

    (2001).Philosophy in Classical India

    Ganeri, J. (2001).Philosophy in Classical India. Routledge

    work page 2001

  13. [13]

    Ganeri, J. (2008). Sanskrit philosophical commentary.Journal of the Indian Council of Philosophical Research25(1): 107–128

    work page 2008

  14. [14]

    Gratzer, D., Sterling, J., Birkedal, L. (2019). Implementing a modal dependent type theory. Proc. ACM Programming Languages3(ICFP), Article 107

    work page 2019

  15. [15]

    (1992).On Being and What There Is

    Halbfass, W. (1992).On Being and What There Is. SUNY Press

    work page 1992

  16. [16]

    Institute for Advanced Study

    The Univalent Foundations Program (2013).Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study. 30

    work page 2013

  17. [17]

    Ingalls, D. H. H. (1951).Materials for the Study of Navya-Ny¯ aya Logic. Harvard Oriental Series 40

    work page 1951

  18. [18]

    k¯ ara.Śabdaśakti-prak¯ aśik¯ a

    Jagad¯ ıśa Tark¯ alam. k¯ ara.Śabdaśakti-prak¯ aśik¯ a. Various editions

    work page

  19. [19]

    Various editions

    Jayadeva Miśra.¯Aloka(commentary on TC). Various editions

    work page

  20. [20]

    Various editions

    Mathur¯ an¯ atha Tarkav¯ ag¯ ıśa.Man.i-prak¯ aśa(commentary on TC). Various editions

    work page

  21. [21]

    Matilal, B. K. (1968).The Navya-Ny¯ aya Doctrine of Negation. Harvard Oriental Series 46

    work page 1968

  22. [22]

    Matilal, B. K. (1985).Logic, Language and Reality. Motilal Banarsidass

    work page 1985

  23. [23]

    Matilal, B. K. (1998).The Character of Logic in India. Eds. J. Ganeri and H. Tiwari. SUNY Press

    work page 1998

  24. [24]

    Mohanty, J. N. (1992).Reason and Tradition in Indian Thought. Oxford University Press

    work page 1992

  25. [25]

    Phillips, S. H. (1995).Classical Indian Metaphysics. Open Court

    work page 1995

  26. [26]

    Potter, K. H. (ed.) (1977).Encyclopedia of Indian Philosophies, Vol. II. Princeton University Press

    work page 1977

  27. [27]

    Praśastap¯ ada.Pad¯ artha-dharma-sam. graha. Various editions

    work page

  28. [28]

    Raghun¯ atha Śiroman.i.Pad¯ artha-tattva-nir¯ upan.am. Ed. and trans. K. H. Potter, Harvard Oriental Series 17, 1957

    work page 1957

  29. [29]

    Sattler, C. (2017). The equivalence extension property and model structures. Preprint

    work page 2017

  30. [30]

    Staal, J. F. (1988).Universals: Studies in Indian Logic and Linguistics. University of Chicago Press

    work page 1988

  31. [31]

    Streicher, T. (1993). Investigations into Intensional Type Theory. Habilitation, Munich

    work page 1993

  32. [32]

    Ga˙ ngeśa Up¯ adhy¯ aya.Tattvacint¯ aman.i. Ed. K¯ am¯ akhy¯ an¯ atha Tarkav¯ ag¯ ıśa. Bibliotheca Indica, 1888–1901

    work page 1901

  33. [33]

    Vezzosi, A., Mörtberg, A., Abel, A. (2021). Cubical Agda.Journal of Functional Program- ming31:e8

    work page 2021

  34. [34]

    Viśvan¯ atha.Bh¯ as.¯ aparicchedawithSiddh¯ antamukt¯ aval¯ ı. Trans. S. M¯ adhav¯ ananda, Almora, 1954

    work page 1954

  35. [35]

    Voevodsky, V. (2014). The origins and motivations of univalent foundations.Institute for Advanced Study Letter. 31

    work page 2014