<figure><img src="image_1.png" /></figure>

HAL
open science

# 'Upon This Quote I Will Build My Church Thesis'

Pierre-Marie Pédrot

► To cite this version:

Pierre-Marie Pédrot. 'Upon This Quote I Will Build My Church Thesis'. Communications of the ACM, 2025, pp.1-8. 10.1145/3715707. hal-05444840

HAL Id: hal-05444840

https://inria.hal.science/hal-05444840v1

Submitted on 6 Jan 2026

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
<figure><img src="image_3.png" /></figure>

<figure><img src="image_4.png" /></figure>

# ‘Upon This Quote I Will Build My Church Thesis’

By Pierre-Marie Pédrot

## ABSTRACT

The internal Church thesis (CT) is a logical principle stating that one can associate to any function $f: N \to N$ a concrete code, in some Turing-complete language, that computes $f$. While the compatibility of CT in simpler systems has been long known, its compatibility with dependent type theory is still an open question.

In this paper, we answer this question positively. We define “MLTT”, a type theory extending MLTT with quote operators in which CT is derivable. We furthermore prove that “MLTT” is consistent, strongly normalizing, and enjoys canonicity using a rather standard logical relation model. All the results in this paper have been mechanized in Coq.ª

## 1. INTRODUCTION

“Calculemus!” With this word, Leibniz famously enjoined the reader to compute. Contemporary logicians took this motto as a founding principle after the progressive discovery of the proof-as-program correspondence. This major breakthrough, also known as the Curry-Howard equivalence, is the seemingly simple observation that proofs and programs are the same object, in an essential way.

One major offshoot of the Curry-Howard philosophical stance is Martin-Löf's type theory (MLTT), the theoretical underpinning of several widely used proof assistants such as Agda, Coq, or Lean.¹⁶ In these systems, there is no formal separation between proofs and programs, as they live in the same syntax and obey the same rules. This monistic credo turns MLTT into the quintessential intuitionistic foundation of our modern times, blending logic and computation into the very same cast. Moreover, in the wake of the Swedish tradition of neutrality, MLTT does not pick a side in the constructivist feud. It neither proves fan principles from the Brouwerian band nor mechanistic axioms from the Markovian clique, and adheres to a strict Bishopian minimalism. If set theory is the paradise of mathematics, then type theory truly is the paradise of constructive mathematics.

Meanwhile, on the other side of the iron curtain, the Russian constructivists led by Markov pushed the computability tenet to an extreme point, postulating that all mathematical objects were indeed algorithms. Their doctrine¹⁵ is materialized by a foundational system that can be summarily described as a neutral Bishop intuitionistic logic ex-

tended with two additional axioms: Markov's principle (MP) and Church's thesis (CT).²³

Of those two axioms, Markov's principle is the simplest to state, as it is pretty much self-contained:

$$ \forall f: N \to N. \neg\neg (\exists n: N. f n = 0) \to \exists n: N. f n = 0. $$

Common alternative formulations include “a Turing machine that does not loop terminates” or “non-zero reals are apart from zero”. MP is a sweet spot of semi-classical logic, as it can be given a computational content preserving the witness property.⁷

Church's thesis is somewhat more involved, as it requires the internal definition of a computation model in the logistic itself. Assuming a logic rich enough, this is traditionally¹³ achieved by defining the decidable Kleene predicate T and its associated primitive recursive decoding function $U: N \to N$. Assuming $p: N$ to be the syntactic code of some program in the chosen Turing-complete computation model, $n: N$ some integer argument, and $k: N$ some encoding of evaluation traces of the model, then $T(p, n, k)$ holds whenever $k$ is the trace of the fact that $p$ applied to $n$ evaluates to some integer $v$. Furthermore, if indeed the predicate holds, then $Uk$ should return the value $v$.

Assuming we have settled this computational paraphernalia, CT is simply the internal statement

$$ \forall f: N \to N. \exists p: N. \forall n: N. \exists k: N. T(p, n, k) \wedge Uk = f n. $$

Said otherwise, any function $f$ definable in the theory is known to be computable by some concrete algorithm $p$ from within the theory.

Contrarily to MP, which is a consequence of excluded middle, CT is a very anti-classical axiom.²³ Assuming very weak forms of choice, it contradicts lesser variants of excluded middle. Similarly, it disproves choice-like principles, such as double negation shift. Finally, it also makes the logistic very intensional as it contradicts function extensionality, under the same kind of weak choice assumptions.

The consistency of MP and CT with regard to some logical system is typically proved via realizability, which is the intended model of the Russian dogma. Quite remarkably, Kleene's seminal paper¹⁴ already proves that CT is compatible with Heyting's arithmetic. For a more expressive theory, the effective topos is a famous example of a realizability topos in which both principles hold.¹⁰

Considering the claim above that in MLTT proofs are programs, it does seem a bit surprising that it is not biased toward the Russian school. Surely it ought to be easy to convert MLTT to the Markovian orthodoxy, for otherwise the Curry-Howard mantra would be but a misleading advertisement. Let us survey the current status of each Russian axiom individually in the canon of dependent type theory.

The original version of this paper was published in *Proceedings of the 39th Annual ACM/IEEE Symp. on Logic in Computer Science*.

<footnote>ª Development browsable at https://bit.ly/Pedrot-GitHub1.</footnote>
As we already hinted at, it is known that MP is not derivable in MLTT.⁴ Since it is a consequence of classical logic, it holds in classical models such as the set-theoretical one,²⁵ but it is also possible to add MP to MLTT while retaining the computational properties through a form of delimited exceptions.¹⁹ Note that, due to the minimalism of MLTT, the alternative statements of MP mentioned previously are not equivalent in this setting.³

As for CT, we already stated that it is negated by classical models, and thus is not a consequence of MLTT. By contrast with MP, the compatibility of CT with dependent type theory is a much more contentious subject. To make things simpler, we will therefore focus on this single principle in this paper, and deliberately ignore Markov's principle. The proviso about phrasing of the statement mattering a lot is even more paramount with CT, which is the chief reason why the problem and its answers are a matter of debate. In the remainder we will prove that MLTT is indeed compatible with the strongest form of Church's thesis usually agreed upon, but for this we first need to explain what we actually mean by these sibylline words. We dedicate the next section to a thorough exegesis of this topic.

## 2. A COMPREHENSIVE CT SCAN

Contrarily to more archaic systems, MLTT does not need a realizability interpretation to turn its proofs into programs. In some sense, it is already a realizability interpretation, as MLTT terms are literally bona fide programs. It should therefore be very natural to add CT to MLTT.

As a matter of fact, as long as the context is empty, the following rule is admissible

$$ \vdash_M : N \to N \quad \vdash \langle M \rangle : \Sigma p : N. \Pi n : N. \Sigma k : N. \overline{T}(p, n, k) \times U k = M n $$

