Searcharxiv⌕ Search

arXiv subjects

Thierry Coquand

Publications and source records attributed to Thierry Coquand.

At least 19 recordsLinked to original sources
arXiv2026

Definitional Inversion, Without Normalisation

We contribute a new proof technique, based on domain theory, to prove key meta-theoretic properties of dependent type systems: definitional inversion properties, i.e. injectivity and no-confusion of type constructors. This proof technique is independent of normalisation, and indeed applies even for the "type-in-type" rule of Martin-Löf's original type theory. Our proof is the first to establish injectivity of type constructors for such a system in the presence of $η$ laws. More generally, the technique is motivated by, and intended for, the metatheory of systems such as Idris, Lean, or dependent Haskell, whose underlying type theory is known to be non-normalising, as well as projects such as MetaRocq or Lean4Lean, where Gödel's second incompleteness theorem means we cannot show normalisation of the object logic in itself. We showcase the method on a small type theory, then explain how it extends to more ambitious extensions.

cs.LO↗
arXiv2026

Auto formalisation of Chaitin and of the surprise incompleteness Theorem

This is a continuation of a previous report on an experiment in autoformalisation of Gödel's second incompleteness theorem in Agda using Claude. Using the framework built in this experiment, Claude could ``automformalise'' Chaitin's proof of the first incompleteness theorem and then the Kritchman-Raz surprise examination paradox version of the second incompleteness. As the first experiment, the project provides a case study of the strengths and limitations of current large language models in mathematics. Since Chaitin's proof involves coding programs, Claude had to represent code as ternary string and could build autonomously a parser and a continuation stack evaluation machine. The fact that we can simulate computations as expected is not completely trivial and we suggested a Gandy/Howard majorisation argument, that Claude had no problem to follow. The resulting formalisation clarifies a number of details left implicit in the original presentation and provides a fully machine-checked proof of these arguments for Church's Basic Recursive Arithmetic.

cs.LO↗
arXiv2026

Auto formalisation of Goedel's Second Incompleteness Theorem in Binary Recursive Arithmetic

We report an experiment in autoformalisation of Gödel's second incompleteness theorem in Agda using Claude. The theorem is formalised for Church's Basic Recursive Arithmetic, following the proof outline given in Guard's 1963 lecture notes. The entire Agda development, comprising approximately 50,000 lines and containing no postulates, was produced through interaction with Claude; the author did not write any Agda code. Beyond the formalisation itself, the project provides a case study of the strengths and limitations of current large language models in mathematics. An initial autonomous attempt based on a paper of Rose failed because of a false Lemma; the resulting formal development produced by Claude established a statement superficially resembling Gödel's theorem but mathematically unrelated to it. This failure was traced to an insufficient specification of the internal provability predicate, illustrating how an LLM may reason correctly from an incorrect formal specification. The final development follows Guard's proof and required the reconstruction of several implicit mathematical arguments, including the role of the internal numeral-encoding operation and the specification of substitution. The resulting formalisation clarifies a number of details left implicit in the original presentation and provides a fully machine-checked proof of Gödel's second incompleteness theorem for Basic Recursive Arithmetic.

cs.LO↗
arXiv2026

Constructive higher sheaf models with applications to synthetic mathematics

There have recently been several developments in synthetic mathematics using extensions of dependent type theory with univalence and higher inductive types: simplicial homotopy type theory, synthetic algebraic geometry and synthetic Stone duality. We provide a foundation of higher sheaf models of type theory in a constructive metatheory and, in particular, build constructive models of these formal systems.

cs.LO↗
arXiv2026

The equivariant model structure on cartesian cubical sets

We develop a constructive model of homotopy type theory in a Quillen model category that classically presents the usual homotopy theory of spaces. Our model is based on presheaves over the cartesian cube category, a well-behaved Eilenberg-Zilber category. The key innovation is an additional equivariance condition in the specification of the cubical Kan fibrations, which can be described as the pullback of an interval-based class of uniform fibrations in the category of symmetric sequences of cubical sets. The main technical results in the development of our model have been formalized in a computer proof assistant.

math.AT↗
arXiv2026

A Generalized Algebraic Theory for Type Theory with Explicit Universe Polymorphism

We present generalized algebraic theories corresponding to slightly modified versions of two of the type theories in our paper Type Theory with Explicit Universe Polymorphism. We first present a generalized algebraic theory for categories with families with extra structure corresponding to Martin-Lof type theory with an external tower of universes. We then present a generalized algebraic theory for level-indexed categories with families with extra structure corresponding to Martin-Lof type theory with explicit universe polymorphism: a theory with universe level judgments, internally indexed universes, and level-indexed products. In this way we get abstract characterizations of the two theories as initial models of their respective generalized algebraic theories. We thus abstract from details of the grammar and inference rules of the type theories and highlight their high-level structure. More broadly, the present work can be viewed as a case study of a uniform approach to categorical logic based on generalized algebraic theories and categories with families. We also discuss the relevance to Voevodsky's initiality conjecture project.

cs.LO↗
arXiv2026

Azumaya algebras and Barr Theorem

