# A logic of judgmental existence and its relation to proof irrelevance

Ivo Pezlar111Czech Academy of Sciences, Institute of Philosophy, Jilska 1,
Prague 110 00.

##### Abstract.

We introduce a simple natural deduction system for reasoning with judgments of
the form “there exists a proof of $\varphi$” to explore the notion of
judgmental existence following Martin-Löf’s methodology of distinguishing
between judgments and propositions. In this system, the existential judgment
can be internalized into a modal notion of propositional existence that is
closely related to truncation modality, a key tool for obtaining proof
irrelevance, and lax modality. We provide a computational interpretation in
the style of the Curry-Howard isomorphism for the existence modality and show
that the corresponding system has some desirable properties such as strong
normalization or subject reduction.

##### Keywords.

judgmental existence, constructive existence, proof irrelevance, truncation,
lax modality, Curry-Howard correspondence, homotopy type theory

##### Funding.

This paper is an outcome of the project Logical Structure of Information
Channels, no. 21-23610M, supported by the Czech Science Foundation and
realized at the Institute of Philosophy of the Czech Academy of Sciences.

##  1 Introduction

In the constructive and intuitionist tradition, we can identify two closely
related but distinct notions of a proposition $\varphi$ being true, let us
call them true1 and true2, informally:

  1. (1)

$\varphi$ is $\textit{true}_{1}$ $\;\Leftrightarrow\;$ we have a proof $a$ of
$\varphi$222Other common variants: “we have found a proof $a$ of $\varphi$”,
“we have constructed $a$ of $\varphi$”, “we know a proof $a$ of $\varphi$”
etc. See, e.g., Nordström et al. (1990), p. 29 (“[t]o know that the
proposition $A$ is true is to have an element $a$ in $A$”), Troelstra and van
Dalen (1988), p. 4 (“[a] statement is true if we have proof of it”), UFP
(2013), p. 41 (“to show that a proposition is true […] corresponds to
exhibiting an element of the type corresponding to that proposition”).

  2. (2)

$\varphi$ is $\textit{true}_{2}$ $\;\Leftrightarrow\;$ there exists a proof of
$\varphi$333Other common variants: “$\varphi$ has a proof”, “$\varphi$ has
been proved”. See, e.g., Dummett (1975), p. 31 (“a mathematical statement is
intuitionistically true if there exists an (intuitionistic) proof of it”),
Martin-Löf (1991), p. 141 (“[i]ntuitionistically, truth of a proposition is
analyzed as existence of a proof; a proposition is true if there exists a
proof of it”), Coquand (1989), p. 4 (“we say that $\varphi$ is true […] iff
$\varphi$ has a proof”). Notice also the subtle difference between “we have a
proof of $\varphi$” vs. “$\varphi$ has a proof” reflecting the difference
between (1) and (2).

At first glance, these notions might seem interchangeable but there is a
subtle and important difference between them. To call something true according
to (1) we need to have the actual proof $a$, i.e., to know its construction.
However, to call something true according to (2), we just need to know that
there exists some proof but what exactly its construction looks like is not
important. Also, note that there is a clear difference in order of conceptual
priority between (1) and (2): first, we have to have a proof $a$ of $\varphi$
to be able to claim that it exists, i.e., true2 is a secondary notion to
true1.

The notion of being true in the sense of (1) is tightly associated with the
idea of proof-relevant approaches to logic and mathematics (which came into
dominance especially with the discovery of the Curry-Howard correspondence
between propositions and types, Curry (1952), Howard (1980)), while the notion
of being true in the sense of (2) is connected with proof-irrelevant
approaches:444The idea of proof irrelevance goes back at least to de Bruijn
(1974), reprinted in Nederpelt et al. (1994).

  * •

proof-relevant approaches: proofs are treated as proper mathematical objects:
it is not enough to know that a proposition is true, we also need to have its
proof, i.e., to know its structure. In practice, this means that we can have
different proofs for the same proposition.

  * •

proof-irrelevant approaches: proofs are not treated as proper mathematical
objects: it is sufficient to know that a proposition is true, the proofs
themselves do not matter beyond the fact that they exist, i.e., their
structure is unimportant. In practice, this means any two proofs of the same
proposition are considered equal (= the proof irrelevance principle).555In
this paper, we will focus on propositional proof irrelevance, not a judgmental
one. In other words, any two proofs of the same will be considered
extensionally equal, not intensionally.

From this perspective, we can view true1 and true2 as capturing proof-relevant
and proof-irrelevant notions of truth, respectively: true1 cares about the
structure of proofs, true2 does not. This also means that $\varphi$ is
$\textit{true}_{1}$ entails $\varphi$ is $\textit{true}_{2}$ (we can always
ignore structure if there is some assumed) but not vice versa (if there was no
structure assumed, we cannot summon it out of nowhere). So, let us call a
proposition $\varphi$ that is $\textit{true}_{1}$ as proof-relevantly true or
simply true and a proposition $\varphi$ that is $\textit{true}_{2}$ as proof-
irrelevantly true or simply just true:666Distinguishing between proof
relevance and proof irrelevance with no explicit proof terms might seem odd at
first but it is still applicable. For example, $\varphi\textit{ true}$ can be
informally interpreted as “we know there is a proof for $\varphi$ and we know
how it looks like” (i.e., the judgment $\varphi\textit{ true}$ is effectively
an abbreviation or coding of $a:\varphi$) while $\varphi\textit{ just true}$
says “we know there is a proof for $\varphi$ but we don’t know how it looks
like” (i.e., we cannot “decode” the judgment $\varphi\textit{ just true}$ back
to $a:\varphi$).

  1. $\varphi$ is $\textit{true}_{1}$ $\;\Leftrightarrow\;$ $\varphi$ is proof-relevantly true $\;\Leftrightarrow\;$ $\varphi\textit{ true}$

  2. $\varphi$ is $\textit{true}_{2}$ $\;\Leftrightarrow\;$ $\varphi$ is proof-irrelevantly true $\;\Leftrightarrow\;$ $\varphi\textit{ just true}$

Now, in a type-theoretic setting, the right-hand side of $\;\Leftrightarrow\;$
in (1), i.e., the judgment “we have a proof $a$ of $\varphi$” is formalized as
the judgment $a:\varphi$:

  * (1′)

we have a proof $a$ of $\varphi$ $\;\Leftrightarrow\;$ $a:\varphi$

It is the basic judgment of modern type theories utilizing the Curry-Howard
correspondence (e.g., Martin-Löf’s constructive type theory (CTT) Martin-Löf
(1984), Coquand and Huet’s calculus of constructions (CoC) Coquand and Huet
(1988), Luo’s unified theory of dependent types (UTT) Luo (1994), homotopy
type theory (HoTT), UFP (2013)).

Surprisingly, however, the right-hand side of $\;\Leftrightarrow\;$ in (2),
i.e., the judgment “there exists a proof of $\varphi$” is effectively absent.
To our knowledge, there are no type theories explicitly working with basic
judgments corresponding to “there exists a proof of $\varphi$” (in Section 5
we discuss some related systems, including Martin-Löf’s constructive type
theory Martin-Löf (1984) which includes the judgment $\varphi\textit{ true}$
similar in its informal meaning to our $\varphi\textit{ just true}$). In this
paper, we will fill this gap and develop and explore a system that directly
deals with a new formal judgment corresponding to the right-hand side of
$\;\Leftrightarrow\;$ in (2), i.e., to the informal judgment “there exists a
proof of $\varphi$”. We will denote it as $a\mathrel{\therefore}\varphi$ and
call it _judgmental existence_ or existential judgment.

Thus, we obtain:

  * (2′)

there exists a proof of $\varphi$ $\;\Leftrightarrow\;$
$a\mathrel{\therefore}\varphi$

However, first, we consider a purely logical variant of the system, i.e., a
non-computational variant without explicit proof expressions where
$a\mathrel{\therefore}\varphi$ will be replaced with the judgment of the form
$\varphi\textit{ just true}$ with the same meaning “there exists a proof of
$\varphi$”.

Note that from (2) and (2′) we also obtain:

  * (2′′)

$\varphi$ is $\textit{true}_{2}$ $\;\Leftrightarrow\;$
$a\mathrel{\therefore}\varphi$

however, we will prefer the reading of $a\mathrel{\therefore}\varphi$ as
“there exists a proof of $\varphi$” to “$\varphi$ is just true” even though
they are interchangeable.

The main contribution of this paper is that we devise a simple calculus for
reasoning with existential judgments of general form “there exists a proof of
$\varphi$”. More specifically, we introduce two variants of the calculus: a
purely logical one for reasoning with existential judgments of the form
$\varphi\textit{ just true}$ and a computational one for reasoning with
existential judgments of the form $a\mathrel{\therefore}\varphi$. In its
present form, the calculus deals only with a fragment of propositional logic
containing two operators, implication ($\to$) and propositional existence
modality ($\triangle$) used for internalization of the existential
judgment.777The term “propositional existence” for propositions of the form
$\triangle\varphi$ may not be ideal, as it could be mistaken for “existential
proposition” which refers to propositions of the form $\exists
x:\varphi,\ldots$. However, we prefer this terminology as it aligns well with
the term “judgmental existence”. We show that the resulting calculus is
strongly normalizing and has the subject reduction property. It also turns out
that the existence modality operator $\triangle$ is closely related to the
notion of propositional truncation $\Box$, a crucial tool for capturing proof
irrelevance in otherwise proof-relevant systems. We do not consider dependent
types and proof irrelevance is assumed to be propositional (not judgmental).
This is sufficient to illustrate all the key concepts presented in the paper.

Earlier, we have said that there are no type theories with a basic judgment
corresponding to “there exists a proof of $\varphi$”. That is, of course, not
to say that the importance of disregarding proofs, i.e., the idea of proof
irrelevance, has gone unnoticed. On the contrary, it is well well-recognized
and studied issue in the literature. However, many of the approaches for
obtaining proof irrelevance do not explicitly introduce judgmental existence,
i.e., judgments of the form $\varphi\textit{ just
true}$/$a\mathrel{\therefore}\varphi$, and treat it only indirectly via a
propositional modality (most notably the truncation modality888Also known as
squash type, bracket type or subsingleton type. We move away from the usual
notation for truncation “$\|\varphi\|$” towards the simpler notation
“$\Box\varphi$”. where, e.g., $\Box\varphi$ can be understood as “$\varphi$ is
inhabited”, see, e.g., Awodey and Bauer (2004), Gilbert et al. (2019), UFP
(2013)). And even those approaches that take into account the judgmental
existence (see, e.g., Valentini (1998), Pfenning (2001), Reed (2002), Abel and
Scherer (2012)), treat the corresponding judgments $\varphi\textit{ just
true}$/$a\mathrel{\therefore}\varphi$ only as a notational abbreviation for
other judgments (we discuss the related approaches more in Section 5). To our
knowledge, there are currently no approaches that would treat $\varphi\textit{
just true}$/$a\mathrel{\therefore}\varphi$ as a basic judgment.

Finally, it is important to note that the judgment $\varphi\textit{ just
true}$ expresses a notion of existence that is distinct from the notion of
existence typically associated with existential propositions, i.e.,
propositions formed via the existential quantifier $\exists$. To see this,
consider the following observation by Martin-Löf (1993) (originally made in
the context of a related judgment $\varphi\textit{ exists}$, see Section 5).
If we were to attempt to express the notion of existence behind
$\varphi\textit{ just true}$ via $\exists$ we would be inadvertently forming a
new proposition of the form $\exists x:\varphi\ldots$ and since it would be a
proposition, we should also be able to explain what it means for it to be true
in the sense of (2). This would get us “a proposition $\exists
x:\varphi\ldots$ is $\textit{true}_{2}$ $\Leftrightarrow$ there exists a proof
of it” but here the notion of judgmental existence appears once more. And, of
course, any further attempts to explain it via $\exists$ again would lead to
an infinite regress. Thus, propositions of the form $\exists x:\varphi\ldots$
(as do all other propositions) presuppose this notion of judgmental existence.

Structure. In Section 2, we introduce a purely logical variant of the calculus
for reasoning with existential judgments of the form $\varphi\textit{ just
true}$. In Section 3, we introduce its computational variant in the style of
the Curry-Howard correspondence for reasoning with existential judgments of
the form $a\mathrel{\therefore}\varphi$ with explicit proof expressions.
Furthermore, we show that the system has some desirable properties such as
strong normalization and subject reduction. In Section 4, we explore the
connection between existential judgment and propositional truncation modality.
In Section 5, we survey some related work, including the relation of existence
modality to lax modality.

##  2 A logical variant

In this section, we introduce a natural deduction calculus for reasoning with
judgments of the form $\varphi\textit{ true}$ (= $\textit{true}_{1}$) and
$\varphi\textit{ just true}$ (= $\textit{true}_{2}$). The former tells us that
$\varphi$ is proof-relevantly true (i.e., the structure of the corresponding
proof of $\varphi$ is known/relevant to us), while the latter tells us that
$\varphi$ is proof-irrelevantly just true (i.e., the structure of the proof of
$\varphi$ is unknown/irrelevant to us). In other words, it only tells us that
there exists a proof of $\varphi$ and nothing more. We consider a fragment of
propositional logic containing only implication $\to$ and existence modality
$\triangle$.

We show that the system satisfies the structural properties of exchange,
weakening, and contraction for both judgments $\varphi\textit{ true}$ and
$\varphi\textit{ just true}$ and we prove the substitution lemma for all
possible combinations of these judgments. Furthermore, we prove some basic
propositions about the relationship of $\to$ and $\triangle$.

###  2.1 Formal system

Language:

$\displaystyle\text{Propositions }\varphi,\psi$
$\displaystyle\;::=\;p\mid\varphi\to\psi\mid\triangle\varphi$
$\displaystyle\text{Hypotheses }\Gamma$
$\displaystyle\;::=\;\cdot\mid\Gamma,\varphi\textit{ true}$

Categorical judgments:

$\varphi\textit{ true}\qquad\varphi\textit{ just true}$

Hypothetical judgments:999Note that existential judgments can appear only in
the consequent of the hypothetical judgments. In other words, we do not allow
assumptions of the form $\varphi\textit{ just true}$.

$\Gamma\vdash\varphi\textit{ true}\qquad\Gamma\vdash\varphi\textit{ just
true}$

These judgments are governed by the following rules and rules schemata:

hyp $\Gamma,\varphi\textit{ true}\vdash\varphi\textit{ true}$
$\Gamma\vdash\varphi\textit{ true}$ just $\Gamma\vdash\varphi\textit{ just
true}$

$\Gamma,\varphi\textit{ true}\vdash\psi\textit{ star}$ $\to$I$\mathrel{\star}$
$\Gamma\vdash\varphi\to\psi\textit{ star}$ $\Gamma\vdash\varphi\to\psi\textit{
star}$ $\Gamma\vdash\varphi\textit{ true}$ $\to$E$\mathrel{\star}$
$\Gamma\vdash\psi\textit{ star}$

$\Gamma\vdash\varphi\textit{ just true}$ $\triangle$I$\mathrel{\star}$
$\Gamma\vdash\triangle\varphi\textit{ star}$
$\Gamma\vdash\triangle\varphi\textit{ star}$ $\Gamma,\varphi\textit{
true}\vdash\gamma\textit{ just true}$ $\triangle$E$\mathrel{\star}$
$\Gamma\vdash\gamma\textit{ just true}$

where star stands for either “true” or “just true” (all occurencens must be
consistent). Thus, e.g., $\to$I and $\to$E will indicate instances of the
rules $\to$I$\mathrel{\star}$ and $\to$E$\mathrel{\star}$ with true, while
$\to$Ij and $\to$Ej with just true. Analogously, $\triangle$I and $\triangle$E
will indicate instances of $\triangle$I$\mathrel{\star}$ and
$\triangle$E$\mathrel{\star}$ with true, while $\triangle$Ij and $\triangle$Ej
with just true.