where $\langle M \rangle$ is some term derived from $M$ in a systematic way. Depending on the pursued goal, this process is variously known in the type theory world as extraction¹⁸ or quotation.²¹ Obviously, a rule that is derivable for closed sequents is not necessarily internalizable in the theory, so there is a non-trivial gap to fill there.

An additional issue is that dependent type theories have various notions of existence. Typically, they contrast dependent sum types $\Sigma x : A. B$ with existential types $\exists x : A. B$. The precise details depend on the exact theory considered, but the general rule is that the former corresponds to actual, constructive evidence, while the latter stands for mere existence—that is, no computational content can be extracted from this type. Such non-computational types are called propositions, an umbrella term for mildly related concepts. The three most common instances of propositions are captured by the realizability-driven Prop universe of CIC,¹⁸ the hProp subuniverse inspired by the univalent world,²⁴ and the SProp universe of strict propositions.⁶ Regardless of the setting, $\Sigma$-types validate choice by construction through large elimination or projections, while existential types do not, in general.

The arithmetic statement of CT mentions two existential quantifiers, hence we have a priori at least four possible translations into MLTT. In practice, the second one

returns an enumerable proposition, so that for most notions of proposition, namely Prop with singleton elimination or hProp with unique choice, the use of $\exists$ or $\Sigma$ results in equivalent statements. We will thus always stick to a $\Sigma$-type for this quantifier. More problematic is the first existential quantifier, the nature of which leads to radically different worlds. We will call $CT_\Sigma$ (resp. $CT_\exists$) the statement of Church's thesis with a $\Sigma$ (resp. $\exists$) type as the first existential quantifier.

