# Dialectica Principles via Gödel Doctrines††thanks: Research supported by the
project MIUR PRIN 2017FTXR IT-MaTTerS (Trotta) and by a School of Mathematics
EPSRC Doctoral Studentship (Spadetto)

Davide Trotta
University of Pisa
<EMAIL_ADDRESS>Matteo Spadetto
University of Leeds
<EMAIL_ADDRESS>Valeria de Paiva
Topos Institute
<EMAIL_ADDRESS>
###### Abstract

Gödel’s Dialectica interpretation was conceived as a tool to obtain the
consistency of Peano arithmetic via a proof of consistency of Heyting
arithmetic in the 40s. In recent years, several proof theoretic
transformations, based on Gödel’s Dialectica interpretation, have been used
systematically to extract new content from classical proofs, following a
suggestion of Kreisel. Thus, the interpretation has found new relevant
applications in several areas of mathematics and computer science. Several
authors have explained the Dialectica interpretation in categorical terms. In
particular, de Paiva introduced the notion of a _Dialectica category_ as an
internal version of Gödel’s Dialectica Interpretation in her doctoral work.
This was generalised by Hyland and Hofstra, who considered the interpretation
in terms of fibrations. In our previous work, we introduced an _intrinsic_
presentation of the Dialectica construction via a generalisation of Hofstra’s
work, using the notion of Gödel fibration and its proof-irrelevant version, a
Gödel doctrine. The key idea is that Gödel fibrations (and doctrines) can be
thought of as fibrations generated by some basic elements playing the role of
_quantifier-free elements_. This categorification of quantifier-free elements
is crucial not only to show that our notion of Gödel fibration is equivalent
to Hofstra’s Dialectica fibration in the appropriate way, but also to show how
Gödel doctrines embody the main logical features of the Dialectica
Interpretation. To show that, we derive the soundness of the interpretation of
the implication connective, as expounded by Troelstra, in the categorical
model. This requires extra logical principles, going beyond intuitionistic
logic, namely Markov Principle (MP) and the Independence of Premise (IP)
principle, as well as some choice. We show how these principles are satisfied
in the categorical setting, establishing a tight (internal language)
correspondence between the logical system and the categorical framework. This
tight correspondence should come handy not only when discussing the
traditional applications of the Dialectica, but also when dealing with some
newer uses of the interpretation, as in modelling games or concurrency theory.
Finally, to complete our analysis, we characterise categories obtained as
results of the tripos-to-topos of Hyland, Johnstone and Pitts applied to Gödel
doctrines.

Keywords. Gödel doctrine; Hyperdoctrine; Dialectica doctrine; Dialectica
category; Dialectica interpretation; Logical principles.

##  1 Introduction

Gödel is known, amongst many other things, by his Platonistic views of
Mathematics. This is not what the ‘Gödel doctrines’ in our title are about.
Doctrines in our title are meant in Lawvere’s sense of ‘hyperdoctrines’, a
special kind of functor in Category Theory [20]. Gödel doctrines then refer to
Gödel because of his Dialectica Interpretation [10], a modified form of
Hilbert’s program, which shows consistency of logical systems by interpreting
these systems into collections of “computable functionals”. First and most
importantly, by showing consistency of Heyting arithmetic using his system $T$
of functionals.

In recent years, proof theoretic transformations (also called proof
interpretations) based on Gödel’s Dialectica interpretation [10] have been
used systematically by Kohlenbach and others [17] to extract new content from
proofs, following Kreisel’s suggestion. Thus, the Dialectica interpretation
has found relevant applications in several areas of mathematics and computer
science. Meanwhile, several authors have explained the Dialectica
interpretation in categorical terms. In particular, de Paiva [5] introduced
the notion of a _Dialectica category_ as an internal version of Gödel’s
Dialectica Interpretation. The idea is to construct a category
$\mathfrak{Dial}(\mathsf{C})(\mathsf{C})$ from a category $\mathsf{C}$ with
finite limits. The main focus in de Paiva’s original work is on the
categorical structure of the category obtained, as this notion of Dialectica
category turns out to be also a model of Girard’s Linear Logic [9].

This construction was first generalised by Hyland, who investigated the
Dialectica construction associated to a fibred preorder [15]. Later, Biering
in her PhD work [2] studied the Dialectica construction for an arbitrary
cloven fibration. Hofstra [14] then wrote an exposition and interpretation of
the Dialectica construction from a modern categorical perspective, emphasising
its universal properties. His work gives centre stage to the well-known
concepts of pseudo-monads, simple products and co-products.

Taking advantage of the abstract presentation of Hofstra, in previous works
[34, 35] we introduced an _intrinsic_ presentation of the Dialectica
construction via the notion of Gödel fibration and its proof-irrelevant
version, namely Gödel doctrines. The key idea is that Gödel fibrations (and
doctrines) can be thought of as fibrations generated by some basic elements
playing the role of _quantifier-free elements_. This categorification of
quantifier-free elements is crucial not only to show that the notions of Gödel
fibrations introduced in [34] and Dialectica fibrations (as presented in [14])
are mathematically equivalent in the appropriate way, but also to show how
Gödel doctrines embody the main logical features of the Dialectica
Interpretation [35, 36]. While in [34] we presented a reconstruction of where
the categorification of concepts came from, in [36] we showed that this
categorification worked not only for rules as in [35], but also for the
logical principles themselves, which is always more exciting for logicians
than for category theorists.

The main purpose of the work here is to provide a self-contained and complete
study of Gödel doctrines, presenting in detail the results developed in [35,
36], their connections with [34], and carrying on the analysis of these
doctrines. In this paper, we present in detail the notion of _doctrine_ and
its logical meaning first, and then we discuss the Dialectica interpretation
of the implicational connective and the logical principles involved in the
categorical interpretation of this connective. Moreover, in order to present
our results with a notation familiar to both logicians and category theorists,
we will employ the _internal language_ of a doctrine [29].

As far as the notion of doctrine is concerned, we follow the notation and the
definitions presented in [23, 24], where the authors introduce primary,
elementary and existential doctrines as generalisations of the original notion
of Lawvere’s hyperdoctrine [20].

After recalling the main categorical tools involved, we are going to present a
(hyper)doctrine characterisation of the Dialectica interpretation which
corresponds exactly to its logical description. The _soundness_ of the
interpretation of the implication connective, as expounded on by Spector and
Troelstra [30], in the categorical models will follow as a direct consequence
of this tight correspondence. In particular, recall that such an
interpretation is motivated by the equivalence:

$(\exists u.\forall x.\psi_{D}(u,x)\to\exists v.\forall
y.\phi_{D}(v,y))\leftrightarrow$

$\leftrightarrow\exists f_{0},f_{1}.\forall
u,y.(\psi_{D}(u,f_{1}(u,y))\rightarrow\phi_{D}(f_{0}(u),y))$

where $\psi_{D}$ and $\phi_{D}$ are quantifier-free formulae. Showing this
equivalence requires extra logical principles, going beyond intuitionistic
logic, specifically Markov Principle (MP) and the Independence of Premise (IP)
principle, as well as some choice. While the traditional categorical approach
takes this equivalence as the starting point for defining categorical models,
for example Dialectica categories [5], our approach focuses instead on
abstracting in the setting of doctrines the key logical features that allow us
to conclude such an equivalence.

We show how these key logical features are satisfied in the categorical
setting, establishing a tight correspondence between the logical system and
the categorical framework. Our results are built on the categorical
presentation of existential and universal-free elements we introduced first in
the context of fibrations in [34], and then in the language of doctrines [35].
Having a categorification of such notions is fundamental to properly state
logical principles in categorical terms, since both (IP) and (MP) involve
quantifier-free formulae. Finally, to complete our analysis of Gödel
(hyper)doctrines, we characterise categories obtained as results of the
tripos-to-topos construction of Hyland, Johnstone and Pitts [16] applied to
these doctrines. After recalling the notions and the construction of the
category of predicates associated to a hyperdoctrine from [23], and of exact
completion of a lex category [4], we present an explicit characterisation of
the tripos-to-topos construction associated to a Gödel hyperdoctrine. In
particular, combining our results with the characterisation of exact
completions presented in [32], we show that every category obtained as tripos-
to-topos of a Gödel hyperdoctrine can be equivalently presented as the exact
completion of the category of predicates associated to the hyperdoctrine
itself. We then conclude with a very brief discussion of other work we
envisaged following from our characterisation.

##  2 Doctrines

One of the most relevant notions of categorical logic which enabled the study
of logic from a pure algebraic perspective is that of a _hyperdoctrine_ ,
introduced in a series of seminal papers by F.W. Lawvere to synthesise the
structural properties of logical systems [18, 19, 20]. Lawvere’s crucial
intuition was to consider logical languages and theories as fibrations to
study their 2-categorical properties, so that e.g. connectives, quantifiers
and equality are determined by structural adjunctions. If theories and models
can be viewed as objects and morphisms of a suitable category, i.e. the
category of hyperdoctrines, this is in particular a 2-category, where 2-cells
represent morphisms of models. So, having a 2-categorical structure allows us
not only to compare theories (objects) via models (1-cells), but also to
compare models (1-cells) via the 2-cells that represent morphisms of models.

Recall from [29] that a first-order hyperdoctrine is a contravariant functor:

$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Hey}}$

from a cartesian category $\mathcal{C}$ to the category of Heyting algebras
${\mathbf{Hey}}$ satisfying: for every arrow $A\xrightarrow{f}B$ in
$\mathcal{C}$, the homomorphism $P_{f}\colon P(B)\longrightarrow P(A)$ of
Heyting algebras, where $P_{f}$ denotes the action of the functor $P$ on the
arrow $f$, has a left adjoint $\exists_{f}$ and a right adjoint $\forall_{f}$.
These adjoints satisfy the Beck-Chevalley conditions (BC), i.e. for any
pullback square:

$\textstyle{D\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{h}$$\scriptstyle{k}$$\textstyle{C\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{g}$$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\textstyle{B}$

it is the case that the squares:

$\textstyle{PD\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\exists_{k}}$$\textstyle{PC}$$\textstyle{PA\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{P_{h}}$$\scriptstyle{\exists_{f}}$$\textstyle{PB\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{P_{g}}$
and
$\textstyle{PD\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\forall_{k}}$$\textstyle{PC}$$\textstyle{PA\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{P_{h}}$$\scriptstyle{\forall_{f}}$$\textstyle{PB\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{P_{g}}$

commute, i.e. the equalities:

$\exists_{k}P_{h}=P_{g}\exists_{f}$ and $\forall_{k}P_{h}=P_{g}\forall_{f}$

hold.

Observe that in fact the pointwise inequalities $\exists_{k}P_{h}\leq
P_{g}\exists_{f}$ and $\forall_{k}P_{h}\geq P_{g}\forall_{k}$ always hold from
the adjunctions definitions. The purpose of the Beck-Chevalley conditions is
to guarantee that substitution commutes with quantification, appropriately,
thus BC forces the equality in both diagrams.

A first-order hyperdoctrine determines an appropriate categorical structure to
abstract a first-order theory and its corresponding Tarski semantics.
Semantically, a first-order hyperdoctrine is essentially a generalisation of
the contravariant _powerset functor_ on the category of sets:

$\mathcal{P}\colon\operatorname{\mathbf{Set}}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Hey}}$

sending a set $A$ into the Heyting algebra $\mathcal{P}(A)$ of its subsets
(ordered by inclusion), and a set-theoretic function $A\xrightarrow{f}B$ to
the inverse image functor
$\mathcal{P}B\xrightarrow{\mathcal{P}f=f^{-1}}\mathcal{P}A$. In this case, the
adjoints $\forall_{f}$ and $\exists_{f}$ must be evaluated, on a subset $D$ of
$A$, respectively as the subsets $\exists_{f}(D)=\\{a\in B\;|\;\exists a\in
A.\;(b=f(a)\wedge a\in D)\\}$ and $\forall_{f}(D)=\\{a\in B\;|\;\forall a\in
A.\;(b=f(a)\Rightarrow a\in D)\\}$.

From a syntactic point of view, a first-order hyperdoctrine can be seen as a
generalisation of the _Lindenbaum-Tarski algebra_ of well-formed formulae of a
first order theory. In particular, given a first-order theory T in a many-
sorted first-order language $\mathcal{L}$, one can consider the functor:

$\mathcal{L}\textsc{T}\colon\mathcal{V}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Hey}}$

whose base category $\mathcal{V}$ is the _syntactic_ category of
$\mathcal{L}$, i.e. the one whose objects are ($\alpha$-equivalence classes
of) finite lists $\overrightarrow{x}:=[x_{1}:X_{1},\dots,x_{n}:X_{n}]$ of
typed variables and whose morphisms are lists of substitutions, while the
elements of $\mathcal{L}\textsc{T}(\overrightarrow{x})$ are given by
equivalence classes (with respect to provable reciprocal consequence
$\dashv\vdash$) of well-formed formulae in the context $\overrightarrow{x}$,
and order is given by the provable consequences, according to the fixed theory
T. In this case, the left adjoint to the weakening functor
$\mathcal{L}\textsc{T}_{\pi}$ is computed by existentially quantifying the
variables that are not involved in the substitution induced by the projection
(dually the right adjoint is computed by quantifying universally).

###  2.1 Existential and universal doctrines

Recently, several generalisations of the notion of a Lawvere hyperdoctrine
were considered, and we refer for example to [22, 23, 24] or to [28, 16] for
higher-order versions. For further insights and applications to higher-order
logic or realisability, we refer to [16, 37, 28].

In this work we consider a natural generalisation of the notion of first-order
hyperdoctrine, and we call it simply a _doctrine_.

######  Definition 2.1.

A doctrine is a contravariant functor:

$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Pos}}$