Finally, depending on the occurrences of existential judgments, we will have
the following two substitution rules:

$\Gamma\vdash\varphi\textit{ star}$ $\Gamma,\varphi\textit{
true}\vdash\gamma\textit{ star}$ sub1 $\Gamma\vdash\gamma\textit{ star}$

$\Gamma\vdash\varphi\textit{ true}$ $\Gamma,\varphi\textit{
true}\vdash\gamma\textit{ just true}$ sub2 $\Gamma\vdash\gamma\textit{ just
true}$

Comments on just rule. This rule specifies the meaning of the judgment
$\varphi\textit{ just true}$ (together with the appropriate instance of the
sub1 rule, see below). As discussed in Section 1, it captures the idea that if
we have the actual proof of $\varphi$, i.e., if we know that $\varphi$ is
(proof-relevantly) true, then we can derive that there exists a proof of
$\varphi$, i.e., that $\varphi$ is (proof-irrelevantly) true. In other words,
once we know the structure of a proof, we can always choose to disregard it.

Comments on $\to$I$\mathrel{\star}$ and $\to$E$\mathrel{\star}$. Note that the
true variants $\to$I and $\to$E, where star is replaced with true, are just
ordinary implication introduction and elimination rules for defining the
meaning of the connective $\to$ as known from natural deduction (Prawitz
(1965)). The just true variants $\to$Ij and $\to$Ej, where star is replaced
with just true, are more interesting. $\to$Ij states that if we can derive
that $\psi$ is just true under the assumption that $\varphi$ is true, then we
can derive that $\varphi\to\psi$ is just true. So, it is a proof-irrelevant
variant of the standard implication introduction rule. Analogously, $\to$Ej is
a proof-irrelevant variant of the standard implication elimination rule: it
states that if $\varphi\to\psi$ is just true and if $\varphi$ is true, then we
can derive that $\psi$ is just true. Later, we will show that $\to$Ej can be
actually considered as a derived rule, however, this is not the case for
$\to$Ij, unless we adopt an additional principle (Proposition 10 in Section
5). Both true and just true variants of $\to$E$\mathrel{\star}$ are locally
sound and complete (see Section 2.3).

Comments on $\triangle$I$\mathrel{\star}$ and $\triangle$E$\mathrel{\star}$.
Let us start with the true variants $\triangle$I and $\triangle$E. The
introduction rule $\triangle$I internalizes the judgment $\varphi\textit{ just
true}$ by turning it into a proposition, specifically into the true
proposition $\triangle\varphi$. In other words, it defines the meaning of the
proof existence modality $\triangle$.101010Klev (2023) offers an interesting
account of modalities understood as illocutionary forces of speech acts. From
this perspective, it would be interesting to explore to what kind of
illocutionary force the modality $\triangle$ might intuitively correspond. A
natural candidate seems to be a commissive force or some variant of it:
$\triangle\varphi$ can be regarded as a promise that we have a proof of
$\varphi$ but we are not willing to show it. The elimination rule $\triangle$E
then tells us how can we “unpack” the definition of $\triangle$ and return
back to the existential judgment level with $\gamma\textit{ just true}$. Now,
let us consider the just true variants $\triangle$Ij and $\triangle$Ej.
$\triangle$Ij states that if we can derive that $\varphi$ is just true, then
we can also derive that $\triangle\varphi$ is just true. So, it is a proof-
irrelevant variant of $\triangle$I. Analogously, $\triangle$Ej is a proof-
irrelevant variant of $\triangle$E: it states that if $\triangle\varphi$ is
just true and if $\gamma$ is just true under the assumption that $\varphi$ is
true, then we can derive that $\gamma$ is just true as well. Later, we will
show that both $\triangle$Ij and $\triangle$Ej can be actually considered as
derived rules (Proposition 10 in Section 5). Both true and just true variants
of $\triangle$E$\mathrel{\star}$ are locally sound and complete (see Section
2.3).

Now, to simplify some upcoming proofs, let us introduce a new connective
$\varphi\mathrel{\twoheadrightarrow}\psi$ called existential implication and
defined as $\varphi\to\triangle\psi$. Alternatively, we could also specify it
directly via the following I/E rules:

$\Gamma,\varphi\textit{ true}\vdash\psi\textit{ just true}$
$\mathrel{\twoheadrightarrow}$I$\mathrel{\star}$
$\Gamma\vdash\varphi\mathrel{\twoheadrightarrow}\psi\textit{ star}$
$\Gamma\vdash\varphi\mathrel{\twoheadrightarrow}\psi\textit{ star}$
$\Gamma\vdash\varphi\textit{ true}$
$\mathrel{\twoheadrightarrow}$E$\mathrel{\star}$ $\Gamma\vdash\psi\textit{
just true}$

Note that the rule $\mathrel{\twoheadrightarrow}$I$\mathrel{\star}$
essentially internalizes the hypothetical judgment $\Gamma,\varphi\textit{
true}\vdash\psi\textit{ just true}$ as a proposition
$\varphi\mathrel{\twoheadrightarrow}\psi$ that can be either true or just
true.

Also note that these I/E rules become derivable when we consider
$\varphi\mathrel{\twoheadrightarrow}\psi$ to be defined as
$\varphi\to\triangle\psi$:

$\Gamma,\varphi\textit{ true}\vdash\psi\textit{ just true}$
$\triangle$I$\mathrel{\star}$ $\Gamma,\varphi\textit{
true}\vdash\triangle\psi\textit{ star}$ $\to$I$\mathrel{\star}$
$\Gamma\vdash\varphi\to\triangle\psi\textit{ star}$

$\Gamma\vdash\varphi\to\triangle\psi\textit{ star}$
$\Gamma\vdash\varphi\textit{ true}$ $\to$E$\mathrel{\star}$
$\Gamma\vdash\triangle\psi\textit{ star}$ hyp $\Gamma,\psi\textit{ true
}\vdash\psi\textit{ true}$ just $\Gamma,\psi\textit{ true }\vdash\psi\textit{
just true}$ $\triangle$E$\mathrel{\star}$ $\Gamma\vdash\psi\textit{ just
true}$

###  2.2 Basic properties

######  Lemma 1.

(Exchange) If $\Gamma,\varphi\textit{ true},\psi\textit{
true}\vdash\gamma\textit{ star}$, then $\Gamma,\psi\textit{
true},\varphi\textit{ true}\vdash\gamma\textit{ star}$.

###### Proof.

By structural induction on the derivations of $\Gamma,\varphi\textit{
true},\psi\textit{ true}\vdash\gamma\textit{ true}$ and
$\Gamma,\varphi\textit{ true},\psi\textit{ true}\vdash\gamma\textit{ just
true}$, respectively.

For example, let us consider $\Gamma,\varphi\textit{ true},\psi\textit{
true}\vdash\gamma\textit{ just true}$ for the case of $\triangle$E:

$\mathcal{D}$ =  $\mathcal{D}^{\prime}$ $\Gamma,\tau\textit{
true},\theta\textit{ true}\vdash\triangle\psi\textit{ true}$
$\mathcal{D}^{\prime\prime}$ $\Gamma,\tau\textit{ true},\theta\textit{
true},\psi\textit{ true}\vdash\sigma\textit{ just true}$ $\triangle$E
$\Gamma,\tau\textit{ true},\theta\textit{ true}\vdash\sigma\textit{ just
true}$

  1. 1.

$\Gamma,\theta\textit{ true},\tau\textit{ true}\vdash\triangle\psi\textit{
true}$ (by exchange for judgments of the form $\gamma\textit{ true}$ on
$\mathcal{D}^{\prime}$)

  2. 2.

$\Gamma,\theta\textit{ true},\tau\textit{ true},\psi\textit{
true}\vdash\sigma\textit{ just true}$ (by induction hypothesis, IH, on
$\mathcal{D}^{\prime\prime}$)

  3. 3.

$\Gamma,\theta\textit{ true},\tau\textit{ true}\vdash\sigma\textit{ just
true}$ (by $\triangle$E on 1. and 2.)

######  Lemma 2.

(Weakening) If $\Gamma\vdash\gamma\textit{ star}$, then
$\Gamma,\varphi\textit{ true}\vdash\gamma\textit{ star}$.

Note. Since we disallow just true assumptions, we need to consider only two
cases.

###### Proof.

By structural induction on the derivations of $\Gamma\vdash\gamma\textit{
true}$ and $\Gamma\vdash\gamma\textit{ just true}$, respectively.

For example, let us consider $\Gamma\vdash\gamma\textit{ just true}$ for the
case of $\triangle$E:

$\mathcal{D}$ =  $\mathcal{D}^{\prime}$ $\Gamma\vdash\triangle\psi\textit{
true}$ $\mathcal{D}^{\prime\prime}$ $\Gamma,\psi\textit{
true}\vdash\sigma\textit{ just true}$ $\triangle$E $\Gamma\vdash\sigma\textit{
just true}$

  1. 1.

$\Gamma,\varphi\textit{ true}\vdash\triangle\psi\textit{ true}$ (by weakening
for judgments of the form $\gamma\textit{ true}$ on $\mathcal{D}^{\prime}$)

  2. 2.

$\Gamma,\psi\textit{ true},\varphi\textit{ true}\vdash\sigma\textit{ just
true}$ (by IH on $\mathcal{D}^{\prime\prime}$)

  3. 3.

$\Gamma,\varphi\textit{ true}\vdash\sigma\textit{ just true}$ (by exchange on
2. and $\triangle$E on 1. and 2.)

######  Lemma 3.

(Contraction) If $\Gamma,\varphi\textit{ true},\varphi\textit{
true}\vdash\gamma\textit{ star}$, then $\Gamma,\varphi\textit{
true}\vdash\gamma\textit{ star}$.

###### Proof.

By structural induction.

######  Lemma 4.

(Substitution lemma)

  1. (sub1) If $\Gamma\vdash\varphi\textit{ star}$ and $\Gamma,\varphi\textit{ true}\vdash\gamma\textit{ star}$ then $\Gamma\vdash\gamma\textit{ star}$.

  2. (sub2) If $\Gamma\vdash\varphi\textit{ true}$ and $\Gamma,\varphi\textit{ true}\vdash\gamma\textit{ just true}$ then $\Gamma\vdash\gamma\textit{ just true}$.

###### Proof.

(sub1, star = true) By structural induction on the derivation of
$\Gamma,\varphi\textit{ true}\vdash\gamma\textit{ true}$.

###### Proof.

(sub1, star = just true) By structural induction on the derivation of
$\Gamma\vdash\varphi\textit{ just true}$.

For example, let us consider again the case of $\triangle$E:

$\mathcal{D}$ =  $\mathcal{D}^{\prime}$ $\Gamma\vdash\triangle\psi\textit{
true}$ $\mathcal{D}^{\prime\prime}$ $\Gamma,\psi\textit{
true}\vdash\varphi\textit{ just true}$ $\triangle$E
$\Gamma\vdash\varphi\textit{ just true}$

  1. 1.

$\Gamma,\varphi\textit{ true}\vdash\gamma\textit{ just true}$ (by assumption)

  2. 2.

$\Gamma\vdash\psi\textit{ just true}$ (by inversion111111Inversion is a
metalevel reasoning principle for the level of judgments that essentially
states: if the conclusion of a rule holds, so must its premise(s). on
$\mathcal{D}^{\prime}$)

  3. 3.

$\Gamma\vdash\varphi\textit{ just true}$ (by IH on 2. and
$\mathcal{D}^{\prime\prime}$)

  4. 4.

$\Gamma\vdash\triangle\varphi\textit{ true}$ (by $\triangle$I on 3.)

  5. 5.

$\Gamma\vdash\gamma\textit{ just true}$ (by $\triangle$E on 1. and 4.)

###### Proof.

(sub2) By structural induction on the derivation of $\Gamma,\varphi\textit{
true}\vdash\gamma\textit{ just true}$.

For example, let us consider the case of $\triangle$E:

$\mathcal{D}$ =  $\mathcal{D}^{\prime}$ $\Gamma,\varphi\textit{
true}\vdash\triangle\psi\textit{ true}$ $\mathcal{D}^{\prime\prime}$
$\Gamma,\varphi\textit{ true},\psi\textit{ true}\vdash\sigma\textit{ just
true}$ $\triangle$E $\Gamma,\varphi\textit{ true}\vdash\sigma\textit{ just
true}$

  1. 1.

$\Gamma\vdash\varphi\textit{ true}$ (by assumption)

  2. 2.

$\Gamma\vdash\triangle\psi\textit{ true}$ (by sub1 on 1. and
$\mathcal{D}^{\prime}$)

  3. 3.

$\Gamma,\psi\textit{ true}\vdash\varphi\textit{ true}$ (by weakening on
$\mathcal{D}^{\prime}$)

  4. 4.

$\Gamma,\psi\textit{ true},\varphi\textit{ true}\vdash\sigma\textit{ just
true}$ (by exchange on $\mathcal{D}^{\prime\prime}$)

  5. 5.

$\Gamma,\psi\textit{ true}\vdash\sigma\textit{ just true}$ (by IH on 3. and
4.)

  6. 6.

$\Gamma\vdash\sigma\textit{ just true}$ (by $\triangle$E on 2. and 5.)

###  2.3 Reduction and expansion rules

Reduction and expansion for $\triangle\varphi\textit{ star}$:

$\mathcal{D}$ $\Gamma\vdash\varphi\textit{ just true}$
$\triangle$I$\mathrel{\star}$ $\Gamma\vdash\triangle\varphi\textit{ star}$
$\mathcal{D^{\prime}}$ $\Gamma,\varphi\textit{ true}\vdash\gamma\textit{ just
true}$ $\triangle$E$\mathrel{\star}$ $\Gamma\vdash\gamma\textit{ just true}$
$\Rightarrow_{R}$ $\mathcal{D^{\prime\prime}}$ $\Gamma\vdash\gamma\textit{
just true}$

where $\mathcal{D}^{\prime\prime}$ is constructed from $\mathcal{D^{\prime}}$
by replacing instances of the hypothesis $\varphi\textit{ true}$ with
$\mathcal{D}$ (via sub1).121212Note that these reductions do not operate on
natural deduction derivations with formulas but on demonstrations with
judgments. Thus our natural-deduction-like phrasing “replacing instances of
the hypothesis $\varphi\textit{ true}$ true with $\mathcal{D}$” is somewhat an
abuse of language (this can also be observed in Pfenning and Davies (2001)).
We thank Ansten Klev for this note. A proper judgmental explanation of these
reduction metarules will come later in Section 3 where we introduce
reducibility judgments of the form $\Gamma\vdash
e\Longrightarrow_{R}e^{\prime}$ corresponding to these reductions.

$\mathcal{D}$ $\Gamma\vdash\triangle\varphi\textit{ star}$ $\Rightarrow_{E}$
$\mathcal{D}$ $\Gamma\vdash\triangle\varphi\textit{ star}$ hyp
$\Gamma,\varphi\textit{ true}\vdash\varphi\textit{ true}$ just
$\Gamma,\varphi\textit{ true}\vdash\varphi\textit{ just true}$
$\triangle$E$\mathrel{\star}$ $\Gamma\vdash\varphi\textit{ just true}$
$\triangle$I$\mathrel{\star}$ $\Gamma\vdash\triangle\varphi\textit{ star}$

Reduction and expansion for $\varphi\to\psi\textit{ star}$:

$\mathcal{D}$ $\Gamma,\varphi\textit{ true}\vdash\psi\textit{ star}$
$\to$I$\mathrel{\star}$ $\Gamma\vdash\varphi\to\psi\textit{ star}$
$\mathcal{D^{\prime}}$ $\Gamma\vdash\varphi\textit{ true}$
$\to$E$\mathrel{\star}$ $\Gamma\vdash\psi\textit{ star}$ $\Rightarrow_{R}$
$\mathcal{D^{\prime\prime}}$ $\Gamma\vdash\psi\textit{ star}$