As mere existence does not validate choice by default, $CT_\exists$ is much closer to the traditional first-order setting. When $\exists$ is taken to live in the Prop universe of CIC, the relative expressivity of $CT_\exists$ has been studied extensively in the setting of synthetic computability.⁵ An important remark is that the lack of choice prevents building an internal quoting function ($N \to N \to N$ that associates to some function its concrete code. As already suggested before, this means that $CT_\exists$ does not necessarily contradict function extensionality. Actually, we can even go much further: In the case where propositions are identified with hProps, $CT_\exists$ turns out to be compatible not only with MLTT but also with full-blown univalence.²² More generally and quite counterintuitively, univalence is compatible with many principles that would make the hardcore Bishop-style intuitionist raise a suspicious eyebrow, as long as they are squashed enough and thus made computationally harmless.²²,²⁴

Contrastingly, as $\Sigma$-types come with intuitionistic (non)-choice built-in, $CT_\Sigma$ is the telltale of an extremely weird mathematical realm. For starters, it immediately implies the existence of a quoting function and breaks both function extensionality and classical logic. The consistency of $CT_\Sigma$ with MLTT is an open problem that has been lingering for a while and seems to be considered a difficult question by experts.¹¹,²² The best result thus far is the consistency of $CT_\Sigma$ with a stripped-down version of MLTT without the so-called $\xi$ rule:

$$ \frac{\Gamma, x : A \vdash M \equiv N : B}{\Gamma \vdash \lambda x : A. M \equiv \lambda x : A. N : \Pi x : A. B} $$

The model used to prove this fact is a variant of Kleene realizability tailored for dependent types. Briefly, in this model, terms are interpreted directly as their code in Kleene's first algebra, that is, a natural number, and the equational theory in a context is defined as the closure of code equality by ground substitutions.

This representation makes the implementation of $CT_\Sigma$ trivial, as it boils down to the identity. Yet, for this to work, it is critical that two functions convertible in the model have literally the same code. This is exactly where the restriction to ground substitutions comes into play, as it will identify functions with their concrete syntax. Unfortunately, the same restriction also destroys non-trivial higher-order equations and in particular invalidates the $\xi$ rule.

Although we understand the difficulties experienced by the authors of this paper and acknowledge their distinct goals, we consider that removing this congruence from MLTT when precisely trying to implement a principle implying the existence of a quoting function is unarguably throwing the baby with the bath water. Ubiquitary conversion under $\lambda$-abstractions is a stepping stone of MLTT for program
<figure><img src="image_5.png" /><figcaption>**Figure 1. Syntax of MLTT.**</figcaption></figure>

reasoning, so treating functions as black boxes is a no-go and the $\xi$ rule a *sine qua non*.

Given the strong relationship between quoting functions and metaprogramming, we should also mention some attempts at making the latter a first-class citizen of dependent type theory. These systems are built with practical programming in mind rather than constructive mathematics, but the endeavours are similar enough that they are worth highlighting. There is in particular a wealth of literature on contextual types,¹⁷ a special kind of modal type⁸ capturing well-typed terms in an object context. Although contextual types can coexist with dependent types, the ability to pattern-match on code in these settings is still a difficult problem that is only satisfyingly handled in the absence of dependent types.¹²

### 3. HIGH-LEVEL DESCRIPTION

We now give the high-level intuitions that we develop technically later on. In this paper, we define “MLTT”, read “MLTT with quotes”, a minute extension of MLTT with quoting operators that implement $CT_\Sigma$ in a straightforward way. As already explained, $CT_\Sigma$ holds externally in MLTT. If we want it as an internal rule, there are two problems to solve: first, handling terms in an arbitrary context, and second, showing that our hypothetical internalization preserves conversion.

Despite the aura of complexity surrounding this question, our solution is disappointingly simple. The first problem will be handled in the most trivial way one can think of. Namely, the primitives computing the internal version of $CT_\Sigma$ will simply block as long as their arguments are not closed. Since the return type of these primitives is first-order, this will not be a problem as it will not endanger canonicity.

The second problem is solved in a similarly obvious manner. Given two terms $M \equiv N: N \rightarrow N$ one needs to ensure that the quotation of these terms agree. In particular, the integer code returned by these operations must be the same. This sounds complicated, as in general two equivalent functions may have different codes. In Turing-complete languages, this is actually impossible to achieve in a computable way, due to Rice's theorem. But in MLTT, there is a very simple way to find a canonical representative of an equivalence class of functions: just pick the normal form! Conversion in MLTT is decidable, as it virtually amounts to comparing the normal forms of the considered terms for syntactic equality. This requires that all well-typed terms have a normal form, but this property is usually taken for granted in dependent type theories and will for sure hold true in “MLTT”.

As the astute reader may complain about, this is not enough in presence of $\eta$-rules, which are included in our system. But even in this case, our normalization trick can be adapted simply by maximally $\eta$-reducing and stripping $\lambda$ and pair annotations from the normal form.

Despite the intuitive simplicity of the above guiding ideas, proofs about dependent type theory are very tedious

and error-prone, let alone when they contain bits of computability. To keep the naysayer at bay, all proofs were mechanized in the Coq proof assistant.

### 4. BASIC TYPE THEORY

Let us fix some conventions. Since we will be juggling quite a bit between levels, we will use a different font style to refer to objects from the metatheory, with types in **bold** and type ascription written in set-theoretic style $x \in X$. Some metatheoretical types of interest are $X \Rightarrow Y$, the metafunctions from $X$ to $Y$, and $N$ the metaintegers. We will write **term** for the type of “MLTT” terms defined later on.

Our base theory will be an instance of MLTT featuring one Russell-style universe, negative $\Pi$ and $\Sigma$ types with definitional $\eta$-rules, together with a natural number type, an empty type, and an identity type. We recall the syntax of this theory in Figure 1. The typing rules are standard and we let the reader refer to the mechanization for details.

We use the usual notations $A \rightarrow B$ and $A \times B$ for non-dependent product and sum. We write $M=N$ for $\mathrm{IdAMN}$ when $A$ is clear from the context. Similarly, we sometimes drop the annotations of $\lambda$-abstractions and pairs. If $n \in N$, we write $[n]_n \in \mathrm{term}$ for the unary numeral associated to $n$. We write $\Lambda := \mathbb{N}$ for numbers intended to code for programs.

Partial computations are usually defined through the partiality monad $\wp(A) := \mathbb{N} \rightarrow \mathrm{option } A$. Since we will only ever consider partial integers, we use a simpler encoding.

**DEFINITION 1 (PARTIAL INTEGERS).**

We define the type of partial integers $N_\wp := \mathbb{N} \rightarrow N$. The intuitive meaning of a partial integer $P: N_\wp$ is the following.

* If for all $n: N, P: n = 0$, then $P$ is undefined.

* Otherwise, let $n_0$ be the smallest integer such that $P: n_0 = S v$ for some $v$. Then $P$ evaluates to $v$.

This can be easily internalized in MLTT.

**DEFINITION 2 (STEP EVALUATION).**

Given $M: N_\wp, V: N$, and $K: N$, we define the step-evaluation predicate.

$$M \rightsquigarrow V \parallel K: \square$$

read “M evaluates to V in K steps” by recursion on K, that captures the above intuition. Most notably if

$$n \in N, M \rightsquigarrow V \parallel [n]_N \text{ is convertible to}$$

$$(M: 0 = 0) \times \dots \times (M[n-1]_N = 0) \times (M[n]_N = S V).$$

Given the algorithmically friendly nature of MLTT, we will pick a slightly nicer, but equivalent, phrasing of $CT_\Sigma$. We will merge the Kleene predicate $T$ and its decoding function $U$ into a single function $\mathrm{run}: \Lambda \rightarrow N \rightarrow N_\wp$.

**DEFINITION 3.**

Henceforth, we will define CT in MLTT as

$$\Pi f: N \rightarrow N. \Sigma p: \Lambda. \Pi n: N. \Sigma k: N. \mathrm{run} \ p \ n \rightsquigarrow f \ n \parallel k$$
for some MLTT term $\mathrm{run}: \Lambda \rightarrow N \rightarrow N_\wp$.
## 5. "MLTT" EXTENSIONS

We now turn to the definition of the extensions that define "MLTT" proper.

**DEFINITION 4.**

The new term constructors of "MLTT" are defined in Figure 2, and will be collectively referred to as the *quoting primitives*.

<caption>**Figure 2.** Additional syntax of "MLTT."</caption>

$$M, N, A, B ::= \dots \mid \mathring{\mathcal{M}} \mid \mathring{\tau} M N \mid \varrho M N$$

We give names exposing the intuition of the meaning of those terms. The term $\varrho M$ is the *quote* of $M$, which is intended to return the code of the function $M$. The term $\zeta MN$ is the *step-count* of $M$ applied to $N$—that is, it will return the number of steps needed to evaluate the quote of $M$ on argument $N$. Finally, $\varrho MN$ is the *reflection* of $M$ applied to $N$, which produces a proof that indeed the quote of $M$ fullfills the expected runtime behavior.

**DEFINITION 5.**

A computation model for "MLTT" is given by a metafunction $|\cdot| \in \mathbf{term} \Rightarrow \mathbf{N}$ and an internal evaluation function $\mathbf{run} \in \mathbf{term}$.

To define the typing system alone we do not need any additional requirements on those objects, but let us offer some intuition before proceeding any further.

The $[\cdot]$ function is just some arbitrary Gödel numbering of the syntax. As already explained, the run function is going to serve as a Kleene predicate expressed in a functional form. In particular, we expect $\mathbf{run}: \Lambda \to \mathbb{N} \to \mathbb{N}_\varrho$ and $\mathbf{run} p n$ to compute the result of the application of the program $p$ to the argument $n$ if it exists. In practice, $\mathbf{run}$ is

<caption>**Figure 3.** Typing rules of "MLTT."</caption>

$$\frac{\Gamma \vdash M : \mathbb{N} \to \mathbb{N}}{\Gamma \vdash \varrho M : \Lambda} \qquad \frac{\Gamma \vdash M : \mathbb{N} \to \mathbb{N}}{\Gamma \vdash \tau M N : \mathbb{N}} \\ \frac{\Gamma \vdash M : \mathbb{N} \to \mathbb{N}}{\Gamma \vdash \varrho M N : M \varrho N}$$

<caption>**Figure 4.** Deep normal / neutral MLTT terms (excerpt).</caption>

$$\frac{\begin{array}{c} \mathrm{dne} \, x \\ \mathrm{dnf} \, M \end{array}}{\begin{array}{c} \mathrm{dnf} \, M \\ \mathrm{dnf} \, (\lambda x : A. M) \end{array}} \qquad \frac{\begin{array}{c} \mathrm{dne} \, M \\ \mathrm{dne} \, M N \end{array}}{\begin{array}{c} \mathrm{dnf} \, A \\ \mathrm{dnf} \, B \end{array}} \\ \frac{\begin{array}{c} \mathrm{dnf} \, P \\ \mathrm{dne} \, V \end{array}}{\begin{array}{c} \mathrm{dnf} \, (\Pi x : A. B) \\ \mathrm{dnf} \, M \\ \mathrm{dnf} \, N \end{array}} \qquad \frac{\begin{array}{c} \mathrm{dnf} \, \langle M, N \:: x : A, B \rangle \end{array}}{\begin{array}{c} \mathrm{dnf} \, M \\ \mathrm{dnf} \, N \end{array}}$$

<caption>**Figure 5.** Deep normal and neutral forms of "MLTT" extensions.</caption>

$$\frac{\neg \mathrm{clos} \, M \qquad \mathrm{dnf} \, M}{\mathrm{dne} \, (\varrho M)} \qquad \frac{\neg (\mathrm{clos} \, M \wedge \mathrm{clos} \, N) \qquad \mathrm{dnf} \, M \qquad \mathrm{dnf} \, N}{\mathrm{dne} \, (\varphi M N)} \qquad \varphi \in \{\tau, \varrho\}$$

expected to be defined in MLTT alone, or for that matter, in a much weaker fragment corresponding to PRA. In the remainder of this paper, we assume a fixed computation model.

**NOTATION 6.**

We write

$$M \dot{Q} N := \mathrm{run} (\varrho M) N \rightsquigarrow M N \parallel \zeta M N$$

for the specification of the quoting operators on $M$ and $N$. Furthermore, given any $p, n, k \in \mathbb{N}$, let

$$\mathbf{run} \ p \ n \ k \in \mathbf{term} := \mathbf{run} [p]_N [n]_N [k]_N.$$

We now have enough to define the typing rules of the additional "MLTT" primitives in Figure 3. We delay the description of the conversion rules of these primitives to a later point, because we still need more infrastructure.

Still, these rules are enough for the following theorem.

**THEOREM 7.**

"MLTT" *proves* CT.

**PROOF.**

The types are just the Skolemization of CT.

To finish the specification of "MLTT", we need to define its conversion rules. This requires some heavy definitions.

**DEFINITION 8 (QUASI-CLOSEDNESS).**

Given $M \in \mathbf{term}$ and $\Gamma \in \mathbf{ctx}$, we say that $M$ is $\Gamma$-quasi-closed, written $\mathrm{clos}_\Gamma M$ if, ignoring $\lambda$ and pair annotations, all free variables of $M$ are in $\Gamma$. When $\Gamma$ is empty, we will write $\mathrm{clos} M$.

**DEFINITION 9 (DEEP NORMAL AND NEUTRAL FORMS).**

We recall the inductive definition of deep normal and neutral forms of MLTT terms at Figure 4 and define the additional rules for "MLTT" at Figure 5.

Normal forms are, as usual, terms which cannot be simplified further. Neutral forms are a subcase of the former, intuitively capturing the notion of a term whose evaluation is blocked due to a variable not bound to a value. In particular, they cannot trigger new conversions when they are substituted for a variable. Our definition is standard for the MLTT fragment, except maybe that we ignore $\lambda$ and pair type annotations just like for the clos predicate. Only worth discussing are the newly introduced terms of "MLTT".

The quote primitives do not generate any new non-neutral normal forms, as their types are concrete, canonical datatypes. They do generate new neutrals, though. The intuition is that these primitives only compute on closed normal forms, so if one of their arguments is not closed, they will block and thus be neutral.

**NOTATION 10.**

We write $\mathrm{clnf} M$ if both $\mathrm{clos} M$ and $\mathrm{dnf} M$.
The last non-trivial ingredient that is needed is erasure of “MLTT” terms. We rely on it to quotient normal forms with regard to the various $\eta$-rules of our system.

**DEFINITION 11 (ERASURE).**

Given $M \in \mathbf{term}$, we define its erasure $\|M\| \in \mathbf{term}$. This operation can be understood as the composition of two finer-grained primitives: first, replace $\lambda$ and pair type annotations with a dummy term, and second, perform maximal $\eta$-reduction of $\lambda$ and pair nodes. We choose $\square$ for the dummy term, but any closed normal term would do. We give the relevant operations in Figure 6; all other cases are term homomorphisms.

<caption>**Figure 6. Term erasure.**</caption>

$$
\begin{align*}
\|\lambda x : A. M\| &:= N & \text{if } \|M\| &= N x \text{ and } x \notin N \\
\|\lambda x : A. M\| &:= \lambda x : \square. \|M\| & \text{otherwise} \\
\|\langle M, N :: x : A, B \rangle\| &:= P & \text{if } \|M\| &= P.\pi_1, \quad \|N\| &= P.\pi_2 \\
\|\langle M, N :: x : A, B \rangle\| &:= \langle \|M\|, \|N\| :: x : \square, \square \rangle & \text{otherwise}
\end{align*}
$$

**NOTATION 12.**

If $M \in \mathbf{term}$, we write $[[M]] \in \mathbf{N} := [[M]]$.

**DEFINITION 13.**

Given $k, v \in \mathbf{N}$ we define $[k, v]_\square \in \mathbf{term}$ by induction on $k$ as

$$
\begin{align*}
[0, v]_{\square} &:= \mathrm{refl} \mathbb{N} (S [v]_{\square}) \\
[k+1, v]_{\square} &:= \langle \mathrm{refl} \mathbb{N} 0, [k, v]_{\square} \rangle.
\end{align*}
$$

We now have all the necessary definitions to define the new conversion rules of “MLTT” at Figure 7. We omit the obvious congruence rules, and we give some intuitions by paraphrasing the rules. The computation rule for $\varphi M$ is simply stating that quoting a closed normal term produces the Gödel number of its erasure. The two other rules reflect the behavior of the run operator in the theory itself. They start by assuming that $M$ is a closed normal term, so its quote is a concrete code. Assuming canonicity, for any $n, k \in \mathbb{N}$, run $[[M]]$ $n$ $k$ must be convertible to a numeral. Similarly, $M [n]_\square$ must be convertible to some numeral $v$.

Since we expect run to model the computation of “MLTT”,

there must be some smallest $k_0 \in \mathbb{N}$ s.t. run $[[M]]$ $n$ $k_0$ is convertible to $S v$. Then $\Sigma M [n]_\square$ returns $k_0$, and $\ominus M [n]_\square$ must provide a closed proof of $MQ [n]_\square$. But given the previous assumptions, $MQ [n]_\square$ is convertible to a finite sequence of products of equalities $0 = 0$ with a trailing equality $S v = S v$. This type is trivially inhabited by $[k_0, v]_\square$.

**6. ADEQUACY AND SOUNDNESS**

There is still one missing piece for “MLTT” to make sense. Indeed, in the intuitive explanation above, we argued that run should model the runtime behavior of “MLTT”. In spite of this, we have made no additional assumption on Definition 5 so far. We make this requirement formal as computational adequacy in this section. This first forces us to endow “MLTT” with a notion of evaluation.

**DEFINITION 14 (EVALUATION).**

We define in the metatheory a step-indexed evaluation function $\downarrow$ that computes the deep normal form. We omit the standard rules for the MLTT fragment, and give them for “MLTT” extensions in Figure 8.

Although we describe it using inference rules, evaluation really is a step-indexed recursive function in the metatheory, of type $\mathbf{term} \Rightarrow \mathbb{N} \Rightarrow \mathbf{option term}$. We write $M \Uparrow_k$ when it returns None. We write $M \Downarrow N$ when there exists $k \in \mathbb{N}$ s.t. $M \Downarrow_k N$.

We discuss briefly the evaluation rules for the quoting primitives. They start by deeply evaluating the subterms and checking whether they are quasi-closed. If not, they immediately return. Otherwise, they perform a macroscopic evaluation step. For $\varphi M$, that just means quoting the closed normal form into a number. For $\Sigma M N$ and $\ominus M N$, it performs a guarded $\mu$-recursion to find the smallest index such that the erasure of $M N$ evaluates to a numeral.

**DEFINITION 15 (COMPUTATIONAL ADEQUACY).**

We say that the computation model is adequate if it satisfies the following:

* We have a derivation $\vdash M : \mathbb{N} \to \mathbb{N} \to \mathbb{N}_\varphi$.

* For all $M \in \mathbf{term}$ and $n, k, v \in \mathbb{N}$, if $M [n]_\square \Uparrow_k$ then run $[[M]]$ $n$ $k \downarrow 0$, if $M [n]_\square \Downarrow_k [v]_\square$ then run $[[M]]$ $n$ $k \downarrow S [v]_\square$.

<caption>**Figure 7. New non-congruence conversion rules of “MLTT.”**</caption>

$$
\begin{array}{c@{\qquad}c@{\qquad}c}
\begin{array}{c}
\Gamma \vdash M : \mathbb{N} \to \mathbb{N} \\
\Gamma \vdash M : \mathbb{N} \to \mathbb{N}
\end{array}
&
\begin{array}{c}
\mathrm{clnf} M \\
\mathrm{clnf} M
\end{array}
&
\begin{array}{c}
\begin{array}{c}
\Gamma \vdash \varphi M \equiv [[M]]_\square : \Lambda \\
\Gamma \vdash \tau M [n]_\square \equiv [k_0]_\square : \mathbb{N}
\end{array} \\
\begin{array}{c}
\Gamma \vdash \varphi M [n]_\square \equiv [k_0, v]_\square : M \varphi [n]_\square
\end{array}
\end{array}
$$

<caption>**Figure 8. Step-indexed evaluation of “MLTT” extensions.**</caption>

$$
\begin{array}{c@{\qquad}c@{\qquad}c}
\begin{array}{c}
M \Downarrow_k M_0 \\
\varphi M \Downarrow_{k+1} [[M_0]]_\square \\
M \Downarrow_k M_0 \quad N \Downarrow_k [n]_\square
\end{array}
&
\begin{array}{c}
\mathbf{clos} M_0 \\
\mathbf{clos} M_0 \quad k_0 \le k \\
\tau M N \Downarrow_{k+1} [k_0]_\square
\end{array}
&
\begin{array}{c}
M \Downarrow_k M_0 \quad N \Downarrow_k N_0 \\
\tau M N \Downarrow_{k+1} \tau M_0 N_0 \\
\|M_0\| [n]_\square \Downarrow_{k_0} [v]_\square \quad \forall k' < k_0. \quad \|M_0\| [n]_\square \Uparrow_{k'}
\end{array}
\end{array}
$$
The last point is essentially stating that the metatheoretical evaluation ⇓ and the internal evaluation run coincide.