where the category $\mathcal{C}$ has finite products and
$\operatorname{\mathbf{Pos}}$ is the category of posets.

Now we recall from [22, 23, 31] the notions of existential and universal
doctrines.

######  Definition 2.2.

A doctrine
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Pos}}$
is existential (resp. universal) if, for every $A_{1}$ and $A_{2}$ in
$\mathcal{C}$ and every projection $A_{1}\times
A_{2}\xrightarrow{{\pi_{i}}}A_{i}$, $i=1,2$, the functor:

${PA_{i}}\xrightarrow{{P_{\pi_{i}}}}{P(A_{1}\times A_{2})}$

has a left adjoint $\exists_{\pi_{i}}$ (resp. a right adjoint
$\forall_{\pi_{i}}$), and these satisfy the Beck-Chevalley condition BC: for
any pullback diagram:

$\textstyle{X^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{{\pi^{\prime}}}$$\scriptstyle{f^{\prime}}$$\textstyle{A^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{{\pi}}$$\textstyle{A}$

where $\pi$ and $\pi^{\prime}$ are projections, and for any $\beta$ in $P(X)$
the equality:

$\exists_{\pi^{\prime}}P_{f^{\prime}}\beta=P_{f}\exists_{\pi}\beta\,\,\,\,\textnormal{
( resp.
}\forall_{\pi^{\prime}}P_{f^{\prime}}\beta=P_{f}\forall_{\pi}\beta\textnormal{
)}$

holds.

Observe that the inequality $\exists_{\pi^{\prime}}P_{f^{\prime}}\beta\leq
P_{f}\exists_{\pi}\beta\textnormal{ ( resp.
}\forall_{\pi^{\prime}}P_{f^{\prime}}\beta\geq
P_{f}\forall_{\pi}\beta\textnormal{ )}$ of BC in Definition 2.2 always holds.

We conclude the current subsection recalling from [22, 23, 24] that doctrines
form a 2-category $\mathsf{Doc}$ where:

  * •

a 1-cell is a pair $(F,\mathfrak{b})$:

|
---|---
$\textstyle{\mathcal{C}^{\operatorname{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{P}$$\scriptstyle{F^{\operatorname{op}}}$$\textstyle{\operatorname{\mathbf{Pos}}}$$\textstyle{\mathcal{D}^{\operatorname{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{R}$$\scriptstyle{\mathfrak{b}}$

such that $\mathcal{C}\xrightarrow{F}\mathcal{D}$ is a finite product
preserving functor between doctrines $P,R$, and:

$P\xrightarrow{\mathfrak{b}}RF^{\operatorname{op}}$

is a natural transformation;

  * •

a 2-cell $(F,\mathfrak{b})\xrightarrow{\theta}(G,\mathfrak{c})$ is a natural
transformation $F\xrightarrow{\theta}G$ such that for every $A$ in
$\mathcal{C}$ and every $\alpha$ in $P(A)$, we have:

$\mathfrak{b}_{A}(\alpha)\leq R_{\theta_{A}}(\mathfrak{c}_{A}(\alpha)).$

We denote as $\mathsf{ExD}$ the 2-full subcategory of $\mathsf{Doc}$ whose
elements are existential doctrines, and whose 1-cells are those 1-cells of
$\mathsf{Doc}$ which preserve the existential structure. Similarly, we denote
by $\mathsf{UnD}$ the 2-full subcategory of $\mathsf{Doc}$ whose elements are
universal doctrines, and whose 1-cells are those 1-cells of $\mathsf{Doc}$
which preserve the universal structure.

From a logical perspective, the intuition is that a 1-cell between doctrines
is a generalisation of the notion of set-theoretic model, whereas 2-cells
represent morphisms of models.

###  2.2 Internal language of doctrines

Over the years, category theory and categorical logic have evolved a
characteristic form of proof by diagram chasing to establish properties
expressible in category theoretic terms. However, in complex cases such
arguments can be difficult to construct and hard to follow because of the
rather limited forms of expression of a purely category-theoretic language.

Categorical logic enables the use of richer and more familiar forms of
expression meant to establish properties of particular kinds of categories.
Indeed, one can define a suitable notion of _internal language_ , naming the
relevant constituents of the category and then applying a categorical
semantics to turn assertions of this language (according to a suitable logic)
into categorical statements. Such a procedure has become highly developed in
the theory of toposes where the internal language of a topos coupled with the
semantics of intuitionistic higher order logic in toposes enables one to
reason about the objects and morphisms of a topos as if they were sets and
functions. The notion of internal language is not just a useful instrument to
simplify the notation, but it is a powerful instrument that allows us to
formally prove a categorical equivalence between doctrines and logical
theories.

First, we briefly recall that theories in a given (possibly many-sorted)
language over a fragment of first-order logic induce doctrines. Let us assume
that we are given a fragment $F$ of first-order logic. Whenever $\mathcal{L}$
is a (possibly) many sorted $F$-language and T is an $\mathcal{L}$-theory, we
can define a doctrine $\mathcal{L}\textsc{T}$ over the syntactic category
$\mathcal{V}$ associated to $\mathcal{L}$, as described in Section 2. Whenever
$P$ is a doctrine over some category $\mathcal{C}$, then $P$ can host models
of T according to a natural generalisation of Tarski’s semantics, which is
sound and complete (for it admits the syntactic model) and is formally defined
as classic Tarski’s semantics for (a fragment of) first-order logic. In fact,
a $\mathcal{L}$-structure $S$ in $P$ consists of:

  * •

an object of $\mathcal{C}$ for every $\mathcal{L}$-sort;

  * •

an arrow of $\mathcal{C}$ (between the appropriate $S$-interpretations of the
sorts) for any $\mathcal{L}$-function symbol;

  * •

for every $\mathcal{L}$-predicate symbol in some context, an element of the
$P$-fibre of the $S$-interpretation of that context.

Then (terms and) formulas are inductively interpreted in $S$ as usual
(formally as for traditional Tarski’s semantics) and we say that $S$ models
some $\mathcal{L}$-sequent $\phi\vdash\psi$ in some given context when it is
the case that:

$\phi^{S}\leq\psi^{S}$

in the $P$-fibre of the $S$-interpretation of the given context (here
$\alpha^{S}$ denotes the $S$-interpretation of some formula $\alpha$).
According to this notion of semantics, it is the case that the $P$-models of
T, together with the model morphisms between them, are bijectively
(equivalently) induced by the $1$-cells $\mathcal{L}\textsc{T}\to P$ of
$\mathsf{Doc}$ and the $2$-cells between them, respectively. Thus, the
identity over $\mathcal{L}\textsc{T}$ induces the syntactic model of T.

Conversely, a language can be defined for a given doctrine
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Pos}}$.
One can associate to each doctrine
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Pos}}$
a language $\mathcal{L}_{P}$ having a sort $A$ for each object $A$ of the base
category $\mathcal{C}$, an $n$-ary function symbol
$A_{1},\dots,A_{n}\xrightarrow{f}A$ for every morphism $A_{1}\times\dots\times
A_{n}\xrightarrow{f}A$ of $\mathcal{C}$ and an $n$-relation symbol $R\colon
A_{1},\dots,A_{n}$ for each element of $P(A_{1}\times\dots\times A_{n})$, all
of this for each finite list of objects $A_{1},\dots,A_{n}$ of $\mathcal{C}$
and every object $A$ of $\mathcal{C}$. The language $\mathcal{L}_{P}$ is
called the internal language of the doctrine $P$. Let $\textsc{T}_{P}$ be the
theory whose sequents $\phi\vdash\psi$ in some context $A$ are precisely those
ones such that $\phi\leq\psi$ in $P(A)$. The doctrine
$\mathcal{L}_{P}\textsc{T}_{P}$ is equivalent to $P$ in $\mathsf{Doc}$ and the
assignment $P\mapsto(\mathcal{L}_{P},\textsc{T}_{P})$ extends to a pseudo
2-inverse to the 2-functor
$(\mathcal{L},\textsc{T})\mapsto\mathcal{L}\textsc{T}$, in such a way that
$\mathsf{Doc}$ is equivalent to the theories in some language over $F$
together with the models (of one of them into the other one) and the model
morphisms (between them).

Whenever
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Pos}}$
is a doctrine, we know that $\mathcal{L}_{P}\textsc{T}_{P}$ is equivalent to
$P$ in $\mathsf{Doc}$. Therefore, the doctrine $P$, together with the
equivalence $\mathcal{L}_{P}\textsc{T}_{P}\to P$, constitutes the syntactic
model of its own theory $\textsc{T}_{P}$ in its own internal language
$\mathcal{L}_{P}$. This fact means that, whenever $\phi$ and $\psi$ are
elements of $P(A)$, for some object $A$ of $\mathcal{C}$, it is the case that
$\phi\leq\psi$ precisely when $\phi\vdash\psi$ is a sequent of
$\textsc{T}_{P}$ in context $A$. This is precisely why we can deduce
properties of $P$ through a purely syntactical procedure: every
$\mathcal{L}_{P}$-sequent corresponds to a categorical statement or a
condition involving $P$, and this is true precisely when that sequent belongs
to $\textsc{T}_{P}$.

Taking advantage of these equivalent ways of reasoning about doctrines and
logic, we define the following notation for this logical syntax, which we use
extensively in this paper. We write in the internal language of a doctrine:

$a_{1}:A_{1},\dots,a_{n}:A_{n}\;|\;\phi(a_{1},\dots,a_{n})\vdash\psi(a_{1},\dots,a_{n})$

instead of:

$\phi\leq\psi$

in the fibre $P(A_{1}\times\cdots\times A_{n})$. Similarly, we write:

$a:A\;|\;\phi(a)\vdash\exists b:B.\psi(a,b)\text{ and
}a:A\;|\;\phi(a)\vdash\forall b:B.\psi(a,b)$

in place of:

$\phi\leq\exists_{\pi_{A}}\psi\text{ and }\phi\leq\forall_{\pi_{A}}\psi$

in the fibre $P(A)$, where $\pi_{A}$ is the projection $A\times B\to A$. In
fact, if a doctrine
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Pos}}$
is existential and $\alpha\in P(A\times B)$ is a formula-in-context:

$a:A,b:B\;|\;\alpha(a,b)$

then $\exists_{\pi_{A}}\alpha\in PA$ represents the formula $a:A\;|\;\exists
b:B.\alpha(a,b)$ in context $A$. Analogously, if the doctrine $P$ is
universal, then $\forall_{\pi_{A}}\alpha\in PA$ represents the formula
$a:A\;|\;\forall b:B.\alpha(a,b)$ in context $A$. This interpretation is sound
and complete for the usual reasons: this is how usual Tarski semantics can be
characterised in terms of categorical properties of the powerset functor
$\mathcal{P}\colon\operatorname{\mathbf{Set}}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Pos}}$.

Also, we write $a:A\;|\;\phi\dashv\vdash\psi$ to abbreviate
$a:A\;|\;\phi\vdash\psi$ and $a:A\;|\;\psi\vdash\phi$ and when the type of a
quantified variable is clear from the context, we will omit that type for sake
of readability. Finally, substitutions via given terms (i.e. reindexings and
weakenings) are modelled by pulling back along those given terms. Applications
of propositional connectives are interpreted by using the corresponding
operations in the fibres of the given doctrine.

##  3 Quantifier-free elements and Gödel doctrines

One of the fundamental notions of logic and proof theory is the notion of
_quantifier-free formula_ , and there are countless results built on the
possibility of detecting quantifier-free formulae in the literature. For
example, in the Dialectica interpretation, this notion is present at every
stage, and we could say the entire translation depends on the fact that,
syntactically, we can identify and distinguish formulae with no occurrences of
quantifiers.

However, while from a syntactic perspective it is effortless and natural to
speak of quantifier-free formulae, abstracting this notion algebraically is
not so obvious. The main problem is that the property of being quantifier-free
is totally syntactic, not involving any other entity different from the
formula itself we are considering. It does not depend, for example, on the
fact that we are working in classical, constructive or intuitionistic logic.
It only depends on how a formula is written in a given formal language.

Therefore, if we want to provide a complete categorical presentation of the
Dialectica interpretation, capable of representing all its logical details, we
have to deal with the problem of representing quantifier-free formulae and
find a suitable _universal property_ to represent predicates that are
quantifier-free categorically. Notice that quantifier-free elements may
satisfy different properties depending on the logical system we are
considering, hence if we want to represent these elements via universal
properties, we have to relativise this notion to a give system, that is the
Dialectica interpretation in our case.

###  3.1 Existential and universal free elements

We discuss a notion to identify those predicates of an existential doctrine:

$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Pos}}$

which are _free from left-adjoints_ $\exists_{\pi}$, and then dualise this
notion to define those predicates that are _free from right-adjoints_
$\forall_{\pi}$. This idea was originally introduced by Trotta and Maietti
[32] and, independently, by Frey in [8]. It was further developed and
generalised to the fibrational setting in [34].

######  Definition 3.1.

Let
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Pos}}$
be an existential doctrine and let $A$ be an object of $\mathcal{C}$. A
predicate $\alpha$ of the fibre $P(A)$ is said to be an existential splitting
if it satisfies the following _weak_ universal property: for every predicate
$\beta\in P(A\times B)$ such that $\alpha(a)\vdash\exists b\colon
B.\beta(a,b)$ (i.e. $\alpha\leq\exists_{\pi_{A}}(\beta)$ in category-theoretic
notation, where $A\times B\xrightarrow{\pi_{A}}A$ is a product projection of
$\mathcal{C}$), there exists an arrow $A\xrightarrow{g}B$ such that:

$\alpha(a)\vdash\beta(a,g(a))\textnormal{ \, \, ( i.e. }\alpha\leq P_{\langle
1_{A},g\rangle}(\beta)\textnormal{ in category-theoretic notation ).}$

Existential splittings stable under re-indexing are called _existential-free
elements_. Thus we introduce the following definition:

######  Definition 3.2.

Let
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Pos}}$
be an existential doctrine and let $I$ be an object of $\mathcal{C}$. A
predicate $\alpha$ of the fibre $P(I)$ is said to be existential-free if
$P_{f}(\alpha)$ is an existential splitting for every morphism
$A\xrightarrow{f}I$.

Employing the presentation of doctrines via internal language, we say that
$i:I\;|\;\alpha(i)$ is free from the existential quantifier if, whenever
$a:A\;|\;\alpha(f(a))\vdash\exists b:B.\beta(a,b)$ for some term
$a:A\;|\;f(a):I$, then there is a term $a:A\;|\;g(a):B$ such that
$a:A\;|\;\alpha(f(a))\vdash\beta(a,g(a))$.

Observe that we always have that $a:A\;|\;\beta(a,g(a))\vdash\exists
b:B.\beta(a,b)$, in other words $P_{\langle
1_{A},g\rangle}\beta\leq\exists_{\pi_{A}}\beta$. In fact, it is the case that
$\beta\leq P_{\pi_{A}}\exists_{\pi_{A}}\beta$ (as this arrow of $P(A\times B)$
is nothing but the unit of the adjunction $\exists_{\pi_{A}}\dashv
P_{\pi_{A}}$), hence a re-indexing by the term $\langle 1_{A},g\rangle$ yields
the desired inequality. Therefore, the property that we require for
$i:I\;|\;\alpha(i)$ turns out to be the following: whenever there are proofs
of $\exists b:B.\beta(a,b)$ from $\alpha(f(a))$, at least one of them factors
through the canonical proof of $\exists b:B.\beta(a,b)$ from $\beta(a,g(a))$
for some term $a:A\;|\;g(a):B$.

Requiring the stability under substitution as in Definition 3.2 is motivated
by the fact that, in logic, if a formula is existential-free, and we apply a
substitution to this formula, then we obtain again an existential-free
formula.

######  Definition 3.3.

Let
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Pos}}$
be an existential doctrine. Then we indicate by
$P^{\exists\text{-free}}\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Pos}}$
the subdoctrine of $P$ whose elements of the fibres
$P^{\exists\text{-free}}(A)$ are existential-free elements of $P(A)$.

Dualising the previous Definitions 3.1 and 3.2 we get the corresponding ones
for the universal quantifier.

######  Definition 3.4.

Let
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Pos}}$
be a universal doctrine and let $A$ be an object of $\mathcal{C}$. A predicate
$\alpha$ of the fibre $P(A)$ is said to be a universal splitting if it
satisfies the following weak universal property: for every predicate $\beta\in
P(A\times B)$ such that $\forall b\colon B.\beta(a,b)\vdash\alpha(a)$, there
exists an arrow $A\xrightarrow{g}B$ such that:

$\beta(a,g(a))\vdash\alpha(a).$

######  Definition 3.5.

Let
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Pos}}$
be a universal doctrine and let $I$ be an object of $\mathcal{C}$. A predicate
$\alpha$ of the fibre $P(I)$ is said to be universal-free if $P_{f}(\alpha)$
is a universal splitting for every morphism $A\xrightarrow{f}I$.

Again, employing the presentation of a doctrine via its internal language, the
property we require of the formula $i:I\;|\;\alpha(i)$, so that it is free
from universal quantifiers, is that, whenever $a:A\;|\;\forall
b:B.\beta(a,b)\vdash\alpha(f(a))$ for some term $a:A\;|\;f(a):I$, then there
is a term $a:A\;|\;g(a):B$ such that
$a:A\;|\;\beta(a,g(a))\vdash\alpha(f(a))$.

######  Definition 3.6.

Let
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Pos}}$
be an existential doctrine. We say that $P$ has enough existential-free
predicates if, for every object $I$ of $\mathcal{C}$ and every predicate
$\alpha\in P(I)$, there exist an object $A$ and an existential-free object
$\beta$ in $P(I\times A)$ such that $\alpha(i)\dashv\vdash\exists i\colon
I.\beta(i,a)$ (i.e. $\alpha=\exists_{\pi_{I}}\beta$).

Analogously, we have the following definition for universal doctrines.

######  Definition 3.7.

Let
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Pos}}$
be a universal doctrine. We say that $P$ has enough universal-free predicates
if, for every object $I$ of $\mathcal{C}$ and every predicate $\alpha\in PI$,
there exist an object $A$ and a universal-free object $\beta$ in $P(I\times
A)$ such that $\alpha(i)\dashv\vdash\forall i\colon I.\beta(i,a)$.

######  Definition 3.8.

Let
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Pos}}$
be an universal doctrine. Then we indicate by
$P^{\forall\text{-free}}\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Pos}}$
the subdoctrine of $P$ whose elements of the fibres
$P^{\forall\text{-free}}(A)$ are universal-free element of $P(A)$.

###  3.2 Skolem and Gödel doctrines

Building over the notions corresponding to quantifier-free elements in
doctrines we introduced in the previous section, we now define two particular
kinds of doctrines, called _Skolem doctrines_ and _Gödel doctrines_.

The _Skolem doctrine_ are so called because these doctrines satisfy a version
of the traditional principle of _Skolemisation_ , namely $\forall u\exists
x\alpha(u,x)\rightarrow\exists f\forall u\alpha(u,fu)$. The name _Gödel
doctrine_ is chosen because we will prove that these doctrines encapsulates in
a pure form the basic mathematical features of the Dialectica interpretation.

######  Definition 3.9.

A doctrine
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Pos}}$
is called a Skolem doctrine if:

  * (i)

the category $\mathcal{C}$ is cartesian closed;

  * (ii)

the doctrine $P$ is existential and universal;

  * (iii)

the doctrine $P$ has enough existential-free predicates;

  * (iv)

the existential-free objects of $P$ are stable under universal quantification,
i.e. if $\alpha\in P(A)$ is existential-free, then $\forall_{\pi}(\alpha)$ is
existential-free for every projection $\pi$ from $A$.

######  Remark 3.10.

The last point $(iv)$ of Definition 3.9 implies that, given a Skolem doctrine
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Pos}}$,
the sub-doctrine
$P^{\exists\text{-free}}\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Pos}}$
of existential-free predicates of $P$ as defined in 3.3 is a universal
doctrine. From a purely logical perspective, requiring existential-free
elements to be stable under universal quantification is quite natural since
this can be also read as _if_ $\alpha(x)$ _is an existential-free formula,
then $\forall x.\alpha(x)$ is again an existential-free formula_.

######  Proposition 3.11 (Skolemisation).

Every Skolem doctrine
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Pos}}$
validates the Skolemisation principle:

$a:A\;|\;\forall b:B.\exists c:C.\alpha(a,b,c)\dashv\vdash\exists
f:C^{B}.\forall b:B.\alpha(a,b,\textnormal{ev}(f,b))$

where $\alpha$ is any predicate in $P(A\times B\times C)$.

###### Proof.

Let us assume that $a:A\;|\;\gamma(a)\vdash\forall b.\exists c.\alpha(a,b,c)$
for some predicate $\gamma\in P(A)$. By point (iv) of Definition 3.9, we
assume without loss of generality that $\gamma(a)$ is existential-free:
otherwise there is an existential-free predicate $\gamma^{\prime}$ covering
$\gamma(a)$ and we get back to our hypothesis by using that $P$ is
existential.

Since $P$ is universal, it is the case that
$a:A,b:B\;|\;\gamma(a)\vdash\exists c.\alpha(a,b,c)$ and, being $\gamma(a)$
existential-free:

$a:A,b:B\;|\;\gamma(a)\vdash\alpha(a,b,g(a,b))$

for some term in context $a:A,b:B\;|\;g(a,b):C$. Being $\mathcal{C}$ cartesian
closed, there is a context $f:C^{B}$ together with a term in context
$f:C^{B},b:B\;|\;\textnormal{ev}(f,b):C$ such that there is a unique term in
context $a:A\;|\;h(a):C^{B}$ satisfying
$a:A,b:B\;|\;g(a,b)=\textnormal{ev}(h(a),b):C$. Hence:

$a:A,b:B\;|\;\gamma(a)\vdash\alpha(a,b,\textnormal{ev}(h(a),b))$

and $P$ being universal, it is the case that:

$a:A\;|\;\gamma(a)\vdash\forall b.\alpha(a,b,\textnormal{ev}(h(a),b)).$

Finally, since:

$a:A\;|\;\forall b.\alpha(a,b,\textnormal{ev}(h(a),b))\vdash\exists f.\forall
b.\alpha(a,b,\textnormal{ev}(f,b))$

(this holds for any predicate $\delta(a,-)$ in place of the predicate $\forall
b.\alpha(a,b,\textnormal{ev}(-,b))$) we conclude that:

$a:A\;|\;\gamma(a)\vdash\exists f.\forall b.\alpha(a,b,\textnormal{ev}(f,b)).$

We are done by taking $\forall b.\exists c.\alpha(a,b,c)$ as the predicate
$\gamma(a)$. ∎

######  Definition 3.12.

A doctrine
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Pos}}$
is called a Gödel doctrine if:

  1. (i)

$P$ is a Skolem doctrine;

  2. (ii)

the sub-doctrine
$P^{\exists\text{-free}}\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Pos}}$
of the existential-free predicates of $P$ has enough universal-free
predicates.

Now we have all the tools needed to introduce the notion of _quantifier-free
predicate_ in the categorical setting of Gödel doctrines.

######  Definition 3.13.

An element $\alpha$ of a fibre $P(A)$ of a Gödel doctrine $P$ that is both an
existential-free predicate of $P$ and a universal-free predicate in the sub-
doctrine $P^{\exists\text{-free}}$ of existential-free elements of $P$ is
called a quantifier-free predicate of $P$. The sub-doctrine of quantifier-free
elements is denoted by
$P^{\exists\forall\text{-free}}\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Pos}}$.

Therefore, given a Gödel doctrine
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Pos}}$,
we have the following canonical inclusions of doctrines:

$\textstyle{P^{\exists\forall\text{-free}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\iota_{1}}$$\textstyle{P^{\exists\text{-free}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\iota_{2}}$$\textstyle{P}$

where
$\textstyle{P^{\exists\forall\text{-free}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\iota_{1}}$$\textstyle{P^{\exists\text{-free}}}$
is a morphism of doctrines, while
$\textstyle{P^{\exists\text{-free}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\iota_{2}}$$\textstyle{P}$
is a morphism of universal doctrines.

######  Remark 3.14.

Notice that a universal-free element of the sub-doctrine
$P^{\exists\text{-free}}$ of a given Gödel doctrine $P$, may not be a
universal-free element in the whole doctrine $P$, because the universal
property of being universal-free is relative only to the elements of
$P^{\exists\text{-free}}$. Therefore, the quantifier-free elements of $P$ as
established in Definition 3.13 _are not the existential and universal free
elements_ of $P$.

In order to simplify the notation, but also to make clear the connection with
the logical presentation in the Dialectica interpretation, for a given Gödel
doctrine
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Pos}}$
we will use the notation $\alpha_{D}$ to indicate an element $\alpha$ of
$P^{\exists\forall\text{-free}}$, i.e. a quantifier-free predicate.

######  Theorem 3.15.

Let
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Pos}}$
be a Gödel doctrine, and let $\alpha$ be an element of $P(A)$. Then there
exists a quantifier-free predicate $\alpha_{D}$ of $P(I\times U\times X)$ such
that:

$i:I\;|\;\alpha(i)\dashv\vdash\exists u:U.\forall x:X.\alpha_{D}(i,u,x).$

###### Proof.

By definition of a Gödel doctrine, in particular since $P$ has enough-
existential free objects, there exists an existential-free element $\beta\in
P(A\times U)$ such that $i:I\;|\;\alpha(i)\dashv\vdash\exists u:U.\beta(i,u)$.
Then, since the subdoctrine of existential-free elements has enough-universal
free elements, we can conclude that there exists a quantifier-free predicate
$\alpha_{D}$ of $P(I\times U\times X)$ such that
$i:I\;|\;\alpha(i)\dashv\vdash\exists u:U.\forall x:X.\alpha_{D}(i,u,x)$. ∎