where $\mathcal{D}^{\prime\prime}$ is constructed from $\mathcal{D}$ by
replacing instances of the hypothesis $\varphi\textit{ true}$ with
$\mathcal{D^{\prime}}$ (via sub1) if star = true, otherwise, i.e., if star =
exist, $\mathcal{D}^{\prime\prime}$ is constructed from $\mathcal{D}$ by
replacing instances of the hypothesis $\varphi\textit{ true}$ with
$\mathcal{D^{\prime}}$ (via sub2).

$\mathcal{D}$ $\Gamma\vdash\varphi\to\psi\textit{ star}$ $\Rightarrow_{E}$
$\mathcal{D}$ $\Gamma\vdash\varphi\to\psi\textit{ star}$ w
$\Gamma,\varphi\textit{ true}\vdash\varphi\to\psi\textit{ star}$ hyp
$\Gamma,\varphi\textit{ true}\vdash\varphi\textit{ true}$
$\to$E$\mathrel{\star}$ $\Gamma,\varphi\textit{ true}\vdash\psi\textit{ star}$
$\to$I$\mathrel{\star}$ $\Gamma\vdash\varphi\to\psi\textit{ star}$

Reduction and expansion for $\varphi\mathrel{\twoheadrightarrow}\psi\textit{
star}$ :

$\mathcal{D}$ $\Gamma,\varphi\textit{ true}\vdash\psi\textit{ just true}$
$\mathrel{\twoheadrightarrow}$I$\mathrel{\star}$
$\Gamma\vdash\varphi\mathrel{\twoheadrightarrow}\psi\textit{ star}$
$\mathcal{D^{\prime}}$ $\Gamma\vdash\varphi\textit{ true}$
$\mathrel{\twoheadrightarrow}$E$\mathrel{\star}$ $\Gamma\vdash\psi\textit{
just true}$ $\Rightarrow_{R}$ $\mathcal{D^{\prime\prime}}$
$\Gamma\vdash\psi\textit{ just true}$

where $\mathcal{D}^{\prime\prime}$ is constructed from $\mathcal{D}$ by
replacing instances of the hypothesis $\varphi\textit{ true}$ with
$\mathcal{D^{\prime}}$ (via sub2).

$\mathcal{D}$ $\Gamma\vdash\varphi\mathrel{\twoheadrightarrow}\psi\textit{
star}$ $\Rightarrow_{E}$ $\mathcal{D}$
$\Gamma\vdash\varphi\mathrel{\twoheadrightarrow}\psi\textit{ star}$ w
$\Gamma,\varphi\textit{
true}\vdash\varphi\mathrel{\twoheadrightarrow}\psi\textit{ star}$ hyp
$\Gamma,\varphi\textit{ true}\vdash\varphi\textit{ true}$
$\mathrel{\twoheadrightarrow}$E$\mathrel{\star}$ $\Gamma,\varphi\textit{
true}\vdash\psi\textit{ just true}$
$\mathrel{\twoheadrightarrow}$I$\mathrel{\star}$
$\Gamma\vdash\varphi\mathrel{\twoheadrightarrow}\psi\textit{ star}$

##### Some propositions.

######  Proposition 1.

$\Gamma\vdash\varphi\to\psi\textit{ just true}$ iff
$\Gamma\vdash\varphi\to\triangle\psi\textit{ true}$.

Informally, it tells us that if $\varphi\to\psi$ is just true, i.e., if there
exists a proof of it, then we can derive that $\varphi\to\triangle\psi$ is
true, i.e., that we have a proof for it, and vice versa. In other words, a
proof of $\varphi\to\triangle\psi$ carries no more information than the
existence of a proof of $\varphi\to\psi$.

###### Proof.

To simplify the proof, we use $\varphi\mathrel{\twoheadrightarrow}\psi$
instead of $\varphi\to\triangle\psi$ (recall that
$\mathrel{\twoheadrightarrow}$ is defined via $\to$ and $\triangle$).

$\Gamma\vdash\varphi\mathrel{\twoheadrightarrow}\psi\textit{ true}$ w
$\Gamma,\varphi\textit{
true}\vdash\varphi\mathrel{\twoheadrightarrow}\psi\textit{ true}$ hyp
$\Gamma,\varphi\textit{ true}\vdash\varphi\textit{ true}$
$\mathrel{\twoheadrightarrow}$E $\Gamma,\varphi\textit{
true}\vdash\psi\textit{ just true}$ $\to$Ij
$\Gamma\vdash\varphi\to\psi\textit{ just true}$

$\Gamma\vdash\varphi\to\psi\textit{ just true}$ w $\Gamma,\varphi\textit{
true}\vdash\varphi\to\psi\textit{ just true}$ hyp $\Gamma,\varphi\textit{
true}\vdash\varphi\textit{ true}$ $\to$Ej $\Gamma,\varphi\textit{
true}\vdash\psi\textit{ just true}$ $\mathrel{\twoheadrightarrow}$I
$\Gamma\vdash\varphi\mathrel{\twoheadrightarrow}\psi\textit{ true}$

Note. If we were interested only in the notion of proof-relevant true, we
could simply transform Proposition 1 into:

  1. $\Gamma\vdash\triangle(\varphi\to\psi)\textit{ true}$ iff $\Gamma\vdash\varphi\to\triangle\psi\textit{ true}$.

via the application of $\triangle$I on the first judgment (analogously for the
following propositions). Also, note that we can prove that if
$\Gamma\vdash\varphi\to\psi\textit{ true}$ then
$\Gamma\vdash\varphi\to\triangle\psi\textit{ true}$ but not vice versa.

$\Gamma\vdash\varphi\to\psi\textit{ true}$ w $\Gamma,\varphi\textit{
true}\vdash\varphi\to\psi\textit{ true}$ hyp $\Gamma,\varphi\textit{
true}\vdash\varphi\textit{ true}$ $\to$E $\Gamma,\varphi\textit{
true}\vdash\psi\textit{ true}$ just $\Gamma,\varphi\textit{
true}\vdash\psi\textit{ just true}$ $\triangle$I $\Gamma,\varphi\textit{
true}\vdash\triangle\psi\textit{ true}$ $\to$I
$\Gamma\vdash\varphi\to\triangle\psi\textit{ true}$

However, from $\Gamma\vdash\varphi\to\triangle\psi\textit{ true}$ we can
derive $\Gamma\vdash\triangle\varphi\to\triangle\psi\textit{ true}$ and vice
versa.

######  Proposition 2.

$\Gamma\vdash\varphi\to\triangle\psi\textit{ true}$ iff
$\Gamma\vdash\triangle\varphi\to\triangle\psi\textit{ true}$.

###### Proof.

To shorten this proof, we will write “$\varphi$” instead of “$\varphi\textit{
true}$” and “$\varphi\textit{ just}$” instead of “$\varphi\textit{ just
true}$” (we will adopt this notation for all upcoming longer proofs):

hyp $\Gamma,\triangle\varphi\vdash\triangle\varphi$
$\Gamma\vdash\varphi\to\triangle\psi$ w
$\Gamma,\varphi\vdash\varphi\to\triangle\psi$ hyp
$\Gamma,\varphi\vdash\varphi$ $\to$E $\Gamma,\varphi\vdash\triangle\psi$ hyp
$\Gamma,\psi\vdash\psi$ w $\Gamma,\psi,\varphi\vdash\psi$ ex
$\Gamma,\varphi,\psi\vdash\psi$ just $\Gamma,\varphi,\psi\vdash\psi\textit{
just}$ $\triangle$E $\Gamma,\varphi\vdash\psi\textit{ just}$ w
$\Gamma,\varphi,\triangle\varphi\vdash\psi\textit{ just}$ ex
$\Gamma,\triangle\varphi,\varphi\vdash\psi\textit{ just}$ $\triangle$E
$\Gamma,\triangle\varphi\vdash\psi\textit{ just}$ $\triangle$I
$\Gamma,\triangle\varphi\vdash\triangle\psi$ $\to$I
$\Gamma\vdash\triangle\varphi\to\triangle\psi$

$\Gamma\vdash\triangle\varphi\to\triangle\psi\textit{ true}$ w
$\Gamma,\varphi\vdash\triangle\varphi\to\triangle\psi\textit{ true}$ hyp
$\Gamma,\varphi\vdash\varphi\textit{ true}$ just
$\Gamma,\varphi\vdash\varphi\textit{ just true}$ $\triangle$I
$\Gamma,\varphi\vdash\triangle\varphi\textit{ true}$ $\to$E
$\Gamma,\varphi\vdash\triangle\psi\textit{ true}$ $\to$I
$\Gamma\vdash\varphi\to\triangle\psi\textit{ true}$

######  Proposition 3.

$\Gamma\vdash\varphi\to\triangle\psi\textit{ true}$ iff
$\Gamma\vdash\triangle\varphi\to\psi\textit{ just true}$.

Proof.

hyp $\Gamma,\triangle\varphi\textit{ true}\vdash\triangle\varphi\textit{
true}$ $\Gamma\vdash\varphi\mathrel{\twoheadrightarrow}\psi\textit{ true}$ w
$\Gamma,\varphi\textit{
true}\vdash\varphi\mathrel{\twoheadrightarrow}\psi\textit{ true}$ hyp
$\Gamma,\varphi\textit{ true}\vdash\varphi\textit{ true}$
$\mathrel{\twoheadrightarrow}$E $\Gamma,\varphi\textit{
true}\vdash\psi\textit{ just true}$ w $\Gamma,\varphi\textit{
true},\triangle\varphi\textit{ true}\vdash\psi\textit{ just true}$ ex
$\Gamma,\triangle\varphi\textit{ true},\varphi\textit{ true}\vdash\psi\textit{
just true}$ $\triangle$E $\Gamma,\triangle\varphi\textit{
true}\vdash\psi\textit{ just true}$ $\to$Ij
$\Gamma\vdash\triangle\varphi\to\psi\textit{ just true}$

$\Gamma\vdash\triangle\varphi\to\psi\textit{ just true}$ w
$\Gamma,\varphi\textit{ true}\vdash\triangle\varphi\to\psi\textit{ just true}$
hyp $\Gamma,\varphi\textit{ true}\vdash\varphi\textit{ true}$ just
$\Gamma,\varphi\textit{ true}\vdash\varphi\textit{ just true}$ $\triangle$I
$\Gamma,\varphi\textit{ true}\vdash\triangle\varphi\textit{ true}$ $\to$Ej
$\Gamma,\varphi\textit{ true}\vdash\psi\textit{ just true}$
$\mathrel{\twoheadrightarrow}$I
$\Gamma\vdash\varphi\mathrel{\twoheadrightarrow}\psi\textit{ true}$

######  Proposition 4.

$\Gamma\vdash\varphi\to\psi\textit{ just true}$ iff
$\Gamma\vdash\triangle\varphi\to\psi\textit{ just true}$.

Proof. Follows from Propositions 1 and 3.

######  Proposition 5.

($\triangle$ distributes over $\to$). If
$\Gamma\vdash\triangle(\varphi\to\psi)\textit{ true}$ then
$\Gamma\vdash\triangle\varphi\to\triangle\psi\textit{ true}$.

Proof.

hyp $\Gamma,\triangle\varphi\vdash\triangle\varphi$
$\Gamma\vdash\triangle(\varphi\to\psi)$ w
$\Gamma,\varphi\vdash\triangle(\varphi\to\psi)$ hyp
$\Gamma,\varphi\to\psi\vdash\varphi\to\psi$ w
$\Gamma,\varphi\to\psi,\varphi\vdash\varphi\to\psi$ ex
$\Gamma,\varphi,\varphi\to\psi\vdash\varphi\to\psi$ hyp
$\Gamma,\varphi\vdash\varphi$ w $\Gamma,\varphi,\varphi\to\psi\vdash\varphi$
$\to$E $\Gamma,\varphi,\varphi\to\psi\vdash\psi$ just
$\Gamma,\varphi,\varphi\to\psi\vdash\psi\textit{ just}$ $\triangle$E
$\Gamma,\varphi\vdash\psi\textit{ just}$ w
$\Gamma,\varphi,\triangle\varphi\vdash\psi\textit{ just}$ ex
$\Gamma,\triangle\varphi,\varphi\vdash\psi\textit{ just}$ $\triangle$E
$\Gamma,\triangle\varphi\vdash\psi\textit{ just}$ $\triangle$I
$\Gamma,\triangle\varphi\vdash\triangle\psi$ $\to$I
$\Gamma\vdash\triangle\varphi\to\triangle\psi$

######  Proposition 6.

$\Gamma\vdash\triangle\triangle\varphi\to\triangle\varphi\textit{ true}$.

Proof.

hyp $\Gamma,\triangle\triangle\varphi\vdash\triangle\triangle\varphi$ hyp
$\Gamma,\triangle\varphi\vdash\triangle\varphi$ hyp
$\Gamma,\varphi\vdash\varphi$ just $\Gamma,\varphi\vdash\varphi\textit{ just}$
w $\Gamma,\varphi,\triangle\varphi\vdash\varphi\textit{ just}$ ex
$\Gamma,\triangle\varphi,\varphi\vdash\varphi\textit{ just}$ $\triangle$E
$\Gamma,\triangle\varphi\vdash\varphi\textit{ just}$ w
$\Gamma,\triangle\varphi,\triangle\triangle\varphi\vdash\varphi\textit{ just}$
ex $\Gamma,\triangle\triangle\varphi,\triangle\varphi\vdash\varphi\textit{
just}$ $\triangle$E $\Gamma,\triangle\triangle\varphi\vdash\varphi\textit{
just}$ $\triangle$I $\Gamma,\triangle\triangle\varphi\vdash\triangle\varphi$
$\to$I $\Gamma\vdash\triangle\triangle\varphi\to\triangle\varphi$

##  3 A computational variant

In this section, we introduce a computational interpretation of the system
from Section 2 with explicit proof expressions in the style of the Curry-
Howard isomorphism. Specifically, instead of purely logical judgments
$\varphi\textit{ true}$ and $\varphi\textit{ just true}$ we will work with
judgments $e:\varphi$ and $e\mathrel{\therefore}\varphi$ where $e$ is a proof
expression representing the proof of $\varphi$. The informal meaning of
$e:\varphi$ and $e\mathrel{\therefore}\varphi$ remains the same, i.e.,
“$\varphi$ is true” and “there exists a proof of $\varphi$”, respectively.
Additionally, we introduce new forms of judgment for expressing the notions of
reducibility $\Longrightarrow$ and computability $\mathbf{R}$ of expressions
$e$ of type $\varphi$.

The computational variant satisfies all the discussed properties of the
logical variant, including the substitution lemma. Furthermore, we show that
the computational variant has the subject reduction property and other useful
properties such as forward and backward preservation, which then allows us to
finally show that it also has the strong normalization property.

###  3.1 Formal system

Language:

$\displaystyle\text{Propositions }\varphi,\psi$
$\displaystyle\;::=\;p\mid\varphi\to\psi\mid\triangle\varphi$
$\displaystyle\text{Terms }t,t^{\prime}$ $\displaystyle\;::=\;x\mid\lambda
x.t\mid\textsf{ap}(t,t^{\prime})\mid\langle e\rangle$
$\displaystyle\text{Expressions }e,e^{\prime}$
$\displaystyle\;::=\;t\mid\textsf{let }\langle x\rangle\textsf{ be }t\textsf{
in
}e\mid\lambda_{\textrm{j}}x.e\mid\textsf{ap}_{\textrm{j}}(e,t^{\prime})\mid\langle
e\rangle_{\textrm{j}}\mid\textsf{let }\langle x\rangle_{\textrm{j}}\textsf{ be
}e^{\prime}\textsf{ in }e$ $\displaystyle\text{Hypotheses }\Gamma$
$\displaystyle\;::=\;\cdot\mid\Gamma,x:\varphi$

