paper-qcoh.tex

\documentclass[oneside,reqno]{amsart}

\usepackage[utf8]{inputenc}
\usepackage[english]{babel}
\usepackage{amsthm,mathtools,stmaryrd,amssymb,graphicx,color}
\usepackage{booktabs}
\usepackage[all]{xy}
\usepackage[protrusion=true,expansion=true]{microtype}
\usepackage{xspace}

% lifted from https://arxiv.org/abs/1506.08870
\DeclareFontFamily{U}{min}{}
\DeclareFontShape{U}{min}{m}{n}{<-> udmj30}{}
\newcommand\yon{\!\text{\usefont{U}{min}{m}{n}\symbol{'210}}\!}

\usepackage[natbib=true,style=numeric,maxnames=10]{biblatex}
\usepackage[babel]{csquotes}
\bibliography{paper-qcoh.bib}

\title{A general Nullstellensatz for generalized spaces}
\author{Ingo Blechschmidt}
\email{ingo.blechschmidt@univr.it}

\theoremstyle{definition}
\newtheorem{defn}{Definition}[section]
\newtheorem{ex}[defn]{Example}

\theoremstyle{plain}
\newtheorem{prop}[defn]{Proposition}
\newtheorem{cor}[defn]{Corollary}
\newtheorem{lemma}[defn]{Lemma}
\newtheorem{thm}[defn]{Theorem}
\newtheorem{scholium}[defn]{Scholium}

\theoremstyle{remark}
\newtheorem{rem}[defn]{Remark}
\newtheorem{question}[defn]{Question}
\newtheorem{speculation}[defn]{Speculation}
\newtheorem{caveat}[defn]{Caveat}
\newtheorem{conjecture}[defn]{Conjecture}

\newenvironment{indentblock}{%
  \list{}{\leftmargin\leftmargin}%
  \item\relax
}{%
  \endlist
}

\newcommand{\xra}[1]{\xrightarrow{#1}}
\newcommand{\aaa}{\mathfrak{a}}
\newcommand{\bbb}{\mathfrak{b}}
\newcommand{\mmm}{\mathfrak{m}}
\newcommand{\C}{\mathcal{C}}
\newcommand{\I}{\mathcal{I}}
\newcommand{\J}{\mathcal{J}}
\newcommand{\E}{\mathcal{E}}
\newcommand{\F}{\mathcal{F}}
\newcommand{\B}{\mathcal{B}}
\renewcommand{\AA}{\mathbb{A}}
\newcommand{\EE}{\mathbb{E}}
\newcommand{\NN}{\mathbb{N}}
\newcommand{\RR}{\mathbb{R}}
\newcommand{\TT}{\mathbb{T}}
\newcommand{\OO}{\mathbb{O}}
\newcommand{\ZZ}{\mathbb{Z}}
\newcommand{\QQ}{\mathbb{Q}}
\renewcommand{\SS}{\mathbb{S}}
\renewcommand{\O}{\mathcal{O}}
\newcommand{\defeq}{\vcentcolon=}
\newcommand{\op}{\mathrm{op}}
\DeclareMathOperator{\Spec}{Spec}
\DeclareMathOperator{\Hom}{Hom}
\DeclareMathOperator{\Sh}{Sh}
\DeclareMathOperator{\PSh}{PSh}
\DeclareMathOperator{\rank}{rank}
\DeclareMathOperator{\length}{length}
\DeclareMathOperator{\List}{List}
\DeclareMathOperator{\id}{id}
\newcommand{\Set}{\mathrm{Set}}
\newcommand{\Eff}{\mathrm{Ef{}f}}
\renewcommand{\_}{\mathpunct{.}\,}
\newcommand{\effective}{ef{}fective\xspace}
\newcommand{\?}{\,{:}\,}
\newcommand{\realizes}{\Vdash}
\newcommand{\notnot}{\emph{not~not}\xspace}
\usepackage{soul}\setul{0.3ex}{}
\let\oldul\ul
\renewcommand{\ul}[1]{\text{\oldul{$#1$}}}
\newcommand{\affl}{\ensuremath{{\ul{\AA}^1}}\xspace}
\newcommand{\speak}[1]{\ulcorner\text{\textnormal{#1}}\urcorner}
\newcommand{\brak}[1]{\llbracket #1 \rrbracket}
\newcommand{\Mod}[1]{{#1}\mathrm{\text{-}mod}}

\newcommand{\stacksproject}[1]{\cite[{\href{https://stacks.math.columbia.edu/tag/#1}{Tag~#1}}]{stacks-project}}

\renewcommand{\paragraph}[1]{\noindent\textbf{#1.}}

\newcommand{\ZFC}{\textsc{zfc}}

\newcommand{\seq}[1]{\mathrel{\vdash\!\!\!_{#1}}}

\begin{document}

\begin{abstract}
  We give a general Nullstellensatz for the generic model of a
  geometric theory, useful as a source of nongeometric sequents validated by
  the generic model, and characterize the first-order and higher-order formulas validated by the
  generic model.
\end{abstract}

\maketitle
\thispagestyle{empty}

\begin{center}
  \textcolor{red}{\textbf{-- rough draft --}}

  \emph{comments welcome at ingo.blechschmidt@univr.it}
\end{center}

\section{Introduction}
\label{sect:introduction}

\paragraph{Generic models} Let~$\TT$ be a geometric theory, such as the theory
of rings, the theory of local rings or the theory of intervals. We follow Caramello's
terminology~\cite{caramello:tst} to mean by \emph{geometric theory} a system
% XXX: The terminology is not due to Olivia, right? Find better expression
given by a set of sorts, a set of finitary function symbols, a set of finitary
relation symbols and a set of axioms consisting of geometric sequents
(sequents of the form~$\varphi \seq{\vec x} \psi$ where~$\varphi$ and~$\psi$
are geometric formulas, that is formulas built from equality and the relation
symbols by the logical connectives~${\top}\,{\bot}\,{\wedge}\,{\vee}\,{\exists}$
and by arbitrary set-indexed disjunctions~$\bigvee$). By (infinitary) \emph{first-order
formula} we will mean a formula which may contain, additionally to the
connectives allowed for geometric formulas, the connectives~${\Rightarrow}$
and~${\forall}$.

A fundamental result is that there is a \emph{generic model}~$U_\TT$ of~$\TT$.
This model is \emph{conservative} in that
for any geometric sequent~$\sigma$, the following notions
coincide:
\begin{enumerate}
\item The sequent~$\sigma$ is provable modulo~$\TT$.
\item The sequent~$\sigma$ holds for any~$\TT$-model in any Grothendieck topos.
\item The sequent~$\sigma$ holds for~$U_\TT$.
\end{enumerate}
One could argue that it is this model which we
implicitly refer to when we utter the phrase ``Let~$M$ be
a~$\TT$-model.''.\footnote{For instance, this point of view is fundamental to
the slogan \emph{continuity is geometricity}, as stressed by
Vickers~\cite{vickers:continuity}.}
It can
typically not be realized as a set-theoretic model, consisting of a set for
each sort, a function for each function symbol and so on; instead it is a model
in a custom-tailored syntactically constructed Grothendieck topos, the
\emph{classifying topos}~$\Set[\TT]$ of~$\TT$, hence consists of an object
of~$\Set[\TT]$ for each sort, a morphism for each function symbol and so on.

To state what it means for a~$\TT$-structure in a topos~$\E$ to verify the
axioms of~$\TT$, rendering it a model, the \emph{internal language} of~$\E$ is
used, roughly reviewed in Section~\ref{sect:review-language} below. We write~``$\E
\models \alpha$'' to mean that a formula~$\alpha$ holds from the internal
point of view of~$\E$. Since this language is a form of a higher-order
intuitionistic extensional dependent type theory, the classifying topos~$\Set[\TT]$ can
be regarded as a higher-order completion of the geometric theory~$\TT$. The
generic model enjoys the universal property that any~$\TT$-model in any
(Grothendieck) topos~$\E$ is the pullback of~$U_\TT$ along an essentially
unique geometric morphism~$\E \to \Set[\TT]$.
\medskip

\paragraph{Nongeometric sequents} Crucially, the
equivalence~$(1)\Leftrightarrow(2)\Leftrightarrow(3)$ relating
provability and truth in~$\Set[\TT]$ only pertains to geometric sequents. The
generic model may validate additional nongeometric sequents which are not
provable from the axioms of~$\TT$ in first-order or even higher-order logic,
and these nongeometric sequents may be quite surprising and have useful
consequences.

One of the most celebrated such sequents arises in the case that~$\TT$ is the
theory of local rings. In this case, the classifying topos~$\Set[\TT]$ is also
known as the \emph{big Zariski topos} of~$\Spec(\ZZ)$ from algebraic geometry,
the topos of sheaves over the site of schemes locally of finite presentation,
and the generic model is the functor~$\affl$ of points of the affine line, the
functor which maps any scheme~$X$ (l.o.f.p.) to~$\Hom_\mathrm{Sch}(X,\mathbb{A}^1) =
\O_X(X)$.

From the point of view of the Zariski topos, the ring object~$\affl$ is not only a
local ring, but even a field in the sense that
any nonzero element is invertible.
As this condition is of nongeometric form, it is not inherited by arbitrary
local rings, which are indeed typically not fields. However, any intuitionistic
consequence of this condition which is of geometric form is inherited
by any local ring in any topos. Hence we may, when verifying a general fact
about local rings which is expressible as a geometric sequent,
suppose without loss of generality that the field axioms holds.
This observation is due to Kock~\cite{kock:univ-proj-geometry}, who exploited it to
develop projective geometry over local rings, and was further used by Reyes to
prove a Jacobian criterion for étale morphisms~\cite{reyes:cramer}.

We surmise that many more reduction techniques along these lines exist for
other kinds of algebraic objects. However, when actually using such techniques
in practice, we face the challenge that while we can use them to prove results
about \emph{all} local rings, \emph{all} modules and so on, it is difficult to
incorporate specific information about a particular local ring or a particular
module at hand. This difficulty is compounded by the fact that interesting
nongeometric properties are typically not inherited by the generic model of
quotient theories -- for instance the generic ring validates the formula~$\forall
x\?U_\TT\_ \neg\neg(x = 0)$ while the generic local ring does not.

Hence it is useful to turn to geometric theories which refer to a given
mathematical object. For instance, given a ring~$A$, there is the theory of
local localizations of~$A$, and its classifying topos is known in algebraic
geometry as the little Zariski topos of~$A$, the topos of sheaves over the
spectrum of~$A$. If~$A$ is reduced, this topos validates the dual field condition that any
noninvertible element is zero. This property has been used to give a short and
even constructive proof of Grothendieck's generic freeness lemma,
substantially improving on previously published
proofs~\cite{blechschmidt:generic-freeness}.

In time, further nongeometric sequents holding in the big Zariski topos of an
arbitrary base scheme have been found~\cite[Section~18.4]{blechschmidt:phd}. These include:
\begin{itemize}
\item $\affl$ is \emph{anonymously algebraically closed} in the sense that
any monic polynomial~$p \? \affl[T]$ of degree at least one does \notnot have a
zero. \smallskip
\item The Nullstellensatz holds:
Let $f_1,\ldots,f_m \in \affl[X_1,\ldots,X_n]$ be polynomials without a common
zero in~$(\affl)^n$. Then there are polynomials~$g_1,\ldots,g_m \in
\affl[X_1,\ldots,X_n]$ such that~$\sum_i g_i f_i = 1$. \smallskip
\item Any function~$\affl \to \affl$ is given by a unique polynomial. \smallskip
\item $\affl$ is microaffine: Let~$\Delta = \{ \varepsilon \?
\affl \,|\, \varepsilon^2 = 0 \}$. Let~$f : \Delta \to \affl$ be an arbitrary
function. Then there are unique elements~$a, b \? \affl$ such
that~$f(\varepsilon) = a + b \varepsilon$ for all~$\varepsilon \? \Delta$. \smallskip
\item $\affl$ is \emph{synthetically quasicoherent}: For any
finitely presentable~$\affl$-algebra~$A$, the canonical homomorphism~$A \to
(\affl)^{\Spec(A)}$, where~$\Spec(A)$ is defined as the set
of~$\affl$-algebra homomorphisms~$A \to \affl$, is bijective.
\end{itemize}
% Take care: In sect:applications, we state that each of these nongeometric
% sequents also holds in the ring classifier.
All of these nongeometric sequents are useful for the purposes of synthetic
algebraic geometry, the desire to carry out algebraic geometry in a language
close to the simple language of the 19th and the beginning of the 20th century
while still being fully rigorous and fully general, working over arbitrary base
schemes instead of restricting to the field of complex numbers.

Nontrivial nongeometric sequents are not an exclusive feature of sheaf toposes.
The generic model of a theory of presheaf type typically also validates such
sequents. For instance, all of the aforementioned properties of the generic
local ring are shared by the generic ring, which lives in the presheaf
topos~$[\mathrm{Ring}_\mathrm{fp}, \Set]$.
\medskip


\paragraph{Characterizing nongeometric sequents} Referring to the field condition in the little Zariski topos,
Tierney remarked around the time that those sequents were first
studied that ``[it] is surely important, though its precise significance is
still somewhat obscure---as is the case with many such nongeometric
formulas''~\cite[p.~209]{tierney:spectrum}. In view of their importance, is
there a way to discover nongeometric sequents in a systematic fashion? To
characterize the nongeometric sequents holding in classifying toposes? To this
end, Wraith put forward a specific conjecture~\cite[p.~336]{wraith:intuitionistic-algebra}:
\begin{quote}
\emph{The problem of characterising all the non-geometric properties of a generic
model appears to be difficult. If the generic model of a geometric theory~$\TT$
satisfies a sentence~$\alpha$ then any geometric consequence of $\TT + \alpha$ has to be a
consequence of~$\TT$. We might call~$\alpha$ $\TT$-redundant. Does the
generic~$\TT$-model satisfy all~$\TT$-redundant sentences?}
\end{quote}
Because classical logic is conservative over intuitionistic logic for geometric
sequents, this question has a trivial negative answer: No, any instance of the
law of excluded middle over the signature of~$\TT$ is~$\TT$-redundant but
typically not validated by the generic~$\TT$-model. Moreover,
Bezem, Buchholtz and
Coquand recently showed that the answer is still negative even if appropriate
care is taken to exclude these
counterexamples~\cite{bezem-buchholtz-coquand:syntactic-forcing-models}. Hence our
characterization of the first-order theory validated by the generic~$\TT$-model
is necessarily more nuanced.

Our starting point was the empirical
observation~\cite[p.~164]{blechschmidt:phd} that in the case of the big
Zariski topos, every true known nongeometric sequent followed from just a
single such, namely the synthetic quasicoherence of the generic
model, and in earlier work we surmised that one could formulate an appropriate
metatheorem explaining this observation and generalizing it to arbitrary
classifying toposes~\cite[Speculation~22.1]{blechschmidt:phd}. This hope turned
out to be true, in the sense we will now indicate.
\medskip


\paragraph{A general Nullstellensatz} To explain the relevant background, the
somewhat vague question ``to which extent does the classifying
topos~$\Set[\TT]$ realize that it is the classifying topos for~$\TT$?'' is useful as
a guiding principle. This is easiest to visualize with a concrete example
for~$\TT$, such as the theory of rings.

Let~$A$ be a ring. A simple version of the classical Nullstellensatz states:
\emph{For any polynomials~$f$ and~$g$ over~$A$, if any zero of~$f$ is also a
zero of~$g$, then there is a polynomial~$h$ such that~$g = hf$.} The
polynomial~$h$ can be regarded as an ``algebraic certificate'' of the
hypothesis. This principle holds for instance in the case that~$A$ is an
algebraically closed field and~$g$ is the unit polynomial. We will see
below that it is also
true, without any restriction on~$g$, for the generic ring.

We could try to generalize the Nullstellensatz to arbitrary geometric theories~$\TT$ as
follows: \emph{For any geometric sequent~$\sigma$, if~$\sigma$ holds for a
given~$\TT$-model~$M$ then~$\sigma$ is provable modulo~$\TT$.} In place of the
algebraic certificate we now have a logical certificate, a \emph{proof}
of~$\sigma$.

However, this generalized statement is typically false, even for
the generic model~$U_\TT$: The statement
\begin{multline*}
  \qquad\qquad\qquad\Set[\TT] \models \ulcorner\text{for any geometric sequent~$\sigma$,} \\
    \text{if~$\sigma$ holds for~$U_\TT$ then~$\ul{\TT}$
    proves~$\sigma$}\urcorner\qquad\qquad\qquad
\end{multline*}
does not hold.\footnote{Here~$\ul{\TT}$ is the internal geometric theory induced
by~$\TT$, obtained by pulling back the set of sorts, the set of function
symbols and so on along the geometric morphism~$\Set[\TT] \to \Set$. For
instance, if~$\TT$ is the theory of rings, then from the internal point of view
of~$\Set[\TT]$ the theory~$\ul{\TT}$ will again be the theory of rings.
More details will be given in Section~\ref{sect:review-theories}. The corner quotes indicate
that for sake of readability, the translation into formal language is to be
carried out by the reader. \par The displayed statement is much stronger than
the statement that for any geometric sequent~$\sigma$, if $\Set[\TT] \models
\speak{$\sigma$ holds for~$U_\TT$}$ then~$\TT$ proves~$\sigma$. This latter statement,
where the universal quantifier and the ``if \ldots then'' have been pulled out,
is true.} In this sense~$\Set[\TT]$ does not believe that~$U_\TT$ is the
generic~$\ul{\TT}$-model.

A concrete counterexample is as follows. Let~$\TT$ be the theory of rings and let~$\sigma$ be
the sequent~$(\top \vdash 1 + 1 = 0)$. Since there is an intuitionistic proof
that~$\TT$ does not prove~$\sigma$ and toposes are sound with respect to
intuitionistic logic, the statement~$\speak{\ul{\TT} proves~$\sigma$}$ is false
from the internal point of view of~$\Set[\TT]$. However, it is not the case
that the statement~$\speak{$1 + 1 = 0$ in~$U_\TT$}$ is false from the internal
point of view. In fact, this statement holds in a nontrivial slice
of~$\Set[\TT]$, the open subtopos coinciding with the classifying topos of
the theory of rings of characteristic two.

Intuitively, the problem is that while the meaning of~$\speak{$\ul{\TT}$
proves~$\sigma$}$ is fixed, the meaning of~$\speak{$\sigma$ holds for~$U_\TT$}$ varies
with the slice, as~$U_\TT$ shifts shape on different stages. This mismatch is solved by passing from~$\ul{\TT}$ to a
varying theory, the internal theory~$\ul{\TT}/U_\TT$ defined in
Section~\ref{sect:main}. If~$\TT$ is the theory of rings, then~$\ul{\TT}/U_\TT$
is the~$\Set[\TT]$-theory of~$U_\TT$-algebras.
Unlike~$\ul{\TT}$, this theory is not the pullback of an external geometric
theory. We then have, subject to some qualifications made precise in
Section~\ref{sect:main}, the following general Nullstellensatz:

\begin{thm}\label{thm:nullstellensatz0}
Let~$\TT$ be a geometric theory. Then, internally to~$\Set[\TT]$:
\begin{equation}\tag{$\dagger$}\label{eq:nullstellensatz0}
\text{A geometric$^*$ sequent~$\sigma$ holds for~$U_\TT$ if and only
if~$\ul{\TT}/U_\TT$ proves~$\sigma$.}
\end{equation}
\end{thm}

To illustrate Theorem~\ref{thm:nullstellensatz0}, let~$\TT$ be the theory of
rings and let~$\sigma$ be the sequent~$(f(x) = 0 \seq{x} g(x) = 0)$ for some
polynomials~$f$ and~$g$. To say that~$\sigma$ holds for~$U_\TT$ amounts to
saying that any zero~$x \? U_\TT$ of~$f$ is also a zero of~$g$, and to say
that~$\ul{\TT}/U_\TT$ proves~$\sigma$ amounts to saying that
in~$U_\TT[X]/(f(X))$, the free~$U_\TT$-algebra on one generator~$X$ subject to
the relation~$f(X) = 0$, the relation~$g([X]) = 0$ holds. Hence we obtain
an algebraic Nullstellensatz:
\[ \Set[\TT] \models
  \forall f,g \? U_\TT[X]\_ \bigl(
    (\forall x \? U_\TT\_ f(x) = 0 \Rightarrow g(x) = 0) \Longleftrightarrow
      \exists h \? U_\TT[X]\_ g = hf\bigr). \]

The statement~\eqref{eq:nullstellensatz0} is not a geometric sequent. Therefore
it is not to be expected that it passes from~$\Set[\TT]$ to a
subtopos~$\Set[\TT']$ corresponding to a quotient theory~$\TT'$ of~$\TT$, and
indeed in general it does not. However, there is still a useful substitute,
which we formulate as Corollary~\ref{corollary:nullstellensatz-horn}. This substitute
broadens the scope of the Nullstellensatz and is, whenever applicable, useful
for simplifying computations.

Summarizing, the situation is as follows.
\begin{itemize}
\item The generic model~$U_\TT$ is a
conservative~$\TT$-model. \smallskip
\item The topos~$\Set[\TT]$ does not believe that~$U_\TT$ is a
conservative~$\ul{\TT}$-model. \smallskip
\item The topos~$\Set[\TT]$ does believe that~$U_\TT$
is a conservative$^\star$~$\ul{\TT}/U_\TT$-model.
\end{itemize}

Theorem~\ref{thm:nullstellensatz0} is a source of nongeometric sequents. Indeed,
it is the universal such source in the sense that any first-order formula
which holds for~$U_\TT$ can be deduced from~\eqref{eq:nullstellensatz0}:

\begin{thm}\label{thm:characterization0}
Let~$\TT$ be a geometric theory. Let~$\varphi$ be a first-order
formula over the signature of~$\TT$. Then the following statements are
equivalent.
\begin{enumerate}
\item The formula~$\varphi$ holds for~$U_\TT$. \smallskip
\item The formula~$\varphi$ is provable in first-order intuitionistic logic
modulo the axioms of~$\TT$ and the additional axiom~\eqref{eq:nullstellensatz0}.
\end{enumerate}
\end{thm}

It is not entirely obvious how to correctly formalize
axiom~\eqref{eq:nullstellensatz0} in unadorned first-order logic, and in
fact, we do not believe that an entirely faithful formalization is possible.
We will resolve this issue in the body of this note, where we will restate
Theorem~\ref{thm:characterization0} in a more precise form (Theorem~\ref{thm:characterization}).

Theorem~\ref{thm:characterization0} characterizes the first-order formulas
which hold for the generic model. We could of course wish for a more explicit
characterization; but since even the characterization of geometric sequents
holding for the generic model (they are precisely those which are provable in
geometric logic modulo~$\TT$) is of a rather implicit nature, this wish appears
unfounded.

We stress that our characterization is more explicit than the tautologous
characterization (``a first-order formula holds for~$U_\TT$ iff it is provable
modulo~$\TT'$, where~$\TT'$ is the first-order theory whose set of axioms is the
set of first-order formulas satisfied by~$U_\TT$'') and the (incorrect)
characterization ``a first-order formula holds for~$U_\TT$ iff it
is~$\TT$-redundant''. Indeed, if~$\TT$ happens to be coherent and recursively
axiomatizable, then in stating Theorem~\ref{thm:characterization0} we may
restrict to coherent existential fixed-point logic, and the resulting theory
will again be recursively axiomatizable.
\medskip


% XXX: mention internal language in general, and SDG?
\paragraph{Related work} The topos-theoretic Nullstellensatz is related to
several precursors. A corollary of the Nullstellensatz is that, over the
first-order theory validated by~$U_\TT$, any first-order formula is in fact
logically equivalent to a geometric formula. This corollary has already been
observed by Butz and Johnstone~\cite[Lemma~4.2]{butz-johnstone:first-order}. At
that point, a characterization of the first-order formulas in the general case,
of the form as in Theorem~\ref{thm:characterization0}, was still missing.

The higher-order variant of our Nullstellensatz
(Theorem~\ref{thm:definability}) relativizes Cara\-mel\-lo's completeness
theorem~\cite[Theorem~2.4(ii)]{caramello:definability}. Her theorem is the
external statement that any subobject of~$U_\TT$ is given by the interpretation
of a geometric formula over the signature of~$\TT$; our relativization states
that, internally to~$\Set[\TT]$, any subset of~$U_\TT$ is given by a
geometric$^\star$ formula over the signature of~$\ul{\TT}/U_\TT$. As in the
first-order case, the passage from the external to the internal phrasing
necessitates the switch from~$\TT$ to~$\ul{\TT}/U_\TT$.

The Nullstellensatz yields for a given (perhaps conditional) truth about the
generic model a proof modulo the axioms of~$\ul{\TT}/U_\TT$. As illustrated in
Section~\ref{sect:applications}, the procedure we typically use to extract
fruitful information from such a proof is to apply it to a
further~$\ul{\TT}/U_\TT$-model which we specifically construct for the purposes
at hand. Hence we go from truth in~$U_\TT$ via provability to truth in a
further model, that is, we use provability as a (one-way) \emph{bridge}:
\[ \xymatrix{
  & \text{$\ul{\TT}/U_\TT$ proves $\sigma$} \\
  \text{$\sigma$ holds for $U_\TT$} \ar@/^1.1pc/@{<=>}[ur] &&
  \text{$\sigma$ holds for $M$} \ar@/_1.1pc/@{<=}[ul]
} \]
This perspective is inspired by Caramello's research
program~\cite{caramello:tst}, though it is not an instance of her main technical
device for establishing bridges, namely exploiting the fact that a single topos
may admit descriptions using quite different sites.
\medskip


\paragraph{Outlook} The Nullstellensatz yields a description of the first-order
and higher-order theory validated by the generic model of a geometric theory.
As already indicated, with more examples and details to be given in
Section~\ref{sect:applications}, this description explains and puts into
perspective several established results and observations.

From the point of view of applications, the main task for the future is to
explore the description in the case of particular geometric theories of
interest. Just as the reduction technique ``any reduced ring is a field'' --
valid because the generic localization of a reduced ring is a field -- enabled
a short and simple proof of Grothendieck's generic freeness
lemma~\cite[Section~11.5]{blechschmidt:phd}, more reduction techniques along
these lines should exist in a wide range of subjects. We hope that with the
Nullstellensatz at hand, the discovery of such techniques can progress in a more
systematic fashion.

From the point of view of theory, the appropriate context for the
Nullstellensatz should be determined. We formulate the Nullstellensatz in the
context of geometric theories and their classifying Grothendieck toposes, but
there should be analogues of the Nullstellensatz in other contexts where it
makes sense to speak of ``classifying gadgets'', and these analogues should
shed light on the topos-theoretic version and ideally even explain it from deeper
principles. In particular, preliminary computations indicate that there is a
version of the Nullstellensatz for arithmetic universes, the predicative cousin
of toposes introduced by Joyal and recently an important object of
consideration by Maietti and Vickers~\cite{maietti:au,maietti-vickers:induction,vickers:sketches}.
\medskip


\paragraph{Outline} In Section~\ref{sect:review}, we review background on the
internal language of toposes, classifying toposes and internal geometric theories.
Section~\ref{sect:main} contains proofs of the main theorems in the
full generality of geometric theories. Restricting to Horn theories allows for
a treatment which is more algebraic and less logical in flavor. For the benefit
of readers with a more algebraic background, we include a mostly self-contained
account of the Horn case as Section~\ref{sect:horn}. We generalize our main
theorems to the higher-order case in Section~\ref{sect:higher-order} and
conclude with applications in Section~\ref{sect:applications}.

Throughout we work in a constructive metatheory, to allow our results to be
interpreted internally to toposes.
\medskip


\paragraph{Acknowledgments} XXX
% don't forget: Thierry, and Steve and Martín for 6WFTop; also of course
% Alexander. Also include grant statement.


\section{Background}
\label{sect:review}

\subsection{Background on the internal language of Grothendieck toposes}
\label{sect:review-language}

% XXX


\subsection{Background on classifying toposes}
\label{sect:review-classifying-toposes}

We use the usual convention of abbreviating~``$x_1\?X_1,\ldots,x_n\?X_n$''
as~``$\vec x \? \vec X$'' or even just~``$\vec x$''.

\begin{defn}The \emph{syntactic site}~$\C_\TT$ of a geometric theory~$\TT$ has:
\begin{enumerate}
\item as objects \emph{geometric formulas in contexts}~$\{x_1\?X_1,\ldots,x_n\?X_n\_
\varphi\}$ where~$\varphi$ is a geometric formula over the signature of~$\TT$
in the displayed context; \smallskip
\item as set~$\Hom_{\C_\TT}(\{\vec x\_ \varphi\}, \{\vec y\_ \psi\})$ of morphisms
the set of formulas~$\theta$ in the
context~$\vec x, \vec y$ which are~$\TT$-provably functional,
modulo~$\TT$-provable equivalence of such formulas; \smallskip
\item as covering families those families~$(\{\vec x_i\_ \varphi_i\} \xrightarrow{\theta_i}
\{\vec y\_ \psi\})_i$ for which~$\TT$ proves the sequent~$(\psi \seq{\vec y} \bigvee_i \exists \vec x_i\_
\theta_i)$.
\end{enumerate}
\end{defn}

\begin{defn}The \emph{classifying topos}~$\Set[\TT]$ of a geometric
theory~$\TT$ is the topos of set-valued sheaves on~$\C_\TT$.\end{defn}

Writing~$\yon : \C_\TT \to \Set[\TT]$ for the Yoneda embedding,\footnote{With
this notational choice we are following Riehl and
Verity~\cite{riehl-verity:elements}.}
the \emph{generic
model}~$U_\TT$ of~$\TT$ interprets a sort~$X$ of~$\TT$ as the sheaf~$\yon\{x\?X\_ \top\}$,
a function symbol~$f : X_1 \cdots X_n \to Y$ as the morphism given by
the~$\TT$-provably functional formula~$f(x_1,\ldots,x_n) = y$ and a relation
symbol~$R \rightarrowtail X_1 \cdots X_n$ by the subobject~$\yon\{\vec x\_ R(\vec
x)\} \rightarrowtail \yon\{\vec x\_ \top\}$.

\begin{rem}\label{rem:unique-descriptions}
Sections of the sheaf~$\yon\{ y \? Y\_ \top \}$ over a stage~$A = \{ \vec x\_
\varphi \} \in C_\TT$ are in one-to-one correspondence with ``unique
descriptions'' over~$A$, that is formulas~$\theta$ in the context~$\vec x, y$
such that~$\TT$ proves~$(\varphi \seq{\vec x} \exists!y\?Y\_ \theta)$, up to
provable equivalence.
\end{rem}

\begin{thm}The generic model is universal in the sense that for any
Grothendieck topos~$\E$, the functor
\[ \text{(category of geometric morphisms~$\E \to \Set[\TT]$)} \longrightarrow
\text{(category of~$\TT$-models in~$\E$)} \]
given by~$f \mapsto f^*U_\TT$ is an equivalence of categories.
\end{thm}

\begin{proof}See, for instance,~\cite[Theorem~2.1.8]{caramello:tst}
or~\cite[discussion before Proposition~D3.1.12]{johnstone:elephant}.\end{proof}

\begin{prop}\label{prop:basic-truth}
Let~$\alpha$ and~$\varphi$ be geometric formulas in a context~$\vec
x$ over the signature of a geometric theory~$\TT$. Then the following
statements are equivalent:
\begin{enumerate}
\item $\Set[\TT] \models \forall \vec x\_ (\alpha \Rightarrow \varphi)$.
\smallskip
\item $\{\vec x\_ \alpha\} \models \varphi$, where the free variables
in~$\varphi$ are interpreted as their generic values over~$\{\vec
x\_\alpha\}$, that is as the projection maps~$\{ \vec x\_ \alpha \} \to \{
x_i\?X_i\_ \top \}$. \smallskip
\item $\TT$ proves~$(\alpha \seq{\vec x} \varphi)$.
\end{enumerate}
\end{prop}

\begin{proof}The equivalence~$(1) \Leftrightarrow (2)$ follows immediately by
unrolling the Kripke--Joyal semantics. The equivalence~$(2) \Leftrightarrow
(3)$ is by induction on the structure of~$\varphi$.\end{proof}


\subsection{Background on internal geometric theories}
\label{sect:review-theories}

The notions of signatures, geometric theories and classifying toposes can be
relativized to the internal world of arbitrary toposes with natural numbers
objects. Basics on internal signatures, internal geometric
theories and internal classifying toposes are
folklore~\cite[p.~334]{wraith:intuitionistic-algebra}; a careful treatment is
due to Shawn Henry~\cite{henry:phd}.

Briefly, an internal signature~$\Sigma$ internal to a topos~$\E$ consists of an
object of sorts, an object of function symbols, an object of relation symbols,
and various morphisms indicating the sorts involved with the function and
relation symbols.

Given an internal signature~$\Sigma$ internal to a Grothendieck topos~$\E$ (or
elementary topos with a natural numbers object), we can successively build the
object of contexts (the object of lists of sorts); the object of terms
(equipped with a morphism to the object of contexts); the object of atomic
propositions (again equipped with such a morphism); the object of geometric
formulas (again so); and the object of geometric sequents (again so). An internal
geometric theory~$\TT$ over~$\Sigma$ is then given by a subobject of the object
of geometric sequents, interpreted as the object of axioms of~$\TT$.
Given such an internal theory~$\TT$, we can build the subobject of the provable
sequents.

For the most part, these objects can be obtained by simply carrying out the
familiar constructions of the set of contexts, of the set of terms and so on in
the internal language of~$\E$. Some care is required in constructing the
object of geometric formulas: Inductively closing the object of basic
propositions under the connectives of geometric logic will fail because of size
issues -- even if we carry this out in~$\Set$, we will end up with a proper
class. Instead the object of geometric formulas should be constructed so as to
only contain geometric formulas in canonical form~(``$\bigvee \exists \cdots
\exists\_ \varphi_1 \wedge \cdots \wedge \varphi_n$'' for atomic
propositions~$\varphi_i$). There is no real loss in this restriction since in
foundations where it makes sense to say this, any geometric formula is provably
equivalent to a geometric formula in canonical form.

Similarly, we cannot construct the subobject of provable sequents by first
constructing an object of raw (arbitrarily-branching) trees and then cutting
down to an object of correctly formed proof trees. Instead, the subobject of
provable sequents can be obtained by intersecting, internally to~$\E$, all
subsets of the set of sequents which are closed under the rules of geometric
logic.\footnote{Equivalently one can appeal to the Knaster--Tarski fixed point
theorem, which is constructively valid in the form we require
here~\cite{bauer-lumsdaine:bourbaki-witt}, to construct the least fixed point
of the operator which, given a set~$M$ of geometric sequents, computes the set of
geometric sequents which can be derived from those in~$M$ in at most one step.
Details on how to carry out such kinds of inductive constructions can be found
in~\cite{blass:induction} and more specifically in
\cite[Chapter~III]{henry:phd}.}

None of these complications arise when setting up the theory of internal
coherent theories, where disjunctions are restricted to be finitary.

\begin{ex}An ordinary geometric theory is the same as a geometric theory
internal to the topos~$\Set$. A geometric sequent is provable in the ordinary
sense if and only if, from the internal point of view of~$\Set$, it is
contained in the object of provable sequents.\end{ex}

\begin{ex}An ordinary geometric theory~$\TT$ over an ordinary
signature~$\Sigma$ can be pulled back along a geometric morphism~$\E \to \Set$
to yield an internal geometric theory~$\ul{\TT}$ over the internal
signature~$\ul{\Sigma}$ in~$\E$. The object of sorts of~$\ul{\Sigma}$ is the pullback of
the set of sorts of~$\Sigma$, the object of function symbols of~$\ul{\Sigma}$
is the pullback of the set of function symbols of~$\Sigma$, and so on.\end{ex}

Disjunctions appearing in internal geometric formulas may be indexed by
arbitrary objects of the topos, just like disjunctions appearing in ordinary
external geometric formulas over an ordinary signature may be indexed by
arbitrary sets. If~$\Sigma$ is an internal signature in a Grothendieck topos~$\E$, the object of geometric
formulas over~$\Sigma$ has an important
subobject, the subobject of those formulas such that locally, any appearing
disjunction is indexed by a constant sheaf. Such internal geometric formulas
will be called \emph{geometric$^\star$ formulas}.

\begin{rem}A priori, there are two different notions of what it could mean that
a geometric$^\star$ formula is provable: It could be provable when regarded as
a geometric formula, or we could allow only geometric$^\star$ formulas as
intermediate formulas in proofs. One can show that these two notions coincide,
similarly to how a coherent sequent is provable in geometric logic if and only
if it is provable in coherent logic. Since we do not require this fact in the
course of this note, we omit a detailed verification.
\end{rem}


\section{The first-order Nullstellensatz}
\label{sect:main}

Given a geometric theory~$\TT$ with its generic model~$U_\TT$ in~$\Set[\TT]$,
our main theorems will reference a certain internal
theory~$\ul{\TT}/U_\TT$ internal to~$\Set[\TT]$. This theory is defined as
follows.

\begin{defn}\label{defn:tu}
Let~$\TT$ be a geometric theory. The theory~$\ul{\TT}/U_\TT$ is the
geometric theory internal to~$\Set[\TT]$ which arises from the pulled-back
theory~$\ul{\TT}$ by adding additional constant symbols~$e_x$ of the
appropriate sorts, one for each element~$x : U_\TT$, axioms~$(\top \vdash
f(e_{x_1},\ldots,e_{x_n}) = e_{f(x_1,\ldots,x_n)})$ for each function
symbol~$f$ and~$n$-tuple of elements of~$U_\TT$ (of the appropriate sorts), and
axioms~$(\top \vdash R(e_{x_1},\ldots,e_{x_n}))$ for each relation symbol~$R$
and~$n$-tuple~$(x_1,\ldots,x_n)$ (of the appropriate sorts) such
that~$R(x_1,\ldots,x_n)$.\end{defn}

From the point of view of~$\Set[\TT]$, a model of~$\ul{\TT}/U_\TT$ is a model
of~$\ul{\TT}$ equipped with a~$\ul{\TT}$-homomorphism from~$U_\TT$. In
particular, the identity~$(U_\TT \to U_\TT)$ is a model of~$\ul{\TT}/U_\TT$.
This is what we mean when we say that~$U_\TT$ is in a canonical way
a~$\ul{\TT}/U_\TT$-model.

\begin{ex}Let~$\TT$ be the theory of rings. Then~$\ul{\TT}/U_\TT$ is, from the
internal point of view of~$\Set[\TT]$, the theory of~$U_\TT$-algebras.\end{ex}

\begin{ex}Let~$\TT$ be a geometric theory. Let~$M$ be a model of~$\TT$ in the
category of sets. Let~$f : \Set \to \Set[\TT]$ be the corresponding geometric
morphism. Then~$f^*(\ul{\TT}/U_\TT)$ is the theory of~$M$-algebras
($\TT$-models equipped with a~$\TT$-homomorphism from~$M$). This is
because~$f^*\ul{\TT} = \TT$, $f^*U_\TT = M$ and because the construction of the
theory~$\ul{\TT}/U_\TT$ is geometric.\end{ex}

\begin{rem}From the internal point of view of~$\Set[\TT]$, we can construct the
classifying topos of~$\ul{\TT}/U_\TT$. Externally, this construction gives rise
to a bounded topos over~$\Set[\TT]$, hence to a Grothendieck topos. Using for
instance the technique described
in~\cite{blechschmidt-hutzler-oldenziel:composition}, one can show that this topos classifies the
theory of homomorphisms between~$\TT$-models. This topos can also be obtained as the
lax pullback~$(\Set[\TT] \Rightarrow_{\Set[\TT]} \Set[\TT])$.
There are two canonical geometric morphisms from this topos to~$\Set[\TT]$, the
morphism computing the domain and the morphism computing the codomain; the
morphism obtained by externalizing the internal construction is the former.
\end{rem}

\begin{lemma}\label{lemma:truth-to-provability}
Let~$\TT$ be a geometric theory. Let~$\alpha$ be a geometric formula over the
signature of~$\TT$ in a context~$x_1\?X_1,\ldots,x_n\?X_n$. Then
\[ \{ \vec x\_ \alpha \} \models \speak{$\ul{\TT}/U_\TT$ proves $(\top
\vdash_{[]} \alpha)$}, \]
where the free variables~$\vec x$ occurring in~$\alpha$ are first interpreted as in
Proposition~\ref{prop:basic-truth} and then regarded as the induced constant
symbols provided by the enlarged signature of~$\ul{\TT}/U_\TT$.
\end{lemma}

\begin{proof}By induction on the structure of~$\alpha$. The cases
of~``$\top$'' and ``$\wedge$'' are trivial; the cases of~``$\bigvee$''
and~``$\exists$'' follow from passing to suitable coverings; and the case of
atomic propositions is by definition of~$\ul{\TT}/U_\TT$.
\end{proof}

\begin{lemma}\label{lemma:locally-constant}
Let~$\TT$ be a geometric theory.
Let~$\varphi$ be a section of the sheaf of geometric$^\star$ formulas over the signature
of~$\ul{\TT}/U_\TT$ over a stage~$A \in \C_\TT$. Then there is a covering~$(A_i \to A)_i$
of~$A$ such that for each index~$i$, there is a formula~$\varphi_i$ over the signature
of~$\TT/U_\TT(A_i)$ such that~$A_i \models \speak{$\ul{\TT}/U_\TT$ proves
$(\varphi \dashv\vdash \varphi_i)$}$.
\end{lemma}

\begin{proof}By passing to a covering, we may suppose that~$\varphi$ is given
by an (external) geometric formula over the signature
of~$\ul{\TT}(A)/U_\TT(A)$.

Any function symbol and relation symbol
of~$\ul{\TT}(A)$ occurring in~$\varphi$ is locally given by a symbol of~$\TT$.
Hence the claim would be trivial if~$\varphi$ were a coherent formula, for in
this case we would just have to pass to further coverings, one for each
occurring symbol, a finite number of times in total.

However, in general, we cannot conclude as easily. Write~$A = \{ \vec x\_
\alpha \}$. Let~$R$ be a relation symbol of~$\ul{\TT}(A)$ occurring
in~$\varphi$. By the explicit description of constant sheaves as sheaves of
locally constant maps, there is a covering~$(\{ \vec y_j\_ \alpha_j \}
\xrightarrow{[\theta_j]} \{ \vec x\_ \alpha \})_j$ such that, restricted to~$\{
\vec y_j\_ \alpha_j \}$, $R$ is given by a relation symbol~$R_j$ of~$\TT$. To construct
the desired formula~$\varphi'$, we replace any such occurrence~$R(\ldots)$
in~$\varphi$ by
\[ \bigvee_j \bigl((\exists \vec y_j\_ \theta_j) \wedge R_j(\ldots)\bigr). \]
(The formulas~$\theta_j$ will typically contain instances of the
variables~$\vec x$. When writing down this replacement, we treat these as in
Lemma~\ref{lemma:truth-to-provability}. Hence this replacement is set in the
same context as~$\varphi$, only that new constant symbols might occur.)
In a similar vein we treat any occurrence of function symbols.

The resulting formula~$\varphi'$ is a geometric formula over the signature
of~$\TT/U_\TT(A)$.
The verification of~$A \models \speak{$\ul{\TT}/U_\TT$ proves
$(\varphi \dashv\vdash \varphi')$}$ rests on the observation
\[ A \models \speak{$\ul{\TT}/U_\TT$ proves $\bigl((\exists \vec y_k\_
\theta_k) \seq{[]} \bigvee \{ \top \,|\, \text{$(\exists \vec y_k\_ \theta_k)$
holds for~$U_\TT$} \}\bigr)$} \]
which in turn can be checked on the covering~$(\{ \vec y_j\_ \alpha_j \}
\xrightarrow{[\theta_j]} \{ \vec x\_ \alpha \})_j$, applying
Lemma~\ref{lemma:truth-to-provability} and using that~$\TT$ (and
hence~$\ul{\TT}$) proves~$((\exists \vec y_j\_ \theta_j) \wedge (\exists \vec
y_k\_ \theta_k) \seq{\vec x} \bigvee \{ \top \,|\, j = k \})$. (This kind of
reasoning also appears, for instance, in~\cite[p.~20]{blass:seven-trees}.)
\end{proof}

\begin{thm}\label{thm:nullstellensatz}
Let~$\TT$ be a geometric theory. Then, internally to~$\Set[\TT]$, for any
geometric$^\star$ sequent~$\sigma$ over the signature of~$\ul{\TT}/U_\TT$, the
following statements are equivalent:
\begin{enumerate}
\item The sequent~$\sigma$ holds for~$U_\TT$. \smallskip
\item The sequent~$\sigma$ is provable modulo~$\ul{\TT}/U_\TT$.
\end{enumerate}
\end{thm}

\begin{proof}The direction~$(2) \Rightarrow (1)$ is immediate because~$U_\TT$ is, from the
internal point of view of~$\Set[\TT]$, a~$\ul{\TT}/U_\TT$-model.

For the direction~$(1) \Rightarrow (2)$ we have to verify that, given any
stage~$A \in \C_\TT$ and any section~$\sigma$ of the sheaf of
geometric$^\star$ sequents over~$A$, if~$A \models
\speak{$\sigma$ holds for~$U_\TT$}$ then~$A \models
\speak{$\ul{\TT}/U_\TT$ proves~$\sigma$}$. By
Lemma~\ref{lemma:locally-constant} we may suppose that~$\sigma$ is an
(external) geometric sequent over the signature of~$\TT/U_\TT(A)$.

Writing~$A = \{ \vec x\_ \alpha \}$ and~$\sigma = (\varphi \seq{\vec y} \psi)$,
we have~$\{ \vec x\_ \alpha \} \models \forall \vec y\_ (\varphi \Rightarrow \psi)$ by assumption,
hence~$\{ \vec x, \vec y\_ \alpha \wedge \varphi \} \models \psi$ (where we
inline any occurence of an element of~$U_\TT(A)$ as a constant symbol
in~$\varphi$, recalling Remark~\ref{rem:unique-descriptions}).
Thus~$\TT$
proves~$(\alpha \wedge \varphi \seq{\vec x, \vec y} \psi)$ (where we now have
to do the same inlining for~$\psi$ as well). This proof can be
pulled back from~$\Set$ to~$\Set[\TT]/\yon A$ to obtain~$A \models
\speak{$\ul{\TT}/U_\TT$ proves~$(\alpha
\wedge \varphi \seq{\vec x, \vec y} \psi)$}$. By
Lemma~\ref{lemma:truth-to-provability}, we also have~$A \models
\speak{$\ul{\TT}/U_\TT$ proves~$(\top \seq{[]} \alpha)$}$ (where the free
variables occurring in~$\alpha$ are interpreted as the generic values available
over~$A$), hence~$A \models \speak{$\ul{\TT}/U_\TT$ proves~$(\varphi
\seq{\vec y} \psi)$}$.
\end{proof}

The force of the Nullstellensatz of Theorem~\ref{thm:nullstellensatz} is for
sequents~$\sigma$ which are not of the form~$(\top \seq{[]} \varphi)$. Indeed,
for those special sequents, the implication~$(\text{$\sigma$ holds for~$U_\TT$}
\Rightarrow \text{$\ul{\TT}/U_\TT$ proves~$(\top \seq{[]} \varphi)$})$
can be proven by a simple induction on the structure of~$\varphi$. Only for more general
sequents does Theorem~\ref{thm:nullstellensatz} express a nontrivial fact: that
truth of an universally-quantified conditional statement implies a single
unquantified unconditional statement.

\begin{rem}The restriction in Theorem~\ref{thm:nullstellensatz} to
geometric$^\star$ sequents cannot be lifted, that is the generalization
of~Theorem~\ref{thm:nullstellensatz} to
arbitrary internal geometric sequents is false. For instance, in the case that~$\TT$ is the
theory of objects, the internal geometric sequent~$(\top \seq{x\?U_\TT}
\bigvee_{a\?U_\TT} (x = e_a))$ trivially holds for~$U_\TT$. However, this sequent is not
provable modulo~$\ul{\TT}/U_\TT$, as for instance the model~$U_\TT \amalg
\{\star\}$ does not validate it.\end{rem}

\begin{cor}\label{corollary:nullstellensatz-horn}
Let~$\TT$ be a geometric theory. Let~$\TT'$ be a quotient theory
of~$\TT$. Assume that the generic model~$U_\TT$ is a sheaf for the topology
on~$\Set[\TT]$ cutting out the subtopos~$\Set[\TT']$. Then the following
statement holds internally to~$\Set[\TT']$:
\[ \text{A geometric$^\star$ sequent~$\sigma$ with Horn consequent holds for~$U_{\TT'}$
  iff~$\ul{\TT}/U_\TT$ proves~$\sigma$.} \]
\end{cor}

\begin{proof}In general, the generic model of~$\TT'$ is the pullback of the
generic model of~$\TT$ to the
subtopos~$\Set[\TT']$~\cite[Lemma~2.3]{caramello:definability}. By the sheaf
assumption, the objects~$U_{\TT'}$ and~$U_\TT$ actually agree, that is~$U_\TT$
is contained in the subtopos and has the universal property of~$U_{\TT'}$.

The ``if'' direction is trivial, as~$U_{\TT'}$ is a~$\ul{\TT}/U_\TT$-model.

For the ``only if'' direction, we use that a statement holds in~$\Set[\TT']$ if
and only if its~$\nabla$-translation holds in~$\Set[\TT]$, where~$\nabla$ is
the modal operator associated to the topology cutting
out~$\Set[\TT']$~\cite[Theorem~6.31]{blechschmidt:phd}. Exploiting some of the
simplification rules of the~$\nabla$-translation~\cite[Section~6.6]{blechschmidt:phd},
it hence suffices to verify, internally to~$\Set[\TT]$, that:
\begin{multline*}
  \text{\emph{For any geometric$^\star$ sequent~$\sigma = (\varphi \seq{\vec x} \psi)$ where~$\psi$ is a Horn formula,}} \\
    \text{\emph{if~$\forall x_1,\ldots,x_n\?U_\TT\_ (\varphi \Rightarrow \nabla
    \psi)$, then~$\ul{\TT}/U_\TT$ proves~$\sigma$.}}
\end{multline*}
Since~$\nabla$ commutes with finite conjunctions and since the sheaf assumption
implies that $\nabla(s = t)$ is equivalent
to~$s = t$ and that, for relation symbols~$R$, the
statement~$\nabla(R(s_1,\ldots,s_m))$ is equivalent to~$R(s_1,\ldots,s_m)$,
the statement~$\nabla\psi$ is equivalent to~$\psi$. Hence the claim follows
from Theorem~\ref{thm:nullstellensatz}.
\end{proof}

A situation in which the sheaf assumption of Corollary~\ref{corollary:nullstellensatz-horn}
is satisfied is when~$\TT$ is a Horn theory and the topology cutting
out~$\Set[\TT']$ is subcanonical. For instance, this is the case if~$\TT$ is
the theory of rings and~$\Set[\TT']$ is one of several well-known toposes in
algebraic geometry such as the big Zariski topos, the big étale topos or the
big fppf topos.

\begin{rem}In the case that the subtopos~$\Set[\TT']$ is a dense subtopos
of~$\Set[\TT]$, Corollary~\ref{corollary:nullstellensatz-horn} can be strengthened to
allow~$\bot$ as consequent, since in this case we have~$(\nabla\psi)
\Rightarrow \psi$ also for~$\psi \equiv \bot$.\end{rem}

Theorem~\ref{thm:nullstellensatz} cannot be strengthened to arbitrary
first-order (or first-order$^\star$ or even finitary first-order) formulas in place of
geometric$^\star$ sequents. For instance, in the case that~$\TT$ is the theory
of rings, the generic model~$U_\TT$ validates the finitary first-order
formula~$\speak{any element~$x$ for which~$(x = 0 \Rightarrow 1 = 0)$ is invertible}$, but~$\ul{\TT}/U_\TT$
does not prove this fact, as it is for instance not validated by the polynomial
algebra~$U_\TT[X]$.

However, Theorem~\ref{thm:nullstellensatz} still plays an
important role in understanding first-order formulas, as it is at the core of
our proposed characterization of the first-order formulas validated by the
generic model.

\begin{scholium}\label{scholium:nullstellensatz-more-specific}
Let~$\TT$ be a geometric theory. Let~$\vec x$ be a context over the signature
of~$\TT$. Let~$(\sigma_i)_i$ be a set of geometric sequents, where each context
is of the form~$\vec x, \vec y_i$ for some additional list~$\vec y_i$.
Write~$\sigma_i = (\varphi_i \seq{\vec x, \vec y_i} \psi_i)$. Then, internally
to~$\Set[\TT]$, it holds that
\[ \forall \vec x\_
  \bigl(\bigwedge_i (\forall \vec y_i\_ \varphi_i \Rightarrow \psi_i)\bigr) \Longrightarrow
  \bigvee_\alpha \alpha,
\]
where the disjunction ranges over all those geometric formulas~$\alpha$ in the
context~$\vec x$ such that for every index~$i$, the theory~$\TT$ proves~$(\alpha
\wedge \varphi_i \seq{\vec x, \vec y_i} \psi_i)$.
\end{scholium}

\begin{proof}Immediate from the proof of Theorem~\ref{thm:nullstellensatz}.
\end{proof}

\begin{thm}\label{thm:characterization}
Let~$\TT$ be a geometric theory. Let~$\chi$ be a (finitary or infinitary) first-order
formula over the signature of~$\TT$. Then the following statements are
equivalent.
\begin{enumerate}
\item The formula~$\chi$ holds for~$U_\TT$. \smallskip
\item The formula~$\chi$ is provable in infinitary first-order intuitionistic
logic modulo the axioms of~$\TT$ adjoined by, for each geometric
sequent~$\sigma = (\varphi \seq{\vec x, \vec y} \psi)$ and for each splitting
of its context into two parts~$\vec x, \vec y$, the additional axiom
\begin{equation}\label{eq:nullstellensatz}\tag{$\ddagger$}
  \forall \vec x\_
  \bigl((\forall \vec y\_ \varphi \Rightarrow \psi) \Longrightarrow
  \bigvee_\alpha \alpha\bigr),
\end{equation}
where the disjunction ranges over all those geometric formulas~$\alpha$ in the
context~$\vec x$ such that~$\TT$ proves~$(\alpha \wedge \varphi \seq{\vec x,\vec
y} \psi)$.
\end{enumerate}
\end{thm}

To a first approximation, axiom scheme~\eqref{eq:nullstellensatz} is just a
rendition of the (nontrivial direction of the) statement of the Nullstellensatz
in infinitary first-order logic. However, the conclusion ``$\sigma$ is provable
modulo~$\ul{\TT}/U_\TT$'' does not seem to be expressible in this logic.
The conclusion~``$\bigvee_\alpha \alpha$'' of axiom
scheme~\eqref{eq:nullstellensatz} is a strengthening of ``$\sigma$ is provable
modulo~$\ul{\TT}/U_\TT$'' which can. We recall that in infinitary first-order
formulas, we allow set-indexed disjunctions (but not set-indexed conjunctions).

\begin{proof}[Proof of Theorem~\ref{thm:characterization}]
Any infinitary first-order formula can be simplified to an equivalent geometric
formula -- on the semantic side by repeatedly applying
Scho\-li\-um~\ref{scholium:nullstellensatz-more-specific}, on the syntactic side by
repeatedly applying axiom scheme~\eqref{eq:nullstellensatz}. Hence we are
reduced to the basic fact (Proposition~\ref{prop:basic-truth}) that, for
geometric formulas~$\varphi$, $\Set[\TT] \models
\varphi$ if and only if~$\TT$ proves~$\varphi$.
\end{proof}

\begin{rem}Both in Scholium~\ref{scholium:nullstellensatz-more-specific} and in
the axiom scheme~\eqref{eq:nullstellensatz}, it suffices to restrict the
disjunction~``$\bigvee_\alpha \alpha$'' to those formulas~$\alpha$ which are of
the form~``$\exists\cdots\exists\_ \varphi$'' with~$\varphi$ of Horn type.
\end{rem}

The Nullstellensatz of Theorem~\ref{thm:nullstellensatz} and the
characterization of Theorem~\ref{thm:characterization} pertain to geometric
logic and hence require some care in dealing with the flexibility of
disjunctions. In particular, the internal statement of
Theorem~\ref{thm:nullstellensatz} requires external ingredients in referring to
geometric$^\star$ sequents. A natural question is
therefore whether, in the case that~$\TT$ is a coherent theory, the statements
of these two theorems can be simplified.

However, while geometric logic is powerful enough to express
provability in geometric logic (or rather the strenghtening we employed in
axiom scheme~\eqref{eq:nullstellensatz}),
coherent logic is not powerful enough
to express provability in coherent logic. ``Coherent logic cannot eat itself.''
Hence the analogue of Theorem~\ref{thm:characterization} cannot be
formulated for coherent logic.

A fragment of logic which is still finitary, but is powerful enough to express
its own provability predicate, is \emph{coherent existential fixed-point
logic}, coherent logic enriched by list sorts and the fixed-point operator of
existential fixed-point logic~\cite{blass:topoi-and-computation,blass:existential-fixed-point-logic}.
The list sorts can be used to express raw terms, raw formulas and raw
sequents; the fixed-point operator can then be used to express well-formedness of
raw terms, raw formulas and raw sequents; and to express provability. For this
fragment, we have the following characterization.

\begin{scholium}Let~$\TT$ be a coherent theory (or more generally a theory in coherent
existential fixed-point logic). Let~$\alpha$ be a finitary first-order
formula over the signature of~$\TT$. Then the following statements are
equivalent.
\begin{enumerate}
\item The formula~$\alpha$ holds for~$U_\TT$. \smallskip
\item The formula~$\alpha$ is provable in coherent existential fixed-point logic
modulo the axioms of~$\TT$ and the additional axioms
\[
  \speak{$\sigma$ holds for~$U_\TT$} \Longrightarrow \speak{$\ul{\TT}/U_\TT$
  proves~$\sigma$}
\]
where~$\sigma$ ranges over the formulas of coherent existential fixed-point
logic over the signature of~$\TT$. (When referring to~``$U_\TT$'', we here mean
the tautologous ``model'' in which any
sort of~$\TT$ is interpreted by the sort itself. For instance, if~$\sigma =
(\varphi \seq{x_1\!\?\!X_1,\ldots,x_n\!\?\!X_n} \psi)$ is a sequent,
then~$\speak{$\sigma$ holds for~$U_\TT$}$ is to be interpreted as the
formula~``$\forall x_1\?X_1\_ \ldots \forall x_n\?X_n\_ (\varphi \Rightarrow
\psi)$''.)
\end{enumerate}
\end{scholium}

\begin{proof}The proofs of Theorem~\ref{thm:nullstellensatz} and
Theorem~\ref{thm:characterization} can be adapted to the setting of coherent
existential fixed-point logic.
\end{proof}

On the other end, we can ask for a generalization of
Theorem~\ref{thm:characterization} to the extension of infinitary first-order
logic where we additionally allow set-indexed conjunctions. Such a
generalization is given by the following scholium.

\begin{scholium}
Let~$\TT$ be a geometric theory. Let~$\chi$ be a formula in infinitary
first-order formula enriched by set-indexed conjunctions over the signature
of~$\TT$. Then the following statements are equivalent.
\begin{enumerate}
\item The formula~$\chi$ holds for~$U_\TT$. \smallskip
\item The formula~$\chi$ is provable in infinitary first-order intuitionistic
logic enriched by set-indexed conjunctions modulo the axioms of~$\TT$ adjoined
by the displayed formulas of
Scholium~\ref{scholium:nullstellensatz-more-specific}.
\end{enumerate}
\end{scholium}

\begin{proof}The proof of Theorem~\ref{thm:characterization} carries over word
for word.
\end{proof}


\section{The special case of Horn theories}
\label{sect:horn}

The purpose of this section is to redo the development in the special case of
Horn theories. XXX

Throughout this section, let~$\TT$ be a Horn theory. It is a basic result that
Horn theories are of presheaf type, that is the classifying topos~$\Set[\TT]$
can be taken as the topos of functors~$\Mod{\TT}_\mathrm{fp} \to \Set$,
where~$\Mod{\TT}_\mathrm{fp}$ is the full subcategory of the category
of~$\TT$-models (in~$\Set$) on the finitely presentable objects~\cite[Theorem~2.1.21]{caramello:tst}. The
% XXX: besser formulieren family of objects
(underlying object of the) generic model is the tautologous functor~$U_\TT : T
\mapsto T$. By~\emph{$U_\TT$-algebra} we mean, in analogy with the terminology in
the case that~$\TT$ is the theory of rings, a~$\TT$-model~$M$ equipped with
a~$\TT$-homomorphism~$U_\TT \to M$.

% XXX: upgrade to cartesian case? maybe as a remark?

\begin{lemma}\label{lemma:free-models}
Let~$X$ be a set equipped with a morphism~$X \to S$ to the set of sorts
of the signature~$\Sigma$ of~$\TT$. Let~$R$ be a set of atomic propositions in which the
elements of~$X$ may appear as new constants of the respective sorts. Then there
is~$\TT\langle X | R \rangle$, the free~$\TT$-model on the generators~$X$ modulo
the relations~$R$.\end{lemma}

\begin{proof}The desired model can be constructed as a term algebra. As a set,
it consists of the terms (in the empty context) of the signature~$\Sigma + X$
modulo the equivalence relation identifying two terms if and only if~$\TT + R$
proves them to be equal. The function symbols~$f$ of~$\Sigma$ are interpreted
by declaring~$\brak{f}([t_1],\ldots,[t_n]) = [f(t_1,\ldots,t_n)]$ and the
relation symbols~$H$ are interpreted by declaring~$([t_1],\ldots,[t_n]) \in
\brak{H} \Leftrightarrow (\TT + R \,\vdash H(t_1,\ldots,t_n))$.

We omit the required verifications and only remark that while the same
construction could be carried out if~$\TT$ was a general geometric theory, the
term algebra would in general not be a model of~$\TT$.
\end{proof}

\begin{lemma}Let~$\sigma = (\varphi_1 \wedge \cdots \wedge \varphi_n
\seq{x_1,\ldots,x_k} \psi_1 \wedge \cdots \wedge \psi_m)$ be a Horn sequent
over the signature of~$\TT$. Then the following statements are equivalent.
\begin{enumerate}
\item The theory~$\TT$ proves~$\sigma$. \smallskip
\item In~$\TT\langle x_1,\ldots,x_k \,|\, \varphi_1,\ldots,\varphi_n \rangle$, the
propositions~$\psi_1,\ldots,\psi_m$ hold for
the~$k$-tuple~$([x_1],\ldots,[x_k])$.
\end{enumerate}
\end{lemma}

\begin{proof}By construction of the term algebra.\end{proof}

\begin{lemma}\label{lemma:char-fp-models}
A~$\TT$-model is finitely presentable as an object of the category
of~$\TT$-models if and only if it is isomorphic to a model of the
form~$\TT\langle X | R \rangle$ where~$X$ is Bishop-finite and~$R$ is
Kuratowski-finite.
\end{lemma}

\begin{proof}It is an instructive exercise to verify that models of the stated
form are compact (in a slightly different context, this is done
in~\cite[Theorem~3.12]{adamek-rosicky:presentable}). Conversely, let
a~$\TT$-model~$M$ be given. Then~$\TT$ is the
filtered colimit of all models over~$M$ which are of the stated form. If~$M$ is
compact, the identity on~$M$ factors over such a model. Hence~$M$ is a
retract of such a model and hence itself isomorphic to a model of this form.
\end{proof}

\begin{lemma}The category of~$\TT$-models (in~$\Set$) is complete and
cocomplete.\end{lemma}

\begin{proof}Limits are computed as the limits of the underlying sets, colimits
are computed by using the construction of Lemma~\ref{lemma:free-models}. For
instance, the coproduct of~$\TT\langle X | R \rangle$ and~$\TT\langle X' | R'
\rangle$ is~$\TT\langle X \amalg X' \,|\, R \cup R' \rangle$.\end{proof}
% XXX sagen, dass jedes Modell (beliebig) präsentiert wird

Having the special case of the theory of rings in mind, we write the coproduct
in the category of~$\TT$-models as~``$\otimes$''.

Any~$\TT$-model~$A$ has a mirror image in the topos~$\Set[\TT]$, namely the
functor~$A^\sim : \Mod{\TT}_\mathrm{fp} \to \Set$ given by~$T \mapsto A \otimes T$.
This object is in a canonical way a~$\TT$-model over~$U_\TT$, hence from the
point of view of~$\Set[\TT]$ a~$\ul{\TT}/U_\TT$-model.

\begin{lemma}The functor~$(\cdot)^\sim$ from~$\TT$-models to~$\ul{\TT}/U_\TT$-models
in~$\Set[\TT]$ is left adjoint to the functor~$\Gamma = \Hom(1, \cdot)$ computing
global elements.
\end{lemma}

\begin{proof}A~$U_\TT$-algebra homomorphism~$\alpha : A^\sim \to M$ yields
the~$\TT$-model homo\-mor\-phism~$\alpha_0 : A \to M(0) = \Gamma(M)$, where~$0$ is the
initial~$\TT$-model. Conversely, a~$\TT$-model homomorphism~$\beta : A \to
\Gamma(M)$ yields a~$U_\TT$-algebra homomorphism by summing~$A \to M(0) \to
M(T)$ with the structure morphism~$T = U_\TT(T) \to
M(T)$.\end{proof}

\begin{defn}The \emph{spectrum}~$\Spec(M)$ of a~$U_\TT$-algebra~$M$ in~$\Set[\TT]$
is the result of constructing, internally to~$\Set[\TT]$, the set
of~$U_\TT$-algebra homomorphisms~$M \to U_\TT$.
\end{defn}

% This is wrong:
% Externally, the spectrum of~$M$ is the functor
% mapping a finitely presented~$\TT$-model~$T$ to~$\Hom_T(M(T), T)$, the set
% of~$\TT$-homomorphisms~$M(T) \to T$ compatible with the structure morphisms~$T
% \to M(T)$ and~$T \to T$.

\begin{lemma}\label{lemma:spec-sim-representable}
Let~$A$ be a~$\TT$-model (not necessarily finitely presentable). Then~$\Spec(A^\sim)$ coincides
with~$\yon A$, the functor~$\Hom_{\Mod{\TT}}(A, \cdot)$.
\end{lemma}

\begin{proof}By the Yoneda lemma, the sections of the presheaf~$\Spec(A^\sim) :
\Mod{\TT}_\mathrm{fp} \to \Set$ on an object~$T$ are given by the set
\begin{align*}
  \Spec(A^\sim)(T) &\cong \Hom(\yon T, \Spec(A^\sim)) =
  \Hom(\yon T, [A^\sim,U_\TT]_{U_\TT}) \\
  &\cong \Hom(\yon T \times A^\sim, U_\TT)_{\text{$U_\TT$-algebra homomorphism in second
  argument}} \\
  &\cong \Hom_{U_\TT}(A^\sim, (U_\TT)^{\yon T})
  \cong \Hom_{U_\TT}(A^\sim, U_\TT|T),
\end{align*}
where~$[A^\sim,U_\TT]_{U_\TT}$ is the object of~$U_\TT$-algebra homomorphisms from~$A^\sim$
to~$U_\TT$ (a subobject of the internal Hom~$(U_\TT)^{A^\sim}$); $\Hom_{U_\TT}$
denotes the set of~$U_\TT$-algebra homomorphisms; $(U_\TT)^{\yon T}$ is the object of morphisms
from~$\yon T$ to~$U_\TT$; and~$U_\TT|T$ is the functor~$U_\TT(T \times \cdot)$, that is
the functor~$S \mapsto T \otimes S$.

An arbitrary element~$f \in (\yon A)(T)$, that is an arbitrary~$\TT$-model
homomorphism~$f : A \to T$, induces a~$U_\TT$-algebra homomorphism~$g : A^\sim \to
U_\TT|T$ by setting~$g_S \defeq f \otimes \id_S : A \otimes S \to T \otimes S$. The
given homomorphism~$f$ can be recovered by~$f = g_0$, the component of~$g$ at
the initial model.

Conversely, a~$U_\TT$-algebra homomorphism~$g : A^\sim \to U_\TT|T$ induces
a~$\TT$-model homomorphism~$f : A \to T$ by setting~$f \defeq g_0$. Because~$g$
is a natural transformation and because~$g$ is compatible with the structure
morphisms~$U_\TT \to A^\sim$ and~$U_\TT \to U_\TT|T$, the morphism~$g$ is determined
by~$f$.
\end{proof}

\begin{lemma}\label{lemma:fp-double-dual}
Let~$A$ be a finitely presentable~$\TT$-model. Then the canonical morphism
\[ A^\sim \longrightarrow (U_\TT)^{\Spec(A^\sim)} \]
is an isomorphism of~$U_\TT$-algebras.
\end{lemma}

\begin{proof}By Lemma~\ref{lemma:spec-sim-representable}, the
functor~$\Spec(A^\sim)$ coincides with~$\yon A$. Since by assumption~$A$ is
contained in the site defining~$\Set[\TT]$, the exponential~$(U_\TT)^{\yon A}$
coincides with~$U_\TT|A$ (notation as in the proof in
Lemma~\ref{lemma:spec-sim-representable}), that is, with the~$U_\TT$-algebra~$A^\sim$.
\end{proof}

\begin{cor}Let~$A$ and~$B$ be~$\TT$-models. Assume that~$B$ is finitely
presentable. Then the canonical morphism
\[ \Hom_{U_\TT}(A^\sim, B^\sim) \longrightarrow \Spec(A^\sim)^{\Spec(B^\sim)}
\]
is an isomorphism.
\end{cor}

\begin{proof}We have the chain of isomorphisms
\begin{align*}
  \Spec(A^\sim)^{\Spec(B^\sim)} &=
  ([A^\sim,U_\TT]_{U_\TT})^{\Spec(B^\sim)} \cong
  [\Spec(B^\sim) \times A^\sim, U_\TT]_{U_\TT} \\
  &\cong
  [A^\sim, U_\TT^{\Spec(B^\sim)}]_{U_\TT} \cong
  [A^\sim, B^\sim],
\end{align*}
where the final isomorphism is by Lemma~\ref{lemma:fp-double-dual}.
\end{proof}

\begin{thm}\label{thm:quasicoherence}
The generic~$\TT$-model is \emph{quasicoherent} in the following sense:
From the point of view of~$\Set[\TT]$, for any finitely
presentable~$U_\TT$-algebra~$A$ (finitely presentable object in the category
of~$U_\TT$-algebras), the canonical~$U_\TT$-algebra homomorphism
\[ A \longrightarrow (U_\TT)^{\Spec(A)},\ x \longmapsto -(x) \]
is an isomorphism.
\end{thm}

We use the term \emph{quasicoherent} in reference to algebraic geometry: For
an~$\affl$-module~$M$ in the big Zariski topos of a scheme~$S$, where~$\affl$
is the functor of points of the affine line over~$S$, there is a
well-established notion of what it means that~$M$ is quasicoherent. This
property can be characterized in the internal language: Such a module~$M$ is
quasicoherent if and only if, from the internal point of view of the big
Zariski topos, the canonical map~$A \otimes_\affl M \to M^{\Spec(A)}$ is an
isomorphism for any finitely
presented~$\affl$-algebra~$A$~\cite[Theorem~18.19]{blechschmidt:phd}.
Specializing to the case~$M = \affl$, we obtain the quasicoherence condition of
Theorem~\ref{thm:quasicoherence}.

\begin{proof}[Proof of Theorem~\ref{thm:quasicoherence}]The proof of
Lemma~\ref{lemma:char-fp-models} is constructive and
thus valid in the internal language of~$\Set[\TT]$. Hence we can apply it,
internally, to the theory~$\ul{\TT}/U_\TT$ to deduce that a~$U_\TT$-algebra~$A$
is finitely presentable if and only if it is isomorphic to a~$U_\TT$-algebra of
the form~$(\ul{\TT}/U_\TT)\langle X | R \rangle$ with~$X$ Bishop-finite and~$R$
Kuratowski-finite.

We therefore have to verify the following internal
statement: \emph{For any number~$n$, for any sorts~$X_1,\ldots,X_n$
of~$\ul{\TT}/U_\TT$, for any number~$m$, for any atomic
propositions~$R_1,\ldots,R_m$ over the signature of~$\ul{\TT}/U_\TT$ extended
by constants~$e_1 \? X_1, \ldots, e_n \? X_n$, the canonical map~$A \to
(U_\TT)^{\Spec(A)}$ where~$A \defeq (\ul{\TT}/U_\TT)\langle
e_1\?X_1,\ldots,e_n\?X_n \,|\, R_1,\ldots,R_m \rangle$ is an isomorphism.}

Following the Kripke--Joyal translation of this statement, let a stage~$T \in
\Mod{\TT}_\mathrm{fp}$,~$T$-elements~$X_1,\ldots,X_n$ of the object of sorts of
the signature of~$\ul{\TT}/U_\TT$ (that is the constant presheaf on the set of
sorts of~$\TT$), and~$T$-elements~$R_1,\ldots,R_m$ of the object of atomic
propositions over the signature of~$\ul{\TT}/U_\TT$ be given. The~$X_i$ are given by sorts of~$\TT$ and
the~$R_j$ are given by atomic propositions over the signature
of~$\TT/U_\TT(T)$.

Since the slice~$\Set[\TT]/\yon T$ is equivalent to~$\Set[\TT/T]$,
hence again the classifying topos of a Horn theory, we may without loss of
generality assume that~$T$ is the initial~$\TT$-model.

In this case the claim follows from Lemma~\ref{lemma:fp-double-dual}, since
the result of constructing, internally to~$\Set[\TT]$, the
model~$(\ul{\TT}/U_\TT)\langle
e_1\?X_1,\ldots,e_n\?X_n \,|\, R_1,\ldots,R_m \rangle$ coincides with
the~$U_\TT$-algebra~$(\TT\langle
e_1\?X_1,\ldots,e_n\?X_n \,|\, R_1,\ldots,R_m \rangle)^\sim$.
\end{proof}

\begin{thm}Let~$\TT'$ be a geometric quotient theory of~$\TT$, not necessarily Horn.
Assume that~$U_\TT$ is a sheaf for the topology
on~$\Set[\TT]$ cutting out the subtopos~$\Set[\TT']$. Then, from the internal
point of view of~$\Set[\TT']$, the canonical map~$A \to (U_{\TT'})^{\Spec(A)}$
is an isomorphism of~$U_\TT$-algebras for every finitely
presented~$U_\TT$-algebra~$A$. (By~``$\Spec(A)$'', we here mean the set
of~$U_\TT$-algebra homomorphisms from~$A$ to~$U_{\TT'}$.)
\end{thm}

\begin{proof}In general, the generic model~$U_{\TT'}$ is the sheafification
of~$U_\TT$~\cite[Lemma~2.3]{caramello:definability}. By the sheaf assumption,
the objects~$U_{\TT'}$ and~$U_\TT$ actually agree as functors
on~$\Mod{\TT}_\mathrm{fp}$.

Following the Kripke--Joyal translation of the claim, similar as in the proof
of Theorem~\ref{thm:quasicoherence}, it suffices to show that
applying the sheafification functor to the isomorphisms provided by
Lemma~\ref{lemma:fp-double-dual} (over arbitrary slices) results in
isomorphisms of the same form. This fact follows from the fact that
the presheaf Hom into a sheaf is already a sheaf itself and
from the observation that the construction~``free~$U_\TT$-module modulo
relations'' is geometric, hence in particular commutes with sheafification.
\end{proof}

% XXX explain how Nullstellensatz follows from the Horn version

\begin{rem}The finite presentability condition in
Lemma~\ref{lemma:fp-double-dual} cannot be dropped. For instance, in the case
that~$\TT$ is the theory of commutative rings with unit and~$A$ is the
ring~$\QQ$ of rational numbers, we have~$\Spec(A^\sim) \cong \Spec(0^\sim)$, where~$0$
is the zero ring, as~$\QQ$ allows ring homomorphisms only to those finitely
presented rings in which~$1 = 0$ holds. Hence~$A^\sim$
and~$(U_\TT)^{\Spec(A^\sim)} \cong (U_\TT)^{\Spec(0^\sim)} \cong 0^\sim$ do not coincide.
\end{rem}


\section{The generalization to the higher-order case}
\label{sect:higher-order}

% XXX introduction

By \emph{extended geometric logic} we mean the extension of geometric logic
where we are allowed to form, in addition to the basic sorts supplied by
a given signature, finite limits of sorts and set-indexed colimits of sorts. By
(intuitionistic) \emph{higher-order logic}, we mean the further extension where
we may also form powersorts. These derived sorts come with respective term
constructors (tuple formers, coprojections, set comprehension) and the usual
rules governing these constructors.
% XXX cite some reference for these "usual rules", perhaps Milly?

An \emph{extended geometric formula} is a formula of extended geometric logic built from equality and
relation symbols by the logical
connectives~${\top}\,{\bot}\,{\wedge}\,{\vee}\,{\exists}$
and by arbitrary set-indexed disjunctions~$\bigvee$. Existential
quantification can be over any of the sorts of extended geometric logic, including the derived sorts. An
\emph{extended geometric sequent} is a sequent of the form~$(\varphi
\seq{\vec x} \psi)$ where~$\varphi$ and~$\psi$ are extended geometric
formulas and the sorts of the variables~$\vec x$ may be derived sorts.

It is possible to extend the Kripke--Joyal semantics so that higher-order logic
can be interpreted in any Grothendieck topos. The truth of a higher-order
sequent~$(\varphi \seq{\vec x} \psi)$ is in general not preserved under
pullback along geometric morphisms, even if~$\varphi$ and~$\psi$ do not
contain~${\forall}$ and~$\Rightarrow$, since powerobjects are in general not
preserved under pullback. However, as can be deduced from the following lemma,
the truth of extended geometric sequents is preserved; as is folklore, extended
geometric logic is just a thin layer over ordinary geometric logic.

\begin{lemma}\label{lemma:extended-conservative}
Let~$\sigma$ be an extended geometric sequent over the signature
of a geometric theory~$\TT$. Then there is a set-indexed family~$(\sigma_i)_i$ of ordinary
geometric sequents over the same signature such that~$\sigma$ is provable in
extended geometric logic if and only if all the sequents~$\sigma_i$ are
provable in ordinary geometric logic.\end{lemma}

\begin{proof}Any existential quantification of the form~``$\exists p \? X
\times Y$'' can be replaced by the string~``$\exists x \? X\_ \exists y \?
Y$'', and similarly for free variables of product sorts appearing in the
context of~$\sigma$. In a similar vein more general finite limits are treated.

An existential quantification of the form~``$\exists x \? \coprod_i X_i$'' can
be replaced by the string~``$\bigvee_i \exists x \? X_i$''.

Finally, for any occurrence of a free variable~$x \?
\coprod_i X_i$ in the context of~$\sigma$, we can replace~$\sigma$ by the
family of sequents~$(\sigma_i)_i$, where the sequent~$\sigma_i$ is the same
as~$\sigma$ only that the free variable~$x$ is changed to be of sort~$X_i$ (and
the corresponding change in the consequent and the antecedent is applied,
applying the appropriate coprojection).

After carrying out these steps, the free variables are only of the basic sorts
supplied by the signature of~$\TT$ and existential quantifications only
range over the basic sorts. However, in the consequents and antecedents, still
tuple formers and coprojections may appear. These can be replaced as suggested
by the rules governing these. For instance, an equation~``$\langle x,y \rangle
= \langle x',y' \rangle$'' can be replaced by the conjunction~``$x = x' \wedge
y = y'$'', and an equation~``$\iota_i(x) = \iota_j(y)$'' (where~$\iota_i$
and~$\iota_j$ are coprojections associated with coproduct sorts) can be
replaced by the subsingleton-indexed disjunction~``$\bigvee\{ x = y \,|\, i = j \}$''.
\end{proof}

\begin{thm}\label{thm:definability}
Let~$\TT$ be a geometric theory. Let~$x_1\?X_1,\ldots,x_n\?X_n$ be a context over the
signature of~$\TT$. Let~$\mathrm{Form}^\star_{\vec
x}(\ul{\TT}/U_\TT)/(\dashv\vdash_{\vec x})$ be the~$\Set[\TT]$-object of
geometric$^\star$ formulas over the signature of~$\ul{\TT}/U_\TT$ in the
context~$\vec x$, where any two such formulas are identified if and only
if~$\ul{\TT}/U_\TT$ proves them equivalent.
Then the canonical morphism
\[ \mathrm{Form}^\star_{\vec x}(\ul{\TT}/U_\TT)/(\dashv\vdash_{\vec x})
  \longrightarrow P(\yon X_1 \times \cdots \times \yon X_n) \]
sending, internally speaking, the equivalence class of a geometric$^\star$
formula~$\varphi$ to the subset~$\{ (x_1,\ldots,x_n) \,|\, \text{$\varphi$
holds for~$(x_1,\ldots,x_n)$} \}$ is an isomorphism.
\end{thm}

\begin{proof}Injectivity is by the Nullstellensatz of
Theorem~\ref{thm:nullstellensatz}. Surjectivity is by the definability
result~\cite[Theorem~2.4]{caramello:definability}, exploiting that the internal
statement localizes well by Lemma~\ref{lemma:truth-to-provability}.
\end{proof}

\begin{rem}\label{rem:definability-entails-nullstellensatz}
The proof of Theorem~\ref{thm:definability} used the Nullstellensatz
of Theorem~\ref{thm:nullstellensatz}. Conversely,
Theorem~\ref{thm:definability} implies Theorem~\ref{thm:nullstellensatz}.
Indeed, arguing internally, let~$\sigma = (\varphi \seq{\vec x} \psi)$ be a
geometric$^\star$ sequent over the signature of~$\ul{\TT}/U_\TT$ such
that~$\sigma$ holds for~$U_\TT$. Then the subsets~$\{ (\vec x) \,|\, \varphi
\}$ and~$\{ (\vec x) \,|\, \varphi \wedge \psi \}$ are equal. Hence the
assumption implies that the formulas~$\varphi$
and~$\varphi \wedge \psi$ are provably equivalent.
Thus~$\ul{\TT}/U_\TT$ proves~$(\varphi \seq{\vec x} \psi)$.
\end{rem}

\begin{cor}Let~$\TT$ be a geometric theory. Let~$\{\vec x\_ \varphi\}$
and~$\{\vec y\_ \psi\}$ be geometric formulas in given contexts. Then,
internally to~$\Set[\TT]$, the canonical map from the set of equivalence classes
of~$\ul{\TT}/U$-provably functional geometric$^\star$ formulas
from~$\{\vec x\_ \varphi\}$ to~$\{\vec y\_ \psi\}$ to the set of maps~$\{(\vec y)
\,|\, \psi \}^{\{(\vec x) \,|\, \varphi\}}$ is a bijection.
\end{cor}

\begin{proof}We argue internally to~$\Set[\TT]$.
The canonical map sends an equivalence class~$[\theta]$ to the unique map~$f :
\{(\vec x) \,|\, \varphi\} \to \{(\vec y) \,|\, \psi \}$ whose graph is given
by the set~$\{ (\vec x, \vec y) \,|\, \theta \}$.

For verifying surjectivity, let a map~$f : \{(\vec x) \,|\, \varphi\} \to
\{(\vec y) \,|\, \psi \}$ be given. Then its graph is a subset of~$\vec X
\times \vec Y$, hence by Theorem~\ref{thm:definability} given by a
geometric$^\star$ formula~$\theta$. Because~$f$ is a map, this formula is
functional; and by the Nullstellensatz, it is~$\ul{\TT}/U_\TT$-provably so.

For verifying injectivity, let~$\theta$ and~$\theta'$
be~$\ul{\TT}/U_\TT$-provably functional formulas which give rise to
identical maps. Then they also give rise to identical graphs, hence
are~$\ul{\TT}/U_\TT$-provably equivalent by
Theorem~\ref{thm:definability}.
\end{proof}

\begin{thm}\label{thm:higher-order-nullstellensatz}
Let~$\TT$ be a geometric theory. Then, internally to~$\Set[\TT]$, for any
extended geometric$^\star$ sequent~$\sigma$ over the signature
of~$\ul{\TT}/U$, the following statements are equivalent:
\begin{enumerate}
\item The sequent~$\sigma$ holds for~$U_\TT$. \smallskip
\item The sequent~$\sigma$ is provable modulo~$\ul{\TT}/U_\TT$ in extended
geometric logic.
\end{enumerate}
\end{thm}

\begin{proof}The implication~$(2) \Rightarrow (1)$ is
immediate since~$U_\TT$ is a model of~$\ul{\TT}/U_\TT$. The converse direction is by
Lemma~\ref{lemma:extended-conservative}, which holds internally in~$\Set[\TT]$
as the proof we supplied is constructive, and by the Nullstellensatz for ordinary
geometric logic of Theorem~\ref{thm:nullstellensatz}.
\end{proof}

\begin{thm}\label{thm:higher-order-characterization}
Let~$\TT$ be a geometric theory. Let~$\chi$ be a higher-order formula over
the signature of~$\TT$. Then the following statements are equivalent:
\begin{enumerate}
\item The formula~$\chi$ holds for~$U_\TT$. \smallskip
\item The formula~$\chi$ is provable in higher-order intuitionistic logic
modulo the axioms of~$\TT$ and the additional axiom scheme
\begin{equation}\label{eq:higher-order-nullstellensatz}\tag{$\P$}
  \speak{the map~$\mathrm{Form}^\star_{\vec
  x}(\ul{\TT}/U_\TT)/(\dashv\vdash_{\vec x}) \longrightarrow P(X_1 \times
  \cdots \times X_n)$ is bijective},
\end{equation}
where~$X_1,\ldots,X_n$ is any list of sorts.
% XXX think about variables...
\end{enumerate}
\end{thm}

\begin{proof}Theorem~\ref{thm:definability} on the semantic side and the axiom
scheme~\eqref{eq:higher-order-nullstellensatz} on the syntactic side allow us to replace any mention of a
powersort~$P(X)$ in~$\chi$
by~$\mathrm{Form}^\star_{x\!\?\!X}(\ul{\TT}/U_\TT)/({\dashv\vdash_x})$,
similarly to how the proof of Lemma~\ref{lemma:extended-conservative} compiles
extended geometric logic to ordinary geometric. Then we
can argue as in the proof of Theorem~\ref{thm:characterization}, noting that
the axiom scheme indeed entails the axiom scheme~\eqref{eq:nullstellensatz} by
Remark~\ref{rem:definability-entails-nullstellensatz}.\end{proof}

% XXX check

%In einem ersten Schritt schreiben wir alle Existenzquantifikationen und freie Variablen
%über Potenzsorten um. Aus "exists A : P(X)" wird "exists φ :
%Form*(T/U_T)_{x:X}/-||-". (Dabei kann X immer noch eine abgeleitete Sorte sein!) Aus
%der freien Variable "A : P(X)" wird analog eine freie Variable.
%
%Entsprechend verändern wir den Rumpf. Aus "x0 ∈ A" wird φ[x0/x].
%
%Dann sind wir fertig mit dem Nullstellensatz für extended geometric logic.
%
%Noch klären:
%* P(X) x Y
%* Form* Teil von extended geometric logic?
%* Beweisbarkeit modulo extended geometric logic ist geometrische Formel?


\section{Applications}
\label{sect:applications}

\subsection{Nongeometric sequents in the object classifier}

Butz and Johnstone~\cite{butz-johnstone:first-order} list several nongeometric sequents holding in the
classifying topos of the theory~$\OO$ of objects, the theory with a single sort and
no function symbols, relation symbols or axioms. In particular, they present
the following ones.
\begin{align*}
  \forall x,y\?U_\OO\_ \neg\neg(x = y) &&
  \forall x_1,\ldots,x_n\?U_\OO\_ \neg \forall y\?U_\OO\_ \bigvee_{i=1}^n (y = x_i)
\end{align*}
Intuitively, the first sequent expresses that~$U_\OO$ is close to a subsingleton, while
the second expresses that~$U_\OO$ is close to being infinite. Using the
Nullstellensatz, these formulas can be verified as follows.

We argue internally to~$\Set[\OO]$. Let~$x,y\?U_\OO$ and assume~$\neg(x = y)$.
By the Nullstellensatz, the theory~$\ul{\OO}/U_\OO$ proves~$(x = y \seq{[]} \bot)$. Hence this sequent holds
of any model of~$\ul{\OO}/U_\OO$, in particular of the
quotient~$U_\OO/(x \sim y)$. Hence~$\bot$ holds for this model, that is, we
have a contradiction.

For the second formula, let~$x_1,\ldots,x_n\?U_\OO$ and assume~$\forall
y\?U_\OO\_ \bigvee_{i=1}^n (y = x_i)$. By the Nullstellensatz, this universal
statement is provable and hence holds for every~$\ul{\OO}/U_\OO$-model. But it
does not hold for~$U_\OO \amalg \{\star\}$.

The argument using the Nullstellensatz makes it transparent that both formulas
are also satisfied by the generic model of any Horn theory~$\TT$: In that case,
instead of constructing the quotient set~$U_\OO/(x \sim y)$, we construct the
quotient model~$(\ul{\TT}/U_\TT)\langle \,|\, x = y \rangle$; and instead of~$U_\OO
\amalg \{\star\}$, we construct the free model~$(\ul{\TT}/U_\TT)\langle \star
\,|\, \rangle$ (XXX need to exclude trivial singleton theory).


\subsection{Nongeometric sequents in the ring classifier}

Each of the nongeometric sequents mentioned in Section~\ref{sect:introduction}
can be deduced from the first-order or higher-order Nullstellensatz. Here we
briefly indicate how this works using two examples.

Let~$\TT$ be the theory of rings. Then, internally to~$\Set[\TT]$, we have for
any element~$x \? U_\TT$:
\begin{align*}
  (x = 0 \Rightarrow 1 = 0) &\Longrightarrow \speak{$x$ is invertible} \quad\text{and} \\
  (\speak{$x$ is invertible} \Rightarrow 1 = 0) &\Longrightarrow \speak{$x$ is nilpotent}.
\end{align*}
To verify the first claim, assume~$(x = 0 \Rightarrow 1 = 0)$. By the
Nullstellensatz of Theorem~\ref{thm:nullstellensatz}, the
theory~$\ul{\TT}/U_\TT$ proves this fact. Hence in particular it holds in
the~$U_\TT$-algebra~$U_\TT/(x)$. Because~$x = 0$ in~$U_\TT/(x)$, we have~$1 =
0$ in~$U_\TT/(x)$, that is~$1 \in (x)$, hence~$x$ is invertible.

To verify the second claim, assume~$(\speak{$x$ is invertible} \Rightarrow 1 =
0)$. By the Nullstellensatz, the theory~$\ul{\TT}/U_\TT$ proves this fact,
hence in particular it holds in~$U_\TT[x^{-1}]$. Because~$x$ is invertible in
this~$U_\TT$-algebra, we have~$1 = 0$ in~$U_\TT[x^{-1}]$. Hence~$x$ is
nilpotent.

Thanks to the version of the Nullstellensatz pertaining Horn consequents given
in Corollary~\ref{corollary:nullstellensatz-horn}, these two arguments can also be
carried out in the classifying topos of local rings. It is instructive to
consider how we would have to argue if we wanted to use only the unmodified
Nullstellensatz:

Assume~$(x = 0 \Rightarrow 1 = 0)$. By the Nullstellensatz, the theory of local
rings proves this fact. From this we may not conclude that it holds
for~$U_\TT/(x)$, as this~$U_\TT$-algebra might not be local. But we may
conclude that it holds for~$\O_{\Spec(U_\TT/(x))}$, the structure sheaf of the affine scheme
given by~$U_\TT/(x)$. This sheaf is not a model of~$\ul{\TT}/U_\TT$, but it is
so from the point of view of the topos of sheaves over~$\Spec(U_\TT/(x))$. From
the point of view of that topos,~$x = 0$ in~$\O_{\Spec(U_\TT/(x))}$, hence~$1 =
0$ in~$\O_{\Spec(U_\TT/(x))}$. This amounts to~$U_\TT/(x)$ being the zero ring,
hence~$x$ is invertible in~$U_\TT$.


\subsection{On the Kock--Lawvere axiom in synthetic differential geometry}

The generic local ring~$\affl$ validates the following strong form of the Kock--Lawvere
axiom (Theorem~\ref{thm:quasicoherence}): \emph{For any finitely
presented~$\affl$-algebra~$A$, the canonical map~$A \to (\affl)^{\Spec(A)}$ is
an isomorphism of~$\affl$-algebras.} The special case~$A \defeq \affl[X]$
implies that any map~$\affl \to \affl$ is given by a polynomial,
since~$\Spec(\affl[X]) = \Hom_\affl(\affl[X],\affl) \cong \affl$.

In contrast, in most models of synthetic differential geometry, we only have
the following weaker statement: \emph{For any Weil algebra~$A$, the canonical
map~$A \to \RR^{\Spec(A)}$ is an isomorphism of~$\RR$-algebras.} Here~$\RR$
refers to the canonical line object (the image of the manifold~$\RR^1$ in the
model) and~$\Spec(A)$ is the set of~$\RR$-algebra homomorphisms~$A \to \RR$.
Any Weil algebra is finitely presented, but the converse fails; in particular,
the polynomial algebra~$\RR[X]$ is not a Weil algebra, hence there is no reason
to believe that any map~$\RR \to \RR$ is given by a polynomial.

The quasicoherence statement of
Theorem~\ref{thm:quasicoherence} can shed light on this discrepancy. % XXX

% XXX

% Zariski

% Kock--Lawvere in SDG

% XXX object classifier and related

%We do have, for any geometric sequent~$\sigma$, that
%\[ \Set[\TT] \models \speak{$\sigma$ holds for~$U_\TT$} \quad\text{iff}\quad
%  \Set[\TT] \models \speak{$\ul{\TT}$ proves~$\sigma$}, \]
%since~$\Set[\TT] \models \speak{$\sigma$ holds for~$U_\TT$}$ implies that~$\TT$
%proves~$\sigma$ and since~$\TT \vdash \sigma$ implies~$\E \models
%(\ul{\TT} \vdash \sigma)$ for any topos~$\E$ over~$\Set$. However, this
%equivalence is not stable under slicing ...



\printbibliography

\end{document}

* Discuss case of SDG: Why does the Kock--Lawvere there hold only for Weil
  algebras? Answer: It doesn't really! We do have that [U,U] is isomorphic to
  the free C^∞-ring on one generator. But this observation doesn't appear to be
  useful for further developments.

* XXX Cite Filip Bár?

* XXX Upgrade Horn section to cartesian theories?

* XXX fix "first-order" usage everywhere

* XXX Cite C2.5.4 or similar

% XXX Check: https://arxiv.org/abs/1811.08838

* Cite
  https://www.semanticscholar.org/reader/c96bd90b00671cf83205e675e59be7edaddee387
  Towards a geometry of syntax, Jonathan Sterling

* Cite: https://link.springer.com/chapter/10.1007/BFb0061363