Theorem 3.15 shows that in a Gödel doctrine every formula admits a
presentation of the precise form used in the Dialectica translation.

The next result establishes the precise connection between Gödel doctrines and
the Dialectica interpretation. Employing the properties of a Gödel doctrine,
we can provide a complete categorical description and presentation of the
chain of equivalences involved in the Dialectica interpretation of
implicational formulae. In particular, we show that the crucial steps where
(IP) and (MP) are applied are represented categorically via the notions of
existential-free element and universal-free element.

######  Theorem 3.16.

Let
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Pos}}$
be a Gödel doctrine. Then for every $\psi_{D}\in P(I\times U\times X)$ and
$\phi_{D}\in P(I\times V\times Y)$ quantifier-free predicates of $P$ we have
that:

$i:I\;|\;\exists u.\forall x.\psi_{D}(i,u,x)\vdash\exists v.\forall
y.\phi_{D}(i,v,y)$

if and only if there exist $I\times U\xrightarrow{f_{0}}V$ and $I\times
U\times Y\xrightarrow{f_{1}}X$ such that:

$i:I,u:U,y:Y\;|\;\psi_{D}(i,u,f_{1}(i,u,y))\vdash\phi_{D}(i,f_{0}(i,u),y).$

###### Proof.

Let us consider two quantifier-free predicates $\psi_{D}\in P(I\times U\times
X)$ and $\phi_{D}\in P(I\times V\times Y)$ of the Gödel doctrine $P$. The
following equivalence follows by definition of left adjoint functor (for sake
of readability we omit the types of quantified variables):

$\displaystyle i:I\;|\;\exists u.\forall x.\psi_{D}(i,u,x)\vdash\exists
v.\forall y.\phi_{D}(i,v,y)$ $\displaystyle\iff$ $\displaystyle
i:I,u:U\;|\;\forall x.\psi_{D}(i,u,x)\vdash\exists v.\forall
y.\phi_{D}(i,v,y)$

Now we employ the fact that the predicate $\forall x.\psi_{D}(i,u,x)$ is
existential-free in the Gödel doctrine, obtaining that there exists an arrow
$I\times U\xrightarrow{f_{0}}V$, such that:

$\displaystyle i:I,u:U\;|\;\forall x.\psi_{D}(i,u,x)\vdash\exists v.\forall
y.\phi_{D}(i,v,y)$ $\displaystyle\iff$ $\displaystyle i:I,u:U\;|\;\forall
x.\psi_{D}(i,u,x)\vdash\forall y.\phi_{D}(i,f_{0}(i,u),y)$

Then, since the universal quantifier is right adjoint to the weakening
functor, we have that:

$\displaystyle i:I,u:U\;|\;\forall x.\psi_{D}(i,u,x)\vdash\forall
y.\phi_{D}(i,f_{0}(i,u),y)$ $\displaystyle\iff$ $\displaystyle
i:I,u:U,y:Y\;|\;\forall x.\psi_{D}(i,u,x)\vdash\phi_{D}(i,f_{0}(i,u),y).$

Now we employ the fact that $\phi_{D}(i,f_{0}(u),y)$ is universal-free in the
subdoctrine of existential-free elements of $P$. Notice that since
$\psi_{D}(i,u,x)$ is a quantifier-free element of the Gödel doctrine, we have
that $\forall x.\psi_{D}(i,u,x)$ is existential free. Recall that this follows
from the fact that in every Gödel doctrine, existential-free elements are
stable under universal quantification (this is the last point of Definition
3.12). Therefore, we can conclude that there exists an arrow $I\times U\times
Y\xrightarrow{f_{1}}X$ of $\mathcal{C}$ such that:

$\displaystyle i:I,u:U,y:Y\;|\;\forall
x.\psi_{D}(i,u,x)\vdash\phi_{D}(i,f_{0}(i,u),y)\iff$ $\displaystyle
i:I,u:U,y:Y\;|\;\psi_{D}(i,u,f_{1}(i,u,y))\vdash\phi_{D}(i,f_{0}(i,u),y)$

Then, combining the first and the last equivalences, we obtain the following
equivalence:

$i:I\;|\;\exists u.\forall x.\psi_{D}(i,u,x)\vdash\exists v.\forall
y.\phi_{D}(i,v,y)\iff$ there exist $(f_{0},f_{1})$ s.t.
$i:I,u:U,y:Y\;|\;\psi_{D}(i,u,f_{1}(i,u,y))\vdash\phi_{D}(i,f_{0}(i,u),y).$

∎

Notice that in Theorem 3.16, the arrow $I\times U\xrightarrow{f_{0}}V$
represents the _witness function_ , i.e. it assigns to every witness $u$ of
the hypothesis a witness $f_{0}(i,u)$ of the thesis, while the arrow $I\times
U\times Y\xrightarrow{f_{1}}X$ represents the _counterexample function_. While
the witness function $f_{0}(i,u)$ depends on the witness $u$ of the
hypothesis, the counterexample function $f_{1}(i,u,y)$ depends on a witness of
the hypothesis and on a counterexample of the thesis. This is a natural fact
because, under the constructive point of view, a counterexample has to be
relative to a witness validating the thesis.

Therefore, Theorem 3.16 shows that the notion of Gödel doctrine encapsulates
in a pure form the basic mathematical feature of the Dialectica
interpretation, namely its interpretation of implication, which corresponds to
the existence of functionals of types $f_{0}:I\times U\to V$ and
$f_{1}:I\times U\times Y\to X$ as described. One should think of this as
saying that a proof of a formula of the form $\exists u.\forall
x.\psi_{D}(i,u,x)\rightarrow\exists v.\forall y.\phi_{D}(i,v,y)$ is obtained
by transforming it to:

$\forall u.\exists v.\forall y.\exists
x.(\psi_{D}(i,u,x)\rightarrow\phi_{D}(i,v,y))$

by means of the Principle of Independence of Premises and Markov Principle,
and then Skolemising twice.

Therefore, combining Theorems 3.11, 3.15 and 3.16 we obtain strong evidence
that the notion of Gödel doctrine really provides the categorical abstraction
of the main concepts involved in the Dialectica translation. We discus this in
more details in the next subsection.

##  4 A characterisation of Dialectica doctrines

The concept of Dialectica category was originally introduced by de Paiva [5],
and it was generalised to the fibrational setting by Hofstra [14].

Let us briefly recall the notion of a Dialectica category
$\mathfrak{Dial}(\mathcal{C})$ associated to a finitely complete category
$\mathcal{C}$ (see [5] for further details):

  * •

An object of $\mathfrak{Dial}(\mathcal{C})$ is a triple $(U,X,\alpha)$, where
$\alpha$ is a subobject of $X\times U$ in $\mathcal{C}$. We think of such a
triple as a formula $\exists u.\forall x.\alpha(u,x)$.

  * •

An arrow from $\exists u.\forall x.\alpha(u,x)$ to $\exists v.\forall
y.\beta(v,y)$, for two objects $(U,X,\alpha)$ and $(V,Y,\beta)$ in
$\mathfrak{Dial}(\mathcal{C})$ is a pair $(U\xrightarrow{F}V,\,U\times
Y\xrightarrow{f}X)$ of arrows of $\mathcal{C}$, i.e. a pair:

$(u\colon U\;|\;F(u):V,\;\;\;u\colon U,y\colon Y\;|\;f(u,y):X)$

of terms in context (as usual, we are thinking of $\mathcal{C}$ as the
category of contexts associated to some type theory), satisfying the
condition:

$\alpha(u,f(u,y))\leq\beta(F(u),y)$

between the reindexed subobjects, where the squares:

$\textstyle{\alpha(u,f(u,y))\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\alpha\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{U\times
Y\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{{\langle\pi_{U},f\rangle}}$$\textstyle{U\times
X}$
$\textstyle{\beta(F(u),y)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\beta\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{U\times
Y\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{{F\times
1_{Y}}}$$\textstyle{V\times Y}$

are pullbacks.

Our notation is motivated by the notion of internal language of a doctrine
(see Section 2.2). In fact, a finitely complete category $\mathcal{C}$ is
nothing but an instance of a doctrine, if we look at $\mathcal{C}$ itself as a
category of contexts associated to some type theory and at the subobjects
$\alpha$ of a given object $X$ of $\mathcal{C}$ as the predicates $\alpha(x)$
in context $x\colon X$.

The notions of object and arrow of $\mathfrak{Dial}(\mathcal{C})$ are
motivated by Gödel’s notion of Dialectica interpretation (see [11]), and in
particular by its action on formulas in the language of arithmetic of the form
$A\to B$. In detail, we recall that one can define a many-sorted language
$\mathcal{L}$ together with an inductive notion of a formula $A^{D}$ of
$\mathcal{L}$, whenever $A$ is a given formula in the language of arithmetic.
The formula $A^{D}$ is in prenex normal form:

$\exists\vec{u}.\forall\vec{x}.A_{D}(\vec{u},\vec{x})$

for some inductively defined quantifier-free formula $A_{D}$ of $\mathcal{L}$.
Finally, there exists an $\mathcal{L}$-theory T, called System T, that enjoys
the quantifier-elimination property and that allows the interpretation
$(-)^{D}$ to satisfy the following:

######  Theorem 4.1 (Gödel 1958, Soundness).

Let $A$ be a formula in the language of arithmetic. Whenever
$\textsc{HA}\vdash A$, where HA is Heyting’s Arithmetic, then
$\textsc{T}\vdash A^{D}$ by means of an application of the rules of
introduction of quantifiers to $A_{D}$, that is:

$\textsc{T}\vdash A_{D}(\vec{t},\vec{x})$

for some (finite sequence of) closed terms $\vec{t}$.

in such a way that a result of relative consistency of HA holds: Heyting’s
Arithmetic is consistent, provided that the System T (which is quantifier-free
in $\mathcal{L}$) is.

We conclude the present subsection by recalling what $(A\to B)^{D}$ looks
like, so that the notion of $\mathfrak{Dial}(\mathcal{C})$ is justified, and
refer the reader to [11, 30] for further details. If $A$ and $B$ are formulas
in the language of arithmetic, then $(A\to B)^{D}$ is the formula:

$\exists F.\exists f.\forall u.\forall y.(\;A_{D}(u,f(u,y))\to
B_{D}(F(u),y)\;)$

of $\mathcal{L}$. Hence our notion of arrow of $\mathfrak{Dial}(\mathcal{C})$
is nothing but a categorical way of expressing the action of $(-)^{D}$ on
$A\to B$.

As we anticipated, the notion of Dialectica category was generalised to an
arbitrary fibration/doctrine by Hyland [15], Biering [2] and Hofstra [14], for
both a proof-irrelevant and a proof-relevant predicative settings. Here we
consider the proof-irrelevant version of this construction, associating a
doctrine $\mathfrak{Dial}(P)$ called a _dialectica doctrine_ to a given
doctrine $P$.

###  4.1 Dialectica doctrines

The notions of Dialectica category and Dialectica fibration are introduced in
terms of instances of a free construction called the _Dialectica construction_
, i.e. a category is called a _Dialectica category_ if it is the output of the
Dialectica construction.

From a modern categorical perspective, Dialectica categories or Dialectica
fibrations are the free algebras of the Dialectica pseudo-monad
$\mathfrak{Dial}(-)$, described by Hofstra [14]. Here we will deal with the
proof-irrelevant version of such construction:

Dialectica construction. Let
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Pos}}$
be a doctrine whose base category $\mathcal{C}$ is cartesian closed. The
dialectica doctrine
$\mathfrak{Dial}(P)\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Pos}}$
is defined as the functor sending:

  * •

an object $I$ into the poset $\mathfrak{Dial}(P)(I)$ defined as follows:

    * –

objects are quadruples $(I,U,X,\alpha)$ where $I,U$ and $X$ are objects of the
base category $\mathcal{C}$ and $\alpha\in P(I\times U\times X)$;

    * –

partial order: we stipulate that $(I,U,X,\alpha)\leq(I,V,Y,\beta)$ if there
exists a pair $(f_{0},f_{1})$, where $I\times U\xrightarrow{f_{0}}V$ and
$I\times U\times Y\xrightarrow{f_{1}}X$ are morphisms of $\mathcal{C}$ such
that:

$\alpha(i,u,f_{1}(i,u,y))\leq\beta(i,f_{0}(i,u),y).$

  * •

an arrow $J\xrightarrow{g}I$ into the poset morphism
$\mathfrak{Dial}(P)(I)\to\mathfrak{Dial}(P)(J)$ sending a predicate
$(I,U,X,\alpha)$ to the predicate:

$(J,U,X,\alpha(g(j),u,x)).$

######  Remark 4.2.

Let
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Pos}}$
be a doctrine and let $I$ be any object of $\mathcal{C}$. Then the poset
$\mathfrak{Dial}(P)(I)$ is isomorphic to the poset reflection of the
dialectica category associated to some category.