Note. All terms are expressions but not vice versa. The main difference
between terms and expressions is that any two expressions $e$ and $e^{\prime}$
of type $\varphi$ are treated as (propositionally) equal, which is not the
case for terms. This is a consequence of the fact existential judgments
capture the notion of proof-irrelevant truth.

Categorical judgments:

$t:\varphi\qquad e\mathrel{\therefore}\varphi$

Hypothetical judgments:

$\Gamma\vdash t:\varphi\qquad\Gamma\vdash e\mathrel{\therefore}\varphi$

Note. The traditional logical reading of the symbol “$\mathrel{\therefore}$”
as “therefore” can still be applied here, i.e., it still makes sense to read
$e\mathrel{\therefore}\varphi$ as “$e$, therefore $\varphi$” – there exists a
proof $e$ for $\varphi$, _therefore_ we can claim that $\varphi$ is true.
Also, from a type-theoretic view, one reads $t:\varphi$ as “$t$ has type
$\varphi$” or “$t$ is typed to $\varphi$”. Analogously,
$t\mathrel{\therefore}\varphi$ can be read as “there exists a term of type
$\varphi$” or “$t$ is irrelevantly typed to $\varphi$”. Or, from a proof-
theoretic view, “there exists a proof of proposition $\varphi$”.

Similarly to the metavariable star standing either for true or just true from
Section 2, we use the metavariable $\mathrel{\star}$ standing either for “$:$”
or “$\mathrel{\therefore}$”, i.e., either proof-relevant or proof-irrelevant
typing (again, all occurrences in rules, theorems, etc. must be consistent):

$\Gamma\vdash e\mathrel{\star}\varphi$

Also, note that since all terms $t$ are expressions $e$ but not vice versa,
instantiating judgment $e\mathrel{\star}\varphi$ with “$:$” leads to
$t:\varphi$, not $e:\varphi$. In other words, in cases where $\mathrel{\star}$
is replaced with “$:$”, expressions $e$ are restricted to terms $t$.

Additionally, to the previous section, we add two new forms of judgments:

$\Gamma\vdash e\Longrightarrow_{R}e^{\prime}\qquad\Gamma\vdash
e\Longrightarrow_{E}e^{\prime}$

The first judgment, $\Gamma\vdash e\Longrightarrow e^{\prime}$, tells us that
in the context $\Gamma$, the expression $e$ reduces to the expression
$e^{\prime}$. The second judgment, $\Gamma\vdash
e\Longrightarrow_{E}e^{\prime}$, tells us that in the context $\Gamma$, the
expression $e$ expands to the expression $e^{\prime}$. In a computational
setting, thanks to the Curry-Howard correspondence, these new judgments on
proof expressions correspond to the local reduction and expansion metarules
$\Rightarrow_{R}$ and $\Rightarrow_{E}$ from previous Section 2. To simplify
the notation a little, we will omit the subscript “$R$” with reductions and
write simply $\Longrightarrow$, while keeping the subscript “$E$” for
expansions.

The above judgments are governed by the following rules:

hyp $\Gamma,x:\varphi\vdash x:\varphi$ $\Gamma\vdash t:\varphi$ just
$\Gamma\vdash t\mathrel{\therefore}\varphi$

To make the presentation of logical rules more surveyable, we skip the
schematic star variants $\to$I$\mathrel{\star}$, $\to$E$\mathrel{\star}$,
$\triangle$I$\mathrel{\star}$, $\triangle$E$\mathrel{\star}$ and present
directly their typed variants instantiated by “$:$” and
“$\mathrel{\therefore}$”, respectively (we will write this as
$\mathrel{\star}$ = $:$ and $\mathrel{\star}$ = $\mathrel{\therefore}$), i.e.,
$\to$I, $\to$E, $\triangle$I, $\triangle$E and $\to$Ij, $\to$Ej,
$\triangle$Ij, $\triangle$Ej. We also add corresponding computations (C) and
expansion (CE) rules.

First, let us present the true variants (i.e., $\mathrel{\star}$ = $:$):

$\Gamma,x:\varphi\vdash t:\psi$ $\to$I $\Gamma\vdash\lambda
x.t:\varphi\to\psi$ $\Gamma\vdash t:\varphi\to\psi$ $\Gamma\vdash
t^{\prime}:\varphi$ $\to$E $\Gamma\vdash\textsf{ap}(t,t^{\prime}):\psi$

$\Gamma,x:\varphi\vdash t:\psi$ $\Gamma\vdash t^{\prime}:\varphi$ $\to$C
$\Gamma\vdash\textsf{ap}(\lambda
x.t,t^{\prime})\Longrightarrow[t^{\prime}/x]t$ $\Gamma\vdash t:\varphi\to\psi$
$\to$CE $\Gamma\vdash t\Longrightarrow_{E}\lambda x.\textsf{ap}(t,x)$

$\Gamma\vdash e\Longrightarrow e^{\prime}$ apC
$\Gamma\vdash\textsf{ap}(e,e^{\prime\prime})\Longrightarrow\textsf{ap}(e^{\prime},e^{\prime\prime})$

$\Gamma\vdash e\mathrel{\therefore}\varphi$ $\triangle$I $\Gamma\vdash\langle
e\rangle:\triangle\varphi$ $\Gamma\vdash t:\triangle\varphi$
$\Gamma,x:\varphi\vdash e\mathrel{\therefore}\gamma$ $\triangle$E
$\Gamma\vdash\textsf{let }\langle x\rangle\textsf{ be }t\textsf{ in
}e\mathrel{\therefore}\gamma$

$\Gamma,x:\varphi\vdash e\mathrel{\therefore}\gamma$ $\Gamma\vdash
t:\triangle\varphi$ $\triangle$C $\Gamma\vdash\textsf{let }\langle
x\rangle\textsf{ be }\langle e^{\prime}\rangle\textsf{ in
}e\Longrightarrow\mathopen{\lsem}e^{\prime}/x\mathclose{\rsem}e$

$\Gamma\vdash t:\triangle\varphi$ $\triangle$CE $\Gamma\vdash
t\Longrightarrow_{E}\langle\textsf{let }\langle x\rangle\textsf{ be }t\textsf{
in }x\rangle$

Now, let us present the just true variant (i.e., $\mathrel{\star}$ =
$\mathrel{\therefore}$):

$\Gamma,x:\varphi\vdash e\mathrel{\therefore}\psi$ $\to$Ij
$\Gamma\vdash\lambda_{\textrm{j}}x.e\mathrel{\therefore}\varphi\to\psi$
$\Gamma\vdash e\mathrel{\therefore}\varphi\to\psi$ $\Gamma\vdash t:\varphi$
$\to$Ej $\Gamma\vdash\textsf{ap}_{\textrm{j}}(e,t)\mathrel{\therefore}\psi$

$\Gamma,x:\varphi\vdash e\mathrel{\therefore}\psi$ $\Gamma\vdash t:\varphi$
$\to$Cj
$\Gamma\vdash\textsf{ap}_{\textrm{j}}(\lambda_{\textrm{j}}x.e,t)\Longrightarrow[t/x]e$
$\Gamma\vdash e\mathrel{\therefore}\varphi\to\psi$ $\to$CEj $\Gamma\vdash
e\Longrightarrow_{E}\lambda_{\textrm{j}}x.\textsf{ap}_{\textrm{j}}(e,x)$

$\Gamma\vdash e\Longrightarrow e^{\prime}$ apCj
$\Gamma\vdash\textsf{ap}_{\textrm{j}}(e,e^{\prime\prime})\Longrightarrow\textsf{ap}_{\textrm{j}}(e^{\prime},e^{\prime\prime})$

$\Gamma\vdash e\mathrel{\therefore}\varphi$ $\triangle$Ij $\Gamma\vdash\langle
e\rangle_{\textrm{j}}\mathrel{\therefore}\triangle\varphi$ $\Gamma\vdash
e^{\prime}\mathrel{\therefore}\triangle\varphi$ $\Gamma,x:\varphi\vdash
e\mathrel{\therefore}\gamma$ $\triangle$Ej $\Gamma\vdash\textsf{let }\langle
x\rangle_{\textrm{j}}\textsf{ be }e^{\prime}\textsf{ in
}e\mathrel{\therefore}\gamma$

$\Gamma,x:\varphi\vdash e\mathrel{\therefore}\gamma$ $\Gamma\vdash
e^{\prime\prime}\mathrel{\therefore}\triangle\varphi$ $\triangle$Cj
$\Gamma\vdash\textsf{let }\langle x\rangle_{\textrm{j}}\textsf{ be }\langle
e^{\prime}\rangle_{\textrm{j}}\textsf{ in
}e\Longrightarrow\mathopen{\lsem}e^{\prime}/x\mathclose{\rsem}e$

$\Gamma\vdash e\mathrel{\therefore}\triangle\varphi$ $\triangle$CEj
$\Gamma\vdash e\Longrightarrow_{E}\langle\textsf{let }\langle
x\rangle_{\textrm{j}}\textsf{ be }e\textsf{ in }x\rangle$

Note that the newly introduced just true variants of canonical and
noncanonical proof expressions, namely
$\lambda_{\textrm{j}}x.e,\textsf{ap}_{\textrm{j}}(e,e^{\prime})$, $\langle
e\rangle_{\textrm{j}}$, $\textsf{let }\langle x\rangle_{\textrm{j}}\textsf{ be
}e^{\prime}\textsf{ in }e$, behave essentially identically to their true
variants, only the associated typing relation changes from the proof-relevant
$:$ to the proof-irrelevant $\mathrel{\therefore}$ . For example, in the
proof-irrelevant application $\textsf{ap}_{\textrm{j}}(e,t^{\prime})$ the
first argument is an expression, while in the proof-relevant application
$\textsf{ap}(t,t^{\prime})$ the first argument is a term.

###  3.2 Basic properties

####  3.2.1 Substitution

$\Gamma\vdash e\mathrel{\star}\varphi$ $\Gamma,x:\varphi\vdash
e^{\prime}\mathrel{\star}\gamma$ sub1
$\Gamma\vdash\mathopen{\lsem}e/x\mathclose{\rsem}e^{\prime}\mathrel{\star}\gamma$
$\Gamma\vdash t:\varphi$ $\Gamma,x:\varphi\vdash e\mathrel{\therefore}\gamma$
sub2 $\Gamma\vdash[t/x]e\mathrel{\therefore}\gamma$

where $[t/x]e$ from sub2 represents the result of substituting $t$ for $x$ in
$e$ while renaming bound variables where necessary to avoid variable capture.
The definition of the new kind of substitution
$\mathopen{\lsem}e/x\mathclose{\rsem}e^{\prime}$ from sub1 is a bit more
tricky. When $\mathrel{\star}$ = $:$, the substitution
$\mathopen{\lsem}e/x\mathclose{\rsem}e^{\prime}$ becomes just
$[t/x]t^{\prime}$. However, when $\mathrel{\star}$ = $\mathrel{\therefore}$,
the substitution $[e/x]e^{\prime}$ behaves differently from the standard
substitution because there occurs a mismatch between what is being substituted
for what. Specifically, when $\mathrel{\star}$ = $\mathrel{\therefore}$, we
are trying to substitute $e$ that is typed irrelevantly (i.e.,
$e\mathrel{\therefore}\varphi$) for a variable $x$ that is typed relevantly
(i.e., $x:\varphi$). Consequently, to account for this mismatch, the
substitution has to be defined inductively on the structure of $e$ not of
$e^{\prime}$ (we base this on Pfenning and Davies (2001)):

$\mathopen{\lsem}e/x\mathclose{\rsem}e^{\prime}=_{df}\begin{cases}[t/x]e^{\prime}&\text{if
}e=t\\\ \textsf{let }\langle y\rangle\textsf{ be }t\textsf{ in
}\mathopen{\lsem}e^{\prime\prime}/x\mathclose{\rsem}e^{\prime}&\text{if
}e=\textsf{let }\langle y\rangle\textsf{ be }t\textsf{ in }e^{\prime\prime}\\\
\textsf{let }\langle y\rangle_{\textrm{j}}\textsf{ be
}e^{\prime\prime\prime}\textsf{ in
}\mathopen{\lsem}e^{\prime\prime}/x\mathclose{\rsem}e^{\prime}&\text{if
}e=\textsf{let }\langle y\rangle_{\textrm{j}}\textsf{ be
}e^{\prime\prime\prime}\textsf{ in }e^{\prime\prime}\\\
\langle\mathopen{\lsem}e^{\prime\prime}/x\mathclose{\rsem}e^{\prime}\rangle&\text{if
}e=\langle e^{\prime\prime}\rangle_{\textrm{j}}\\\
\lambda_{\textrm{j}}x.\mathopen{\lsem}e^{\prime\prime}/x\mathclose{\rsem}e^{\prime}&\text{if
}e=\lambda_{\textrm{j}}x.e^{\prime\prime}\\\
\textsf{ap}_{\textrm{j}}(\mathopen{\lsem}e^{\prime\prime}/x\mathclose{\rsem}e^{\prime},t)&\text{if
}e=\textsf{ap}_{\textrm{j}}(e^{\prime\prime},t)\\\ \end{cases}$

Thus, when expression $e$ is a term $t$,
$\mathopen{\lsem}e/x\mathclose{\rsem}e^{\prime}$ reduces to the standard
substitution $[t/x]e^{\prime}$. Otherwise, i.e., if $e$ is an expression of
any of the specified forms, there is a recursive call of the substitution as
specified by the clauses.

Hence, in practice, we will have the following three substitution rules:

$\Gamma\vdash t:\varphi$ $\Gamma,x:\varphi\vdash t^{\prime}:\gamma$ sub1
($\mathrel{\star}$ = $:$) $\Gamma\vdash[t/x]t^{\prime}:\gamma$

$\Gamma\vdash e\mathrel{\therefore}\varphi$ $\Gamma,x:\varphi\vdash
e^{\prime}\mathrel{\therefore}\gamma$ sub1 ($\mathrel{\star}$ =
$\mathrel{\therefore}$)
$\Gamma\vdash\mathopen{\lsem}e/x\mathclose{\rsem}e^{\prime}\mathrel{\therefore}\gamma$

$\Gamma\vdash t:\varphi$ $\Gamma,x:\varphi\vdash e\mathrel{\therefore}\gamma$
sub2 $\Gamma\vdash[t/x]e\mathrel{\therefore}\gamma$

We can show that the substitution rules sub1 and sub2 are valid using the
following lemma.

######  Lemma 5.

(Substitution lemma)

  1. (sub1) If $\Gamma\vdash e\mathrel{\star}\varphi$ and $\Gamma,x:\varphi\vdash e^{\prime}\mathrel{\star}\gamma$ then $\Gamma\vdash\mathopen{\lsem}e/x\mathclose{\rsem}e^{\prime}\mathrel{\star}\gamma$.

  2. (sub2) If $\Gamma\vdash t:\varphi$ and $\Gamma,x:\varphi\vdash e\mathrel{\therefore}\gamma$ then $\Gamma\vdash[t/x]e\mathrel{\therefore}\gamma$.

###### Proof.

(sub1, $\star$ = $:$) By structural induction on the derivation of
$\Gamma,x:\varphi\vdash t^{\prime}:\gamma$.

###### Proof.

(sub1, $\star$ = $\mathrel{\therefore}$) By structural induction on the
derivation of $\Gamma\vdash e\mathrel{\therefore}\varphi$.

###### Proof.

(sub2) By structural induction on the derivation of $\Gamma,x:\varphi\vdash
e\mathrel{\therefore}\gamma$.

####  3.2.2 Subject reduction

######  Lemma 6.