From now on, we implicitly assume that our globally fixed computational model is adequate. The remainder of the paper is dedicated to the proof of the following theorem.

**THEOREM 16.**

"MLTT" is consistent and strongly normalizing. Furthermore, any closed "MLTT" term $\vdash M : \mathbb{N}$ normalizes to a numeral.

## 7. A MLTT LOGICAL RELATION PRIMER

We will prove Theorem 16 using a logical relation model. The base model is basically the now-famous inductive-recursive one from Abel et al.,¹ with a handful of surprisingly minor tweaks. In this section, we briefly recall the principles of Abel-style logical relations.

From a high-level point of view, Abel-style logical relations for MLTT are just a glorified kind of realizability with a lot of bells and whistles. Notably, in the semantic world, well-formed types $\Gamma \Vdash A$ are defined inductively, while well-typed terms $p_A$ | $\Gamma \Vdash M : A$ are defined recursively over a proof $p_A \in \Gamma \Vdash A$. In turn, well-typedness is extremely similar to, say, Kleene realizability,²³ that is, $p_A$ | $\Gamma \Vdash M : A$ essentially means that M weak-head normalizes to some value V, further satisfying some conditions depending on A. Due to conversion being an integral part of typing, one also needs to provide predicates for type and term convertibility at some semantic type.