###  4.2 Dialectica doctrines via quantifier completions

This subsection is devoted to providing a categorical presentation of the
notion of Dialectica doctrine. Our aim is to connect the notion of Dialectica
construction to the one of a Gödel doctrine and show that, under certain
hypotheses, these notions are equivalent. In order to show this, we ask
ourselves when is it the case that a doctrine is an instance of a dialectica
construction and, in this case, which doctrine do we need to complete in order
to go back to the one we started from.

The main result we need is the following statement. (Here $Q^{\forall}$ and
$Q^{\exists}$ denote the universal and the existential completions of any
doctrine $Q$. We are going to recap these notions later.)

######  Proposition 4.3 (Hofstra [14]).

If
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Pos}}$
is a doctrine, then there is an isomorphism:

$\mathfrak{Dial}(P)\cong(P^{\forall})^{\exists}$

which is natural in $P$.

We briefly recall the notion of existential completion of a doctrine, see [31]
for more details:

Existential completion. Let
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Pos}}$
be a pos-doctrine. The existential completion
$P^{\exists}\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Pos}}$
of $P$ is the doctrine such that, for every object $A$ of $\mathcal{C}$, the
poset $P^{\exists}(A)$ is defined as follows:

  * •

objects: triples $(A,B,\alpha)$, where $A$ and $B$ are objects of
$\mathcal{C}$ and $\alpha$ is a predicate in $P(A\times B)$.

  * •

order: $(A,B,\alpha)\leq(A,C,\beta)$ if there exists an arrow $A\times
B\xrightarrow{f}C$ of $\mathcal{C}$ such that:

$\alpha(a,b)\vdash\beta(a,f(a,b))\textnormal{ \, \, ( i.e. }\alpha\leq
P_{\langle\pi_{A},f\rangle}(\beta)\textnormal{ )}$

in $P(A\times B)$ (here $A\times B\xrightarrow{\pi_{A}}A$ is the projection on
$A$).

Whenever $f$ is an arrow $A\to C$ of $\mathcal{C}$, the functor
$P^{\exists}(C)\xrightarrow{P^{\exists}_{f}}P^{\exists}(A)$ sends an object
$(C,D,\gamma)$ of $P^{\exists}(C)$ to the object:

$(A,D,\gamma(f(a),d))$ ( i.e. $(A,D,P_{\langle
f\pi_{A},\pi_{D}\rangle}(\gamma))$ )

of $P^{\exists}(A)$ (here $\pi_{A},\pi_{D}$ are the projections from $A\times
D$).

We think of a triple $(A,B,\alpha)$ in $P^{\exists}(A)$ as the predicate
$(\exists b\colon B)\alpha(a,b)$. This construction provides a free
completion, i.e. it extends to a 2-functor which is left adjoint to the
corresponding forgetful functor. We remind that the associated monad happens
to be lax-idempotent. Analogously, let us remind the notion of universal
completion of a doctrine:

Universal completion. Let
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Pos}}$
be a pos-doctrine. The universal completion
$P^{\forall}\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Pos}}$
of $P$ is the doctrine such that, for every object $A$ of $\mathcal{C}$, the
poset $P^{\forall}(A)$ is defined as follows:

  * •

objects: triples $(A,B,\alpha)$, where $A$ and $B$ are objects of
$\mathcal{C}$ and $\alpha$ is a predicate in $P(A\times B)$.

  * •

order: $(A,B,\alpha)\leq(A,C,\beta)$ if there exists an arrow $A\times
C\xrightarrow{g}B$ of $\mathcal{C}$ such that:

$\alpha(a,g(a,c))\vdash\beta(a,c)$

in $P(A\times C)$.

Again, if $f$ is an arrow $A\to C$ of $\mathcal{C}$, the functor
$P^{\forall}(C)\xrightarrow{P^{\forall}_{f}}P^{\forall}(A)$ sends an object
$(C,D,\gamma)$ of $P^{\forall}(C)$ to the object $(A,D,\gamma(f(a),d))$ of
$P^{\forall}(A)$.

We think of a triple $(A,B,\alpha)$ in $P^{\forall}(A)$ as the predicate
$(\forall b\colon B)\alpha(a,b)$. Finally, this construction provides a free
completion, i.e. it extends to a 2-functor which is right adjoint to the
obvious forgetful functor inducing a colax-idempotent monad. The universal and
the existential completions of a given doctrine $P$ are related by the
following natural isomorphism:

$P^{\forall}\cong(-)^{\operatorname{op}}((-)^{\operatorname{op}}P)^{\exists}$
(1)

where $(-)^{\operatorname{op}}$ is the functor
$\operatorname{\mathbf{Pos}}\to\operatorname{\mathbf{Pos}}$ which inverts the
order of any poset (see [33]).

We recall that the existential and universal completions are really well-
behaved, in the sense that the instances of such a completion can be
internally characterised without referring to a further doctrine that the
doctrine we are given is a completion of. That is what we talk about in the
following statements, contained in Proposition 4.4 (we refer to [31, 32] for a
proof of this statement and to [34] for its extension to its proof-relevant
version), where the latter follows from the former by means of the natural
isomorphism (1):

######  Proposition 4.4.

Let
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Pos}}$
be a doctrine. Assume that $P$ is existential. Then $P$ is an existential
completion of some other doctrine $P^{\prime}$ precisely when it has enough
existential-free predicates, i.e. when, for every predicate $a\colon
A\;|\;\alpha(a)$ of $P$, there is an existential-free predicate:

$a\colon A,b\colon B\;|\;\beta(a,b)$

of $P$ such that $\alpha(a)\cong(\exists b\colon B)\beta(a,b)$ in $P(A)$. In
this case, such a doctrine $P^{\prime}$ is the full sub-doctrine
$P^{\exists\text{-free}}$ of $P$ whose predicates are the existential-free
ones of $P$.

Analogously, if $P$ is a universal doctrine, then $P$ is a universal
completion of some doctrine $P^{\prime}$ precisely when it has enough
universal-free predicates, i.e. when, for every predicate $a\colon
A\;|\;\alpha(a)$ of $P$, there is a universal-free predicate:

$a\colon A,b\colon B\;|\;\beta(a,b)$

of $P$ such that $\alpha(a)\cong(\forall b\colon B)\beta(a,b)$ in $P(A)$. In
this case, such a doctrine $P^{\prime}$ is the full sub-doctrine
$P^{\forall\text{-free}}$ of $P$ whose predicates are the universal-free
predicates of $P$.

By means of the Proposition 4.4 above, the following result follows. This
provides a characterisation of the free-algebras of the monad
$\mathfrak{Dial}(-)$.

######  Theorem 4.5.

Let us assume that the category $\mathcal{C}$ is cartesian closed. Then the
doctrines
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Pos}}$
that are dialectica completions of some doctrine $P^{\prime}$ are precisely
those that are Gödel doctrines. Moreover, in this case, such a doctrine
$P^{\prime}$ is the full sub-doctrine $P^{\exists\forall\text{-free}}$ of the
quantifier-free predicates of $P$.

We end the current session with the following:

######  Remark 4.6.

The existential completion of a universal doctrine whose base is cartesian
closed happens to be universal as well (see [14] for more details). Therefore,
by Theorem 4.5, it is the case that Gödel doctrines happen to be both
existential and universal.

Complementing this description, one can also look at the dialectica completion
as a procedure to add the existential and the universal quantifications to the
predicative part of a type theory containing at least the simply typed lambda
calculus. Trotta and Spadetto [33] analyse which logical structure, that we
might assume to be already present in the predicative part of our type theory,
is preserved –or at least maintained– by this procedure.

##  5 Logical principles in Gödel doctrines

Gödel doctrines provide a categorical framework that generalises the principal
concepts underlying the Dialectica translation, such as the existence of
witness and counterexample functions, whenever we have an implication
$i:I\;|\;\exists u.\forall x.\psi_{D}(u,x,i)\vdash\exists v.\forall
y.\phi_{D}(v,y,i)$. The key idea is that, intuitively, the notion of
_existential-quantifier-free_ objects can be seen as a reformulation of the
_principle of independence of premises_ , while _product-quantifier-free_
objects can be seen as a reformulation of _Markov principle_. Notice that in
the proof of Theorem 3.16 existential and universal free elements play the
same role that (IP) and (MP) have in the Dialectica interpretation of
implicational formulae.

The main goal of this section is to formalise this intuition, showing the
exact connection between the principles (IP) and (MP) and Gödel first-order
hyperdoctrines.

Notation. to denote the rule-version of the logical principles we consider, we
will add R- to the name of principles. For example we will denote by (R-IP)
the rule:

$\top\vdash\theta\rightarrow\exists u.\eta(u)\ \text{ implies
}\top\vdash\exists u.(\theta\rightarrow\eta(u))$

corresponding to the principle of independence of premise (IP):

$\top\vdash(\theta\rightarrow\exists u.\eta(u))\rightarrow\exists
u.(\theta\rightarrow\eta(u))$

and similarly we will use (R-MP) for Markov rule.

###  5.1 Dialectica interpretation of implication

Gödel’s Dialectica interpretation [11, 10] associates to each formula $\phi$
in the language of arithmetic its _Dialectica interpretation_ $\phi^{D}$, i.e.
a formula of the form:

$\phi^{D}=\exists u.\forall x.\phi_{D}$

where $\phi_{D}$ is a quantifier-free formula in the language of system T,
trying to be _as constructive as possible_. The associations $(-)^{D}$ and
$(-)_{D}$ are defined inductively on the structure of the formulae, and we
refer to [11, 10] for a complete description. The most complicated clause of
the translation (and, in Gödel’s words, “the most important one”) is the
definition of the translation of the implication connective
$(\psi\rightarrow\phi)^{D}$. This involves two logical principles which are
usually not acceptable from an intuitionistic point of view, namely a form of
the _Principle of Independence of Premise_ (IP) and a generalisation of
_Markov Principle_ (MP). The interpretation is given by:

$(\psi\rightarrow\phi)^{D}=\exists V,X.\forall
u,y.(\psi_{D}(u,X(u,y))\rightarrow\phi_{D}(V(u),y)).$

The motivation provided in the collected works of Gödel for this translation
is that given a witness $u$ for the hypothesis $\psi_{D}$ one should be able
to obtain a witness for the conclusion $\phi_{D}$, i.e. there exists a
function $V$ assigning a witness $V(u)$ of $\phi_{D}$ to every witness $u$ of
$\psi_{D}$. Moreover, this assignment has to be such that from a
counterexample $y$ of the conclusion $\phi_{D}$ we should be able to find a
counterexample $X(u,y)$ to the hypothesis $\psi_{D}$. This transformation of
counterexamples of the conclusion into counterexamples for the hypothesis is
what gives Dialectica its essential bidirectional character.

We first recall the technical details behind the translation of
$(\psi\rightarrow\phi)^{D}$ ([10]) showing the precise points in which we have
to employ the non-intuitionistic principles (MP) and (IP). First notice that
$\psi^{D}\rightarrow\phi^{D}$, that is:

$\exists u.\forall x.\psi_{D}(u,x)\rightarrow\exists v.\forall
y.\phi_{D}(v,y)$ (2)

is equivalent to:

$\forall u.(\forall x.\psi_{D}(u,x)\rightarrow\exists v.\forall
y.\phi_{D}(v,y)).$ (3)

If we apply a special case of the Principle of Independence of Premise,
namely:

$\displaystyle(\forall x.\theta(x)\rightarrow\exists v.\forall
y.\eta(v,y))\rightarrow\exists v.(\forall x.\theta(x)\rightarrow\forall
y.\eta(v,y))$ (IP*)

we obtain that (3) is equivalent to:

$\forall u.\exists v.(\forall x.\psi_{D}(u,x)\rightarrow\forall
y.\phi_{D}(v,y)).$ (4)

Moreover, we can see that this is equivalent to:

$\forall u.\exists v.\forall y.(\forall
x.\psi_{D}(u,x)\rightarrow\phi_{D}(v,y)).$ (5)

The next equivalence is motivated by a generalisation of Markov’s Principle,
namely:

$\neg\forall x.\theta(u,x)\rightarrow\exists x.\neg\theta(u,x).$ (MP)

By applying (MP) we obtain that (5) is equivalent to:

$\forall u.\exists v.\forall y.\exists
x.(\psi_{D}(u,x)\rightarrow\phi_{D}(v,y)).$ (6)

To conclude that $\psi^{D}\rightarrow\phi^{D}=(\psi\rightarrow\phi)^{D}$ we
have to apply the Axiom of Choice (or Skolemisation), i.e.:

$\forall y.\exists x.\theta(y,x)\rightarrow\exists V.\forall y.\theta(y,V(y))$
(AC)

twice, obtaining that (6) is equivalent to:

$\exists V,X.\forall u,y.(\psi_{D}(u,X(u,y))\rightarrow\phi_{D}(V(u),y)).$

This analysis (from Gödel’s Collected Works, page 231) highlights the key role
the principles (IP), (MP) and (AC) play in the Dialectica interpretation of
implicational formulae. The role of the axiom of choice (AC) has been
discussed from a categorical perspective both by Hofstra [14] and in our
previous work [34]. We re-examine the two principles (IP) and (MP) in the next
subsections, following what we discussed in [34].