(Subject reduction) If $\Gamma\vdash e\mathrel{\star}\varphi$ and
$\Gamma\vdash e\Longrightarrow e^{\prime}$ then $\Gamma\vdash
e^{\prime}\mathrel{\star}\varphi$.

###### Proof.

By structural induction on the derivation $\Gamma\vdash e\Longrightarrow
e^{\prime}$ and by inversion on $\Gamma\vdash e\mathrel{\star}\varphi$.

For example, let us consider the case of computation rule for $\triangle$:

$\Gamma,x:\varphi\vdash e\mathrel{\therefore}\gamma$ $\Gamma\vdash
t:\triangle\varphi$ $\triangle$C $\Gamma\vdash\textsf{let }\langle
x\rangle\textsf{ be }\langle e^{\prime}\rangle\textsf{ in
}e\Longrightarrow\mathopen{\lsem}e^{\prime}/x\mathclose{\rsem}e$

where $e=\textsf{let }\langle x\rangle\textsf{ be }\langle
e^{\prime}\rangle\textsf{ in }e\mathrel{\therefore}\varphi$.

  1. 1.

$\Gamma\vdash\textsf{let }\langle x\rangle\textsf{ be }\langle
e^{\prime}\rangle\textsf{ in }e\mathrel{\therefore}\varphi$ (by assumption)

  2. 2.

$\Gamma\vdash\langle e^{\prime}\rangle:\triangle\psi$ and $\Gamma,x:\psi\vdash
e\mathrel{\therefore}\varphi$ (by inversion on 1.)

  3. 3.

$\Gamma\vdash e^{\prime}\mathrel{\therefore}\psi$ (by inversion on 2.)

  4. 4.

$\Gamma\vdash\mathopen{\lsem}e^{\prime}/x\mathclose{\rsem}e\mathrel{\therefore}\varphi$
(by sub1 on 3. and 2.)

####  3.2.3 Normalization

We prove strong normalization, i.e., the property that every reduction of an
expression ends with a value, by Tait’s reducibility method (Tait (1967)),
also known as the method of logical relations (Plotkin (1973)).

First, let us introduce a new form of judgment:

$\Gamma\vdash e\star\varphi\in\mathbf{R}$

This judgment means that in the context $\Gamma$ expression $e$ (which is
typed either relevantly $e:\varphi$ or irrelevantly
$e\mathrel{\therefore}\varphi$) belongs to the set $\mathbf{R}$ of reducible
expressions of type $\varphi$.131313Typically, these sets are regarded as
unary logical relations, i.e., predicates on terms and written as
$\mathbf{R}_{\varphi}(e)$. However, since our system additionally
distinguishes between relevant and irrelevant typing, i.e., between
$t:\varphi$ and $e\mathrel{\therefore}\varphi$, we use this nonstandard
notation to keep the typing information explicit.

The set R, or more precisely, the judgment of the form $\Gamma\vdash
e\mathrel{\star}\varphi\in\mathbf{R}$, is defined for $\triangle\varphi$ and
$\varphi\to\psi$ as follows (recall that
$\varphi\mathrel{\twoheadrightarrow}\psi$ is defined as
$\varphi\to\triangle\psi$):141414Note that the property $\mathbf{R}$ of
reducible expressions is inductively defined over the structure of
$\triangle\varphi$, so it is well-founded.

  * •

$\Gamma\vdash e\mathrel{\star}\triangle\varphi\in\mathbf{R}$ $=_{df}$
$\Gamma\vdash e\mathrel{\star}\triangle\varphi$ and $\Gamma\vdash
e\Longrightarrow\langle a\rangle$ for some proof term $a$ such that
$\Gamma\vdash a:\varphi\in\mathbf{R}$. In a rule form:

$\Gamma\vdash e\mathrel{\star}\triangle\varphi$ $\Gamma\vdash
e\Longrightarrow\langle a\rangle$ $\Gamma\vdash a:\varphi\in\mathbf{R}$
$\Gamma\vdash e\mathrel{\star}\triangle\varphi\in\mathbf{R}$

  * •

$\Gamma\vdash e\mathrel{\star}\varphi\to\psi\in\mathbf{R}$ $=_{df}$
$\Gamma\vdash e\mathrel{\star}\varphi\to\psi$ and $\Gamma\vdash
e\Longrightarrow\lambda x.t$ and there exists a term $t$ such that for all
$a$, $\Gamma\vdash a:\varphi\in\mathbf{R}$ implies
$\Gamma\vdash\textsf{ap}(t,a)\mathrel{\star}\psi\in\mathbf{R}$. In a rule
form:

$\Gamma\vdash e\mathrel{\star}\varphi\to\psi$ $\Gamma\vdash
e\Longrightarrow\lambda x.t$ $\Gamma,x:\varphi\vdash t\mathrel{\star}\psi$
$\Gamma\vdash e\mathrel{\star}\varphi\to\psi\in\mathbf{R}$

with the additional condition on term $t$ as above.

The proof of the normalization proceeds in two steps. First, we show that if
expression $e$ (typed either relevantly or irrelevantly to $\varphi$) has the
property R in context $\Gamma$, then the reduction of $e$ terminates, i.e.,
ends with a value (Lemma 7). Then, we show that if we substitute for the free
variables of $e$ terms that have the property R, then the result will have the
property R as well (Lemma 8).

######  Lemma 7.

(Existence of value) If $\Gamma\vdash e\mathrel{\star}\varphi\in\mathbf{R}$,
then $\Gamma\vdash v\mathrel{\therefore}\varphi$, i.e., there exists a
canonical proof expression, i.e., value $v$ of the type $\varphi$, such that
$\Gamma\vdash e\Longrightarrow v$.

###### Proof.

Follows from the definition of judgments of the form $\Gamma\vdash
e\mathrel{\star}\varphi\in\mathbf{R}$.

######  Lemma 8.

(Fundamental lemma) If $\Gamma\vdash
e(x_{1},\ldots,x_{n})\mathrel{\star}\varphi$, where
$\Gamma=x_{1}:\gamma_{1},\ldots,x_{n}:\gamma_{n}$, and $t_{1},\ldots,t_{n}$
are terms such that $\Gamma\vdash t_{i}:\gamma_{i}\in\mathbf{R}$, $0<i\leq n$,
then $\Gamma\vdash e(t_{1},\ldots,t_{n})\mathrel{\star}\varphi\in\mathbf{R}$.

where $\mathrel{\star}$ stands for either “$:$” or “$\mathrel{\therefore}$”
symbol (all occurencens must be consistent; also, recall that all terms $t$
are expressions $e$ but not vice versa).

###### Proof.

By structural induction on the derivation $\Gamma\vdash
e(x_{1},\ldots,x_{n})\star\varphi$ (with the help of preservation and backward
preservation lemmas, see below).

For example:

Case $\triangle$I (where $\mathrel{\star}$ = $:$):

$\Gamma\vdash e(x_{1},\ldots,x_{n})\mathrel{\therefore}\varphi$ $\triangle$I
$\Gamma\vdash\langle e(x_{1},\ldots,x_{n})\rangle:\triangle\varphi$

  1. 1.

$\Gamma\vdash
t_{1}:\gamma_{1}\in\mathbf{R},\ldots,t_{n}:\gamma_{n}\in\mathbf{R}$ (by
assumption)

  2. 2.

$\Gamma\vdash e(t_{1},\ldots,t_{n})\mathrel{\therefore}\varphi\in\mathbf{R}$
(by IH)

  3. 3.

$\Gamma\vdash\langle
e(t_{1},\ldots,t_{n})\rangle:\triangle\varphi\in\mathbf{R}$ (by def. of
$t:\triangle\varphi\in\mathbf{R}$)

Case $\triangle$E (where $\star$ = $:$):

$\Gamma\vdash t(x_{1},\ldots,x_{n}):\triangle\varphi$ $\Gamma,x:\varphi\vdash
e(x_{1},\ldots,x_{n},x)\mathrel{\therefore}\gamma$ $\triangle$E
$\Gamma\vdash\textsf{let }\langle x\rangle\textsf{ be
}t(x_{1},\ldots,x_{n})\textsf{ in
}e(x_{1},\ldots,x_{n})\mathrel{\therefore}\gamma$

  1. 1.

$\Gamma\vdash t(t_{1},\ldots,t_{n}):\triangle\varphi\in\mathbf{R}$ (by IH)

  2. 2.

$\Gamma\vdash e(t_{1},\ldots,t_{n},x)\mathrel{\therefore}\gamma\in\mathbf{R}$
for all $x$ such that $\Gamma\vdash x:\varphi\in\mathbf{R}$ (by IH)

  3. 3.

$\Gamma\vdash t(t_{1},\ldots,t_{n})\Longrightarrow\langle
a\rangle:\triangle\varphi$ for some $a$ such that $\Gamma\vdash
a:\varphi\in\mathbf{R}$ (by def. of $t:\triangle\varphi\in\mathbf{R}$ from 1.)

  4. 4.

$\Gamma\vdash\textsf{let }\langle x\rangle\textsf{ be }\langle
a\rangle\textsf{ in
}e(t_{1},\ldots,t_{n},x)\Longrightarrow\mathopen{\lsem}a/x\mathclose{\rsem}e(t_{1},\ldots,t_{n},x)$
(by def. of let)

  5. 5.

$\Gamma\vdash\textsf{let }\langle x\rangle\textsf{ be }\langle
a\rangle\textsf{ in }e(t_{1},\ldots,t_{n},x)\Longrightarrow
e(t_{1},\ldots,t_{n},a)$ (by def. of sub1 on 4.)

  6. 6.

$\Gamma\vdash e(t_{1},\ldots,t_{n},a)\mathrel{\therefore}\gamma\in\mathbf{R}$
(by IH from 2. and 3.)

  7. 7.

$\Gamma\vdash\textsf{let }\langle x\rangle\textsf{ be
}t(t_{1},\ldots,t_{n})\textsf{ in
}e(t_{1},\ldots,t_{n})\mathrel{\therefore}\gamma\in\mathbf{R}$ (by 3., 4, 5.,
and backward preservation lemma)

Case $\to$Ij (i.e., $\to$I$\mathrel{\star}$ where $\mathrel{\star}$ =
$\mathrel{\therefore}$):

$\Gamma,x:\varphi\vdash e(x_{1},\ldots,x_{n},x)\mathrel{\therefore}\psi$
$\to$Ij
$\Gamma\vdash\lambda_{\textrm{j}}x.e(x_{1},\ldots,x_{n},x)\mathrel{\therefore}\varphi\to\psi$

  1. 1.

$\Gamma\vdash
t_{1}:\gamma_{1}\in\mathbf{R},\ldots,t_{n}:\gamma_{n}\in\mathbf{R}$ (by
assumption)

  2. 2.

$\Gamma\vdash e(t_{1},\ldots,t_{n},x)\mathrel{\therefore}\psi\in\mathbf{R}$
for all $x$ such that $\Gamma\vdash x:\varphi\in\mathbf{R}$. (by IH)

  3. 3.

$\Gamma\vdash a:\varphi\in\mathbf{R}$ for some arbitrary $a$ (by assumption)

  4. 4.

$\Gamma\vdash a\Longrightarrow v$ for some $v$ (by def. of $\mathbf{R}$ from
3.)

  5. 5.

$\Gamma\vdash v:\varphi\in\mathbf{R}$ (by preservation lemma on 4.)

  6. 6.

$\Gamma\vdash e(t_{1},\ldots,t_{n},v)\mathrel{\therefore}\psi\in\mathbf{R}$
(by IH from 2. and 5.)

  7. 7.

$\Gamma\vdash\textsf{ap}_{\textrm{j}}(\lambda_{\textrm{j}}x.e(t_{1},\ldots,t_{n},x),v)\Longrightarrow
e(t_{1},\ldots,t_{n},v)$ (by def. of $\to$Cj)

  8. 8.

$\Gamma\vdash\textsf{ap}_{\textrm{j}}(\lambda_{\textrm{j}}x.e(t_{1},\ldots,t_{n},x),v)\mathrel{\therefore}\psi\in\mathbf{R}$
(by backward preservation lemma from 7.)

  9. 9.

$\Gamma\vdash\lambda_{\textrm{j}}x.e(t_{1},\ldots,t_{n},x)\mathrel{\therefore}\varphi\to\psi\in\mathbf{R}$
(by def. of $\varphi\to\psi\in\mathbf{R}$ from 8. since $a$ was chosen
arbitrarily)

Case $\to$Ej (i.e., $\to$E$\mathrel{\star}$ where $\mathrel{\star}$ =
$\mathrel{\therefore}$):

$\Gamma\vdash e(x_{1},\ldots,x_{n})\mathrel{\therefore}\varphi\to\psi$
$\Gamma\vdash t(x_{1},\ldots,x_{n}):\varphi$ $\to$Ej
$\Gamma\vdash\textsf{ap}_{\textrm{j}}(e(x_{1},\ldots,x_{n}),t(x_{1},\ldots,x_{n}))\mathrel{\therefore}\psi$

  1. 1.

$\Gamma\vdash
e(t_{1},\ldots,t_{n})\mathrel{\therefore}\varphi\to\psi\in\mathbf{R}$ (by IH)

  2. 2.

$\Gamma\vdash t(t_{1},\ldots,t_{n}):\varphi\in\mathbf{R}$ (by IH)

  3. 3.

$\Gamma\vdash\textsf{ap}_{\textrm{j}}(e(t_{1},\ldots,t_{n}),t(t_{1},\ldots,t_{n}))\mathrel{\therefore}\psi\in\mathbf{R}$
(by def. of $e\mathrel{\star}\varphi\to\psi\in\mathbf{R}$ on 1., specifically
we use the additional condition instantiated with 2.)

######  Theorem 1.

(Strong normalization) If $\Gamma\vdash e\mathrel{\star}\varphi$, then
$\Gamma\vdash e\Longrightarrow v$.

###### Proof.

Follows from Lemmas 7 and 8. By choosing the context to be empty, i.e., by
taking the expression $e$ to be closed (with no free variables), we obtain
that $e$ is normalizable whenever $\vdash e\mathrel{\star}\varphi$.

######  Lemma 9.

(Backward preservation) If $\Gamma\vdash
e^{\prime}\mathrel{\star}\varphi\in\mathbf{R}$ and $\Gamma\vdash
e\Longrightarrow e^{\prime}$ then $\Gamma\vdash
e\mathrel{\star}\varphi\in\mathbf{R}$.

###### Proof.

By induction on the judgment $\Gamma\vdash e\Longrightarrow e^{\prime}$.

For example:

Case let:

$\Gamma,x:\varphi\vdash e_{2}\mathrel{\therefore}\gamma$ $\Gamma\vdash
t:\triangle\varphi$ $\triangle$C $\Gamma\vdash\textsf{let }\langle
x\rangle\textsf{ be }\langle e_{1}\rangle\textsf{ in
}e_{2}\Longrightarrow\mathopen{\lsem}e_{1}/x\mathclose{\rsem}e_{2}$

Let $e=\textsf{let }\langle x\rangle\textsf{ be }\langle e_{1}\rangle\textsf{
in }e_{2}$ and $e^{\prime}=\mathopen{\lsem}e_{1}/x\mathclose{\rsem}e_{2}$.

  1. 1.

$\Gamma\vdash\textsf{let }\langle x\rangle\textsf{ be }\langle
e_{1}\rangle\textsf{ in
}e_{2}\Longrightarrow\mathopen{\lsem}e_{1}/x\mathclose{\rsem}e_{2}$ (by
assumption)

  2. 2.

$\Gamma\vdash\mathopen{\lsem}e_{1}/x\mathclose{\rsem}e_{2}\mathrel{\star}\varphi\in\mathbf{R}$
(by assumption)