We study etale topology and the notion of Azumaya algebra over a commutative ring constructively. As an application of the syntactic version of Barr's Theorem, we show the equivalence between two definitions of Azumaya algebra.

math.AC↗
arXiv2025

A Note About Models of Synthetic Algebraic Geometry

We show how to build models of Synthetic Algebraic Geometry over rings k such that finitely presented k-algebra have a decidable equality. The construction is done in a constructive and weak (same proof theoretic strength as dependent type theory with universes) meta theory.

math.LO↗
arXiv2025

Projective Space in Synthetic Algebraic Geometry

Synthetic algebraic geometry is a new approach to algebraic geometry. It consists in using homotopy type theory extended with three axioms, together with the interpretation of these in a higher version of the Zariski topos, in order to do algebraic geometry internally to this topos. In this article, we will show basic properties of projective n-space $\mathbb{P}^n$ in synthetic algebraic geometry. In particular, we show that the automorphism group of $\mathbb{P}^n$ is $\mathrm{PGL}_{n+1}(R)$ and that the picard group is $\mathbb{Z}$. We will provide different proofs of the latter statement, where the most synthetic approach naturally leads to the refined statement that the type of line bundles on $\mathbb{P}^n$ is the higher type $\mathbb{Z}\times K(R^\times,1)$, where $K(R^\times,1)$ is a delooping of the group of units of the internal base ring $R$.

math.AG↗
arXiv2025

Controlling unfolding in type theory

We present a new way to control the unfolding of definitions in dependent type theory. Traditionally, proof assistants require users to fix whether each definition will or will not be unfolded in the remainder of a development; unfolding definitions is often necessary in order to reason about them, but an excess of unfolding can result in brittle proofs and intractably large proof goals. In our system, definitions are by default not unfolded, but users can selectively unfold them in a local manner. We justify our mechanism by means of elaboration to a core theory with extension types -- a connective first introduced in the context of homotopy type theory -- and by establishing a normalization theorem for our core calculus. We have implemented controlled unfolding in the cooltt proof assistant, inspiring an independent implementation in Agda.

cs.LO↗
arXiv2025

Heitmann dimension of distributive lattices and commutative rings

This paper is the English translation of the first 4 sections of the article ``Dimension de Heitmann des treillis distributifs et des anneaux commutatifs. Publications Mathématiques de Besançon. Algèbre et théorie des nombres, 2006'', after some corrections. Sections 5-7 of the original article are treated a bit more simply in the book ``Henri Lombardi and Claude Quitté. Commutative algebra: constructive methods. Finite projective modules. Springer, 2015.'' We study the notion of dimension introduced by Heitmann in his remarkable article ``Generating non-Noetherian modules efficiently, Mich. Math. J., 31, (1084)'' as well as a related notion, only implicit in his proofs. We first develop this within the general framework of the theory of distributive lattices and spectral spaces. -- Cet article est une version corrigée des 4 premières sections de l'article ``Dimension de Heitmann des treillis distributifs et des anneaux commutatifs. Publications Mathématiques de Besançon. Algèbre et théorie des nombres, 2006'' Les sections 5 à 7 de l'article original sont traitées de manière un peu plus simple dans ``Henri Lombardi and Claude Quitté. Commutative algebra: constructive methods. Finite projective modules. Springer, 2015.'' Nous étudions la notion de dimension introduite par Heitmann dans son article remarquable ``Generating non-Noetherian modules efficiently, Mich. Math. J., 31, (1084)'', ainsi qu'une notion voisine, seulement implicite dans ses démonstrations. Nous développons ceci d'abord dans le cadre général de la théorie des treillis distributifs et des espaces spectraux. Nous appliquons ensuite cette problématique dans le cadre de l'algèbre commutative.

math.AC↗
arXiv2024

Constructive theory of ordinals

In Chapter 3 of his Notes on constructive mathematics, Martin-L{ö}f describes recursively constructed ordinals. He gives a constructively acceptable version of Kleene's computable ordinals. In fact, the Turing definition of computable functions is not needed from a constructive point of view. We give in this paper a constructive theory of ordinals that is similar to Martin-L{ö}f's theory, but based only on the two relations "$x \leq y$" and "$x < y$", i.e., without considering sequents whose intuitive meaning is a classical disjunction. In our setting, the operation "supremum of ordinals" plays an important rôle through its interactions with the relations "$x \leq y$" and "$x < y$". This allows us to approach as much as we may the notion of linear order when the property "$α\leq β$ or $β\leq α$" is provable only within classical logic. Our aim is to give a formal definition corresponding to intuition, and to prove that our constructive ordinals satisfy constructively all desirable properties. Note that by adding classical logic, we would recover the ordinals of usual classical mathematics, at the cost of a loss of computability for most statements given in the usual form.

math.LO↗
arXiv2024

A Foundation for Synthetic Stone Duality