The major departure from usual realizability in this kind of model is the proper handling of variables. All semantic predicates are actually presheaves over contexts equipped with weakenings. Furthermore, neutral terms enjoy a very specific status; see, for example, Lemma 22. This will turn out to be important for our goals.

The relation itself is parameterized by syntactic predicates for the various notions of typing and reduction.

These predicates must satisfy a list of closure properties, which are typically weaker than the ones enjoyed by the standard typing rules of MLTT. Another way to understand this is that logical relations turn a liberal type system, called *declarative*, with many closure rules that is easy to work with, into a lower-level type system that is hardly usable but which is similar in spirit to the steps performed by a typing algorithm. Proofs in this generic system are in some sense *normalized* compared to the declarative system. As a matter of fact, this is a way to prove decidability of type-checking, since an algorithmic presentation of type-checking will satisfy the low-level closure properties. A notable difference with the declarative system is that generic typing requires making explicit the notion of neutral terms, through the introduction of neutral convertibility, which can be understood as the usual convertibility restricted to neutral terms.

In the remainder of this section, we assume fixed some instance of syntactic typing and reduction rules for MLTT. Due to their sheer size and the fact they are neither surprising nor new, we will not state the closure properties here, but rather refer to the corresponding Coq code.

**DEFINITION 17.**

A set of typing rules is generic when it enjoys a specific list of (weak) closure properties.

Given generic notions of typing and reduction, one can define reducibility in the abstract. Our base logical relation is unchanged with regard to Abel et al.,¹ so we will not give the full definition here. To begin with, writing everything in full on paper would be both unreadable and uninformative, and probably ridden with typos. Rather, we sketch below some representative type formers to build intuition. We also ignore bookkeeping details that clutter the simplicity of logical relations, such as universe levels. Our results are backed up by a mechanized proof, so we can go for a fearless human-readable paper.

<caption>**Figure 9. Reducibility (excerpt).**</caption>

Reducibly well-formed types

$$ \Gamma \Vdash^N A := \{ \text{red} \in \Gamma \vdash A \to^* \mathbb{N} \} \quad \Gamma \Vdash^\Pi A := \left\{ \begin{array}{l} \text{dom} \in \text{term} \\ \text{cod} \in \text{term} \\ \text{red} \in \Gamma \vdash A \to^* \Pi x : \text{dom. cod} \\ \text{dom} \in \Pi(\rho : \Delta \leq \Gamma) \cdot \Delta \Vdash \text{dom}\{\rho\} \\ \text{cod} \in \Pi(\rho : \Delta \leq \Gamma) \cdot (x : \text{dom} | \Delta \Vdash x : \text{dom}\{\rho\}) \cdot \Delta \Vdash \text{cod}\{\rho, x\} \\ \dots \end{array} \right\} $$

Reducibly well-typed terms at type $\mathbb{N}$ for $p \in \Gamma \Vdash^N A$