Now, in general, to be able to claim that $\Gamma\vdash
e\mathrel{\star}\varphi\in\mathbf{R}$, i.e., that $e$ is reducible, we have to
show that all possible reductions of $e$ result in terms that are also
reducible. In other words, we need to show that to whatever $e^{\prime\prime}$
the $e$ reduces, it has the $\mathbf{R}$ property. So, let us assume:

  1. 3.

$\textsf{let }\langle x\rangle\textsf{ be }\langle e_{1}\rangle\textsf{ in
}e_{2}\Longrightarrow e^{\prime\prime}$ (by assumption)

Since let has only one reduction rule, i.e., $\textsf{let }\langle
x\rangle\textsf{ be }\langle e_{1}\rangle\textsf{ in
}e_{2}\Longrightarrow\mathopen{\lsem}e_{1}/x\mathclose{\rsem}e_{2}$, it means
that
$e^{\prime\prime}=e^{\prime}=\mathopen{\lsem}e_{1}/x\mathclose{\rsem}e_{2}$.
And, by assumption 2, we know that
$\mathopen{\lsem}e_{1}/x\mathclose{\rsem}e_{2}\mathrel{\star}\varphi\in\mathbf{R}$.
Thus, we can conclude that:

  1. 4.

$\Gamma\vdash\textsf{let }\langle x\rangle\textsf{ be }\langle
e_{1}\rangle\textsf{ in }e_{2}\mathrel{\star}\varphi\in\mathbf{R}$

######  Lemma 10.

(Preservation) If $\Gamma\vdash e\mathrel{\star}\varphi\in\mathbf{R}$ and
$\Gamma\vdash e\Longrightarrow e^{\prime}$ then $\Gamma\vdash
e^{\prime}\mathrel{\star}\varphi\in\mathbf{R}$.

###### Proof.

By induction on the structure of the type $\varphi$.

For example:

Case $\varphi=\triangle\varphi$:

  1. 1.

$\Gamma\vdash e:\triangle\varphi\in\mathbf{R}$ (by assumption)

  2. 2.

$\Gamma\vdash e\Longrightarrow\langle a\rangle$ for some $\Gamma\vdash
a:\varphi\in\mathbf{R}$ (by def. of $\triangle\varphi\in\mathbf{R}$ from 1.)

  3. 3.

$\Gamma\vdash a\Longrightarrow v$ (by def. of $\mathbf{R}$ from 2.)

  4. 4.

$\Gamma\vdash v:\varphi\in\mathbf{R}$ (by IH from 2. and 3.)

  5. 5.

$\Gamma\vdash e^{\prime}:\triangle\varphi\in\mathbf{R}$ (by def. of
$\triangle\varphi\in\mathbf{R}$ from 4.)

Case $\varphi=\varphi\to\psi$:

  1. 1.

$\Gamma\vdash t:\varphi\to\gamma\in\mathbf{R}$ (by assumption)

  2. 2.

$\Gamma\vdash t\Longrightarrow t^{\prime}$ (by assumption)

  3. 3.

$\Gamma\vdash a:\varphi\in\mathbf{R}$ for some arbitrary $a$ (by assumption)

  4. 4.

$\Gamma\vdash\textsf{ap}(t,a):\psi\in\mathbf{R}$ (by def. of
$\varphi\to\psi\in\mathbf{R}$ from 1. and 3.)

  5. 5.

$\Gamma\vdash\textsf{ap}(t,a)\Longrightarrow\textsf{ap}(t^{\prime},a)$ (by apC
from 2. and 4.)

  6. 6.

$\Gamma\vdash\textsf{ap}(t^{\prime},a):\psi\in\mathbf{R}$ (by IH on 4. and 5.)

  7. 7.

$\Gamma\vdash t^{\prime}:\varphi\to\gamma\in\mathbf{R}$ (by def. of
$\varphi\to\psi\in\mathbf{R}$ from 6., since it holds for arbitrary $a$)

##  4 Truncation

Truncation, or more specifically, propositional truncation, is a fundamental
concept in many type theories, most notably in homotopy type theory (HoTT),
for obtaining controlled propositional proof irrelevance in otherwise proof-
relevant frameworks. It is commonly treated as a modality $\Box$ (see, e.g.,
UFP (2013), Awodey and Bauer (2004), Kraus (2015), Corfield (2020), Rijke
(2022)) that allows us to turn an arbitrary type $\varphi$ into a type
$\Box\varphi$ of mere propositions, i.e., propositions for which all proofs
are considered equal. In other words, truncation hides all the specific
information about proofs of a particular proposition except for their
existence. Thus, $\Box\varphi$ represents the proposition that $\varphi$ is
just true, i.e., that there exists a proof for it without revealing any more
information about it. Or, to use type-theoretic terminology, it represents a
proposition that $\varphi$ is inhabited while keeping the inhabitants
anonymous.

###  4.1 An example

How do we use truncation in practice? Let us consider an example originally
presented by de Bruijn to highlight the distinctions between proof relevance
and proof irrelevance:

> the logarithm of a real number is defined for positive numbers only. So
> actually [from the view of constructive proof-relevant reasoning] the log is
> a function of two variables; and if we use the expression
> $\textsf{log}(p,q)$, we have to check that $p$ is a real number and $q$ is a
> proof for the proposition “$p>0$”. (de Bruijn (1974), reprinted in de Bruijn
> (1994), p. 286)

So, the type of this common logarithm function log would be:

$\textsf{log}:(\forall x:\mathbb{R})\,\textsf{isPositive}(x)\to\mathbb{R}$

However, when using the log function, we typically are not concerned with the
specific proofs demonstrating the positivity of its arguments, i.e., that
$\textsf{isPositive}(x)$ holds of them, we just care about the values of the
function. Or to put it differently, we would not want log returning different
values for the same argument $p$ just because its proofs of positivity might
have been different. The straightforward way to express this with truncation
is to simply truncate the corresponding type $\textsf{isPositive}(x)$, and
thus obtain a new function $\textsf{log}_{\Box}$ with slightly tweaked
type:151515This option was, of course, not yet available to de Bruijn in the
70s, as the idea of truncation first appears in the 80s as far as we know
(see, e.g., Constable et al. (1986)).

$\textsf{log}_{\Box}:(\forall
x:\mathbb{R})\,\Box(\textsf{isPositive}(x))\to\mathbb{R}$

Now, what the truncation gives us is that while $\textsf{log}(p,q_{1})$ might
not be necessarily equal to $\textsf{log}(p,q_{2})$ since the proofs $q_{1}$
and $q_{2}$ of $\textsf{isPositive}(x)$ might be different,
$\textsf{log}_{\Box}(p,q_{1})$ will be equal $\textsf{log}_{\Box}(p,q_{1})$ no
matter what $q_{1}$ and $q_{2}$ we choose as the function
$\textsf{log}_{\Box}$ does not care about their inner structure only about
their existence. In other words, the function $\textsf{log}_{\Box}$ would
return the same values for the same argument $p$ no matter what its proofs of
positivity might look like.

It is important to emphasize, however, that truncation is not just a technical
tool for simplification as the example above might suggest. It can greatly
extend the capabilities of the underlying type-theoretic systems (e.g., it
allows us to define subsets and properly formulate the axiom of choice, see,
e.g., UFP (2013)) but, most importantly, it sheds new light on the notions of
truth, existence, and proof in a constructive setting. Specifically, it can
help us conceptualize the distinction between the existence of proof and the
structure of the proof, and thus ultimately its constructive content, a
distinction that is often blurred in classical, i.e. non-constructive setting,
if present at all. Most importantly, by acknowledging the existence of a proof
without committing to any specific construction of it, truncation provides a
bridge to classical reasoning. Specifically, with the help of truncation, we
can recapture classical reasoning within an otherwise constructive setting.
For example, the law of excluded middle can be applied to truncated
propositions since they represent just simple truths without additional
information, constructive content, or structure. In other words, analogously
to a classical proposition, which is either true or false, for a truncated
proposition there either exists a proof for it (= it is inhabited) or it does
not (= it is empty), there is nothing in between.161616The general need for
truncation, or proof irrelevance in general, also indicates that identifying
propositions and types, according to the famous dicto “propositions as types”,
might be simply too heavy-handed from some perspectives and that a more
careful and discerning approach should be chosen.

Finally, note that in the above explanation of truncation $\Box$, the notion
of proof existence was repeatedly used. However, this was always done at the
metalevel, never directly at the object level. This approach is not unique to
our explanation. For example, for Kraus “$\Box\varphi$ [in HoTT] intuitively
represent[s] the statement that $\varphi$ is inhabited” (Kraus (2015) p. 36)
where “$\varphi$ is inhabited” is just a different way of saying that “there
exists a proof/construction of $\varphi$”. But HoTT contains no object-level
judgment corresponding to the statement “$\varphi$ is inhabited”, it always
appears only as a metalevel informal judgment.171717Later we will see that
this causes some inconsistencies with their intended interpretation of the
truncation introduction rule (see also Section 5). We only get the
propositional approximation of the form $\Box\varphi$.

###  4.2 Truncation and existence

Now, let us explore the link between the truncation modality $\Box$ and the
existence modality $\triangle$. In HoTT, propositional truncation is defined
via the following three clauses (UFP (2013), Sec. 3.7, see also Kraus (2015),
Def. 232):

  1. (a)

for any $t:\varphi$ we have $|\,t\,|:\Box\varphi$

  2. (b)

if $\psi$ is a mere proposition and we have $f:\varphi\to\psi$, then we have
$g:\Box\varphi\to\psi$

  3. (c)

$\Box\varphi$ is a mere proposition

First, note that clause (a) can be regarded as truncation introduction rule
and (b) as truncation elimination rule (with added context $\Gamma$):

$\Gamma\vdash t:\varphi$ $\Gamma\vdash|\,t\,|:\Box\varphi$ $\Gamma\vdash
f:\varphi\to\psi$ $\Gamma\vdash g:\Box\varphi\to\psi$

Now, we will show that our system’s direct notational correlates of these
rules, that is:181818The symbol “$\Box$” is replaced with “$\triangle$” and in
(a) “$|\,t\,|$” is replaced with “$\langle t\rangle$” and in (b) “$:$” is
replaced with “$\mathrel{\therefore}$” (due to the (b)’s prerequisite that
$\psi$ is a mere proposition, we explain this change later when discussing
(c)).

$\Gamma\vdash t:\varphi$ $\Gamma\vdash\langle t\rangle:\triangle\varphi$
$\Gamma\vdash f\mathrel{\therefore}\varphi\to\psi$ $\Gamma\vdash
g\mathrel{\therefore}\triangle\varphi\to\psi$

are actually derivable rules. In other words, the I/E rules for truncation
modality can be derived from the I/E rules for existence modality, thus
showing that truncation $\Box$ can be reduced to existence $\triangle$. Below
we will see that even a judgment corresponding to clause (c) can be
established in our system.

Let us start with (a). In our system, we can derive the corresponding rule
simply as follows:

$\Gamma\vdash t:\varphi$ just $\Gamma\vdash t\mathrel{\therefore}\varphi$
$\triangle$I $\Gamma\vdash\langle t\rangle:\triangle\varphi$

The rule corresponding to (b) can be derived in the following way:191919Note
that the requirement from (b) that $\psi$ has to be a mere proposition
corresponds to the fact that $\psi$ has to be a just true proposition as
evidenced by the judgment
$\ldots\vdash\textsf{ap}(f,x)\mathrel{\therefore}\psi$.

hyp $\Gamma,y:\triangle\varphi\vdash y:\triangle\varphi$ $\Gamma\vdash
f\mathrel{\therefore}\varphi\to\psi$ w $\Gamma,x:\varphi\vdash
f\mathrel{\therefore}\varphi\to\psi$ hyp $\Gamma,x:\varphi\vdash x:\varphi$
$\to$Ej
$\Gamma,x:\varphi\vdash\textsf{ap}_{\textrm{j}}(f,x)\mathrel{\therefore}\psi$
w
$\Gamma,x:\varphi,y:\triangle\varphi\vdash\textsf{ap}_{\textrm{j}}(f,x)\mathrel{\therefore}\psi$
ex
$\Gamma,y:\triangle\varphi,x:\varphi\vdash\textsf{ap}_{\textrm{j}}(f,x)\mathrel{\therefore}\psi$
$\triangle$E $\Gamma,y:\triangle\varphi\vdash\textsf{let }\langle
x\rangle\textsf{ be }y\textsf{ in
}\textsf{ap}_{\textrm{j}}(f,x)\mathrel{\therefore}\psi$ $\to$Ij
$\Gamma\vdash\lambda_{\textrm{j}}y.\textsf{let }\langle x\rangle\textsf{ be
}y\textsf{ in
}\textsf{ap}_{\textrm{j}}(f,x)\mathrel{\therefore}\triangle\varphi\to\psi$

where $g=\lambda_{\textrm{j}}y.\textsf{let }\langle x\rangle\textsf{ be
}y\textsf{ in }\textsf{ap}_{\textrm{j}}(f,x)$.

Note. Consider the provided informal explanation for clause (a) in UFP (2013):

> “The first constructor means that if $\varphi$ is inhabited, so is
> $\Box\varphi$.” (UFP (2013), p. 117)

But note that this is not a precise interpretation: the meaning explanation of
the constructor/introduction rule for truncation does not fit the rule itself
(observe, however, that it fits exactly our introduction rule for existence
$\triangle$I). More specifically, the actual premise of the constructor does
not say merely that “$\varphi$ is inhabited”, i.e., that there exists a proof
of it, but there is a stronger claim saying that we actually have a concrete
proof for $\varphi$, i.e., “$t:\varphi$”. In other words, “$\varphi$ is
inhabited” (= there exists a proof for it) is a different judgment from
“$t:\varphi$” (= we have a proof $t$ for it).202020Note that this is exactly
the “common mistake which intuitionists are particularly prone to” observed by
Martin-Löf (1993) (p. 141), namely, saying that $\varphi\textit{ exists}$
means that an object of type $\varphi$ has been found. In other words, to
borrow Martin-Löf’s terminology, the mistake lies in conflating bare existence
and actual existence.

Of course, it is easy to diagnose why this imprecise explanation occurs: it is
because HoTT has no object-level equivalent of the metalevel judgment
“$\varphi$ is inhabited”. In our system, however, we have an appropriate
judgment to capture this: $\varphi\textit{ just true}$ or the typed variant
$t\mathrel{\therefore}\varphi$.212121Of course, purely syntactically, the term
$t$ is still retrievable from $\langle t\rangle$, however, it is no longer
accessible from within the system, i.e., we cannot inspect it by, e.g.,
running case distinction on it, etc. For all computational/constructive
intents and purposes, it is a (non-empty) black box.

Now, let us finally take a closer look at the last clause:

  * (c)

$\Box\varphi$ is a mere proposition.

where a mere proposition is a proposition for which all proofs are equal. As
hinted earlier, the requirement that $\Box\varphi$ is a mere proposition
corresponds in our system to the requirement that $\Box\varphi$ is a just true
proposition, i.e., $\Gamma\vdash e\mathrel{\therefore}\Box\varphi$. The reason
for this is that from the perspective of mere propositions, our judgment
$e\mathrel{\therefore}\varphi$ (as well as $\varphi\textit{ just true}$) plays
double duty. Specifically, it captures two facts about $\varphi$ at the same
time: that $\varphi$ is true and that $\varphi$ is also a “mere proposition”
since it is not only true but specifically just true and all just true
propositions can be shown to be mere propositions. Informally, since $\varphi$
is a just true proposition, it means there exists some proof for it (according
to initial definition (2)), let us call it $e$. Now, let us assume there
exists another proof for $\varphi$ called $e^{\prime}$. So, we only know that
proofs $e$ and $e^{\prime}$ of $\varphi$ exist but we have no means of
distinguishing between them since we do not know their structure. But having
no means of distinguishing between them is just another way of saying that
they are effectively equal, which is what we wanted to show.222222As a
concrete example of this double duty, in our system we can show that
$\Gamma\vdash\varphi\leftrightarrow\triangle\varphi\textit{ just true}$, i.e.,
that both $\Gamma\vdash\varphi\to\triangle\varphi\textit{ just true}$ and
$\Gamma\vdash\triangle\varphi\to\varphi\textit{ just true}$. This essentially
corresponds to the HoTT Lemma 3.9.1 (UFP (2013), p. 120) stating that if
$\varphi$ is a mere proposition, then $\varphi$ and $\Box\varphi$ are
(homotopy) equivalent. Thus, saying that $\varphi$ is a just true proposition,
i.e., that there exists a proof of $\varphi$, formally, $\Gamma\vdash
e\mathrel{\therefore}\varphi$, entails that $\varphi$ is a mere proposition.