###  5.2 Independence of Premise

In logic and proof theory, the Principle of Independence of Premise states
that:

$(\theta\rightarrow\exists u.\eta(u))\rightarrow\exists
u.(\theta\rightarrow\eta(u))$

where $u$ is not a free variable of $\theta$. While this principle is valid in
classical logic (it follows from the law of the excluded middle), it does not
hold in intuitionistic logic, and it is not generally accepted constructively
[1]. The reason why the principle (IP) is not generally accepted
constructively is that, from a constructive perspective, turning any proof of
the premise $\phi$ into a proof of $\exists u.\eta(u)$ means turning a proof
of $\theta$ into a proof of $\eta(t)$ where $t$ is a witness for the
existential quantifier depending on the proof of $\theta$. In particular, the
choice of the witness _depends_ on the proof of the premise $\theta$, while
the (IP) principle tell us, constructively, that the witness can be chosen
independently of any proof of the premise $\theta$.

In the Dialectica translation we only need a particular version of the (IP)
principle:

$\displaystyle(\forall y.\theta(y)\rightarrow\exists u.\forall
v.\eta(u,v))\rightarrow\exists u.(\forall y.\theta(y)\rightarrow\forall
v.\eta(u,v))$ (IP*)

which means that we are asking (IP) to hold not for every formula, but only
for those formulas of the form $\forall y.\theta(y)$ with $\theta$ quantifier-
free. We recall a useful generalisation of the (IP*) principle, namely:

$\displaystyle(\theta\rightarrow\exists u.\eta(u))\rightarrow\exists
u.(\theta\rightarrow\eta(u))$ (IP)

where $\theta$ is $\exists$-free, i.e. $\theta$ contains neither existential
quantifiers nor disjunctions (of course, it is also assumed that $u$ is not a
free variable of $\theta$). Therefore, the condition that (IP) holds for every
formula of the form $\forall y.\theta(y)$ with $\theta(y)$ quantifier-free is
replaced by asking that it holds for every formula _free from the existential
quantifier_.

###  5.3 Markov Principle

Markov Principle is a statement that originated in the Russian school of
constructive mathematics. Formally, Markov principle is usually presented as
the statement:

$\neg\neg\exists x.\phi(x)\rightarrow\exists x.\phi(x)$

where $\phi$ is a quantifier-free formula. Thus, MP in the Dialectica
interpretation, namely:

$\neg\forall x.\phi(x)\rightarrow\exists x.\neg\phi(x)$ (MP)

with $\phi(x)$ a quantifier-free formula, can be thought of as a
generalisation of the Markov Principle above. As remarked in [1], the reason
why MP is not generally accepted in constructive mathematics is that in
general there is no reasonable way to choose constructively a witness $x$ for
$\neg\phi(x)$ from a proof that $\forall x.\phi(x)$ leads to a contradiction.
However, in the context of Heyting Arithmetic, i.e. when $x$ ranges over the
natural numbers, one can prove that these two formulations of Markov Principle
are equivalent. More details about the computational interpretation of Markov
Principle can be found in [25].

A natural generalisation of (MP) is given by the following principle, that we
call Modified Markov principle: i.e. whenever $\beta_{D}\in P(A)$ is a
quantifier-free predicate and $\alpha\in P(A\times B)$ is an existential-free
predicate, it is the case that:

$(\forall x.\phi(x)\rightarrow\psi(y))\rightarrow\exists
x.(\phi(x)\rightarrow\psi(y))$ (MMP)

where $\psi(y)$ is quantifier free, $\alpha(x)$ is existential-free and the
variable $x$ does not occur free in $\psi(y)$. Notice that (MP) is obtained by
(MMP) by replacying $\psi(y)$ with $\bot$.

###  5.4 Gödel hyperdoctrines

The main purpose of this subsection is to show in which sense the principles
(IP) and (MP) are satisfied in a Gödel hyperdoctrine. In this subsection we
deal with their rule versions. First we have to equip Gödel doctrines with the
appropriate Heyting structure in the fibres in order to be able to formally
express these principles. Therefore, we have to consider Gödel hyperdoctrines.

######  Definition 5.1.

A hyperdoctrine
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Hey}}$
is said a Gödel hyperdoctrine when $P$ is a Gödel doctrine.

Notice that from a logical perspective, one might want the quantifier-free
predicates to be closed with respect to all the propositional connectives,
since this is what happens in logic. However, for sake of generality, we start
requiring just the Heyting structures of the fibres and studying the logical
principles.

######  Theorem 5.2.

Every Gödel first-order hyperdoctrine
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Hey}}$
satisfies the _Rule of Independence of Premise_ , i.e. whenever $\beta\in
P(A\times B)$ and $\alpha\in P(A)$ is a existential-free predicate, it is the
case that:

$a:A\;|\;\top\vdash\alpha(a)\rightarrow\exists b.\beta(a,b)\mbox{ implies that
}a:A\;|\;\top\vdash\exists b.(\alpha(a)\rightarrow\beta(a,b)).$

###### Proof.

Let us assume that $a:A\;|\;\top\vdash\alpha(a)\rightarrow\exists
b.\beta(a,b)$. Then it is the case that $a:A\;|\;\alpha(a)\vdash\exists
b.\beta(a,b)$. Since $\alpha(a)$ is free from the existential quantifier, it
is the case that there is a term in context $a:A\;|\;t(a):B$ such that:

$a:A\;|\;\top\vdash\alpha(a)\rightarrow\beta(a,t(a)).$

Therefore, since:

$a:A\;|\;\alpha(a)\rightarrow\beta(a,t(a))\vdash\exists
b.(\alpha(a)\rightarrow\beta(a,b))$

(as this holds for any predicate $\gamma(a,-)$ in place of the predicate
$\alpha_{D}(a)\rightarrow\beta(a,-)$) we conclude that:

$a:A\;|\;\top\vdash\exists b.(\alpha(a)\rightarrow\beta(a,b)).$

∎

Similarly we can prove the following result.

######  Theorem 5.3.

Every Gödel first-order hyperdoctrine
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Hey}}$
satisfies the following _Modified Markov Rule_ , i.e. whenever $\beta_{D}\in
P(A)$ is a quantifier-free predicate and $\alpha\in P(A\times B)$ is an
existential-free predicate, it is the case that:

$a:A\;|\;\top\vdash(\forall b.\alpha(a,b))\rightarrow\beta_{D}(a)\mbox{
implies that }a:A\;|\;\top\vdash\exists
b.(\alpha(a,b)\rightarrow\beta_{D}(a)).$

###### Proof.

Let us assume that $a:A\;|\;\top\vdash(\forall
b.\alpha(a,b))\rightarrow\beta_{D}(a)$. Then it is the case that
$a:A\;|\;(\forall b.\alpha(a,b))\vdash\beta_{D}(a)$. Hence, since $\beta_{D}$
is quantifier-free and $\alpha$ is existential-free, there exists a term in
context $a:A\;|\;t(a):B$ such that:

$a:A\;|\;\top\vdash\alpha(a,t(a))\rightarrow\beta_{D}(a)$

therefore, since:

$a:A\;|\;\alpha(a,t(a))\rightarrow\beta(a)\vdash\exists
b.(\alpha(a,b)\rightarrow\beta_{D}(a))$

we can conclude that:

$a:A\;|\;\top\vdash\exists b.(\alpha(a,b)\rightarrow\beta_{D}(a)).$

∎

To obtain Markov rule from Theorem 5.3 we have to require the bottom element
to be quantifier-free.

######  Corollary 5.4.

Every Gödel first-order hyperdoctrine
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Hey}}$
such that $\bot$ is a quantifier-free predicate satisfies _Markov Rule_ , i.e.
for every quantifier-free element $\alpha_{D}\in P(A\times B)$ it is the case
that:

$b:B\;|\;\top\vdash\neg\forall a.\alpha_{D}(a,b)\mbox{ implies that
}b:B\;|\;\top\vdash\exists a.\neg\alpha_{D}(a,b).$

###### Proof.

It follows by Theorem 5.3 just by replacing $\beta_{D}$ with $\bot$, that is
quantifier-free by hypothesis. ∎

In Theorems 5.3 and 5.2 we proved that the universal properties of existential
and universal free elements allow us to prove that a Gödel first-order
hyperdoctrine satisfies Modified Markov Rule and the Rule of Independence of
Premise.

From a logical perspective, the intuition behind Theorem,5.2 is that the
existential-free elements of a Gödel first-order hyperdoctrine correspond to
formulae satisfying (R-IP). Similarly, we have that the elements of a Gödel
doctrine that are quantifier-free, are exactly those satisfying a (R-MMP) by
Theorem 5.3.

Notice also that applying the definitions of existential-free and universal-
free elements, we immediately obtain the following presentation of the _Rule
of Choice_ , see [22] (also called _explicit definability_ in [27]) and the
_Counterexample Property_ , previously defined in [33].

######  Corollary 5.5.

Every Gödel first-order hyperdoctrine
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Hey}}$
such that $\bot$ is a quantifier-free object satisfies the _Counterexample
Property_ , that is, whenever:

$a:A\;|\;\forall b.\alpha(a,b)\vdash\bot$

for some predicate $\alpha(a,b)\in P(A\times B)$, then it is the case that:

$a:A\;|\;\alpha(a,g(a))\vdash\bot$

for some term in context $a:A\;|\;g(a):B$.

######  Corollary 5.6.

Every Gödel first-order hyperdoctrine
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Hey}}$
such that $\top$ is existential-free satisfies the _Rule of Choice_ , that is,
whenever:

$a:A\;|\;\top\vdash\exists b.\alpha(a,b)$

for some existential-free predicate $\alpha\in P(A\times B)$, then it is the
case that:

$a:A\;|\;\top\vdash\alpha(a,g(a))$

for some term in context $a:A\;|\;g(a):B$.

###  5.5 Logical principles

In the previous results, we have seen which _rules_ hold in Gödel first-order
hyperdoctrines. This subsection is devoted to the analysis of the respective
logical _principles_ in Gödel first-order hyperdoctrines. In detail, we look
for the right hypotheses that allow us to produce models of the stronger
formulation of the rules as principles. The following theorem is the first of
this series of results and involves the Independence of Premise:

######  Theorem 5.7.

Every Gödel first-order hyperdoctrine
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Hey}}$
such that existential-free elements are closed with respect to finite
conjunctions satisfies the _Principle of Independence of Premise_ , i.e.
whenever $\beta\in P(A\times B)$ and $\alpha\in P(A)$ is an existential-free
predicate, it is the case that:

$a:A\;|\;\top\vdash(\alpha(a)\rightarrow\exists
b.\beta(a,b))\rightarrow\exists b.(\alpha(a)\rightarrow\beta(a,b)).$

###### Proof.

First, since every Gödel doctrine has enough existential-free elements, there
exists an existential-free element $\gamma(a,c)\in P(A\times C)$ such that:

$a:A\;|\;\exists c.\gamma(a,c)\dashv\vdash\alpha(a)\rightarrow\exists
b.\beta(a,b).$

In particular, we have that
$a:A,c:C\;|\;\gamma(a,c)\vdash\alpha(a)\rightarrow\exists b.\beta(a,b).$ Then
we have that:

$a:A,c:C\;|\;\gamma(a,c)\wedge\alpha(a)\vdash\exists b.\beta(a,b)$

and $\gamma(a,c)\wedge\alpha(a)$ is an existential-free elements, since both
$\gamma(a,c)$ and $\alpha(a)$ are existential-free elements and existential-
free elements are closed with respect finite conjunction by hypethesis.
Therefore, we can conclude that there exists a term $a:A,c:C\;|\;t(a,c):B$
such that:

$a:A,c:C\;|\;\gamma(a,c)\wedge\alpha(a)\vdash\beta(a,t(a,c)).$

Hence we have:

$a:A,c:C\;|\;\gamma(a,c)\vdash\alpha(a)\rightarrow\beta(a,t(a,c))$

and since $\alpha(a)\rightarrow\beta(a,t(a,c)$ is exaclty
$(\alpha(a)\rightarrow\beta(a,b))[t(a,c)/b]$ and it always holds that:

$a:A,c:C\;|\;(\alpha(a)\rightarrow\beta(a,b))[t(a,c)/b]\vdash\exists
b.(\alpha(a)\rightarrow\beta(a,b))$

we can conclude that:

$a:A,c:C\;|\;\gamma(a,c)\vdash\exists b.(\alpha(a)\rightarrow\beta(a,b)).$

Therefore we get that:

$a:A\;|\;\exists c.\gamma(a,c)\vdash\exists
b.(\alpha(a)\rightarrow\beta(a,b)).$

and, since $a:A\;|\;\exists
c.\gamma(a,c)\dashv\vdash\alpha(a)\rightarrow\exists b.\beta(a,b)$, it is the
case that:

$a:A\;|\;\top\vdash(\alpha(a)\rightarrow\exists
b.\beta(a,b))\rightarrow\exists b.(\alpha(a)\rightarrow\beta(a,b)).$

∎

As a corollary of the previous result, we obtain the following presentation of
the principle (IP*) introduced in Section 5.2 in terms of Gödel first-order
hyperdoctrines. We recall that (IP*) is precisely the form of the Priciple of
Independece of Premise we need in the Dialectica interpretation.

######  Corollary 5.8.

Every Gödel first-order hyperdoctrine
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Hey}}$
such that the existential-free elements are closed with respect to finite
conjunction satisfies (IP*), i.e. whenever $\beta\in P(C\times B)$ and
$\alpha_{D}\in P(A)$ is an quantifier-free predicate, it is the case that:

$-|\;\top\vdash(\forall a.\alpha_{D}(a)\rightarrow\exists b.\forall
c.\beta(c,b))\rightarrow\exists b.(\forall a.\alpha_{D}(a)\rightarrow\forall
c.\beta(c,b)).$

###### Proof.

It follows from Theorem 5.7 and from the fact that if $\alpha_{D}$ is
quantifier-free then $\forall a.\alpha_{D}$ is existential-free. ∎

Similarly, we can prove the following result for Markov principle.

######  Theorem 5.9.

Every Gödel first-order hyperdoctrine
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Hey}}$
such that existential-free elements are closed with respect to implication
satisfies the following _Modified Markov principle_ , i.e. whenever
$\beta_{D}\in P(A)$ is a quantifier-free predicate and $\alpha\in P(A\times
B)$ is an existential-free predicate, it is the case that:

$a:A\;|\;\top\vdash(\forall
b.\alpha(a,b)\rightarrow\beta_{D}(a))\rightarrow\exists
b.(\alpha(a,b)\rightarrow\beta_{D}(a)).$

###### Proof.

Since $\alpha$ is an existential-free predicate and $\beta_{D}$ is quantifier-
free we have that $\forall b.\alpha(a,b)\rightarrow\beta_{D}(a)$ is an element
of $P^{\exists\text{-free}}(A)$. Thus, since $P^{\exists\text{-free}}$ has
enough quantifier-free elements by defintion of Gödel doctrine, there exists
an universal-free predicate of $P^{\exists\text{-free}}$, i.e. a quantifier-
free predicate $\sigma_{D}\in P^{\exists\text{-free}}(\times C)$ such that
$a:A\;|\;\forall c.\sigma_{D}(a,c)\dashv\vdash\forall
b.\alpha(a,b)\rightarrow\beta_{D}(a)$. In particular, we have that
$a:A\;|\;\forall c.\sigma_{D}(a,c)\wedge\forall
b.\alpha(a,b)\vdash\beta_{D}(a)$, and hence $a:A\;|\;\forall c.\forall
b.(\sigma_{D}(a,c)\wedge\alpha(a,b))\vdash\beta_{D}(a)$. Now, since
$\beta_{D}$ is quantifier-free, i.e. it is universal-free in
$P^{\exists\text{-free}}$, there exist two terms $a:A\;|\;t(a):B$ and
$a:A\;|\;t^{\prime}(a):C$ such that:

$a:A\;|\;\sigma_{D}(a,t^{\prime}(a))\wedge\alpha(a,t(a))\vdash\beta_{D}(a).$

Therefore we have that
$a:A\;|\;\sigma_{D}(a,t^{\prime}(a))\vdash(\alpha(a,b)\rightarrow\beta_{D}(a))[t(a)/b]$.
Now, since we always have that $a:A\;|\;\forall
c.\sigma_{D}(a,c)\vdash\sigma_{D}(a,t^{\prime}(a))$ and
$a:A\;|\;(\alpha(a,b)\rightarrow\beta_{D}(a))[t(a)/b]\vdash\exists
b.(\alpha(a,b)\rightarrow\beta_{D}(a))$, we can conclude that:

$a:A\;|\;\top\vdash(\forall
b.\alpha(a,b)\rightarrow\beta_{D}(a))\rightarrow\exists
b.(\alpha(a,b)\rightarrow\beta_{D}(a)).$

∎

To obtain the usual presentation of Markov Principle as corollary of Theorem
5.9, we simply have to require the bottom element $\bot$ of a Gödel first-
order hyperdoctrine to be _quantifier-free_.

######  Corollary 5.10.

Every Gödel first-order hyperdoctrine
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Hey}}$
such that existential-free elements are closed with respect to implication and
$\bot$ is a quantifier-free predicate satisfies _Markov Principle_ , i.e. for
every quantifier-free element $\alpha_{D}\in P(A\times B)$ it is the case
that:

$b:B\;|\;\top\vdash\neg\forall a.\alpha_{D}(a,b)\rightarrow\exists
a.\neg\alpha_{D}(a,b).$

###### Proof.

It follows by Theorem 5.9 just by replacing $\beta_{D}$ with $\bot$, that is
quantifier-free by hypothesis. ∎

We have proved that under suitable hypotheses, a Gödel first-order
hyperdoctrine satisfies (IP), (MP), (GMP) and the principle of Skolemisation.

Therefore, combining Theorem 5.7, Theorem 5.9 (and Corollary 5.10), and
Proposition 3.11, we can repeat the chain of equivalences we provided in
Section 5.1, and obtain the following main result.

######  Theorem 5.11.

Let
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Hey}}$
be a Gödel first-order hyperdoctrine such that:

  * •

existential-free elements are closed with respect to implication and finite
conjunction;

  * •

falsehood $\bot$ is a quantifier-free predicate.

Then for every $\psi_{D}$ in $P(I\times U\times X)$ and $\phi_{D}$ in
$P(I\times V\times Y)$ quantifier-free predicates of $P$ we have that the
formula:

$i:I\;|\;\exists u.\forall x.\psi_{D}(i,u,x)\to\exists v.\forall
y.\phi_{D}(i,v,y)$

is provably equivalent to:

$i:I\;|\;\exists f_{0},f_{1}.\forall
u,y.(\psi_{D}(i,u,f_{1}(i,u,y))\rightarrow\phi_{D}(i,f_{0}(i,u),y)).$

Theorem 5.11 fully represents a categorical version of the translation of the
implication connective in the Dialectica interpretation. In particular, it
shows that the equivalence
$(\psi\rightarrow\phi)^{D}\leftrightarrow(\psi^{D}\rightarrow\phi^{D})$
presented in Section 5.1 is perfectly modelled by a Gödel first-order
hyperdoctrine satisfying the natural additional closure properties of Theorem
5.11.

######  Remark 5.12.

Observe that Theorem 5.11 can be considered a stronger version of Theorem
3.16. Hence, once more, it converts the rule stated in the latter theorem into
an actual principle.

In detail, by the thesis of Theorem 5.11, it is enough to observe that the
first sequent of the statement of Theorem 3.16 is equivalent to the sequent:

$i:I\;|\;\top\vdash\exists u.\forall x.\psi_{D}(i,u,x)\to\exists v.\forall
y.\phi_{D}(i,v,y)$

by the elimination and introduction rules for the implication, and that the
second one is equivalent to the following:

$i:I\;|\;\top\vdash\exists f_{0},f_{1}.\forall
u,y.(\psi_{D}(i,u,f_{1}(i,u,y))\rightarrow\phi_{D}(i,f_{0}(i,u),y)).$

For this second equivalence one applies the implicational elimination and
introduction to convert the second sequent of 3.16 into:

$i:I,u:U,y:Y\;|\;\top\vdash\psi_{D}(i,u,f_{1}(i,u,y))\rightarrow\phi_{D}(i,f_{0}(i,u),y)$

which is actually equivalent to $i:I\;|\;\top\vdash\exists f_{0},f_{1}.\forall
u,y.(\psi_{D}(i,u,f_{1}(i,u,y))\rightarrow\phi_{D}(i,f_{0}(i,u),y))$, by
Corollary 5.6 and being the formula:

$i:I\;|\;\forall
u,y.(\psi_{D}(i,u,f_{1}(i,u,y))\rightarrow\phi_{D}(i,f_{0}(i,u),y))$

existential-free.

Theorem 5.11 follows as a consequence of the fragment of first-order logic
under which the internal language of a Gödel first-order hyperdoctrine is
closed. Observe that this fragment contains at least the whole intuitionistic
first-order logic together with the Principle of Independence of Premise, the
Modified Markov Principle and the Principle of Skolemisation. These
principles, together with the rules of intuitionistic first-order logic are
precisely what is needed to get the equivalence
$(\psi\rightarrow\phi)^{D}\leftrightarrow(\psi^{D}\rightarrow\phi^{D})$ in a
Gödel first-order hyperdoctrine.

Clearly any boolean doctrine satisfies these principles as well, as it models
every inference rule of classic first-order logic. However, in general they
are not satisfied by a usual hyperdoctrine, because they are not necessarily
true in intuitionistic first-order logic. It turns out that the fragment of
first-order logic modelled by a Gödel hyperdoctrine is right in-between the
intuitionistic first-order logic and the classical first-order logic: it is
powerful enough to guarantee the equivalences in Section 5.1 that justify the
Dialectica interpretation of the implication.

##  6 Tripos-to-topos and Gödel doctrines

The tripos-to-topos construction was originally introduced in [28, 16] as a
generalisation of the construction of the category of sheaves of a locale.
Recently, this construction has been proved to be an instance of the exact
completion of an elementary existential doctrine, we refer to [24, 22] for all
the details. Let us briefly recall it.

Tripos-to-topos. Given a first-order hyperdoctrine
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Hey}}$,
the category $\mathsf{T}_{P}$ consists of:

  * •

objects: are pairs $(A,\rho)$ where $\rho\in P(A\times A)$ satisfies:

    * –

_symmetry:_ $a_{1},a_{2}:A\;|\;\rho(a_{1},a_{2})\vdash\rho(a_{2},a_{1})$;

    * –

_transitivity:_
$a_{1},a_{2},a_{3}:A\;|\;\rho(a_{1},a_{2})\wedge\rho(a_{2},a_{3})\vdash\rho(a_{1},a_{3})$.

  * •

arrows $(A,\rho)\xrightarrow{\phi}(B,\sigma)$: are objects $\phi\in P(A\times
B)$ such that:

    1. 1.

$a:A,b:B\;|\;\phi(a,b)\wedge\rho(a,a)\vdash\sigma(b,b)$;

    2. 2.

$a_{1},a_{2}:A,b:B\;|\;\rho(a_{1},a_{2})\wedge\phi(a_{1},b)\vdash\phi(a_{2},b)$;

    3. 3.

$a:A,b_{1},b_{2}:B\;|\;\sigma(b_{1},b_{2})\wedge\phi(a,b_{1})\vdash\phi(a,b_{2})$;

    4. 4.

$a:A,b_{1},b_{2}:B\;|\;\phi(a,b_{1})\wedge\phi(a,b_{2})\vdash\sigma(b_{1},b_{2})$;

    5. 5.

$a:A\;|\;\rho(a,a)\vdash\exists b.\phi(a,b)$.

Then the following holds:

######  Theorem 6.1.

Let
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Hey}}$
be a hyperdoctrine. Then $\mathsf{T}_{P}$ is an exact category.

The construction of the category $\mathsf{T}_{P}$ can be presented in the more
general context of elementary and existential doctrines, and it is also called
the exact completion of the elementary existential doctrine $P$, since it
lifts to an adjunction between the 2-category of exact categories and that of
elementary and existential doctrine. We refer to [24, Cor. 3.4] for a complete
description of the construction in the general case.

###  6.1 Tripos-to-topos and exact completions

We recall from [32] a useful characterisation of the tripos-to-topos
construction of a first-order hyperdoctrine arising as an existential
completion. Again, in the present work we present the results for
hyperdoctrines, but the characterisation presented in [32] works for an
arbitrary elementary and existential doctrine.

To properly present such a characterisation we first need to recall from [22,
24, 23] the construction of the category of _predicates_ of a first-order
hyperdoctrine. The construction of this category is related to the
_comprehension and comprehensive diagonal completion_.

######  Definition 6.2.

Given a first-order hyperdoctrine
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Hey}}$
we define the comprehension completion
$P_{c}\colon\mathcal{G}_{P}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Hey}}$
of $P$ as follows:

  * •

an object of $\mathcal{G}_{P}$ is a pair $(A,\alpha)$ where $A$ is a set and
$\alpha\in P(A)$;

  * •

an arrow $(A,\alpha)\xrightarrow{f}(B,\beta)$ is an arrow $A\xrightarrow{f}B$
such that:

$a:A\;|\;\alpha(a)\vdash\beta(f(a)).$

The fibres $P_{c}(A,\alpha)$ are given by those elements $\gamma$ of $P(A)$
such that $a:A\;|\;\gamma(a)\vdash\alpha(a)$ (i.e. $\gamma\leq\alpha$).
Moreover, the action of $P_{c}$ on a morphism $f:(B,\beta)\ \rightarrow\
(A,\alpha)$ is defined as $P_{c}(f)(\gamma)=P_{f}(\gamma)\,\wedge\,\beta$ i.e.
the predicate:

$b:B\;|\;\gamma(f(b))\wedge\beta(b)$

where $\gamma\in P(A)$ is such that $\gamma\leq\alpha$.

Similarly, the construction which freely adds comprehensive diagonal is
provided by the _extensional reflection_. We denote
$\delta_{A}:=\exists_{\Delta}(\top_{A})$. According to the internal language
of a given doctrine $P$, the element $\delta_{A}\in P(A\times A)$ corresponds
to the predicate:

$a_{1}\colon A,a_{2}\colon A\;|\;a_{1}=a_{2}.$

######  Definition 6.3.

Given an elementary doctrine
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Hey}}$
we can define extensional reflection
$P_{x}\colon\mathcal{X}_{P}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Pos}}$
of $P$ as follows: the base category $\mathcal{X}_{P}$ is the quotient
category of $\mathcal{C}$ with respect to the equivalence relation where
$f\sim g$ when:

$\top\vdash f(a)=g(a)\textnormal{ \, \, ( i.e. }\top_{A}\leq P_{\langle
f,g\rangle}(\delta_{B})\textnormal{ in category-theoretic notation )}$

in context $a\colon A$, for two parallel arrows $f,g\colon A\to B$. The
equivalence class of a morphism $f$ of $\mathcal{C}$, i.e. an arrow of
$\mathcal{X}_{P}$, is denoted by $[f]$.

Finally, we denoted by $\mathbf{Pred}(P)$ the category of predicates of a
doctrine $P$, i.e. the category defined as:

$\mathbf{Pred}(P):=\mathcal{X}_{P_{c}}$

where $P_{c}$ is the comprehension completion of $P$. Again, we refer to [22,
24, 23] for a complete description of these constructions. Now we have all the
instruments to recall the characterisation of tripos-to-topos of existential
completions from [32]. Such a characterisation essentially shows that every
tripos-to-topos of an existential completion is an instance of
$(-)_{\mathsf{ex}/\mathsf{lex}}$ completion, namely the exact completion of a
lex category in the sense of [4, 3].

######  Theorem 6.4.

Let
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Hey}}$
be a first-order hyperdoctrine. Then we have the equivalence:

$\mathsf{T}_{P^{\exists}}\equiv\mathbf{Pred}(P)_{\mathsf{ex}/\mathsf{lex}}$

of exact categories.

###  6.2 Tripos-to-topos for Gödel first-order hyperdoctrines

We recall that a Gödel first-order hyperdoctrine is in particular the
existential completion of its subdoctrine of existential-free elements by
Theorem 4.5 and Proposition 4.4. Therefore, we are able (i.e. have the
necessary conditions for) to apply Theorem 6.4 and can conclude the following
characterisation of the tripos-to-topos construction of Gödel first-order
hyperdoctrines:

######  Theorem 6.5.

Let
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Hey}}$
be a Gödel first-order hyperdoctrine. The the equivalence of exact categories:

$\mathsf{T}_{P}\equiv\mathbf{Pred}(P^{\exists\text{-free}})_{\mathsf{ex}/\mathsf{lex}}$

holds.

We recall from [28, 16] that when a doctrine is a tripos, then its tripos-to-
topos is a topos. Hence, we have the following corollary for Gödel first-order
hyperdoctrines:

######  Corollary 6.6.

Let
$P\colon\mathcal{C}^{\operatorname{op}}\longrightarrow\operatorname{\mathbf{Hey}}$
be a Gödel first-order hyperdoctrine. If $P$ is a tripos, then
$\mathbf{Pred}(P^{\exists\text{-free}})_{\mathsf{ex}/\mathsf{lex}}$ is a
topos.

Given this corollary we might be tempted to call these toposes Dialectica
toposes. These are however different from Biering’s Dialectica toposes.

######  Remark 6.7.

The notion of _Dialectica topos_ was introduced in [2] as the tripos-to-topos
of a suitable tripos called _dialectica tripos_. In [13] Hofstra characterises
triposes arising in terms of ordered PCAs equipped with a filter. This
characterisation includes Effective Topos-like triposes, but also the triposes
for relative, modified and extensional realisability and the dialectica
tripos. Therefore, the dialectica tripos can been seen as a tripos araising
from a suitable ordered PCA. Triposes given by PCAs are known to be instances
of a general completion that freely adds left adjoints along arbitrary maps.
Hofstra was the first to obserce this fact, see [13, 12], but later in [8] and
[32] it is proved that the construction identified by Hofstra is a particular
case of the full existential completion of a primary doctrine.

In this paper we have proposed a different approach to the definition of
doctrines related to dialectica interpretation, focusing on the logical
principles and rules we need to properly translate the implication connective
as in the Dialectica. Therefore, we could say that our approach is more
syntactic, and not related to realisability in general. The Dialectica tripos
introduced in [2] is not a Gödel doctrine in general, since Gödel doctrines
are given by an existential completion just along projections (and by a
universal completion), while the Dialectica tripos is an instance of the full
existential completion. Therefore the Dialectica tripos satisfies different
structural properties with respect to an arbitrary Gödel doctrine. For
example, the Dialectica tripos has left adjoints along every arrow, satisfying
Beck Chevalley conditions, while in an arbitrary Gödel doctrine the Beck
Chevalley conditions are not satisfied along arbitrary maps. Employing the
universal properties of the existential and universal completions, one can
show that the Dialectica tripos just contains a Gödel doctrine, but it is not
equivalent to such a doctrine.

We can also relate this work to Maietti’s work on Joyal’s arithmetic
universes.

######  Remark 6.8.

Observe that categories arising as tripos-to-topos results of Gödel first-
order hyperdoctrines have the same abstract presentation as the so called
_Joyal-arithmetic universes_ introduced by Maietti in [21]. Recall that a
Joyal-arithmetic universe is defined as the exact completion
$\mathbf{Pred}(\mathcal{S})_{\mathsf{ex}/\mathsf{lex}}$ of the category of
predicates of a Skolem theory $\mathcal{S}$ as defined in [21, Def. 2.2],
namely a cartesian category with a parameterised natural numbers object where
all the objects are finite products of the natural numbers object.

##  7 Conclusion

This article is the culmination of various intertwined investigations begun in
[34] and [35]. Inspired by Hofstra [14] and Hyland [15], as well as by the
work of Maietti and Trotta [32], itself inspired by Trotta [31], we embarked
in the programme of expanding the characterisation of the categorical version
of the Dialectica Interpretation, to complete the work in Hofstra as far as
the characterisation of the Dialectica is concerned and to make sure that all
the logical principles involved in the interpretation are represented in the
categorical models obtained.

Since the work on the fibrational setting seemed too abstract and hard to
grasp, especially for the logic audience we intended to communicate with, we
opted for descriptions on the level of hyperdoctrines in [35] and [36], where
the doctrines are the poset reflections of the fibrations used early on. This
crystallised our understanding of the issue of quantifier-free formulae in the
categorical setting, but also made clear the import of non-intuitionistic
principles such as Independence of Premise and the Markov Principle, that had
been discussed by logicians, but not in categorical terms, as far as we are
aware. Our investigation is, so far, restricted to the environment of the
Dialectica interpretation, but it has wider reach, helping to complete the
program of categorification of logic, as originally suggested by Lawvere.

We hope to carry on exploring other side issues of this investigation. We
started connecting this work to the work on categorical realisability and
computability, as described by Pitt’s tripos theory and the tripos to topos
construction [28] in the final section of this article, but much remains to be
done. A different direction that we have not even started to explore is the
extension of our work to generalised versions of the Dialectica
interpretation, as already hinted in the text, to dependent type theory [26].
Finally the work in the original Dialectica category model [6] has had several
applications to computer science problems like concurrency theory, in the
shape of Petri Nets [7] and others [38]. We plan to investigate if these and
other applications can be improved by our doctrinal version of the models.

## References

  * [1] J. Avigad and S. Feferman.  Gödel’s functional (Dialectica) interpretation.  Handbook of Proof Theory, 137, 02 1970.
  * [2] B. Biering.  Dialectica interpretations – a categorical analysis (PhD Thesis).  2008\.
  * [3] A. Carboni and R. Celia Magno.  The free exact category on a left exact one.  Journal of the Australian Mathematical Society. Series A. Pure Mathematics and Statistics, 33(3):295–301, 1982.
  * [4] A. Carboni and E.V. Vitale.  Regular and exact completions.  Journal of Pure and Applied Algebra, 125(1):79 – 116, 1998.
  * [5] V. de Paiva.  The Dialectica categories.  Categories in Computer Science and Logic, 92:47–62, 1989.
  * [6] V. de Paiva.  The Dialectica categories, phd thesis.  Technical report, University of Cambridge, Computer Laboratory, 1991.
  * [7] E. di Lavore, W. Leal, and V. de Paiva.  Dialectica petri nets.  arXiv, 2105.12801, 2021.
  * [8] J. Frey.  Categories of partial equivalence relations as localizations.  preprint, 2020.
  * [9] J.Y. Girard.  Linear logic.  Theoretical computer science, 50(1):1–101, 1987.
  * [10] K. Gödel, S. Feferman, et al.  Kurt Gödel: Collected Works: Volume II: Publications 1938-1974, volume 2.  Oxford University Press, 1986.
  * [11] K. Gödel.  Über eine bisher noch nicht benützte erweiterung des finiten standpunktes.  Dialectica, 12(3-4):280–287, 1958.
  * [12] P. Hofstra.  Completions in Realizability.  PhD thesis, Universiteit Utrecht, 2003.
  * [13] P. Hofstra.  All realizability is relative.  Mathematical Proceedings of the Cambridge Philosophical Society, 141(2):239–264, 2006.
  * [14] P. Hofstra.  The Dialectica monad and its cousins.  Models, logics, and higherdimensional categories: A tribute to the work of Mihály Makkai, 53:107–139, 2011.
  * [15] J.M. Hyland.  Proof theory in the abstract.  Annals of Pure and Applied Logic, 114(1):43 – 78, 2002.  Troelstra Festschrift.
  * [16] J.M. Hyland and A.M. Johnstone, P.T.and Pitts.  Tripos theory.  Math. Proc. Camb. Phil. Soc., 88:205–232, 1980.
  * [17] U. Kohlenbach.  Gödel’s functional interpretation and its use in current mathematics.  Dialectica, 62(2):223–267, 2008.
  * [18] F.W. Lawvere.  Adjointness in foundations.  Dialectica, 23:281–296, 1969.
  * [19] F.W. Lawvere.  Diagonal arguments and cartesian closed categories.  In Category Theory, Homology Theory and their Applications, volume 2, page 134–145. Springer, 1969.
  * [20] F.W. Lawvere.  Equality in hyperdoctrines and comprehension schema as an adjoint functor.  In A. Heller, editor, New York Symposium on Application of Categorical Algebra, volume 2, page 1–14. American Mathematical Society, 1970\.
  * [21] M.E. Maietti.  Joyal’s arithmetic universe as list-arithmetic pretopos.  Theory and Applications of Categories, 24(3):39–83, 2010.
  * [22] M.E. Maietti, F. Pasquali, and G. Rosolini.  Triposes, exact completions, and Hilbert’s $\varepsilon$-operator.  Tbilisi Mathematical Journal, 10, 11 2017.
  * [23] M.E. Maietti and G. Rosolini.  Quotient completion for the foundation of constructive mathematics.  Log. Univers., 7(3):371–402, 2013.
  * [24] M.E. Maietti and G. Rosolini.  Unifying exact completions.  Appl. Categ. Structures, 23:43–52, 2013.
  * [25] M. Manighetti.  Computational interpretations of Markov’s principle, 2016.
  * [26] S.K. Moss and T. von Glehn.  Dialectica models of type theory.  In 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, page 739–748, New York, NY, USA, 2018. Association for Computing Machinery.
  * [27] T. Nemoto and M. Rathjen.  The independence of premise rule in intuitionistic set theories, 11 2019\.
  * [28] A. M. Pitts.  Tripos theory in retrospect.  Math. Struct. in Comp. Science, 12:265–279, 2002.
  * [29] A.M. Pitts.  Categorical logic.  In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 6, pages 39–.129. Oxford Univ. Press, 1995.
  * [30] A.S. Troelstra.  Metamathematical Investigation of Intuitionistic Arithmetic and Analysis.  Springer, Berlin, 1973.
  * [31] D. Trotta.  The Existential Completion.  Theory and Applications of Categories, 35:1576–1607, 2020.
  * [32] D. Trotta and M.E. Maietti.  Generalized existential completions and their regular and exact completions.  arXiv, 2021.
  * [33] D. Trotta and M. Spadetto.  Quantifier completions, choice principles and applications.  arXiv, 2020.
  * [34] D. Trotta, M. Spadetto, and V. de Paiva.  The Gödel Fibration.  In 46th International Symposium on Mathematical Foundations of Computer Science (2021), volume 202 of LIPIcs, pages 87:1–87:16, 2021\.
  * [35] D. Trotta, M. Spadetto, and V. de Paiva.  Dialectica logical principles.  In S. Artemov and A. Nerode, editors, Logical Foundations of Computer Science, pages 346–363, Cham, 2022. Springer International Publishing.
  * [36] D. Trotta, M. Spadetto, and V. de Paiva.  Dialectica logical principles, not only rules.  Manuscript (submitted), 2022.
  * [37] J. van Oosten.  Realizability: An Introduction to its Categorical Side.  ISSN. Elsevier Science, 2008.
  * [38] G. Winskel.  Making concurrency functional.  arXiv, 2202.13910, 2022.