$$ \frac{\Gamma \vdash M \to^* 0 : \mathbb{N}}{p \mid \Gamma \Vdash^N M : A} \qquad \frac{\Gamma \vdash M \to^* S N : \mathbb{N}}{p \mid \Gamma \Vdash^N M : A} \qquad \frac{p \mid \Gamma \Vdash^N N : A}{p \mid \Gamma \Vdash^N M : A} \qquad \frac{\Gamma \vdash M \to^* N : \mathbb{N}}{p \mid \Gamma \Vdash^N M : A} \qquad \frac{\Gamma \vdash M \to^* N : \mathbb{N}}{\Gamma \vdash_{\text{whne}} N : \mathbb{N}} $$

Reducibly well-typed terms at $\Pi$-type for $p \in \Gamma \Vdash^\Pi A$

$$ p \mid \Gamma \Vdash^\Pi M : A := \left\{ \begin{array}{l} \text{nf} \in \text{term} \\ \text{red} \in \Gamma \vdash M \to^* \text{nf} : \Pi x : \text{dom. cod} \\ \text{app} \in \Pi(\rho : \Delta \leq \Gamma) \cdot (x : \text{dom} | \Delta \Vdash x : \text{dom}\{\rho\}) \cdot \text{cod} x \cdot \Delta \Vdash \text{nf}\{\rho\} \cdot x : \text{cod}\{\rho, x\} \\ \dots \end{array} \right\} $$
**DEFINITION 18 (REDUCIBILITY).**

We give a partial but evocative definition of reducibility at Figure 9.

As already explained, we gloss over the details and instead concentrate on the high-level view. We abuse implicit arguments in Figure 9 to keep things readable, and we also omit additional well-formedness conditions. At the risk of repeating ourselves, this is really just the run-of-the-mill complete presheaf model for MLTT, where presheaves have been manually encoded by means of quantifications over all weakenings of the current context. Note the lack of naturality conditions thanks to Lemma 19. In our setting, typed reduction is simply untyped reduction annotated with proofs that both sides are well-typed and convertible. Similarly, well-typed neutrals are untyped neutrals together with a proof of well-typedness and self-convertibility. Without further consideration for the low-level details, the logical relation satisfies some salient properties we list below.

**LEMMA 19 (REDUCIBILITY IRRELEVANCE).**

For all proofs of type reducibility $\mathbf{p}_A$, $\mathbf{q}_A \in \Gamma \Vdash A$, if $\mathbf{p}_A \mid \Gamma \Vdash M : A$ then $\mathbf{q}_A \mid \Gamma \Vdash M : A$ and similarly for the other statements.

This allows us to silently drop the proof of type formation for reducibility statements as a notational device. As long as there is one, it does not matter which one we pick.

**LEMMA 20 (ESCAPE).**

If $\Gamma \Vdash M : A$ then $\Gamma \vdash M : A$ and similarly for the other statements.

**LEMMA 21 (ANTI-REDUCTION).**

Reducibility is closed by typed anti-weak-reduction.

**LEMMA 22 (REFLECTION).**

Well-typed neutrals are reducible.

Just like for standard realizability, we need to close reducibility by substitution to state the fundamental lemma. The relation resulting from this closure is known in the literature as validity. We refer to the development for reference.

**THEOREM 23.**

Well-typed MLTT terms are valid.

**8. The "MLTT" Logical Relation**

For technical reasons, we will work with a slightly tweaked version of "MLTT" rules. Figure 7 is given for readability purposes; these rules will be derivable in the actual system. The differences are the following:

First, instead of a global typing axiom for run, we add it as a premise to the "MLTT" rules for $\Sigma$ and $\rho$. This is a cosmetic change to strengthen induction over "MLTT" derivations.

Second, for reasons that will become clear soon, we turn the well-typedness premises of those rules into self-convertibility. For instance, the introduction rule of $\varphi$ becomes:

$$ \frac{\Gamma \vdash M \equiv M : \mathbb{N} \rightarrow \mathbb{N}}{\Gamma \vdash \varphi M : \Lambda} $$

By reflexivity of term conversion, it is clear that these rules

imply the ones from Figure 7. After Theorem 33, we will also be able to derive that self-convertibility implies well-typedness, which shows that the two versions are equivalent.

The model itself is defined in terms of a small-step reduction relation, so we need to define it properly for MLTT, in addition to the big-step variant from Section 6.

**DEFINITION 24.**

We mutually define weak-head and deep reductions, respectively written $M \Rightarrow N$ and $M \Rightarrow\Rightarrow N$. The MLTT rules are standard, and the "MLTT" rules are defined in Figure 10. Weak-head and deep reductions coincide for the quoting primitives.

<caption>Figure 10. Weak-head reduction of "MLTT" extensions.</caption>

$$ \frac{\begin{array}{c} M \Rightarrow M' \\ \varphi M \Rightarrow \varphi M' \end{array}}{\begin{array}{c} M \Rightarrow M' \\ \varphi M N \Rightarrow \varphi M' N \end{array}} \qquad \frac{\begin{array}{c} \mathrm{clnf} M \\ \varphi M N \Rightarrow \varphi M' N' \end{array}}{\begin{array}{c} \mathrm{dnf} M \\ \varphi M N \Rightarrow \varphi M' N' \end{array}} \qquad \varphi \in \{\tau, \varrho\} \\ \frac{\begin{array}{c} \mathrm{clnf} M \\ \|M\| [n]_N \Downarrow_{k_0} [v]_N \quad \forall k < k_0. \quad \|M\| [n]_N \Uparrow_k \end{array}}{\begin{array}{c} \tau M [n]_N \Rightarrow [k_0]_N \\ \varrho M [n]_N \Rightarrow [k_0, v]_\varrho \end{array}} \qquad \tau M [n]_N \Rightarrow [k_0, v]_\varrho $$

Note that deep reduction is simply iterated weak-head reduction on the subterms of weak-head normal forms. Deep reduction is a specific sequentialization of evaluation, and its reflexive-transitive closure computes the same normal forms. Importantly, both reductions are deterministic.

One major remark for our proof to go through is that in Abel-style logical relations, the closure properties of conversion preserve deep normalization. Said otherwise, we never perform conversion on terms potentially introducing non-termination. We leverage this by the following decoration.

**DEFINITION 25 (DEEP CONVERSION).**

We define deep term conversion $\Gamma \vdash_{\mathrm{nf}} M \equiv N : A$ as the predicate $\Gamma \vdash M \equiv N : A$ extended with the following side-conditions.

* For $T \in \{M, N\}$, there is some $T_0$ s.t. $T \Downarrow T_0$ and $\Gamma \vdash T \equiv T_0 : A$.

* $M_0$ and $N_0$ have the same erasure, that is, $\|M_0\| = \|N_0\|$.

We define similarly deep-type and neutral conversions.

When instantiating the logical relation with deep conversions, one gets access to the fact that both sides of the conversion deeply normalize to terms that have the same erasure. This is why we turn the typing premises of the quoting primitives into self-convertibility. Before the fundamental lemma, syntactic deep self-convertibility gives more information than just syntactic typability.

**LEMMA 26 (DEEP TYPING).**

The typing rules where the various conversion predicates are replaced by their deep equivalent satisfy the generic typing interface.