It is worth noting that the axiomatic stipulation (c) often comes in a rule
form explicitly utilizing (propositional) identity:232323Judgmental identity
can be used as well, then leading to judgmental proof irrelevance, but as
mentioned earlier, in this paper we focus only on the propositional proof
irrelevance.

$\Gamma\vdash t:\Box\varphi$ $\Gamma\vdash t^{\prime}:\Box\varphi$
$\Gamma\vdash t=t^{\prime}$

which states that any two terms $t$ and $t^{\prime}$ of type $\Box\varphi$ are
propositionally equal (in other words, this rule effectively stipulates that
$\Box\varphi$ is a proof-irrelevant type).

However, since we do not currently have judgments of the form $\Gamma\vdash
e=e^{\prime}$, i.e., we do not have propositional identity amongst our logical
constant, there is no direct correlate in our present system for the rule
variant of the stipulation. For now, we just say that if we were to extend our
system with propositional identity (i.e., introduce $e=e^{\prime}$ as a new
type of a proposition together with its corresponding introduction rules,
elimination rules, etc.), our correlate of the rule above, i.e.,

$\Gamma\vdash e\mathrel{\therefore}\varphi$ $\Gamma\vdash
e^{\prime}\mathrel{\therefore}\varphi$ $\Gamma\vdash e=e^{\prime}$

would not need to be added as an extra stipulation but could be actually
derived just as the truncation I/E rules corresponding to clauses (a) and (b)
since, as discussed above, any two proofs of _just true_ propositions are
naturally indistinguishable. Further exploration of the notion of a mere
proposition from the perspective of logic of judgemental existence would be
interesting but it is beyond the scope of the present paper.

##  5 Related work

###  5.1 General remarks

The investigation of judgmental existence is directly motivated by Martin-Löf
(1993) who informally considers a new judgment of the form $\varphi\textit{
exists}$ as expressing the notion of “bare existence” (or perhaps more
fittingly, “mere existence”). This notion is explained via the following rule:

$a:\varphi$ $\varphi\textit{ exists}$

or, if $\varphi$ is assumed to be a proposition:242424Nordström et al. (1990)
also consider this rule as the “Proposition as set” rule: “If we have an
element in a set, then we will interpret that set as a true proposition.” (p.
37)

$a:\varphi$ $\varphi\textit{ true}$

That is, $\varphi\textit{ exists }$ has the same meaning as $\varphi\textit{
true}$ if $\varphi$ is a proposition (Martin-Löf (1993), p. 140). To our
knowledge, however, he does not ever adopt judgments of the form
$\varphi\textit{ exists}$ into a particular type-theoretic system (only in the
form of the “abbreviation” judgment $\varphi\textit{ true}$ in Martin-Löf
(1984), which will be discussed below), nor does he consider its
internalization into a propositional level via a modality.252525We want to
emphasize that our intention is not to reconstruct Martin-Löf’s notion of bare
existence or to reduce it into our notion of just truth (i.e., proof
existence), we only take it as a source of inspiration.

In the computational variant of our system, the rule above corresponds to the
following rule:

$\Gamma\vdash a:\varphi$ just $\Gamma\vdash a\mathrel{\therefore}\varphi$

only instead of syntactically hiding the proof expression $a$ we render it
“invisible” via the proof-irrelevant typing $\mathrel{\therefore}$. That is,
instead of $\varphi\textit{ exists}$ we use the more explicit variant
$a\mathrel{\therefore}\varphi$. In the logical variant of our system, it would
correspond to the rule:

$\Gamma\vdash\varphi\textit{ true}$ just $\Gamma\vdash\varphi\textit{ just
true}$

where true captures the proof-relevant notion of truth, and just true the
proof-irrelevant one (recall Section 1).

As mentioned above, in Martin-Löf’s constructive type theory (CTT) (Martin-Löf
(1984)) we can encounter judgments of the form $\varphi\textit{ true}$ which
more or less correspond to our judgments of the form $\varphi\textit{ just
true}$ from the pure logical variant of our system. However, the judgments of
the form $\varphi\textit{ true}$ from Martin-Löf (1984) do not seem to be
fully incorporated into the system itself. For example, they are missing from
the initial specification of the basic judgments of the system and the
substitution rules make no use of them. This, of course, makes sense if we
regard $\varphi\textit{ true}$ just as an abbreviation of the basic judgment
$a:\varphi$ which, going by the textual evidence alone, seems to be what
Martin-Löf intented (see Martin-Löf (1984), p. 33; see also Nordström et al.
(1990), p. 25). However, this explanation of the judgment $\varphi\textit{
true}$ is somewhat inconsistent with the one provided in Martin-Löf (1993).
There $\varphi\textit{ true}$ is regarded as having the same meaning as the
judgment $\varphi\textit{ exists}$ which is treated as a basic form of a
judgment.262626As pointed out by Ansten Klev in personal communication,
$\varphi\textit{ exists}$ does not seem to be an abbreviation in any
reasonable sense and has to be really understood as a basic form of judgment.
We can contrast this, e.g., with the judgment of the form $\varphi\textit{
false}$, where $\varphi$ is a proposition. Constructively, we can define it as
$\varphi\textit{ false}=_{df}\neg\varphi\textit{ true}$ and unlike the meaning
explanation of judgment $\varphi\textit{ exists}$ provided in Martin-Löf
(1993) this has the form of an explicit definition. Assuming $\varphi$ is a
proposition, this would then mean that all judgments $\varphi\textit{ true}$,
$\varphi\textit{ exists}$, and $a:\varphi$ have the same meaning, which cannot
be correct.

Note that our proof-relevant judgment $\varphi\textit{ true}$ is essentially
just an abbreviation or coding of $a:\varphi$ with no information lost: from
$\varphi\textit{ true}$ we should still be able, at least in principle, obtain
back the information about the proof $a$ of $\varphi$. This is, however, not
the case for proof-irrelevant judgment $\varphi\textit{ just true}$ where the
information about $a$ is forgotten and cannot be obtained back. From this
perspective, an interesting middle ground was explored by Valentini (1998) who
proposed a system for “soft forgetting”: he works with judgments
$\varphi\textit{ true}$ which are interpreted similarly to our
$\varphi\textit{ just true}$272727“The meaning of $\varphi\textit{ true}$ is
that there exists an element $t$ such that $t:\varphi$ but it does not matter
which particular element $t$ is” (Valentini (1998), p. 275) or “$\varphi$ is
inhabited” (Valentini (1998), p. 278) but the system he devises allows us to
get not only from $a:\varphi$ to $\varphi\textit{ true}$ but also from
$\varphi\textit{ true}$ back to $a:\varphi$.

Our proof-irrelevant judgment $\varphi\textit{ just true}$ is also related to
the similar judgment “$\varphi$ is inhabited” from Homotopy Type Theory (HoTT,
UFP (2013)). However, we should be careful about conflating these two: in our
system, the metalevel judgment “there exists a proof of $\varphi$” has a
direct object level correlate in the form of the judgment $\varphi\textit{
just true}$, however, in HoTT the metalevel judgment “$\varphi$ is inhabited”
has no such object level correlate in the form of a judgment.282828From this
perspective, it should be evident that our logic of judgmental existence could
be also considered as a logic of judgmental inhabitance just by interpreting
$\varphi\textit{ just true}$ as “$\varphi$ is inhabited” instead of “there
exists a proof of $\varphi$”.

The notion of existential judgment as such is, of course, much older and can
be found in the literature under different names, e.g., “incomplete
communication” (unvollständige Mitteilung) or “partial judgment”
(Partialurteil) (Hilbert and Bernays (1968), Kleene (1945)) or “judgment
abstract” (Urteilsabstrakt) (Weyl (1921a), English translation in Mancosu
(1998)). In contrast to Weil, however, our existential judgments are
considered as proper judgments that describe existential state of affairs
which are not regarded just as “an empty invention of logicians” (Weyl
(1921b), p. 97).292929Although, as Van Dalen (1995) points out, Weyl’s use of
the term “judgment” is not in complete agreement with our present-day use of
the term.

Concerning the relation of our system to other proof-irrelevant ones, Pfenning
(2001), Reed (2002), Abel and Scherer (2012) work with a judgment of the form
$a\div\varphi$ that roughly corresponds to our $a\mathrel{\therefore}\varphi$,
however, their judgment $a\div\varphi$ itself is not a basic judgment of the
system in contrast to our $a\mathrel{\therefore}\varphi$. For them, it is a
notational abbreviation for a judgment $a:\varphi$ made under “irrelevant”
just true assumptions of the form $x\div\varphi$ which, on the other hand, we
do not consider. Yet, similar to Pfenning (2001), we have a two-step
truncation: $\langle a\rangle:\triangle\varphi$ cannot be derived directly
from $a:\varphi$, we need the “pretruncation” middle step
$a\mathrel{\therefore}\varphi$. This is in contrast to Awodey and Bauer
(2004), UFP (2013), Kraus (2015). Furthermore, unlike Hofmann’s approach
(Hofmann (1995), Proposition 5.3.12), the truncation/existence modality
$\triangle$ is derived directly from the judgment level (similarly to Pfenning
(2001)) without the need to invoke propositional identity type.

###  5.2 Relation to Pfenning and Davies’s lax logic

Our calculus of judgmental existence is directly inspired by Pfenning and
Davies (2001) system of judgmental reconstruction of modal logic,303030The
fact that our logic for judgments of the general form “$\varphi$ is just true”
is similar to the logic for judgments of the general form “$\varphi$ is
possible” can be made clearer if we consider the following Martin-Löf’s
observation: “The important point to observe here is the change from is in $A$
is true to can in $A$ can be verified, or $A$ is verifiable. Thus what is
expressed in terms of being in the first formulation really has the modal
character of possibility” (Martin-Löf (1996), p. 25). which is in turn
inspired by Martin-Löf’s general methodology of distinguishing between
judgments and propositions. Formally, our calculus shares the most resemblance
with their possibility logic (although our system does not contain necessity
modality and no corresponding validity assumptions of the form
$\varphi\textit{ valid}$), and especially their lax logic: our I/E rules for
existence modality $\triangle$ directly correspond to their I/E rules for lax
modality $\medcircle$. Actually, we can show that our $\triangle$ modality
obeys the lax modality $\medcircle$ axioms (Fairtlough and Mender (1997)):

  * i)

$\varphi\to\medcircle\varphi$

  * ii)

$\medcircle\medcircle\varphi\to\medcircle\varphi$

  * iii)

$(\varphi\to\psi)\to\medcircle\varphi\to\medcircle\psi$

######  Proposition 7.

  1. i)

$\Gamma\vdash\varphi\to\triangle\varphi\textit{ true}$

  2. ii)

$\Gamma\vdash\triangle\triangle\varphi\to\triangle\varphi\textit{ true}$

  3. iii)

$\Gamma\vdash(\varphi\to\psi)\to\triangle\varphi\to\triangle\psi\textit{
true}$

Proof.

i)

hyp $\Gamma,\varphi\textit{ true}\vdash\varphi\textit{ true}$ just
$\Gamma,\varphi\textit{ true}\vdash\varphi\textit{ just true}$ $\triangle$I
$\Gamma,\varphi\textit{ true}\vdash\triangle\varphi\textit{ true}$ $\to$I
$\Gamma\vdash\varphi\to\triangle\varphi\textit{ true}$

ii) See Proposition 6.

iii)

hyp $\Gamma,\triangle\varphi\vdash\triangle\varphi$ w
$\Gamma,\triangle\varphi,\varphi\to\psi\vdash\triangle\varphi$ hyp
$\Gamma,\varphi\to\psi\vdash\varphi\to\psi$ w
$\Gamma,\varphi\to\psi,\varphi\vdash\varphi\to\psi$ hyp
$\Gamma,\varphi\vdash\varphi$ w $\Gamma,\varphi,\varphi\to\psi\vdash\varphi$
ex $\Gamma,\varphi\to\psi,\varphi\vdash\varphi$ $\to$E
$\Gamma,\varphi\to\psi,\varphi\vdash\psi$ just
$\Gamma,\varphi\to\psi,\varphi\vdash\psi\textit{ just}$ w
$\Gamma,\varphi\to\psi,\varphi,\triangle\varphi\vdash\psi\textit{ just}$ ex
$\Gamma,\triangle\varphi,\varphi\to\psi,\varphi\vdash\psi\textit{ just}$
$\triangle$E $\Gamma,\triangle\varphi,\varphi\to\psi\vdash\psi\textit{ just}$
$\triangle$I $\Gamma,\triangle\varphi,\varphi\to\psi\vdash\triangle\psi$ ex
$\Gamma,\varphi\to\psi,\triangle\varphi\vdash\triangle\psi$ $\to$I
$\Gamma,\varphi\to\psi\vdash\triangle\varphi\to\triangle\psi$ $\to$I
$\Gamma\vdash(\varphi\to\psi)\to\triangle\varphi\to\triangle\psi$

Thus, we can conclude that $\triangle$ is a lax modality.

However, at first glance, there appears to be a clear difference between
Pfenning and Davies’s system of lax logic and ours: their system does not
utilize the just true variants (or rather in their case, the lax variants) of
I/E rules (see Section 3.1).

First, let us show a fragment of a logical variant of our system without these
just true variants of I/E rules (i.e., without the j-variants $\to$Ij,
$\to$Ej, $\triangle$Ij, $\triangle$Ej), is actually equivalent to Pfenning and
Davies’s system of lax logic. First, let us specify a translation function
$\ell$ for propositions and contexts of our system into Pfenning and Davies’s
lax logic (Pfenning and Davies (2001)):
$\ell(\varphi\to\psi)=\ell(\varphi)\Rightarrow\ell(\psi)$,
$\ell(\triangle\varphi)=\medcircle\ell(\varphi)$, $\ell(p)=p$,
$\ell(\Gamma,\varphi\textit{ true})=\ell(\Gamma),\ell(\varphi)\textit{ true}$.

Let us denote judgments derivable in our (logical) fragment as
$\Gamma\vdash_{E}\varphi\textit{ true}$ and judgments derivable in Pfenning
and Davies’s lax logic as $\Gamma\vdash_{L}\varphi\textit{ true}$.

######  Proposition 8.

(Correctness of translation)

  1. If $\Gamma\vdash_{E}\varphi\textit{ true}$ then $\ell(\Gamma)\vdash_{L}\ell(\varphi)\textit{ true}$.

  2. If $\Gamma\vdash_{E}\varphi\textit{ just true}$ then $\ell(\Gamma)\vdash_{L}\ell(\varphi)\textit{ lax}$.

###### Proof.

By simultaneous induction on the structure of the given derivations. This is
straightforward, as the logical rules of our fragment and of Pfenning and
Davies’s lax logic closely correspond to each other (we essentially just need
to replace $\triangle$ with $\medcircle$ and just true with lax).

