1. Paraconsistent logic
  2. Homotopy type theory
  3. Navya-Nyāya

Paraconsistent logic

The contemporary logical orthodoxy has it that, from contradictory premises, anything can be inferred. Let ⊨ be a relation of logical consequence, defined either semantically or proof-theoretically. Call ⊨ explosive if it validates {A, ¬A} ⊨ B for every A and B (ex contradictione quodlibet (ECQ)). Classical logic, and most standard ‘non-classical’ logics too such as intuitionist logic, are explosive. Inconsistency, according to received wisdom, cannot be coherently reasoned about.

Paraconsistent logic challenges this orthodoxy. A logical consequence relation, ⊨, is said to be paraconsistent if it is not explosive. Thus, if ⊨ is paraconsistent, then even if we are in certain circumstances where the available information is inconsistent, the inference relation does not explode into triviality. Thus, paraconsistent logic accommodates inconsistency in a sensible manner that treats inconsistent information as informative. The prefix ‘para’ in English has two meanings: ‘quasi’ (or ‘similar to, modelled on’) or ‘beyond’.

Homotopy type theory

Homotopy type theory is a new branch of mathematics that combines aspects of several different fields in a surprising way. It is based on a recently discovered connection between homotopy theory and type theory. Homotopy theory is an outgrowth of algebraic topology and homological algebra, with relationships to higher category theory, while type theory is a branch of mathematical logic and theoretical computer science. Although the connections between the two are currently the focus of intense investigation, it is increasingly clear that they are just the beginning of a subject that will take more time and more hard work to fully understand. It touches on topics as seemingly distant as the homotopy groups of spheres, the algorithms for type checking, and the definition of weak ∞-groupoids.

Homotopy type theory also brings new ideas into the very foundation of mathematics. On the one hand, there is Voevodsky’s subtle and beautiful univalence axiom. The univalence axiom implies, in particular, that isomorphic structures can be identified, a principle that mathematicians have been happily using on workdays, despite its incompatibility with the “official” doctrines of conventional foundations. On the other hand, we have higher inductive types, which provide direct, logical descriptions of some of the basic spaces and constructions of homotopy theory: spheres, cylinders, truncations, localizations, etc. When combined in homotopy type theory, these innovations permit an entirely new kind of “logic of homotopy types.”

This suggests a new conception of foundations of mathematics with intrinsic homotopical content, an “invariant” conception of the objects of mathematics, and convenient machine implementations, which can serve as a practical aid to the working mathematician. This is the univalent foundations program.


Two older Indian philosophical traditions, the Nyāya (grounded in Gautama Akṣapāda's Nyāya-sūtra, c. 100 C.E., and dealing mainly with logic, epistemology, and the theory of debate) and the Vaiśeṣika (grounded in Kaṇāda's Vaiśeṣika-sūtra, c. 100 B.C.E., dealing mainly with ontology), developed in parallel until, at some point in the 11th or 12th century, they merged to form a new school, called “Navya-Nyāya”, the new Nyāya. Despite its name, Navya-Nyāya incorporates and develops classical Vaiśeṣika metaphysics as well as classical Nyāya epistemology. The Navya-Nyāya authors also develop a precise technical language through the employment of which many traditional philosophical problems could be clarified and resolved. Navya-Nyāya techniques proved to be so versatile that they were employed, not just by philosophers, but also in poetics, linguistics, legal theory, and other domains of medieval Indian thought. The foundational text of this school was Gaṅgeśa's brilliant and innovative Jewel of Reflection on the Truth (Tattvacintāmaṇi). The school continued to develop for about four centuries, reaching its heights with the works of Raghunātha, Jagadīśa and Gadādhara. The sophisticated use this school made of its technical vocabulary made it increasingly inaccessible, and so, in the 17th and 18th centuries, several manuals or compendia were written to explain in simplified language the basic tenets of the school.