Note that erasing normal forms before comparing them is critical for the above lemma. Indeed, generic conversion
rules for negative types are given directly as η-expansions. Therefore, two convertible normal forms may differ on their annotations or up to some η-expansion. Erasing all annotations and maximally η-reducing ensures thus that the result is unique for each equivalence class.

As a result, the logical relation instantiated with deep typing is a model of MLTT. We only have to check that the additional “MLTT” rules are also interpreted. Since semantic self-convertibility is equivalent to semantic well-typedness, it is enough to check the rules from Figure 7; the ones from Figure 3 are a consequence of the former.

**LEMMA 27 (QUOTE REDUCIBILITY).**

*The conversion rules for the $\ominus$ primitive hold in the reducibility model.*

**PROOF.**

We focus on the more general congruence rule. Assume $\Gamma \Vdash M \equiv M' : \mathbb{N} \to \mathbb{N}$, we now have to show that $\Gamma \Vdash \emptyset M \equiv \emptyset M' : \mathbb{N}$. By escape, $\Gamma \vdash_{\mathrm{nf}} M \equiv M' : \mathbb{N} \to \mathbb{N}$. We thus have two terms $M_0$ and $M'_0$ s.t. $M \llcorner M_0, M' \llcorner M'_0$ and $\| M_0 \| = \| M'_0 \|$. Either both $M_0$ and $M'_0$ are quasi-closed or both are not. In the latter case, both $\emptyset M_0$ and $\emptyset M'_0$ are neutral and convertible, so by reflection they are reducibly convertible. Otherwise, they reduce to $[[M_0]]_{\mathbb{N}}$ and $[[M'_0]]_{\mathbb{N}}$, which are equal numerals and thus reducibly convertible. In either case, we conclude by anti-reduction.

To prove reducibility of $\Sigma$ and $\ominus$, we need a fair amount of rewriting theory. The computation model is completely untyped, and we only care about erased terms, so we must consider reductions that ignore $\lambda$ and pair annotations. The following are textbook results, except for the interleaving of weak and deep reduction for the quoting primitives.

**DEFINITION 28.**

We define parallel and standard reductions up to $\lambda$ and pair annotations for “MLTT” in the usual way.

**LEMMA 29.**

*Deep red. $\subseteq$ parallel red. $\subseteq$ standard red.*

**LEMMA 30.**

*Parallel reduction is confluent.*

**LEMMA 31.**

*Standard reduction to a dnf implies deep evaluation up to annotations, and is preserved by erasure.*

We can now tackle the remaining reducibility proofs.

**LEMMA 32.**

*The conversion rules for the $\Sigma$ and $\ominus$ primitives hold in the reducibility model.*

**PROOF.**

Once again we focus on the congruence rule. Since the two primitives behave computationally the same, we only treat the $\ominus$ case, which is more involved typingwise. Let us assume $\Gamma \Vdash M \equiv M' : \mathbb{N} \to \mathbb{N}$ and $\Gamma \Vdash N \equiv N' : \mathbb{N}$. As before, we have deeply normal terms $M_0, M'_0$ (resp. $N_0$ and $N'_0$) convertible to the original terms and with the same

erasure, and thus the same closedness.

If not all these terms are closed, then $\emptyset M_0 N_0$ and $\emptyset M'_0 N'_0$ are convertible neutral terms, we conclude as above.

Otherwise, by reducibility, $N_0 = N'_0 = [n]_{\mathbb{N}}$ for some $n \in \mathbb{N}$. Since reducibility is closed by application, we get $\Gamma \Vdash M N \equiv M' N' : \mathbb{N}$. This implies that both applications deeply evaluate to the same semantic integer, that is, a series of successors ending either with 0 or a neutral. By confluence, we rule out the second case as $M_0 N_0$ is closed, so these terms reduce to some numeral $[v]_{\mathbb{N}}$. By confluence and standardization, $M_0 [n]_{\mathbb{N}}$ also evaluates to $[v]_{\mathbb{N}}$. By irrelevance of erasure, $\| M_0 \| [n]_{\mathbb{N}}$ also evaluates to $[v]_{\mathbb{N}}$. By computational adequacy, there exists some $k_0$ s.t. run $[[M_0]]$ $n k_0 \llcorner S [v]_{\mathbb{N}}$ and run $[[M_0]]$ $n k_0 \llcorner 0$ for all $k' < k_0$. Given that $M_0$ and $M'_0$ have the same erasure, this also holds for $M'_0$. Hence, $\Sigma MN$ and $\Sigma M'N'$ evaluate to $[k_0]_{\mathbb{N}}$ and $\emptyset MN$ and $\emptyset M'N'$ evaluate to $[k_0, v]_{\emptyset}$. The only remaining problem is to show that this value is indeed of semantic type $M Q [n]_{\mathbb{N}}$. But this is a trivial consequence of the normalization properties of the terms implied.

Finally, one also has to prove validity for these conversion rules, that is, that they are stable by substitution. This turns out to be obvious. Congruence rules are stable by substitution by construction. For the other rules, it is enough to observe that both quasi-closedness and erasure of quasi-closed terms are stable by substitution. We thus get the result below, of which Theorem 16 is an immediate corollary.

**THEOREM 33.**

*Well-typed “MLTT” terms are valid.*

# 9. MECHANIZATION

While the Abel et al. proof has been implemented in Agda,¹ our mechanization is written in Coq and is based upon a recent work by Adjedj et al.² that relies on a small induction-recursion encoding.³ Apart from this, the two formalizations are globally the same. The only advantage of the Coq version, which we believe to be decisive, is the availability of tactics. The largish corpus of proofs relating the numerous untyped reductions is rendered tractable by careful automation.

All theorems stated in the paper have been formalized. The only thing we did not formally prove was the actual existence of adequate models of computation. We globally axiomatized one in the development instead.

The reader may reasonably complain about the use of axioms, as they may very well be inconsistent. Yet, the existence of adequate models is at the same time an utterly trivial fact and a technically extremely challenging task. Indeed, at an intuitive level, run has already been implemented in MLTT, because we defined evaluation as a step-indexed function in our metatheory, which turns out to be a variant of MLTT. As explained before, we do not even need that much; the fragment we use to implement it basically fits into PRA. In any paper proof, such a computability result would be immediately brushed off as obvious, barely requiring any explanation. Now, given the non-trivial size of our untyped
language, implementing evaluation and proving anything about it in Coq was already quite cumbersome. By contrast, doing the same directly in the object theory is monstrous enough to drive any sane person into sheer madness, not even mentioning that we have to work up to a Gödel encoding. Out of common decency, we will not attempt to close this unquestionable gap.

## 10. FUTURE WORK