The language of homotopy type theory has proved to be appropriate as an internal language for various higher toposes, for example with Synthetic Algebraic Geometry for the Zariski topos. In this paper we apply such techniques to the higher topos corresponding to the light condensed sets of Dustin Clausen and Peter Scholze. This seems to be an appropriate setting to develop synthetic topology, similar to the work of Martín Escardó. To reason internally about light condensed sets, we use homotopy type theory extended with 4 axioms. Our axioms are strong enough to prove Markov's principle, LLPO and the negation of WLPO. We also define a type of open propositions, inducing a topology on any type. This leads to a synthetic topological study of (second countable) Stone and compact Hausdorff spaces. Indeed all functions are continuous in the sense that they respect this induced topology, and this topology is as expected for these classes of types. For example, any map from the unit interval to itself is continuous in the usual epsilon-delta sense. We also use the synthetic homotopy theory given by the higher types of homotopy type theory to define and work with cohomology. As an application, we prove Brouwer's fixed-point theorem internally.

math.LO↗
arXiv2024

An introduction to Lorenzen's "Algebraic and logistic investigations on free lattices" (1951)

Lorenzen's ``Algebraische und logistische Untersuchungen über freie Verbände'' appeared in 1951 in The Journal of Symbolic Logic. These ``Investigations'' have immediately been recognised as a landmark in the history of infinitary proof theory. Their approach and method of proof have not been incorporated into the corpus of proof theory. Lorenzen proves the admissibility of cut by double induction, on the cut formula and on the complexity of the derivations, without using any ordinal assignment, contrary to the presentation of cut elimination in most standard texts on proof theory. We propose this introduction with the intent of giving a new impetus to their reception. The ``Investigations'' are best known for providing a constructive proof of consistency for ramified type theory without axiom of reducibility. They do so by showing that it is a part of a trivially consistent ``inductive calculus'' that describes our knowledge of arithmetic without detour. The proof resorts only to the inductive definition of formulas and theorems. They propose furthermore a definition of a semilattice, of a distributive lattice, of a pseudocomplemented semilattice, and of a countably complete boolean algebra as deductive calculuses, and show how to present them for constructing conservatively the respective free object over a given preordered set. They illustrate that lattice theory is a bridge between algebra and logic for which the construction of an element corresponds to a step in a proof. We shall describe the history of their reception, which focusses mainly on the omega-rule. The fruitfulness of this device is immediately recognised by Kurt Schütte. It triggers the analysis by Ackermann (1951) of the infinitary inductive definition of the accessibility predicate with the goal of proving transfinite induction up to ordinal terms beyond epsilon_0, which is also taken over by Schütte (1952).

math.LO↗
arXiv2024

In 1955, Paul Lorenzen clears the sky in foundations of mathematics for Hermann Weyl

In 1955, Paul Lorenzen is a mathematician who devotes all his research to foundations of mathematics, on a par with Hans Hermes, but his academic background is algebra in the tradition of Helmut Hasse and Wolfgang Krull. This shift from algebra to logic goes along with his discovery that his ``algebraic works [...] have been concerned with a problem that has formally the same structure as the problem of consistency of the classical calculus of logic'' (letter to Carl Friedrich Gethmann dated 14 January 1988). After having provided a proof of consistency for arithmetic in 1944 and published it in 1951, Lorenzen inquires still further into the foundations of mathematics and arrives at the conviction that analysis can also be given a predicative foundation. Wilhelm Ackermann as well as Paul Bernays have pointed out to him in 1947 that his views are very close to those proposed by Hermann Weyl in Das Kontinuum (1918): sets are not postulated to exist beforehand; they are being generated in an ongoing process of comprehension. This seems to be the reason for Lorenzen to get into contact with Weyl, who develops a genuine interest into Lorenzen's operative mathematics and welcomes with great enthusiasm his Einf{ü}hrung in die operative Logik und Mathematik (1955), which he studies line by line. This book's aim is to grasp the objects of analysis by means of inductive definitions; the most famous achievement of this enterprise is a generalised inductive formulation of the Cantor-Bendixson theorem that makes it constructive. This mathematical kinship is brutally interrupted by Weyl's death in 1955; a planned visit by Lorenzen at the Institute for Advanced Study in Princeton takes place only in 1957--1958. As told by Kuno Lorenz, Lorenzen's first Ph.D. student, a discussion with Alfred Tarski during this visit provokes a turmoil in Lorenzen's operative research program that leads to his abandonment of language levels and to a great simplification of his presentation of analysis by distinguishing only between ``definite'' and ``indefinite'' quantifiers: the former govern domains for which a proof of consistency is available and secures the use of the law of excluded middle; the latter govern those for which there isn't, e.g. the real numbers. Lorenzen states in his foreword to Differential und Integral (1965) that he is faithful to Weyl's approach of Das Kontinuum in this simplification. This history motivates a number of mathematical and philosophical issues about predicative mathematics: how does Weyl's interest into Lorenzen's operative mathematics fit with his turn to Brouwer's intuitionism as expressed in ``{Ü}ber die neue Grundlagenkrise der Mathematik'' (1921)? Why does Lorenzen turn away from his language levels and how does this turn relate to Weyl's conception of predicative mathematics? What do Lorenzen's conceptions of mathematics reveal about Weyl's conceptions?

math.HO↗