Now, let us specify a translation function $\varepsilon$ for propositions and
contexts of Pfenning and Davies’s lax logic into our system:
$\varepsilon(\varphi\Rightarrow\psi)=\varepsilon(\varphi)\to\varepsilon(\psi)$,
$\varepsilon(\medcircle\varphi)=\triangle\varepsilon(\varphi)$,
$\varepsilon(p)=p$, $\varepsilon(\Gamma,\varphi\textit{
true})=\varepsilon(\Gamma),\varepsilon(\varphi)\textit{ true}$. It holds that
$\varepsilon(\ell(\varphi))=\varphi$.

######  Proposition 9.

(Completness of translation)

  1. If $\Gamma\vdash_{L}\varphi\textit{ true}$ then $\varepsilon(\Gamma)\vdash_{E}\varepsilon(\varphi)\textit{ true}$.

  2. If $\Gamma\vdash_{L}\varphi\textit{ lax}$ then $\varepsilon(\Gamma)\vdash_{E}\varepsilon(\varphi)\textit{ just true}$.

###### Proof.

By simultaneous induction on the structure of the given derivations.

Putting together Propositions 8 and 9, from
$\ell(\Gamma)\vdash_{L}\ell(\varphi)\textit{ true}$ we can derive
$\varepsilon(\ell(\Gamma))\vdash_{E}\varepsilon(\ell(\varphi))\textit{ true}$,
and thus $\Gamma\vdash_{E}\varphi\textit{ true}$, and finally conclude that
$\Gamma\vdash_{E}\varphi\textit{ true}$ iff
$\ell(\Gamma)\vdash_{L}\ell(\varphi)\textit{ true}$.

Thus, a fragment of our logical system without the rules $\to$Ij, $\to$Ej,
$\triangle$Ij, $\triangle$Ej can be translated into Pfenning and Davies’s lax
logic. However, we can go a little bit further. As it turns out, all the just
true variants of rules $\to$Ij, $\to$Ej, $\triangle$Ij, $\triangle$Ej can be
actually derived in our system from the standard true variants $\to$I, $\to$E,
$\triangle$I, $\triangle$E if we add the following rule (note that it
corresponds to the right-to-left direction of Proposition 1):

$\Gamma\vdash\varphi\to\triangle\psi\textit{ true}$ r
$\Gamma\vdash\varphi\to\psi\textit{ just true}$

This also means that we can reduce a full logical variant of our system into
Pfenning and Davies’s lax logic extended by the rule r.

######  Proposition 10.

The rules $\to$Ij, $\to$Ej, $\triangle$Ij, $\triangle$Ej are derivable from
$\to$I, $\to$E, $\triangle$I, $\triangle$E together with the structural rules
and the r rule.

Proof.

$\to$Ij:

$\Gamma,\varphi\textit{ true}\vdash\psi\textit{ just true}$ $\triangle$I
$\Gamma,\varphi\textit{ true}\vdash\triangle\psi\textit{ true}$ $\to$I
$\Gamma\vdash\varphi\to\triangle\psi\textit{ true}$ r
$\Gamma\vdash\varphi\to\psi\textit{ just true}$

$\to$Ej:

$\Gamma\vdash\varphi\to\psi\textit{ just}$ $\triangle$I
$\Gamma\vdash\triangle(\varphi\to\psi)$ hyp
$\Gamma,\varphi\to\psi\vdash\varphi\to\psi$ $\Gamma\vdash\varphi$ w
$\Gamma,\varphi\to\psi\vdash\varphi$ $\Gamma,\varphi\to\psi\vdash\psi$ just
$\Gamma,\varphi\to\psi\vdash\psi\textit{ just}$ $\triangle$E
$\Gamma\vdash\psi\textit{ just}$

$\triangle$Ij:

$\Gamma\vdash\varphi\textit{ just true}$ $\triangle$I
$\Gamma\vdash\triangle\varphi\textit{ true}$ just
$\Gamma\vdash\triangle\varphi\textit{ just true}$

$\triangle$Ej:

$\Gamma\vdash\triangle\varphi\textit{ just}$ $\triangle$I
$\Gamma\vdash\triangle\triangle\varphi$ hyp
$\Gamma,\triangle\varphi\vdash\triangle\varphi$
$\Gamma,\varphi\vdash\gamma\textit{ just}$ w
$\Gamma,\varphi,\triangle\varphi\vdash\gamma\textit{ just}$ ex
$\Gamma,\triangle\varphi,\varphi\vdash\gamma\textit{ just}$ $\triangle$E
$\Gamma,\triangle\varphi\vdash\gamma\textit{ just}$ $\triangle$E
$\Gamma\vdash\gamma\textit{ just}$

##  6 Concluding remarks

The main novelty of our system in comparison to others found in the literature
is that it allows a rigorous treatment of basic judgments of the form “there
exists a proof of $\varphi$” which are in other systems (e.g., HoTT, CTT)
treated only as metalevel judgments or internalized as modal propositions.
Furthermore, our system distinguishes between judgmental and propositional
existence, while the latter is derived from the former. The link between
propositional existence $\triangle$ and truncation $\Box$ thus suggests that
the notion of truncation is ultimately based on the notion of judgmental
existence. From this perspective, it would be interesting to explore a weaker
variant of truncation introduced by Kraus (2015) and called anonymous
existence.313131An unexpected connection between truncation and the notion of
presupposition of inquisitive logic was recently observed by Punčochář and
Pezlar  (forthcoming), which also suggests a link to our calculus of
judgmental existence. Similarly, the links between the existence modality
$\triangle$ and lax modality $\medcircle$ of Fairtlough and Mender (1997) and
intuitionistic knowledge modality K of Artemov and Protopopescu (2016)323232We
thank Szymon Chlebowski for bringing our attention to this paper. seem
intriguing and would deserve further investigation. It also remains an open
question what exactly is the relationship between the proof-relevant judgments
$\varphi\textit{ true}$ and proof-irrelevant existential judgments
$\varphi\textit{ just true}$. We have mentioned that the former entails the
latter but not vice versa, however, more can be definitely said about this
relationship.

The main limitation of the present calculus is that we are considering only a
propositional fragment with $\to$ and $\triangle$. Extending the system with
other connectives (including identity), then generalizing it towards first-
order logic, and finally towards dependent type theory are the most
straightforward directions for future development.333333Or, alternatively,
extending systems like HoTT or CTT with judgments of the form $\varphi\textit{
inhab}$/$a\mathrel{\therefore}\varphi$. It is also worth noting that in
impredicative versions of HoTT, it is possible to define truncation $\Box$
without introducing a new type constructor. This suggests that existence
$\triangle$ might also be definable in such a way. Furthermore, the ability to
define truncation as a higher-inductive type opens the question whether
existence $\triangle$ could be defined in a similar manner. The addition of
propositional identity (so that we could form new propositions such as $p:a=b$
and thus also $p\mathrel{\therefore}a=b$) would be especially interesting as
it would allow us to fully explore the notion of propositional proof
irrelevance and related notions such as mere propositions. A natural next step
would be to also adopt judgmental identity (so that we could form new
judgments such as $a\equiv b:\varphi$ and thus also $a\equiv
b\mathrel{\therefore}\varphi$) as it would allow us to start exploring the
notion of judgmental proof irrelevance as well.

## References

  * Abel and Scherer (2012) Andreas Abel and Gabriel Scherer.  On Irrelevance and Algorithmic Equality in Predicative Type Theory.  _Logical Methods in Computer Science_ , Volume 8, Issue 1(1):1–36, 3 2012.  ISSN 1860-5974.  doi: 10.2168/LMCS-8(1:29)2012.
  * Artemov and Protopopescu (2016) Sergei Artemov and Tudor Protopopescu.  Intuitionistic Epistemic Logic.  _The Review of Symbolic Logic_ , 9(2):266–298, 6 2016.  ISSN 1755-0203.  doi: 10.1017/S1755020315000374.
  * Awodey and Bauer (2004) Steven Awodey and Andrej Bauer.  Propositions as [Types].  _Journal of Logic and Computation_ , pages 447–471, 2004.
  * Constable et al. (1986) Robert L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, D. J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, J. T. Sasaki, and S. F. Smith.  _Implementing Mathematics with the NuPRL Proof Development System_.  Prentice-Hall, Inc., Upper Saddle River, NJ, 1986.
  * Coquand (1989) Thierry Coquand.  Metamathematical investigations of a calculus of constructions.  Technical report, RR-1088, INRIA, 1989.  URL https://inria.hal.science/inria-00075471.
  * Coquand and Huet (1988) Thierry Coquand and Gerard Huet.  The calculus of constructions.  _Information and Computation_ , 76(2-3):95–120, 2 1988.  doi: https://doi.org/10.1016/0890-5401(88)90005-3.
  * Corfield (2020) David Corfield.  _Modal Homotopy Type Theory: The Prospect of a New Logic for Philosophy_.  Oxford University Press, Oxford, 2020.  ISBN 9780198853404.
  * Curry (1952) Haskell B. Curry.  The Permutability of Rules in the Classical Inferential Calculus.  _Journal of Symbolic Logic_ , 17(4):245–248, 1952.
  * de Bruijn (1974) Nicolaas G. de Bruijn.  Some Extensions of Automath: The AUT-4 Family.  Technical report, Eindhoven University of Technology, Eindhoven, 1974.
  * de Bruijn (1994) Nicolaas G. de Bruijn.  Some Extensions of Automath: The AUT-4 Family.  In _Studies in Logic and the Foundations of Mathematics_ , volume 133, pages 283–288. Elsevier, 1 1994.  doi: 10.1016/S0049-237X(08)70209-X.
  * Dummett (1975) Michael Dummett.  The Philosophical Basis of Intuitionistic Logic.  _Studies in Logic and the Foundations of Mathematics_ , 80:5–40, 1 1975.  ISSN 0049237X.  doi: 10.1016/S0049-237X(08)71941-4.
  * Fairtlough and Mender (1997) Matt Fairtlough and Michael Mender.  Propositional Lax Logic.  _Information and Computation_ , 137(1):1–33, 1997.
  * Gilbert et al. (2019) Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau.  Definitional proof-irrelevance without k.  _Proceedings of the ACM on Programming Languages_ , 3(POPL), 1 2019.  ISSN 24751421.  doi: 10.1145/3290316.
  * Hilbert and Bernays (1968) David Hilbert and Paul Bernays.  _Grundlagen der Mathematik I_.  Springer, Berlin, 2nd (1st ed. 1934) edition, 1968.
  * Hofmann (1995) Martin Hofmann.  _Extensional Concepts in Intensional Type Theory_.  PhD thesis, University of Edinburgh, Edinburgh, 1995.
  * Howard (1980) William Alvin Howard.  The formulae-as-types notion of construction.  In Haskell B. Curry, J. Roger Hindley, and Jonathan P. Seldin, editors, _To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism_. Academic Press, London, 1980.
  * Kleene (1945) Stephen C. Kleene.  On the Interpretation of Intuitionistic Number Theory.  _The Journal of Symbolic Logic_ , 10(4):109–124, 12 1945.  ISSN 0022-4812.  doi: 10.2307/2269016.
  * Klev (2023) Ansten Klev.  Modality and the Structure of Assertion.  In Igor Sedlár, editor, _The Logica Yearbook 2022_ , pages 39–53, London, 2023. College Publications.
  * Kraus (2015) Nicolai Kraus.  _Truncation levels in homotopy type theory_.  PhD thesis, University of Nottingham, Nottingham, 7 2015.
  * Luo (1994) Zhaohui Luo.  _Computation and reasoning: a type theory for computer science_.  Clarendon Press, 1994.  ISBN 9780198538356.
  * Mancosu (1998) Paolo Mancosu.  _From Brouwer to Hilbert. The Debate on the Foundations of Mathematics in the 1920s_.  Oxford University Press, 1998.
  * Martin-Löf (1984) Per Martin-Löf.  _Intuitionistic type theory: Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980_.  Bibliopolis, Napoli, 1984.
  * Martin-Löf (1991) Per Martin-Löf.  A path from logic to metaphysics.  In _Atti del Congresso Nuovi problemi della Logica e della Filosofia dela Scienza. II_ , pages 141–149. CLUEB, Bologna, 1991.
  * Martin-Löf (1993) Per Martin-Löf.  _Philosophical aspects of intuitionistic type theory_.  Lecture notes edition, 1993.  URL https://pml.flu.cas.cz/uploads/PML-LeidenLectures93.pdf.
  * Martin-Löf (1996) Per Martin-Löf.  On the meanings of the logical constants and the justifications of the logical laws.  _Nordic Journal of Philosophical Logic_ , 1(1):11–60, 1996.
  * Nederpelt et al. (1994) Rob P. Nederpelt, J. Herman Geuvers, and Roel C. de Vrijer, editors.  _Selected papers on Automath_ , volume 133.  Elsevier, Amsterdam, 1994.
  * Nordström et al. (1990) Bengt Nordström, Kent Petersson, and Jan M. Smith.  _Programming in Martin-Löf’s type theory: an introduction_.  Clarendon Press, Oxford, 1990.  ISBN 9780198538141.
  * Pfenning (2001) Frank Pfenning.  Intensionality, extensionality, and proof irrelevance in modal type theory.  _Proceedings - Symposium on Logic in Computer Science_ , pages 221–230, 2001.  doi: 10.1109/LICS.2001.932499.
  * Pfenning and Davies (2001) Frank Pfenning and Rowan Davies.  A judgmental reconstruction of modal logic.  _Mathematical Structures in Computer Science_ , 11(4):511–540, 2001.  ISSN 1469-8072.  doi: 10.1017/S0960129501003322.
  * Plotkin (1973) Gordon D. Plotkin.  Lambda-definability and logical relations (Memorandum SAI-RM-4).  Technical report, University of Edinburgh, Edinburgh, 1973.
  * Prawitz (1965) Dag Prawitz.  _Natural Deduction: A Proof-theoretical Study_.  Almqvist & Wiksell, Stockholm, reprinted edition, 1965.  ISBN 9780486446554.
  * (32) Vít Punčochář and Ivo Pezlar.  Informative Presupposition in Inquisitive Logic (forthcoming).
  * Reed (2002) Jason Reed.  _Proof Irrelevance and Strict Definitions in a Logical Framework_.  PhD thesis, Carnegie Mellon University, BSc thesis, 2002.
  * Rijke (2022) Egbert Rijke.  _Introduction to Homotopy Type Theory_.  Cambridge University Press, Cambridge, pre-publication edition, 12 2022.  URL https://arxiv.org/abs/2212.11082v1.
  * Tait (1967) William Walker Tait.  Intensional Interpretations of Functionals of Finite Type I.  _Journal Symbolic Logic_ , 32(2):198–212, 1967.
  * Troelstra and van Dalen (1988) Anne S. Troelstra and Dirk van Dalen.  _Constructivism in Mathematics_.  North Holland, Amsterdam, 1988.
  * UFP (2013) UFP.  _Homotopy Type Theory: Univalent Foundations of Mathematics_.  https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  * Valentini (1998) Silvio Valentini.  The forget-restore principle: a paradigmatic example.  In Giovanni Sambin and Jan M. Smith, editors, _Twenty-five years of constructive type theory: proceedings of a congress held in Venice, October 1995_ , pages 275–283, Oxford, 1998. Clarendon Press.
  * Van Dalen (1995) Dirk Van Dalen.  Hermann Weyl’s Intuitionistic Mathematics.  _Bulletin of Symbolic Logic_ , 1(2):145–169, 1995.  ISSN 19435894.  doi: 10.2307/421038.
  * Weyl (1921a) Hermann Weyl.  Über der neue Grundslagenkrise der Mathematik.  _Mathematische Zeitschrift_ , (10):37–79, 1921a.
  * Weyl (1921b) Hermann Weyl.  On the New Foundational Crisis in Mathematics.  In _From Brouwer to Hilbert: The Debate on the Foundations of Mathematics in the 1920s_ , pages 86–122. Clarendon Press, Oxford, 1921b.