Although we did not formally prove it out of unrepented sloth, it is quite clear that “MLTT” enjoys decidability of type-checking. Since type interpretation is unchanged in the logical relation, the global shape of the algorithm remains the same as the one for MLTT. Handling the quoting primitives should not cause any trouble since their reduction rules enjoy the same kind of properties as in vanilla MLTT. Given that our Coq proof is based on a development that proves decidability of type-checking for MLTT, it should be quite simple to extend it to “MLTT”.

Another interesting topic is the compatibility of MLTT with the full Russian axiomatic. We now know it is compatible with MP and CT in isolation. Hence, a natural question is whether it can accommodate both axioms at the same time. We are convinced that not only this is the case, but also that the model described here can be easily extended to handle MP. The reason for this confidence lies in the uncanny similarity between those two principles. Just like CT, it is true that Markov's rule, the external version of MP, is derivable in MLTT using Friedman's trick.²⁰ Again, like CT, the return type of this rule is a concrete data type—that is, a $Σ_1^0$ formulae. It should therefore be easy to add a term

$$ \frac{\Gamma \vdash M : \mathbb{N} \rightarrow \mathbb{N} \quad \Gamma \vdash N : \neg(\Sigma n : \mathbb{N}.M n = 0)}{\Gamma \vdash \mu M N : \Sigma n : \mathbb{N}.M n = 0} $$

that only computes when both arguments are closed and returns the witness extracted by Friedman's trick. One must be careful to return the same integer for convertible arguments, but this is easily obtained by returning the smallest index $k$ s.t. $M k$ is 0.

We believe that many axioms can be added to MLTT this way, provided they are admissible on closed terms and return $Σ_1^0$ formulae that have sufficiently unique inhabitants. We leave the exploration of this subject to a later time.

## 11. CONCLUSION

In this paper, we proved it was possible to add $CT_Σ$ to MLTT without disrupting any of the desirable properties of the resulting system, such as consistency, strong normalization, and canonicity. Against all odds, the model used for this is the most straightforward one can conceive, as it boils down to the standard logical relation for MLTT. The computational content of our variant of Church's thesis is too borderline stupid to even be considered unsurprising: It computes on closed terms, period. The only mildly non-trivial phenomenon is the need for erasure of annotations and maximal η-reduction, but that trick is hardly worthy of attention. As a result, we are still bewildered about the reason for which this problem was believed to be hard.

The theorems have been formalized in Coq, greatly reducing the risk of an accidental error in the proof. For simplicity, the development still axiomatizes the computation model in the object theory. In all likelihood, these axioms would be deemed self-evident in a computability theory paper proof.

Finally, we believe that the generic recipe we followed for this model can be generalized to many other admissible principles in dependent type theory.

## References

1. Abel, A., Ohman, J., and Vezzosi, A. Decidability of conversion for type theory in type theory. In Proc. ACM Program. Lang. 2, POPL (Dec. 2017).

2. Adjedi, A. et al. Martin-Löf à la Coq. In Proc. 13th ACM SIGPLAN Intern. Conf. on Certified Programs and Proofs, Blazy, S., Pientka, B., Timany, A., and Traytel, D. ACM, (2024).

3. Cohen, L. et al. Separating Markov's principles. In Proc. 39th Annual ACM/IEEE Symp. on Logic in Computer Science, ACM (2024).

4. Coquand, T. and Mannaa, B. The independence of Markov's principle in type theory. Log. Methods Comput. Sci. 13, 3, (2017).

5. Forster, Y. Computability in Constructive Type Theory. Ph.D. thesis, Saarland University, Germany, (2021).

6. Gilbert, G. A Type Theory with Definitional Proof-Irrelevance. Ph.D. thesis, Mines ParisTech, France, (2019).

7. Gödel, K. Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica 12, 3-4 (1958), 280-287.

8. Gratzer, D., Kavvos, G. A., Nuyts, A., and Birkedal, L. Multimodal dependent type theory. Log. Methods Comput. Sci. 17, 3 (2021).

9. Hancock, P. et al. Small induction recursion. Typed Lambda Calculi and Applications. Springer, Berlin Heidelberg, Hasegawa, M. (ed) 156-172.

10. Hyland, J. The effective topos. Studies in Logic and the Foundations of Mathematics 110, (1982), 165-216.

11. Ishihara, H., Maietti, M. E., Maschio, S., and Streicher, T. Consistency of the intensional level of the minimalist foundation with church's thesis and axiom of choice. Arch. Math. Log., 57, 7-8 (2018), 873-888.

12. Jang, J., Gélineau, S., Monnier, S., and Pientka, B. Moebius: Metaprogramming using contextual types: The stage where system f can pattern match on itself. In Proc. ACM Program. Lang. 6, POPL (2022), 1-27.

13. Kleene, S. C. Recursive predicates and quantifiers. Transactions of the American Mathematical Society 53, (1943), 41-73.

14. Kleene, S.C. On the interpretation of intuitionistic number theory. J. Symbolic Logic 10, (1945), 109-124.

15. Margenstern, M. L'école constructive de markov. Revue d'histoire des Mathématiques, (1995).

16. Martin-Löf, P. Intuitionistic Type Theory. Volume 1 of Studies in Proof Theory. Bibliopolis, (1984).

17. Nanevski, A., Pfenning, F., and Pientka, B. Contextual modal type theory. ACM Trans. Comput. Log. 9, 3 (2008), 23:1-23:49.

18. Paulin-Mohring, C. Program Extraction in the Calculus of Constructions. Ph.D. thesis, Paris Diderot University, France, (1989).

19. Pédrot, P. Russian constructivism in a prefascist theory. In Proc. 35th Ann. ACM/IEEE Symp. on Logic in Computer Science. Hermanns, H., Zhang, L., Kobayashi, N., and Miller, D. (ed). ACM, (2020), 782-794.

20. Pédrot, P. and Tabareau, N. Failure is not an option—An exceptional type theory. In Programming Languages and Systems-27th European Symp. on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, Springer, Ahmed, A. (ed.), (2018), 245-271.

21. Sozeau, M. et al. The metacog project. J. Autom. Reason. 64, 5 (2020), 947-999.

22. Swan, A.W. and Uemura, T. On Church's thesis in cubical assemblies. Math. Struct. Comput. Sci. 31, 10 (2021), 1185-1204.

23. Troelstra, A. and Dalen, D. Constructivism in Mathematics: An Introduction. North-Holland, (1988).

24. T. Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, (2013); https://homotopytypetheory.org/book.

25. Werner, B. Sets in types, types in sets. In Abadi, M. and Ito, T., editors, Theoretical Aspects of Computer Software, Third Intern. Symp., TACS '97. Sendai, Japan, September 23-26, 1997, Proceedings, volume 1281 of Lecture Notes in Computer Science, Springer, (1997), 530-546.

Pierre-Marie Pédrot (pierre-marie.pedrot@inria.fr.) is a researcher with the Gallinette team at Inria, Nantes, France.

<figure><img src="image_6.png" /></figure>

This work is licensed under a Creative Commons Attribution International 4.0 License.

© 2025 Copyright held by the owner/author(s).