\documentstyle[12pt]{article}

\title{Intuitive Counterexamples for Constructive Fallacies}

\author{
        James Lipton\\
        Wesleyan University \and
        Michael J. O'Donnell\\
        The University of Chicago
}

\date{Presented 25 August, 1994}

\input macros

\begin{document}

\maketitle

This paper was presented at the {\it Mathematical Foundations of
Computer Science 1994 --- 19th International Symposium, MFCS '94,
Ko\u{s}ice, Slovakia, August 1994 --- Proceedings, Lecture Notes in
Computer Science,} volume 841, Igor Pr\'{\i}vara, Branislav Rovan and
Peter Ru\u{z}i\u{c}ka editors, Springer-Verlag, 1984, pp.\ 87--111.

\begin{abstract}
Formal countermodels may be used to justify the unprovability of
formulae in the Heyting calculus (the best accepted formal system for
constructive reasoning), on the grounds that unprovable formulae are
constructively invalid. We argue that the {\em intuitive\/} impact of
such countermodels becomes more transparent and convincing as we move
from Kripke/Beth models based on possible worlds, to L\"auchli
realizability models. We introduce a new semantics for constructive
reasoning, called {\em relational realizability,} which strengthens
further the intuitive impact of L\"auchli realizability. But, none of
these model theories provides countermodels with the compelling impact
of classical truth-table countermodels for classically unprovable
formulae.

We prove soundness of the Heyting calculus for relational
realizability, and conjecture that there is a constructive choice-free
proof of completeness. In this respect, relational realizability
improves the metamathematical constructivity of L\"auchli
realizability (which uses choice in two crucial ways to prove
completeness) in the same sort of way Beth semantics improves Kripke
semantics.
\end{abstract}

\section{The Intuitive Impact of Countermodels}

Imagine that we believe in the suitability of a formal system ${\cal
P}$ of proof as a basis for useful reasoning in some language ${\cal
L}$. We are trying to sell ${\cal P}$ to a customer. The customer is
not trained in formal metamathematics, but she has an excellent
intuitive grasp of the meanings of given formulae in concrete
circumstances. There are a number of grounds on which the customer
might challenge the suitability of ${\cal P}$, but we focus attention
on one. Suppose that she produces a formula $\alpha$ that is not
provable in ${\cal P}$, and argues that therefore ${\cal P}$ is not
powerful enough for practical use. We must convince her, on intuitive
grounds, that the failure of ${\cal P}$ to prove $\alpha$ is a useful
feature, rather than a serious lacuna. To this end, we must describe a
{\em conceivable set of circumstances\/} ${\cal C}$ that might occur
in the real world that language ${\cal L}$ describes, and interpret
the primitive nonlogical symbols of $\alpha$ in ${\cal C}$ in such a
way that $\alpha$ is clearly false. So, we argue, ${\cal P}$ is
excused from proving $\alpha$ because $\alpha$ is not {\em valid\/}
(not reliably true in all circumstances).

In order to prepare for such a debate, we might study formal
semantics. In particular, we formalize the notion of a ``conceivable
set of circumstances'' as a {\em model\/} for ${\cal L}$, and define
what it means for a formula $\alpha$ of ${\cal L}$ to be true in a
particular model ${\cal M}$. Then, we formalize {\em validity\/} of a
formula as truth in all models. Finally, we demonstrate that ${\cal
P}$ is {\em sound\/} (every provable formula is valid) and {\em
complete\/} (every valid formula is provable) with respect to our
formal model theory. Soundness may help to answer a challenge of
incorrect proof, while completeness may help to answer the challenge
of insufficient power proposed above.

Back to the customer, who has criticized ${\cal P}$ for its inability
to prove $\alpha$. Our demonstration of completeness, if it is
appropriately constructive, provides us with a {\em countermodel\/}
${\cal M}_C$ in which $\alpha$ is false. In order to convince the
customer, we must translate ${\cal M}_C$ into an intuitive description
of conceivable real circumstances in which $\alpha$ is clearly false.
Of course the success of our argument depends on the intuitive beliefs
that our customer holds. If the customer's beliefs support classical
logic, and ${\cal P}$ is a complete formal system for classical proof,
then we are on very strong ground. The usual truth-table models for
classical logic translate naturally into simple sorts of conceivable
circumstances and absolutely concrete interpretations of primitive
nonlogical symbols. But, if our customer's beliefs support
constructive logic, and ${\cal P}$ is the Heyting calculus (which is
complete for several well-known formal model-theoretic semantics), the
translation of a formal countermodel into an intuitively convincing
description is quite a bit harder.

In this paper, we compare the intuitive impact of three sorts of
models for constructive logic: {\em Kripke/Beth\/} models based on
possible worlds, {\em L\"auchli realizability\/} models based on the
formulae as types idea, and a new sort of model that we call {\em
relational realizability\/} models, refining L\"auchli's ideas. There
appear to be a number of different intuitive ideologies that lead to a
belief in constructive logic. We do not insist on Brouwer's,
Heyting's, Kolmogorov's, Bishop's or any other predetermined ideology
supporting constructive logic. Rather, for each formal model theory,
we seek the most natural intuitive explanation of it. We do not argue
about which intuitive ideologies are metaphysically correct (perhaps
each is correct for a different application of logical
reasoning). Rather, we criticize the transparency with which each
formal model theory is justified by its natural intuitive
explanation. We find that this transparency improves from Kripke/Beth
models through L\"auchli models to relational realizability models,
but it never approaches the clear connection between classical
intuitions and truth-table models.

\section{Formulae, Proofs, and Sequents}

The rest of this paper discusses formulae, proofs of formulae, and
models for formulae in the {\em positive first-order predicate
calculus\/} and the {\em positive propositional calculus.}
``Positive'' means that we do not allow the logical negation symbol
($\lnot$). Every one of the systems that we discuss can be extended
easily to deal with negation, but in some cases that extension is
somewhat subtle to understand---for example see~\cite{KMO} for a
discussion of negation in L\"auchli realizability models. We use a
predicate calculus without function symbols and without equality. All
of the proposed systems can be extended to deal with functions and
equality, but such an extension would only obscure the message of this
paper.

\begin{definition}
\label{def:formula}
{\raggedright
  Assume that there is an infinite set\/ $\Var$ of {\em variables.}
  Also, for each\/ \mbox{$i\geq 0$} there is an infinite set\/
  $\Pred{i}$ of\/ {\em $i$-ary predicate symbols.}
  The set of {\em atomic formulae\/} is
  $$\AT=\setof{\gamma(x_1,\ldots,x_n)}{\gamma\in\Pred{n}\mbox{, }
    x_1,\ldots,x_n\in\Var}$$
  (the degenerate case\/
  \mbox{$\alpha()$} where\/ \mbox{$\alpha\in\Pred{0}$} is written\/
  $\alpha$).
  The set\/ $\PF$ of {\em positive first-order predicate formulae\/} is
  defined inductively as follows: \mbox{$\AT\subseteq\PF$}, and
  iff\/ \mbox{$\alpha,\beta\in\PF$} and\/ \mbox{$x\in\Var$}, then
      $$\begin{array}{lllll}
       (\alpha\lor\beta)\in\PF &
       (\alpha\land\beta)\in\PF &
       (\alpha\limplies\beta)\in\PF &
       (\forall x\sepdot\alpha)\in\PF &
       (\exists x\sepdot\alpha)\in\PF
      \end{array}$$
  The concepts of\/ {\em subformulae,} and\/ {\em free\/} and\/ {\em
  bound\/} occurrences of variables, are defined in the usual manner
  \cite{stenlund}. $\subst{x}{y}{\alpha}$ denotes the result of
  substituting\/ $x$ for every free occurrence of\/ $y$ in\/ $\alpha$
  after renaming bound variables of\/ $\alpha$ so that the
  substituted\/ $x$s are free in the result. A formula with no free
  variables is a {\em closed formula,} or a {\em sentence.}

  Although it does not appear in formulae, for metalogical discussion
  an additional formal symbol $\Ind$ is useful to stand for the domain
  of individuals over which variables range.

  The set\/ $\PPF$ of {\em positive propositional formulae\/} is the
  subset of $\PF$ consisting of all formulae with no occurrence of the
  quantifiers $\forall$ and $\exists$ and no occurrence of predicates
  with arity greater than $0$.
}
\end{definition}

Proofs are the formal analogues of rigorously reasoned arguments.
Formal descriptions of proofs are often treated as mere syntactic
devices for enumerating true formulae. In constructive logic, we can
get a deeper insight into proofs by regarding a proof formula as a
syntactic object denoting a semantic construction. So proof formulae,
as well as propositional formulae, have semantic content. The
essential idea is that a proof formula is a term in the {\em typed
lambda calculus,} and the type of the term is the theorem that it
proves~\cite{prawitz,stenlund,GirardLT}. It is straightforward to read
a typed lambda term of type $\alpha$, on the one hand as a {\em
natural deduction\/} proof of $\alpha$, or on the other hand as a
program defining a uniform construction demonstrating the validity of
$\alpha$. The interpretation of typed ambda terms as propositional
proof formulae is discussed in more detail in~\cite{KMO}. {\em Sequent
derivations\/} are less transparent to the intuition than proof terms,
but more flexible for certain metamathematical arguments, so for this
paper we define proof in terms of sequents.

\begin{definition}
  \label{def:sequent}
{\raggedright
  A\/ {\em sequent\/} is an ordered pair of finite subsets of\/ $\PF$.
}
\end{definition}
When \mbox{$\Gamma,\Psi\subseteq\PF$} are finite sets of formulae, the
sequent \mbox{$\tuple{\Gamma,\Psi}$} is written
\mbox{$\Gamma\proves\Psi$}. Furthermore, set braces are omitted in
descriptions of $\Gamma$ and $\Psi$, and unions are denoted by commas.
So, for example, \mbox{$\Gamma,\alpha\proves\beta,\Psi$} denotes the
pair \mbox{$\tuple{\Gamma\cup\{\alpha\},\{\beta\}\cup\Psi}$}. The
intended meaning of \mbox{$\Gamma\proves\Psi$} is that, whenever the
conjunction of $\Gamma$ holds, the disjunction of $\Psi$ holds as well.
\begin{definition}
  \label{def:derivable-sequent}
{\raggedright
  A sequent\/ \mbox{$\Gamma\proves\Psi$} is\/ {\em derivable\/} if and
  only if there is a finite sequence $\Gamma_0\proves\Psi_0,$
  $\ldots,$ $\Gamma_n\proves\Psi_n$ of sequents such that
  \mbox{$\Gamma_n=\Gamma$}, \mbox{$\Psi_n=\Psi$}, and for each\/
  \mbox{$0\leq i\leq n$} there exists\/ \mbox{$m\geq 0$} and\/
  \mbox{$j_1,\ldots,j_m<i$} such that\/ \mbox{$\Gamma_i\proves\Psi_i$}
  follows from\/ \mbox{$\Gamma_{j_1}\proves\Psi_{j_1},\ldots,
  \Gamma_{j_m}\proves\Psi_{j_m}$} by one of the rules in
  Table~\ref{tab:sequent-rules}.  These are essentially Beth's tableaux
  rules~\cite{beth:foundations-of-mathematics,fitting:intuitionistic-logic},
  translated into sequent notation.  Notice that the basis rule (B)
  has no hypotheses, corresponding to\/ \mbox{$m=0$} in the last
  clause above.
}
  \begin{table}[htpb]\fbox{\parbox{\textwidth}{
  \begin{displaymath}
  \begin{array}{c@{\hspace{2.5cm}}c}
\\
    % Line 1: (B)
    \multicolumn{2}{c}{\rmbox{(B)}~\Gamma,\alpha\proves\alpha,\Psi}\\ \\

    % Line 2: (and-L) (and-R)
    \rmbox{($\land$L)}~
    \derive{\Gamma,\alpha,\beta,\alpha\land\beta\proves\Psi}
           {\Gamma,\alpha\land\beta\proves\Psi} &

    \rmbox{($\land$R)}~
    \derive{\Gamma\proves\alpha\land\beta,\alpha,\Psi\\
            \Gamma\proves\alpha\land\beta,\beta,\Psi}
           {\Gamma\proves\alpha\land\beta,\Psi}\\ \\

    % Line 3: (or-L) (or-R)
    \rmbox{($\lor$L)}~
    \derive{\Gamma,\alpha,\alpha\lor\beta\proves\Psi\\
            \Gamma,\beta,\alpha\lor\beta\proves\Psi}
           {\Gamma,\alpha\lor\beta\proves\Psi} &

    \rmbox{($\lor$R)}~
    \derive{\Gamma\proves\alpha\lor\beta,\alpha,\beta,\Psi}
           {\Gamma\proves\alpha\lor\beta,\Psi}\\ \\

    % Line 4: (=>L) (=>R)
    \rmbox{($\limplies$L)}~
    \derive{\Gamma,\alpha\limplies\beta\proves\alpha,\Psi\\
            \Gamma,\beta,\alpha\limplies\beta\proves\Psi}
           {\Gamma,\alpha\limplies\beta\proves\Psi} &

    \rmbox{($\limplies$RS)}~
    \derive{\Gamma,\alpha\proves\beta}
           {\Gamma\proves\alpha\limplies\beta,\Psi}\\ \\

    % Line 5: (=>RW)
%    &
%    \rmbox{($\limplies$RW)}~
%    \derive{\Gamma\proves\alpha\limplies\beta,\beta,\Psi}
%           {\Gamma\proves\alpha\limplies\beta,\Psi}\\ \\

    % Line 6: (AL) (AR)
    \rmbox{($\forall$L)}~
    \derive{\Gamma,\subst{y}{x}{\alpha},\forall x\sepdot\alpha\proves\Psi}
           {\Gamma,\forall x\sepdot\alpha\proves\Psi} &

    \rmbox{($\forall$R)\footnotemark[1]}~
    \derive{\Gamma\proves\forall x\sepdot\alpha,\subst{y}{x}{\alpha}\Psi}
           {\Gamma\proves\forall x\sepdot\alpha,\Psi}\\ \\

    % Line 7: (EL) (ER)
    \rmbox{($\exists$L)\footnotemark[1]}~
    \derive{\Gamma,\subst{y}{x}{\alpha},\exists x\sepdot\alpha\proves\Psi}
           {\Gamma,\exists x\sepdot\alpha\proves\Psi} &

    \rmbox{($\exists$R)}~
    \derive{\Gamma\proves\exists x\sepdot\alpha,\subst{y}{x}{\alpha},\Psi}
           {\Gamma\proves\exists x\sepdot\alpha,\Psi}

  \end{array}
  \end{displaymath}
  \begin{center}
    {}\footnotemark[1]In $\forall$R and $\exists$L,
      $x$ must not be free in $\Gamma$, $\Psi$.
  \end{center}
  \caption{Constructive Sequent Rules\label{tab:sequent-rules}}}}
  \end{table}
\end{definition}

The proof formulae and the constructive sequent rules are variations
on the {\em Heyting predicate
calculus\/}~\cite{heyting:regeln-intuitionistischen-logik}. A formula
$\alpha$ is said to be proved constructively when we derive the
sequent $\proves\alpha$. The derivability of sequents
$\Gamma\proves\Psi$ with nonempty left-hand sides is important for the
understanding of provable {\em inferences,} which go beyond provable
{\em formulae,} but this paper is concerned mostly with the provable
formulae.

\section{Classical Truth-Table Models}
\label{sec:classical}

The definition of classical truth-table models is very
familiar~\cite{tarski:classical-semantics,wittgenstein:tractatus} so
we omit it here, and merely consider one particular example. The
propositional formula
$(\alpha\limplies\beta)\limplies(\beta\limplies\alpha)$ is not
provable. When challenged by our customer to justify this omission, we
may use a demonstration of completeness for classical logic to produce
the countermodel given by the truth table in
Figure~\ref{fig:2-countermodels}a.
\begin{figure}\fbox{\parbox{\textwidth}{
\begin{displaymath}
\renewcommand{\arraystretch}{2}
\begin{array}{c@{\hspace{2cm}}c}
\renewcommand{\arraystretch}{1}
\begin{array}[b]{|c|c|}
\hline
\alpha & F \\
\hline
\beta & T \\
\hline
\end{array} &
{\setlength{\unitlength}{.1 cm}
  \begin{picture}(20,20)(-10,-6)
    \thicklines
    \put(1,1){        \vector(1,1){8}                         }
    \put(-1,1){       \vector(-1,1){8}                        }
    \put(0,0){        \circle*{1}                             }
    \put(0,-3){       \makebox(0,0)[t]{$\set{}$}              }
    \put(-10,10){     \circle*{1}                             }
    \put(-10,13){     \makebox(0,0)[b]{$\set{\alpha}$} }
    \put(10,10){      \circle*{1}                             }
    \put(10,13){      \makebox(0,0)[b]{$\set{\beta}$}  }
  \end{picture}
} \\
\parbox{6cm}{\centering a. Classical countermodel for\\
  $(\alpha\limplies\beta)\limplies(\beta\limplies\alpha)$} &
\parbox{6cm}{\centering b. Kripke countermodel for\\
  $(\alpha\limplies\beta)\lor(\beta\limplies\alpha)$}
\end{array}
\end{displaymath}
\caption{Classical and Kripke Countermodels for Unprovable Formulae
\label{fig:2-countermodels}}}}
\end{figure}
Then, we may use this countermodel to answer the customer with the
following argument.
\begin{quote}{\em
Suppose that $\alpha$ is the proposition, {\em ``In the diagram of
Figure~\ref{fig:2-countermodels}a, the symbol `$\alpha$' appears in
the same row with the symbol `$T$',''} and $\beta$ is the proposition,
{\em ``In the diagram of Figure~\ref{fig:2-countermodels}a, the symbol
`$\beta$' appears in the same row with the symbol `$T$'.''}  Clearly
$\alpha$ is false, but $\beta$ is true. So,
\mbox{$\alpha\limplies\beta$} is true, and
\mbox{$\beta\limplies\alpha$} is false. Therefore
\mbox{$(\alpha\limplies\beta)\limplies(\beta\limplies\alpha)$} is
false.
}\end{quote}
Our argument is hard to resist, because we have interpreted $\alpha$
and $\beta$ as absolutely concrete propositions in natural language,
referring to a physical presentation of a diagram. And, in arguing that
$(\alpha\limplies\beta)\limplies(\beta\limplies\alpha)$, we rely only
on the facts that everything implies a truth, and that truth cannot
imply falsehood. These facts are admitted by constructivists as well
as classical reasoners. The shortcoming of classical truth-table
models for justifying formal systems of constructive proof is that
they provide no countermodels for other formulae, such as
$(\alpha\limplies\beta)\lor(\beta\limplies\alpha)$, that are provable
classically but not constructively.

\section{Kripke/Beth Models}

In order to justify the unprovability of formulae such as
$(\alpha\limplies\beta)\lor(\beta\limplies\alpha)$, we need new sorts
of countermodels, and new translations of countermodels into intuitive
circumstances. The best-known formal model theory for constructive
logic is due to Kripke~\cite{kripke:semantics-of-intuitionism} (an
important variation due to Beth~\cite{beth:foundations-of-mathematics}
is technically superior for some purposes, but is open to the same
critique as Kripke semantics from the standpoint of intuitive
counterexamples). The Heyting calculus is sound and complete for
Kripke and Beth model theory.  Soundness may be proved
constructively. Completeness with respect to Kripke semantics is
constructive for the propositional calculus, but inherently
nonconstructive for the predicate calculus; completeness with respect
to a variant of Beth semantics is constructive for the predicate
calculus~\cite{troelstra-van-dalen}.

Kripke and Beth interpret constructive logic as a modal system, in
which $\land$ and $\lor$ behave classically, but $\alpha \limplies
\beta$ has the modal interpretation that in every {\em reachable\/}
world where $\alpha$ holds, $\beta$ holds as well. That is, $\alpha$
constructively implies $\beta$ if {\em necessarily\/} $\alpha$
classically implies $\beta$. The reachability relation is required to
be reflexive and transitive, but not necessarily symmetric. In the
terminology of modal semantics, these are the $S_4$
models~\cite{kripke:modal-semantics-I}. For brevity, we present only
Kripke models for the propositional calculus---the extension to
predicate calculus is known~\cite{troelstra-van-dalen}, but not needed
here.

\begin{definition}
  \label{def:kripke-model}
{\raggedright
  A\/ {\em Kripke model\/} for the positive constructive propositional
  calculus is a quadruple\/
  $\model{M}=\tuple{\universe{W},\preceq,\nu}$, where\/ $\universe{W}$
  is a set of\/ {\em worlds\/}, $\preceq$ is a reflexive, transitive
  binary relation on\/ $\universe{W}$ called\/ {\em reachability\/},
  and\/ $\nu$ is a function, called\/ {\em satisfaction\/}, from\/
  $\universe{W}$ to valuations on atomic propositional symbols. $\nu$
  is closed under reachability, i.e., if\/
  $\world{v}\preceq\world{w}$, and if\/ $\nu_{\world{v}}(\alpha)$,
  then\/ $\nu_{\world{w}}(\alpha)$.
}
\end{definition}
Notice that we write $\nu_{\world{w}}(\alpha)$ rather than
$\nu(\world{w})(\alpha)$.  We extend the satifaction function from
atomic formulae to arbitrary formulae as follows:

\begin{definition}
  \label{def:kripke-truth}
{\raggedright
  Let $\model{M}=\tuple{\universe{W},\preceq,\nu}$ be a Kripke
  model. The relation $\model{M},\world{w}\kmodels\alpha$ is defined
  inductively for $\world{w}\in\universe{W}$ and propositional formulae
  $\alpha$ as follows:
  \begin{itemize}
    \item If $\alpha$ is an atomic propositional symbol, then
      $\model{M},\world{w}\kmodels\alpha$ if and only if
      $\nu_{\world{w}}(\alpha)$;
    \item $\model{M},\world{w}\kmodels\alpha\land\beta$ if and only if
      $\model{M},\world{w}\kmodels\alpha$ and $\model{M},\world{w}
      \kmodels\beta$;
    \item $\model{M},\world{w}\kmodels\alpha\lor\beta$ if and only if
      $\model{M},\world{w}\kmodels\alpha$ or $\model{M},\world{w}
      \kmodels\beta$;
    \item $\model{M},\world{w}\kmodels\alpha\limplies\beta$ if and
      only if for every world $\world{v}$ such that $\world{w}\preceq
      \world{v}$, and such that $\model{M}, \world{v}\kmodels\alpha$, we
      also have $\model{M},\world{v}\kmodels\beta$.
  \end{itemize}
  $\alpha$ is {\em true\/} in $\model{M}$ (written
  $\model{M}\kmodels\alpha$) if and only if $\model{M},\world{w}
    \kmodels\alpha$ for every world $\world{w}$ in $\universe{W}$.
}
\end{definition}
The natural Kripke countermodel for
$(\alpha\limplies\beta)\lor(\beta\limplies\alpha)$ is shown in
Figure~\ref{fig:2-countermodels}b.

The natural intuitive interpretation of the formal model requires us
to understand constructive logic in terms of temporal-epistemic
concepts, with branching time. Roughly, $\world{w}\preceq\world{v}$
means that $\world{w}$ and $\world{v}$ are conceivable sets of
instantaneous circumstances such that in the circumstances of
$\world{w}$, one possible future is the circumstances of $\world{v}$.
$\model{M},\world{w}\kmodels\alpha$ means, not just that $\alpha$ is
true at $\world{w}$, but that $\alpha$ is constructively knowable at
$\world{w}$. $\alpha\limplies\beta$ means that, for every possible
future in which $\alpha$ is knowable, $\beta$ is also knowable. Kripke
and Beth models are very useful for metamathematical investigations,
but they do not correspond convincingly to sets of intuitive
circumstances. Dummet~\cite{dummett:intuitionism} discusses the
intuitive shortcomings of Kripke and Beth semantics. Here, we merely
note the apparent difficulties in interpreting the diagram of
Figure~\ref{fig:2-countermodels}b as a description of circumstances
conceivable to a constructive intuition.

When our customer challenges the unprovability of
$(\alpha\limplies\beta)\lor(\beta\limplies\alpha)$, the natural
response based on the countermodel of
Figure~\ref{fig:2-countermodels}b is something like:
\begin{quote}{\em
Suppose that neither $\alpha$ nor $\beta$ can be verified
constructively right now. Suppose in addition that there is one possible future
in which $\alpha$ can be verified constructively but not $\beta$, and
another possible future in which $\beta$ can be verified
constructively but not $\alpha$. Because of the first possible future,
\mbox{$\alpha\limplies\beta$} is not true, and because of the second
one \mbox{$\beta\limplies\alpha$} is not true.
}\end{quote}
This argument is inherently subjunctive, and does not hold up well if
one wishes to understand the future as a single potential reality but
rather requires the customer to believe in a particular layout of
different contingencies, not all of which will ever be realized. The
requirement for branching time is particularly suspect: we know that
there is only one real future, even though we do not know its
nature. Why can we not use the unicity of the future in constructive
reasoning? The customer must also accept that the {\em particular\/}
diagram given by this model represents a conceivable state of
affairs. It may well be that the fundamental nature of constructions
restricts the possible temporal developments of knowledge in a
significant way. With no formal representations of constructions in
the theory, it is very difficult to judge whether a given formal model
corresponds to an intuitively conceivable state of affairs. Finally,
there does not appear to be any natural interpretation of $\alpha$ and
$\beta$ as concrete propositions based on a Kripke or Beth
countermodel. Where classical truth-table countermodels provide
concrete interpretations of atomic propositional symbols, Kripke and
Beth countermodels represent the possible future results of attempting
to verify those symbols, without interpreting the symbols themselves
in a concrete intuitive way.

\section{Realizability Models}

In order to provide stronger connections between formal models and
constructive intuitions, we seek models that contain explicit
representatives for constructions. Such models arise from the {\em
realizability\/} concepts of
Kleene~\cite{kleene:intuitionistic-number-theory,kleene:realizability-59,kleene-vesley:foundations}
and L\"auchli~\cite{lauchli:realizability-70} and the {\em formulae as
types\/} concepts of Howard and
Tait~\cite{howard:formulae-as-types,curry-feys:combinatory-logic}. We
call such models, with explicit objects standing for constructions,
{\em realizability models.} The word ``realizability'' comes from the
notion that a formula is constructively valid precisely if it is
realized by some construction that demonstrates its validity.

Roughly, a realizability model provides classes of primitive objects
representing evidence for each atomic formula, and builds up evidence
for other formulae by the following rules
{\raggedright
\begin{itemize}
\item evidence for $\alpha\land\beta$ consists of evidence for
  $\alpha$ paired with evidence for $\beta$
\item evidence for $\alpha\lor\beta$ consists either of evidence for
  $\alpha$ or of evidence for $\beta$, marked in such a way that we
  can tell which formula it supports
\item evidence for $\alpha\limplies\beta$ is some sort of function
  transforming evidence for $\alpha$ into evidence for $\beta$
\item evidence for $\forall x\sepdot\alpha$ is some sort of function
  transforming each individual value $d$ into evidence for
  $\subst{d}{x}{\alpha}$
\item evidence for $\exists x\sepdot\alpha$ consists of an individual
  value $d$ paired with evidence for $\subst{d}{x}{\alpha}$
\end{itemize}
}
The basic idea of the nature of constructive evidence results from a
long discussion of evidence with key contributions by Brouwer,
Heyting, and Kolmogorov, for which it is often called the {\em BHK
interpretation\/}~\cite{troelstra-van-dalen}. But, depending on the
precise way in which each item above is interpreted, the BHK
interpretation may support a variety of formal systems, including
classical logic~\cite{troelstra-van-dalen}.

A realizability model theory consists of a precise formalization of
the BHK rules (there are many ways to do this), and also a formal
criterion for distinguishing certain pieces of evidence as realizers.
A formula is true in a model if it has a realizer in the model, and a
formula is valid if it has a realizer in every model. A piece of
evidence for $\alpha$ that is not a realizer has no direct impact on
the truth of $\alpha$, but it affects the truth of formulae containing
$\alpha$, such as $\alpha\limplies\beta$, since a realizer for the
implication must map every piece of evidence for $\alpha$, not just
the realizers. This {\em a posteriori\/} judgement that certain
evidence is a constructively valid realizer, rather than an {\em a
priori\/} inclusion of only the realizers in a model, appears to be
crucial to the technical success of realizability model theories.

It is natural, straightforward, and plausible to interpret classes of
evidence as sets (constructively conceived), and to construct evidence
sets for nonatomic formulae by associating $\land$ with Cartesian
product, $\lor$ with disjoint union, $\limplies$ with the function
space, $\forall$ with the dependent product, and $\exists$ with the
dependent sum (for certain higher-order formal systems, a classical
set-theoretic interpretation fails~\cite{reynolds}, but a constructive
set theory succeeds~\cite{pitts}). The problem is to define what are
the realizers in each of these evidence sets. If we define every piece
of evidence to be a realizer, then we get classical logic---the empty
set represents falsehood, each nonempty set represents truth, and it
is easy to see that the set-theoretic constructions are equivalent to
the classical truth-functional rules. Ideally, we would define the
realizers to be precisely the {\em uniformly constructible\/} objects,
if we only had a formal characterization of uniform
constructibility. The most natural attempt at such a characterization
is to define realizers as the computable objects in each evidence set.
Kleene~\cite{kleene:intuitionistic-number-theory,kleene:realizability-59,kleene-vesley:foundations}
studied this idea, and developed an important theory of computability
on higher types. But, Rose~\cite{rose} showed that the formula
$$((\lnot\lnot\gamma\limplies\gamma)\limplies
(\lnot\lnot\gamma\lor\lnot\gamma))\limplies
(\lnot\lnot\gamma\lor\lnot\gamma)\mbox{ where }
\gamma=(\lnot\alpha\lor\lnot\beta)$$ has a Kleene
realizer. The Rose formula is not provable in the Heyting calculus,
and is generally believed to be invalid for a constructive intuition
(it is known to be invalid in formal Kripke and Beth semantics, as
well as several varieties of realizability semantics).

There is some reason to believe that it is impossible to give a
satisfactory precise characterization of the uniformly constructible
objects, for roughly the same reasons that it is impossible to
enumerate the total computable functions. So, we consider model
theories in which the formal realizers include objects that are
clearly not computable, and therefore not uniformly constructible.
That is, we define the realizers to be the objects satisfying some
intuitively plausible {\em necessary but not sufficient\/} condition
for uniform constructibility. If a formula $\alpha$ has no evidence
satisfying these necessary conditions, then {\em a fortiori\/} it has
no uniformly constructible evidence. In this way, we get countermodels
whose intuitive interpretations no longer depend on the disturbing
notions of contingency and branching time involved in the usual
temporal interpretation of Kripke and Beth models. Unfortunately, we
still cannot produce interpretations of propositional formulae with
the concrete impact of those associated with classical truth table
countermodels in Section~\ref{sec:classical} above.

\subsection{L\"auchli's Realizability Models}

The material in this section summarizes work by Kurtz, Mitchell and
O'Donnell~\cite{KMO} based on L\"auchli's seminal
paper~\cite{lauchli:realizability-70}. L\"auchli analyzed realizability
models in which a piece of evidence is a realizer if and only if it
is invariant under certain permutations. We generalize L\"auchli's
semantics in the obvious way to allow models built from arbitrary
groups of permutations at the atomic level, and we vary L\"auchli's
treatment of quantification to make the connection between evidence in
models and intuitive constructions easier to follow.
\begin{definition}
  \label{def:lauchli-model}
{\raggedright
  A\/ {\em L\"auchli realizability model\/} is a quadruple\/ $\model{M} =
  \tuple{\universe{D},\universe{U},\evidence{P},\noise{N}}$, where
  \begin{itemize}
    \item $\universe{D}$ is a set, called the\/ {\em domain of individuals}
    \item $\universe{U}$ is a set, called the\/ {\em domain of evidence}
    \item $\evidence{P}$ is a mapping from\/
      \mbox{$\{\Ind\}\union\Union_i\Pred{i}$} to subsets of\/
      \mbox{$\universe{D}\union\Union_i(\universe{U}^{\universe{D}^i})$}
      such that\/
      \mbox{$\evidence{P}(\Ind)\subseteq\universe{D}$} and,
      for all\/ \mbox{$i\geq 0$}, \mbox{$\alpha\in\Pred{i}$},
        \mbox{$\evidence{P}(\alpha)\subseteq\universe{U}^{\universe{D}^i}$}
  \item $\noise{N}$ is a group of permutations of\/
    $\universe{D}\union\universe{U}$, setwise stabilizing\/ $\universe{D}$
      and\/ $\universe{U}$, that represent noise in the interpretation
      of members of\/ $\universe{D}$ and\/ $\universe{U}$
  \end{itemize}
}
\end{definition}
It is convenient to discuss formulae that use arbitrary members of
$\universe{D}$ as if they were constant symbols.
\begin{definition}
  \label{def:extended-formula-lauchli}
{\raggedright
  Let\/ \mbox{$\model{M}=
    \tuple{\universe{D},\universe{U},\evidence{P},\noise{N}}$} be a
  L\"auchli model.
  The set\/ $\EF_{\model{M}}$ of\/
  {\em extended formulae\/} for\/ $\model{M}$ is the same as\/ $\PF$
  (Definition~\ref{def:formula}) except that individuals\/
  \mbox{$d\in\universe{D}$} may appear wherever free variables\/
  \mbox{$x\in\Var$} may appear.

  An extended formula\/ $\alpha$ is\/ {\em closed\/} if
  and only if there is no free variable in\/ $\alpha$.
}
\end{definition}
\begin{definition}
  \label{def:exended-evidence}
{\raggedright
  Extend\/ $\evidence{P}$ to closed extended formulae inductively as
  follows:
  \begin{itemize}
    \item for atomic \mbox{$\alpha(d_1,\ldots,d_n)$},
      \mbox{$\evidence{P}(\alpha(d_1,\ldots,d_n))=
      \evidence{P}(\alpha)(d_1,\ldots,d_n)$} (and
      \mbox{$\evidence{P}(\Ind)=\universe{D}$})
    \item $\evidence{P}(\alpha\land\beta)=
      \evidence{P}(\alpha)\times\evidence{P}(\beta)$ {\em (cross product)}
    \item $\evidence{P}(\alpha\lor\beta)=
      (\set{0}\times\evidence{P}(\alpha))\union
      (\set{1}\times\evidence{P}(\beta))$ {\em (marked union)}
    \item $\evidence{P}(\alpha\limplies\beta)=
      \evidence{P}(\beta)^{\evidence{P}(\alpha)}$ {\em (function space)}
    \item $\evidence{P}(\forall x\sepdot\beta)=
      \setof{c\in(\Union_d\evidence{P}(\subst{d}{x}{\beta}))^{\universe{D}}}
      {(cd)\in\evidence{P}(\subst{d}{x}{\beta})
      \mbox{ for all }d\in\universe{D}}$ {\em (dependent product)}
    \item $\evidence{P}(\exists x\sepdot\beta)=
      \setof{\tuple{d,b}}{d\in\universe{D}\mbox{ and }
      b\in\evidence{P}(\subst{d}{x}{\beta})}$ {\em (dependent sum)}
  \end{itemize}
}
\end{definition}
Finally, we extend the noise permutations to $\evidence{P}(\alpha)$
for all $\alpha\in\PF$.
\begin{definition}
  \label{def:extended-permutations}
{\raggedright
  If $\model{M}=\tuple{\universe{U},\evidence{P},\noise{N}}$ is a
  L\"auchli model, then we define the permutations
  $f_{\alpha}$ of $\evidence{P}(\alpha)$ for every
  $f\in\noise{N}$ and formula $\alpha\in\PF$
  as follows:
  \begin{itemize}
    \item if $\alpha$ is an atomic formula, and $\evidence{a}\in
      \evidence{P}(\alpha)$, then $f_{\alpha}(\evidence{a})=f(\evidence{a})$
      (and if $d\in\universe{D}$, then $f_{\Ind}(d)=f(d)$)

    \item if $\tuple{\evidence{a},\evidence{b}}\in\evidence{P}(\alpha\land
      \beta)$, then $f_{\alpha\land\beta}(\tuple{\evidence{a},\evidence{b}})=
      \tuple{f_{\alpha}(\evidence{a}),f_{\beta}(\evidence{b})}$

    \item if $\tuple{0,\evidence{a}}\in\evidence{P}(\alpha\lor\beta)$,
      then $f_{\alpha\lor\beta}(\tuple{0,\evidence{a}})=
      \tuple{0,f_{\alpha}(\evidence{a})}$

    \item if $\tuple{1,\evidence{b}}\in\evidence{P}(\alpha\lor\beta)$,
      then $f_{\alpha\lor\beta}(\tuple{1,\evidence{b}})=
      \tuple{1,f_{\beta}(\evidence{b})}$

    \item if $\evidence{c}\in\evidence{P}(\alpha\limplies\beta)$, then
      $f_{\alpha\limplies\beta}(\evidence{c})=
      f_{\beta}\circ\evidence{c}\circ f_{\alpha}^{-1}$

    \item if $\evidence{c}\in\evidence{P}(\forall x\sepdot\alpha)$, then
      $f_{\forall x\sepdot\alpha}(\evidence{c})=
      f_{\beta}\circ\evidence{c}\circ f_{\Ind}^{-1}$

    \item if $\tuple{d,\evidence{a}}\in\evidence{P}
      (\exists x\sepdot\alpha)$, then
      $f_{\exists x\sepdot\alpha}(\tuple{d,\evidence{a}})=
      \tuple{f_{\Ind}(d),f_{\subst{f_{\Ind}(d)}{x}{\alpha}}(\evidence{a})}$
  \end{itemize}

  A formula $\alpha$ is {\em true\/} in the L\"auchli model
  $\model{M}$ above if and only if $\evidence{P}(\alpha)$ is inhabited
  by at least one object that is invariant under
  $f_{\alpha}$ for all permutations $f\in\noise{N}$.
}
\end{definition}
The hierarchies of permutations $\set{f_{\alpha}}$ defined by
L\"auchli models are examples of the {\em logical
relations\/}~\cite{StatRel,MitchTCS} used to study definability in the
lambda calculus. L\"auchli proved that the first-order Heyting
predicate calculus is sound and complete for L\"auchli models. The
proof of completeness is highly nonconstructive, and appears to depend
in an essential way on the axiom of choice. \cite{KMO} explains in
some detail a plausible intuition behind L\"auchli models, and
reformulates the proof of completeness at the propositional level to
make the constructive and nonconstructive elements more
transparent. We summarize below the argument that invariance under the
permutations in L\"auchli models is a plausible necessary condition
for uniform constructibility.

Logical demonstrations are linguistic constructions, manipulating the
{\em names\/} of objects rather than the objects themselves. Since the
atomic formulae have no predetermined logical meanings, the assignment
of names to constructions for atomic formulae is essentially
arbitrary, except that a single name may not be assigned to two
different objects. The symbols $\land$, $\lor$, $\limplies$, $\forall$
and $\exists$ however, have definite logical meanings, so the names
for their constructions have logical content, and the assignment of
names to constructions is derived from the assignments associated with
atomic formulae.

Given the arbitrary nature of the assignment of names to constructions
of atomic formulae, we would expect that different minds would make
different assignments. Indeed, a single mind might make different
assignments at different times. This renders impossiblethe task of
communicating (or even remembering, which might viewed as the special
case of communicating with oneself) constructions for atomic formulae
by purely logical methods. For composite formulae, however, there is
hope. For example, the lambda term $(\lambda x :
\alpha\sepdot x)$ reliably names a specific construction of
$\alpha\limplies\alpha$---the identity function. This description of
the identity function says essentially, {\em ``Whatever you are given
as input, give it back as output.''} This description does not depend
on the identities of specific objects of type $\alpha$. We are
confident that we will interpret the identity function the same way
next year as we do today, and that when we communicate it to others,
they will interpret it in the same way as we do.

Every constructive proof formula should, like $(\lambda x:
\alpha\sepdot x)$, denote a {\em uniform\/} piece of evidence, in the sense
that it reliably names a construction independently of the assignment
of names to evidence for atomic formulae. Suppose that $m_1$ maps some
fixed set of names to a fixed set of pieces of evidence so that for
each name $x$, $m_1(x)$ is the object that we choose to name by
$x$. Similarly, $m_2(x)$ is the (possibly different) object that our
colleague Jane Doe names by $x$.  $m_1$ and $m_2$ are {\em type
consistent\/} if and only if for every name $x$ and formula $\alpha$,
$m_1(x)$ and $m_2(x)$ are either both in $\evidence{P}(\alpha)$, or
both not in this set. In a realizability model, we can lift $m_1$ and
$m_2$ to act consistently on names of realizers of arbitrary type. A
name $x$ is {\em $(m_1,m_2)$-uniform\/} (that is, it is understood in
the same way by Jane Doe and by us) if $m_1(x)=m_2(x)$.

In the special case where $m_1$ and $m_2$ are {\em bijections,}
$f=m_2\circ m_1^{-1}$ is a permutation on the set of evidence; when
$m_1$ and $m_2$ are furthermore type consistent, then $f$ setwise
stabilizes the evidence for each formula $\alpha$.  When we try to
communicate $a$ to Jane Doe, she will misunderstand it to be
$f(a)$. Clearly, a name $x$ is $(m_1,m_2)$-uniform if and only if
$m_1(x)$ is {\em invariant\/} under $f$. L\"auchli's permutations may
be understood as derived in this way from different ways of naming
evidence, but given the permutations we have no need to formalize
names in the model. So, even though our explanation of L\"auchli
models refers to the use of some language for communicating
constructions, there is no commitment to any particular formal
language---rather L\"auchli model theory deals with {\em
communicability in principle.} If we have more than one colleague
(Richard Roe, Peter Poe, etc.), then there are more than two possible
naming functions, and we get more permutations. Notice that if an
object is invariant under two permutations, it is also invariant under
their compositions and inverses. Therefore, there is no advantage in
considering arbitrary sets of permutations: it suffices to consider
just those sets that form groups. There may in reality be naming
functions that are not bijections, but we may legitimately ignore them
since we demand only a necessary condition for uniform
constructibility. We do not claim that all invariant evidence is
uniformly constructible (in fact, some arbitrarily high degree
uncomputable functions are invariant), nor do we claim that invariance
provides an adequate formalization of the notion of uniformity. It
suffices for our purposes that we can justify the informal claim that
every uniform construction is an invariant piece of evidence, so that
L\"auchli countermodels can be understood intuitively as evidence for
nonvalidity.

Given a permutation $f$ and an atomic formula $\alpha$, we define
$f_{\alpha}$ to be the restriction of $f$ to
$\evidence{P}(\alpha)$. This is guaranteed to be a permutation by the
{\em setwise stabilizing\/} clause of
Definition~\ref{def:lauchli-model}. Assume that we have defined the
action of $f\in\noise{N}$ on $\evidence{P}(\alpha)$ and
$\evidence{P}(\beta)$. Clearly, the action of $f$ on an element of
$\evidence{P}(\alpha \land \beta)$ must be to permute the components
of each distinguished pair independently, according to the action that
has already been defined on $\evidence{P}(\alpha)$ and
$\evidence{P}(\beta)$. Similarly, the action of $f$ on
$\evidence{P}(\alpha \lor \beta)$ must be to permute each marked
member of $\evidence{P}(\alpha)$ according to its action on
$\evidence{P}(\alpha)$, leaving the mark unchanged, and analogously
for marked elements of $\evidence{P}(\beta)$.

The action of permutation $f$ on $\evidence{P}(\alpha\limplies\beta)$
must be to map $c\in\evidence{P}(\alpha\limplies\beta)$ to a new
function $f_{\alpha\limplies\beta}(c)$. Since $c$ operates from and to
{\em unpermuted\/} evidence, and $f_{\alpha\limplies\beta}(c)$
operates from and to {\em permuted\/} evidence,
$f_{\alpha\limplies\beta}(c)$ should have the same action on permuted
evidence that $c$ has on unpermuted evidence (see
Figure~\ref{fig:permuted-function}).
\begin{figure}\fbox{\parbox{\textwidth}{
\begin{center}
\setlength{\unitlength}{0.012500in}%
\begin{picture}(145,177)(55,635)
\thicklines
\put(100,760){\vector( 1, 0){ 80}}
\put(100,640){\vector( 1, 0){ 80}}
\put( 80,740){\vector( 0,-1){ 80}}
\put(200,740){\vector( 0,-1){ 80}}
\put( 80,755){\makebox(0,0)[b]{$\evidence{a}_1$}}
\put(200,755){\makebox(0,0)[b]{$\evidence{b}_1$}}
\put( 80,635){\makebox(0,0)[b]{$\evidence{a}_2$}}
\put(200,635){\makebox(0,0)[b]{$\evidence{b}_2$}}
\put( 80,800){\makebox(0,0)[b]{$\alpha$}}
\put(200,800){\makebox(0,0)[b]{$\beta$}}
\put(140,770){\makebox(0,0)[b]{$\evidence{c}$}}
\put(140,650){\makebox(0,0)[b]{$f_{\alpha\limplies\beta}\evidence{c}$}}
\put( 70,705){\makebox(0,0)[r]{$f_{\alpha}$}}
\put(190,705){\makebox(0,0)[r]{$f_{\beta}$}}
\end{picture}
\end{center}
  \caption{Diagram of the permuted function
   $f_{\alpha\limplies\beta}\evidence{c}$
           \label{fig:permuted-function}}}}
\end{figure}
From this diagram, it is clear that
$f_{\alpha\limplies\beta}(\evidence{c})$ must satisfy
$f_{\alpha\limplies\beta}(\evidence{c})\evidence{a}= f_{\beta}
(\evidence{c}(f_{\alpha}^{-1}\evidence{a}))$, so
$f_{\alpha\limplies\beta}\evidence{c}= f_{\beta}\circ\evidence{c}\circ
f_{\alpha}^{-1}$. The arguments for $f_{\forall x\sepdot\alpha}$ and
$f_{\exists x\sepdot\alpha}$ are analogous to those for
$f_{\alpha\limplies\beta}$ and $f_{\alpha\land\beta}$, respectively.
We see now that, e.g., the identity function on each class
$\evidence{P}(\alpha)$ is invariant under all permutations, as well as
the function in
$\evidence{P}((\alpha\land(\alpha\limplies\beta))\limplies\beta)$ that
applies the $\evidence{P}(\alpha\limplies\beta)$ component of its
input to the $\evidence{P}(\alpha)$ component.

Now, consider the natural L\"auchli countermodel for the unprovable formula
$(\alpha\limplies\beta)\lor(\beta\limplies\alpha)$, shown in
Figure~\ref{fig:lauchli-countermodel}.
\begin{figure}\fbox{\parbox{\textwidth}{
\begin{center}
\setlength{\unitlength}{0.012500in}%
\begin{picture}(270,252)(40,600)
\thicklines
\put(100,640){\vector(-4, -1){0}}
\put(100,700){\oval( 40,120)[br]}
\put(100,700){\oval( 40,120)[tr]}
\put(260,640){\vector(-4, -1){0}}
\put(260,700){\oval( 40,120)[br]}
\put(260,700){\oval( 40,120)[tr]}
\put( 60,760){\vector( 4, 1){0}}
\put( 60,700){\oval( 40,120)[tl]}
\put( 60,700){\oval( 40,120)[bl]}
\put(220,760){\vector( 4, 1){0}}
\put(220,700){\oval( 40,120)[tl]}
\put(220,700){\oval( 40,120)[bl]}
\put( 70,617){\oval( 14, 26)[tl]}
\put( 80,617){\oval( 34, 34)[bl]}
\put( 80,617){\oval( 34, 34)[br]}
\put( 90,617){\oval( 14, 26)[tr]}
\put( 90,630){\vector(-4, 1){0}}
\put(230,617){\oval( 14, 26)[tl]}
\put(240,617){\oval( 34, 34)[bl]}
\put(240,617){\oval( 34, 34)[br]}
\put(250,617){\oval( 14, 26)[tr]}
\put(250,630){\vector(-4, 1){0}}
\put( 90,783){\oval( 14, 26)[br]}
\put( 80,783){\oval( 34, 34)[tr]}
\put( 80,783){\oval( 34, 34)[tl]}
\put( 70,783){\oval( 14, 26)[bl]}
\put( 70,770){\vector( 4, -1){0}}
\put(250,783){\oval( 14, 26)[br]}
\put(240,783){\oval( 34, 34)[tr]}
\put(240,783){\oval( 34, 34)[tl]}
\put(230,783){\oval( 14, 26)[bl]}
\put(230,770){\vector( 4, -1){0}}
\put( 80,755){\makebox(0,0)[b]{$a_1$}}
\put(240,755){\makebox(0,0)[b]{$b_1$}}
\put( 80,635){\makebox(0,0)[b]{$a_2$}}
\put(240,635){\makebox(0,0)[b]{$b_2$}}
\put( 80,840){\makebox(0,0)[b]{$\evidence{P}(\alpha)$}}
\put(240,840){\makebox(0,0)[b]{$\evidence{P}(\beta)$}}
\put( 30,700){\makebox(0,0)[r]{$f_{2}$}}
\put(110,700){\makebox(0,0)[r]{$f_{2}$}}
\put(190,700){\makebox(0,0)[r]{$f_{1}$}}
\put(270,700){\makebox(0,0)[r]{$f_{1}$}}
\put(80,810){\makebox(0,0)[b]{$f_{1}$}}
\put(80,590){\makebox(0,0)[t]{$f_{1}$}}
\put(240,810){\makebox(0,0)[b]{$f_{2}$}}
\put(240,590){\makebox(0,0)[t]{$f_{2}$}}
\end{picture}
\end{center}
  \caption{Lauchli Countermodel for
     $(\alpha\limplies\beta)\lor(\beta\limplies\alpha)$
     \label{fig:lauchli-countermodel}}}}
\end{figure}
No function from \mbox{$\evidence{P}(\alpha)$} to
\mbox{$\evidence{P}(\beta)$} can be invariant under
$f_1$, and no function from \mbox{$\evidence{P}(\beta)$} to
\mbox{$\evidence{P}(\alpha)$} can be invariant under $f_2$, so
\mbox{$(\alpha\limplies\beta)\lor(\beta\limplies\alpha)$} is not true
in the model.When our customer challenges the unprovability of
\mbox{$(\alpha\limplies\beta)\lor(\beta\limplies\alpha)$}, we might
respond with an argument like:
\begin{quote}{\em
Suppose that there are two pieces of evidence for $\alpha$, and two
others for $\beta$. Suppose also that a construction for
\mbox{$(\alpha\limplies\beta)\lor(\beta\limplies\alpha)$} must be
communicated to two colleagues, Jane Doe and Richard Roe. Suppose that
Jane Doe uses the same names that we do for $\alpha$ evidence, but
reverses our naming of $\beta$ evidence; Richard Roe agrees with our
naming of $\beta$ evidence, but reverses our naming of $\alpha$
evidence. No construction for \mbox{$\alpha\limplies\beta$} can be
communicated uniquely to Jane Doe, and no construction for
\mbox{$\beta\limplies\alpha$} can be communicated uniquely to Richard
Roe, so we cannot communicate to the community of our colleagues
constructive evidence for
$(\alpha\limplies\beta)\lor(\beta\limplies\alpha)$.
}\end{quote}
The L\"auchli countermodel does not provide obvious and natural
concrete interpretations of $\alpha$ and $\beta$---in this respect it
is intuitively inferior to classical truth-table countermodels. But,
it avoids some of the most unfortunate qualities of the Kripke
countermodel. The circumstances represented by the L\"auchli
countermodel consist entirely of a single potential reality, without
any subjunctive or contingent components. For a constructive reasoner
who believes that constructions must be uniquely communicable, the
L\"auchli countermodel carries substantial intuitive force, although
it is not absolutely compelling. L\"auchli countermodels have two
obvious intuitive weakness: they rely on metacircumstances relating to
the language in which constructions are communicated, and they insist
on communicating constructions uniquely, while it may be sufficient
for reasoning to have confidence in the correctness of a construction
even if there is confusion as to {\em which\/} of several correct
constructions it is.

At a technical level, there is a straightforward construction of a
Kripke model given a L\"auchli model~\cite{KMO}. The essential idea is
that each subgroup of $\noise{N}$ represents a Kripke world, and that
the subgroup relation determines accessibility. Truth in an individual
world is just posession of an invariant under the smaller permutation
group. The translation from L\"auchli models produces Kripke models
with a lot of structure (for example, they are lattices). It is
intriguing to try to interpret this structure as a restriction on the
layouts of possible futures that can actually arise in the
circumstances of constructive reasoning.

\subsection{Relational Realizability Models}
\label{sec:relational-realizability}

Sections~\ref{sec:relational-realizability} and~\ref{sec:soundness}
describe work in progress by Lipton and O'Donnell. All of the proofs
in these sections are constructive and in particular choice-free. We
designed relational realizability models to improve on L\"auchli
models for two purposes: to support constructive proofs of soundness
and completeness, and to strengthen the intuitive force of
countermodels by allowing a construction to be communicated
ambiguously, as long as all parties agree that the construction is
correct. Both of these purposes seem to demand that constructions are
allowed to be {\em nondeterministic,} as long as all of their possible
outcomes are satisfactory. With nondeterministic evidence functions
(in effect, relations), it is unproductive to define the realizers to
be invariants under permutations, since for example the universal
relation is invariant under all permutations. Rather, we must now
allow permutations to confuse elements of different types, and define
realizers to be pieces of evidence that land in the right type under
all permutations.

\begin{definition}
  \label{def:finite}
{\raggedright
  Let\/ $S,T$ be sets, and let\/ \mbox{$r\subseteq S\times T$} be a
  relation.

  $r$ is\/ {\em entire\/} from\/ $S$ to\/ $T$ if and only if, for all\/
  \mbox{$s\in S$}, there exists\/ \mbox{$t\in T$} such that\/
  \mbox{$s[r]t$}.

  $r$ is\/ {\em injective\/} from\/ $S$ to\/ $T$ if and only if, for all\/
  \mbox{$s_1,s_2\in S$}, \mbox{$t\in T$}, if\/ \mbox{$s_1[r]t$} and\/
  \mbox{$s_2[r]t$}, then\/ \mbox{$s_1=s_2$}.

  $r$ is\/ {\em surjective\/} from\/ $S$ to\/ $T$ if and only if, for all\/
  \mbox{$t\in T$}, there exists\/ \mbox{$s\in S$} such that\/
  \mbox{$s[r]t$}.

  $r$ is a\/ {\em partial function\/} from\/ $S$ to\/ $T$ if and only
  if, for all\/
  \mbox{$s\in S$}, \mbox{$t_1,t_2\in T$}, if\/ \mbox{$s[r]t_1$} and\/
  \mbox{$s[r]t_2$}, then\/ \mbox{$t_1=t_2$}.
 
  $r$ is a\/ {\em function\/} if and only if it is an entire partial function.

  A set\/ $S$ is\/ {\em finite\/} if and only if there exists an
  integer\/ $n$ and a surjective function\/ $r$ from\/ \mbox{$\{1,\ldots,n\}$}
  to\/ $S$.
}
\end{definition}
Notice that the $n$ associated with a finite set $S$ is {\em not\/}
neccessarily the cardinality of $S$, because the surjective function
$r$ is not required to be injective.
\begin{lemma}
  \label{lem:finite-union}
{\raggedright
  Let\/ ${\cal S}$ be a finite set of finite sets. Then\/
  \mbox{$\Union{\cal S}$} is finite.
}
\end{lemma}
\begin{lemma}
  \label{lem:choice}
{\raggedright
  Let\/ ${\cal S}$ be a finite set, such that
  every member\/ \mbox{$S\in{\cal S}$} is an inhabited set (there
  exists\/ \mbox{$x\in S$}). Then there is a finite set\/ $T$ such
  that, for every\/ \mbox{$S\in{\cal S}$}, \mbox{$T\inter S$} is
  inhabited.
}
\end{lemma}
{\raggedright
\paragraph{Proof:}
  By induction on $n$ such that
  there is a surjective function from \mbox{$\{1,\ldots,n\}$}
  to ${\cal S}$.
\paragraph{Basis.} Assume \mbox{$n=0$}.
  Let \mbox{$T=\emptyset$}.
\paragraph{Induction.} Assume the lemma holds for $0,\ldots,n-1$.
  Let $r$ be a surjective function from \mbox{$\{1,\ldots,n\}$}
  to ${\cal S}$.
  Write \mbox{${\cal S}=\{S_1,\ldots,S_n\}$}, where each $S_i$ is the
  unique member of ${\cal S}$ such that \mbox{$i[r]S_i$}.
  By induction hypothesis, there is a finite set $T_{n-1}$ such that,
  for every \mbox{$S\in\{S_1,\ldots,S_{n-1}\}$}, \mbox{$T_{n-1}\inter S$}
  is inhabited.
  Since \mbox{$S_n\in{\cal S}$} is inhabited, there exists an
  \mbox{$x\in S$}.
  Define \mbox{$T=T_{n-1}\union\{x\}$}.
  For \mbox{$i\leq n-1$}, \mbox{$T\inter S_i$} is inhabited by
  definition of $T_{n-1}$.
  \mbox{$T\inter S_n$} is inhabited by $x$.
}
\eop{Lemma~\ref{lem:finite-union}}
\begin{definition}
  \label{def:reliable-mapping}
{\raggedright
  Let\/ $S,S',T,T'$ be sets, with\/ \mbox{$S\subseteq S'$},
  \mbox{$T\subseteq T'$}, and let\/ \mbox{$r\subseteq S'\times T'$} be
  a relation.
  \begin{itemize}
  \item $r$ is\/ {\em $S$--$T$ entire\/} from\/ $S'$ to\/ $T'$ if and only if\/
    \mbox{$S\subseteq r^{-1}[T]$}
    (that is, for all\/ \mbox{$s\in S$}, there exists\/ \mbox{$t\in T$} such
    that\/ \mbox{$s\relation{R}t$}).
   \item $r$ is\/ {\em $S$--$T$ reliable\/} from\/ $S'$ to\/ $T'$
     if and only if\/
     \mbox{$r[S]\subseteq T$} (that is, for all\/
     \mbox{$s\in S$} and\/ \mbox{$t\in T'$} such that\/
     \mbox{$s\relation{r}t$}, \mbox{$t\in T$}).
  \end{itemize}

  $r$ is a\/ {\em reliable mapping\/} from\/ $S$ in\/ $S'$ to\/ $T$ in\/ $T'$
  if and only if\/ $r$ is\/ $S'$--$T'$ entire and\/ $S$--$T$ reliable.
  Notice that this implies\/ $S$--$T$ entirety as well.

  The set of reliable mappings from\/ $S$ in\/ $S'$ to\/ $T$ in\/ $T'$
  is written\/ \mbox{$S',S\hookrightarrow T,T'$}. $S'$ and/or\/ $T'$
  may be omitted when clear from the context.
}
\end{definition}
\begin{definition}
  \label{def:sum-product}
{\raggedright
  Let\/ $S$ be a set, and let\/ \mbox{$T(s)$} be a set for each\/
  \mbox{$s\in S$}. Let\/ \mbox{${\cal T}=\Union\setof{T(s)}{s\in S}$}.
  The\/ {\em dependent sum\/} of\/ \mbox{$T$} over\/
  $S$ is
  $$\summ{s\in S}{T(s)}=
    \setof{\tuple{s,t}}{t\in T(s)}$$
  The\/ {\em reliable relational dependent product\/} of\/ $T$
  over\/ $S$ is
  $$\product{s\in S}{T(s)}=
    \setof{r\subseteq S\times{\cal T}}
      {r\mbox{ is entire from $S$ to ${\cal T}$, and }
        s[r]t\mbox{ implies }t\in T(s)\mbox{ for all }s,t}$$
}
\end{definition}
\begin{definition}
  \label{def:approximation}
{\raggedright
  Let\/ $S$ be a set. The\/ {\em finite approximation universe for\/}
  $S$ is\/ \mbox{$\appu{S}=\setof{A\subseteq S}{A\mbox{ is finite}}$}.
  Let\/ \mbox{$T\subseteq S$}. The set of\/ {\em finite approximations
    to\/} $T$ {\em in\/} $S$ is\/
  \mbox{$\appel{T}{S}=\setof{A\in\appu{S}}{A\inter T\mbox{ is inhabited}}$}.
}
\end{definition}

\begin{definition}
  \label{def:relational-realizability-model}
{\raggedright
  A\/ {\em relational realizability model\/} is a quadruple
  \mbox{$\model{M}=\tuple{\universe{D},\universe{U},\evidence{P},\noise{N}}$}
  where
  \begin{itemize}
    \item $\universe{D}$ is a set, called the\/ {\em domain of individuals}
    \item $\universe{U}$ is a set, called the\/ {\em domain of evidence}
    \item $\evidence{P}$ is a mapping from\/
      \mbox{$\{\Ind\}\union\Union_i\Pred{i}$} to subsets of\/
      \mbox{$\Union_i(\universe{D}^i\times\universe{U})$} such that\/
      \mbox{$\evidence{P}(\Ind)\subseteq\universe{D}$} and,
      for all\/ \mbox{$\alpha\in\Pred{i}$},
      \mbox{$\evidence{P}(\alpha)\subseteq\universe{D}^i\times\universe{U}$}
    \item $\noise{N}\subseteq
      (\universe{D}\union\universe{U})^{\universe{D}\union\universe{U}}$
      is a set of permutations, setwise stabilizing\/ $\universe{D}$
      and\/ $\universe{U}$, that represent noise in the interpretation
      of members of\/ $\universe{D}$ and\/ $\universe{U}$
  \end{itemize}
}
\end{definition}
Notice that $\noise{N}$ is an arbitrary set of permutations, not necessarily a group.
\begin{definition}
  \label{def:extended-formula-relational}
{\raggedright
  Let\/ \mbox{$\model{M}=
    \tuple{\universe{D},\universe{U},\evidence{P},\noise{N}}$} be a
  relational realizability model.
  The\/ set of {\em finite approximations\/} for\/ $\universe{D}$ is
  \mbox{$\hat{\universe{D}}=\appu{\universe{D}}$}.
  The set\/ $\EF_{\model{M}}$ of\/
  {\em extended formulae\/} for\/ $\model{M}$ is the same as\/ $\PF$
  (Definition~\ref{def:formula}) except that approximate individuals\/
  \mbox{$D\in\hat{\universe{D}}$} may appear wherever free variables\/
  \mbox{$x\in\Var$} may appear.

  An extended formula\/ $\alpha$ is\/ {\em closed\/} if
  and only if there is no free variable in\/ $\alpha$.
}
\end{definition}
\begin{definition}
  \label{def:relational-closure}
{\raggedright
  For each closed extended formula\/ \mbox{$\alpha\in\EF_{\model{M}}$}
  define the set\/ $\universe{U}_{\alpha}$ inductively by\/
  \begin{itemize}
  \item for atomic\/ \mbox{$\alpha(D_1,\ldots,D_m)$},
    \mbox{$\universe{U}_{\alpha(D_1,\ldots,D_m)}=\universe{U}$}
  \item \mbox{$\universe{U}_{\alpha\land\beta}=
     \hat{\universe{U}}_{\alpha}\times\hat{\universe{U}}_{\beta}$}
     {\em (cross product)}
  \item \mbox{$\universe{U}_{\alpha\lor\beta}=
     (\{0\}\times\hat{\universe{U}}_{\alpha})\cup
     (\{1\}\times\hat{\universe{U}}_{\beta})$} {\em (marked union)}
  \item \mbox{$\universe{U}_{\alpha\limplies\beta}=
     \setof{r\subseteq
       \hat{\universe{U}}_{\alpha}\times\hat{\universe{U}}_{\beta}}
     {r\mbox{ is entire from }\hat{\universe{U}}_{\alpha}
     \mbox{ to }\hat{\universe{U}}_{\beta}}$}
     {\em (space of entire binary relations)}
  \item \mbox{$\universe{U}_{\forall x\sepdot\alpha}=
     \product{D\in\hat{\universe{D}}}
       {\hat{\universe{U}}_{\subst{D}{x}{\alpha}}}$}
        {\em (reliable relational product)}
  \item \mbox{$\universe{U}_{\exists x\sepdot\alpha}=
     \summ{D\in\hat{\universe{D}}}
       {\hat{\universe{U}}_{\subst{D}{x}{\alpha}}}$}
         {\em (dependent sum)}
  \end{itemize}
  where for each formula\/ $\alpha$,
  \mbox{$\hat{\universe{U}}_{\alpha}=\appu{\universe{U}_{\alpha}}$}.
  Notice that\/ $\universe{U}_{\alpha}$ and\/
  $\hat{\universe{U}}_{\alpha}$ depend on the structure
  of\/ $\alpha$, but not on the identities of the atomic formulae
  and individuals in it.

  The\/ {\em relational realizability closure\/} of\/ $\universe{U}$ is\/
  \mbox{$\bar{\universe{U}}=
    \Union\setof{\hat{\universe{U}}_{\alpha}}{\alpha\in\PF}$}.

  $\evidence{P}$ extends to a function mapping each closed extended
  formula\/ $\alpha$ to a subset of\/
  $\universe{U}_{\alpha}$, and also to a function\/ $\hat{\evidence{P}}$
  mapping each\/ $\alpha$ to a subset of\/ $\hat{\universe{U}}_{\alpha}$.
  Each noise permutation\/ $f\in\noise{N}$
  induces permutations\/ $f_{\alpha}$ on\/ $\universe{U}_{\alpha}$, and
  also permutations\/ $\hat{f}_{\alpha}$ on\/
  $\hat{\universe{U}}_{\alpha}$, as follows:
  \begin{itemize}

   \item
     \begin{itemize}

     \item $\evidence{P}(\alpha(D_1,\ldots,D_m))=$\\
       $\setof{u\in\universe{U}}
         {\tuple{d_1,\ldots,d_m,u}\in\evidence{P}(\alpha)
         \mbox{ for some }d_1\in D_1,\ldots,d_m\in D_m}$
       (and\/ \mbox{$\evidence{P}(\Ind)=\universe{D}$})

     \item \mbox{$f_{\alpha(D_1,\ldots,D_m)}(a)=f(a)$}
       (and\/ \mbox{$f_{\Ind}(d)=f(d)$})

     \end{itemize}

   \item
     \begin{itemize}

     \item \mbox{$\evidence{P}(\alpha\land\beta)=
       \hat{\evidence{P}}(\alpha)\times
       \hat{\evidence{P}}(\beta)$}
       {\em (cross product)}

     \item \mbox{$f_{\alpha\land\beta}(\tuple{A,B})=
       \tuple{\hat{f}_{\alpha}(A),\hat{f}_{\beta}(B)}$}

     \end{itemize}

    \item
      \begin{itemize}

      \item \mbox{$
        \evidence{P}(\alpha\lor\beta)=
          (\{0\}\times\hat{\evidence{P}}(\alpha))\cup
          (\{1\}\times\hat{\evidence{P}}(\beta))$}
        {\em (marked union)}

      \item \mbox{$f_{\alpha\lor\beta}(\tuple{0,A})=
        \tuple{0,\hat{f}_{\alpha}(A)}$}\\
        \mbox{$f_{\alpha\lor\beta}(\tuple{1,A})=
        \tuple{1,\hat{f}_{\beta}(B)}$}

      \end{itemize}

    \item
      \begin{itemize}

      \item \mbox{$\evidence{P}(\alpha\limplies\beta)=
       \hat{\universe{U}}_{\alpha},\hat{\evidence{P}}(\alpha)\hookrightarrow
        \hat{\evidence{P}}(\beta),\hat{\universe{U}}_{\beta}$} {\em
        (space of reliable mappings)}

      \item \mbox{$f_{\alpha\limplies\beta}(r)=
        \setof{\tuple{\hat{f}_{\alpha}(A),\hat{f}_{\beta}(B)}}
        {A\relation{r}B}$}

      \end{itemize}

    \item
      \begin{itemize}

      \item \mbox{$\evidence{P}(\forall x\sepdot\alpha)=
        \setof{r\in\product{D\in\hat{\universe{D}}}
          {\hat{\universe{U}}_{\subst{D}{x}{\alpha}}}}
          {(D\in\hat{\evidence{P}}(\Ind)\mbox{ and }D[r]A)\mbox{ implies }
          A\in\hat{\evidence{P}}(\subst{D}{x}{\alpha})}$}
        {\em (reliable relational product)}

      \item \mbox{$f_{\forall x\sepdot\alpha}(r)=
        \setof{\tuple{\hat{f}_{\Ind}(D),
          \hat{f}_{\subst{\hat{f}_{\Ind}(D)}{x}{\alpha}}(A)}}
          {D[r]A}$} (since\/ $\hat{f}_{\gamma}$ depends only on the
        structure of\/ $\gamma$,
        \mbox{$\hat{f}_{\subst{\hat{f}_{\Ind}(D)}{x}{\alpha}}=
          \hat{f}_{\subst{D}{x}{\alpha}}$}, but the former is more
        informative intensionally)

      \end{itemize}

    \item
      \begin{itemize}

      \item \mbox{$\evidence{P}(\exists x\sepdot\alpha)=
        \setof{\tuple{D,A}}{D\in\hat{\evidence{P}}(\Ind)\mbox{ and }
          A\in\hat{\evidence{P}}(\subst{D}{x}{\alpha})}$}
        {\em (dependent sum)}

      \item \mbox{$f_{\exists x\sepdot\alpha}(\tuple{D,A})=
        \tuple{\hat{f}_{\Ind}(D),
          \hat{f}_{\subst{\hat{f}_{\Ind}(D)}{x}{\alpha}}(A)}$}

      \end{itemize}

  \end{itemize}
  where for each formula\/ $\alpha$
  \begin{itemize}
  \item
    \begin{itemize}
    \item \mbox{$\hat{\evidence{P}}(\alpha)=
      \appel{\evidence{P}(\alpha)}{\hat{\universe{U}}_{\alpha}}$}
      (and\/ \mbox{$\hat{\evidence{P}}(\Ind)=
        \appel{\evidence{P}(\Ind)}{\hat{\universe{D}}}$})
    \item \mbox{$\hat{f}_{\alpha}(A)=\setof{f_{\alpha}(a)}{a\in A}$}
      (and\/ \mbox{$\hat{f}_{\Ind}(D)=\setof{f_{\Ind}(d)}{d\in D}$})
    \end{itemize}
  \end{itemize}
  Notice that\/ \mbox{$\evidence{P}(\alpha)$} and\/
  \mbox{$\hat{\evidence{P}}(\alpha)$} depend on\/ $\alpha$, but\/
  $f_{\alpha}$ and\/ $\hat{f}_{\alpha}$, like\/ $\universe{U}_{\alpha}$ and\/
  $\hat{\universe{U}}_{\alpha}$ before, depend only on the structure
  of\/ $\alpha$, and not on the identities of its atomic formulae and its
  individuals.
}
\end{definition}
\begin{definition}
  \label{def:environment}
{\raggedright
  Let\/ \mbox{$\model{M}=
    \tuple{\universe{D},\universe{U},\evidence{P},\noise{N}}$}
  be a relational realizability model. An\/ {\em environment\/} for\/
  $\model{M}$ is a function\/
  \mbox{$\eta\colon\Var\rightarrow\hat{\universe{D}}$}.

  Let\/ $\eta$ be an environment for\/ $\model{M}$. Extend\/ $\eta$ to
  a function from\/ $\EF_{\model{M}}$ to\/ $\hat{\universe{D}}$ by\/
  $$\eta(\alpha)=
    \subst{\eta(x_1),\ldots,\eta(x_m)}{x_1,\ldots,x_m}{\alpha}$$
  where $x_1,\ldots,x_m$ is a list of the free variables in\/ $\alpha$. 
}
\end{definition}
\begin{lemma}
  \label{lem:environment}
{\raggedright
  Let\/ \mbox{$\model{M}=
    \tuple{\universe{D},\universe{U},\evidence{P},\noise{N}}$}
  be a relational realizability model, let\/ \mbox{$\eta_1,\eta_2$}
  be environments for\/ $\model{M}$, and let\/ $\alpha$ be an extended
  formula with free variables\/ $x_1,\ldots,x_m$. If\/
  \mbox{$\eta_1(x_i)=\eta_2(x_i)$} for all\/ \mbox{$i\leq m$}, then\/
  \mbox{$\eta_1(\alpha)=\eta_2(\alpha)$}.
  If\/ $\alpha$ is closed, then\/
  \mbox{$\eta_1(\alpha)=\eta_2(\alpha)=\alpha$}.
}
\end{lemma}
\begin{definition}
  \label{def:relational-theory}
{\raggedright
  Let\/ \mbox{$\model{M}=
    \tuple{\universe{D},\universe{U},\evidence{P},\noise{N}}$}
  be a relational realizability model, $\eta$ an environment
  for\/ $\model{M}$.
  \begin{itemize}
  \item For\/ \mbox{$A\in\universe{U}_{\alpha}$},
    \mbox{$\model{M},\eta\nmodels A\colon\alpha$} if and only if, for all\/
    \mbox{$f\in\noise{N}$},
    \mbox{$\hat{f}_{\alpha}(A)\in\hat{\evidence{P}}(\eta(\alpha))$}.
  \item \mbox{$\model{M},\eta\nmodels\alpha$} if and only if there exists\/
    \mbox{$A\in\hat{\universe{U}}_{\alpha}$} such that\/
    \mbox{$\model{M},\eta\nmodels A\colon\alpha$}.
  \item When\/ $\alpha$ is closed, \mbox{$\model{M}\nmodels A\colon\alpha$}
    if and only if\/ \mbox{$\model{M},\eta\nmodels A\colon\alpha$} for
    an arbitrary environment\/ $\eta$; similarly for\/
    \mbox{$\model{M}\nmodels\alpha$}.
  \end{itemize}
}
\end{definition}

Consider the relational realizability countermodel for
\mbox{$(\alpha\limplies\beta)\lor(\beta\limplies\alpha)$} shown in
Figure~\ref{fig:relational-countermodel}.
\begin{figure}\fbox{\parbox{\textwidth}{
\begin{center}
\setlength{\unitlength}{0.012500in}%
\begin{picture}(260,230)(30,540)
\thicklines
\put(  0,685){\vector(-4, -1){0}}
\put(  0,698){\oval( 14, 26)[br]}
\put(-10,698){\oval( 34, 34)[tr]}
\put(-10,698){\oval( 34, 34)[tl]}
\put(-20,698){\oval( 14, 26)[bl]}
\put( 85,685){\vector(-4, -1){0}}
\put( 85,698){\oval( 14, 26)[br]}
\put( 75,698){\oval( 34, 34)[tr]}
\put( 75,698){\oval( 34, 34)[tl]}
\put( 65,698){\oval( 14, 26)[bl]}
\put(170,685){\vector(-4, -1){0}}
\put(170,698){\oval( 14, 26)[br]}
\put(160,698){\oval( 34, 34)[tr]}
\put(160,698){\oval( 34, 34)[tl]}
\put(150,698){\oval( 14, 26)[bl]}
\put(255,685){\vector(-4, -1){0}}
\put(255,698){\oval( 14, 26)[br]}
\put(245,698){\oval( 34, 34)[tr]}
\put(245,698){\oval( 34, 34)[tl]}
\put(235,698){\oval( 14, 26)[bl]}
\put(340,685){\vector(-4, -1){0}}
\put(340,698){\oval( 14, 26)[br]}
\put(330,698){\oval( 34, 34)[tr]}
\put(330,698){\oval( 34, 34)[tl]}
\put(320,698){\oval( 14, 26)[bl]}
\put(  0,570){\vector(-4, -1){0}}
\put(  0,583){\oval( 14, 26)[br]}
\put(-10,583){\oval( 34, 34)[tr]}
\put(-10,583){\oval( 34, 34)[tl]}
\put(-20,583){\oval( 14, 26)[bl]}
\put( 85,570){\vector(-4, -1){0}}
\put( 85,583){\oval( 14, 26)[br]}
\put( 75,583){\oval( 34, 34)[tr]}
\put( 75,583){\oval( 34, 34)[tl]}
\put( 65,583){\oval( 14, 26)[bl]}
\put(170,570){\vector(-4, -1){0}}
\put(170,583){\oval( 14, 26)[br]}
\put(160,583){\oval( 34, 34)[tr]}
\put(160,583){\oval( 34, 34)[tl]}
\put(150,583){\oval( 14, 26)[bl]}
\put(255,570){\vector(-4, -1){0}}
\put(255,583){\oval( 14, 26)[br]}
\put(245,583){\oval( 34, 34)[tr]}
\put(245,583){\oval( 34, 34)[tl]}
\put(235,583){\oval( 14, 26)[bl]}
\put(340,570){\vector(-4, -1){0}}
\put(340,583){\oval( 14, 26)[br]}
\put(330,583){\oval( 34, 34)[tr]}
\put(330,583){\oval( 34, 34)[tl]}
\put(320,583){\oval( 14, 26)[bl]}
\put(160,670){\makebox(0,0)[b]{$a_0$}}
\put(160,555){\makebox(0,0)[b]{$b_0$}}
\put(-10,720){\makebox(0,0)[b]{$f_1$}}
\put( 75,720){\makebox(0,0)[b]{$f_1$}}
\put(160,720){\makebox(0,0)[b]{$f_1$}}
\put(245,720){\makebox(0,0)[b]{$f_1$}}
\put(330,720){\makebox(0,0)[b]{$f_1$}}
\put(-10,605){\makebox(0,0)[b]{$f_2$}}
\put( 75,605){\makebox(0,0)[b]{$f_2$}}
\put(160,605){\makebox(0,0)[b]{$f_2$}}
\put(245,605){\makebox(0,0)[b]{$f_2$}}
\put(330,605){\makebox(0,0)[b]{$f_2$}}
\put(110,545){\dashbox{6}(100,105){}}
\put(110,660){\dashbox{6}(100,105){}}
\put(160,745){\makebox(0,0)[b]{$\evidence{P}(\alpha)$}}
\put(160,630){\makebox(0,0)[b]{$\evidence{P}(\beta)$}}
\put(175,670){\vector(1,0){55}}
\put(200,675){\makebox(0,0)[b]{$f_2$}}
\put(245,670){\makebox(0,0)[b]{$a_1$}}
\put(260,670){\vector(1,0){55}}
\put(285,675){\makebox(0,0)[b]{$f_2$}}
\put(330,670){\makebox(0,0)[b]{$a_2$}}
\put(370,670){\makebox(0,0)[b]{$\cdots$}}
\put( 90,670){\vector(1,0){55}}
\put(120,675){\makebox(0,0)[b]{$f_2$}}
\put( 75,670){\makebox(0,0)[b]{$a_{-1}$}}
\put(  5,670){\vector(1,0){55}}
\put( 30,675){\makebox(0,0)[b]{$f_2$}}
\put(-10,670){\makebox(0,0)[b]{$a_{-2}$}}
\put(-50,670){\makebox(0,0)[b]{$\cdots$}}
\put(175,555){\vector(1,0){55}}
\put(200,560){\makebox(0,0)[b]{$f_1$}}
\put(245,555){\makebox(0,0)[b]{$b_1$}}
\put(260,555){\vector(1,0){55}}
\put(285,560){\makebox(0,0)[b]{$f_1$}}
\put(330,555){\makebox(0,0)[b]{$b_2$}}
\put(370,555){\makebox(0,0)[b]{$\cdots$}}
\put( 90,555){\vector(1,0){55}}
\put(120,560){\makebox(0,0)[b]{$f_1$}}
\put( 75,555){\makebox(0,0)[b]{$b_{-1}$}}
\put(  5,555){\vector(1,0){55}}
\put( 30,560){\makebox(0,0)[b]{$f_1$}}
\put(-10,555){\makebox(0,0)[b]{$b_{-2}$}}
\put(-50,555){\makebox(0,0)[b]{$\cdots$}}
\end{picture}
\\
The iterated functions $f^i_1$ and $f^j_2$ are present for all
integers $i$, $j$
\end{center}
  \caption{Relational Realizability Countermodel for
     $(\alpha\limplies\beta)\lor(\beta\limplies\alpha)$
     \label{fig:relational-countermodel}}}}
\end{figure}
Because of the noise functions $f^i_1$, there can be no reliable mapping
from \mbox{$\hat{\evidence{P}}(\alpha)$} to
\mbox{$\hat{\evidence{P}}(\beta)$}, and the $f^j_2$s prevent a mapping from
\mbox{$\hat{\evidence{P}}(\beta)$} to
from \mbox{$\hat{\evidence{P}}(\alpha)$}. When our customer challenges
the unprovability of
\mbox{$(\alpha\limplies\beta)\lor(\beta\limplies\alpha)$}, we might
respond with an argument like:
\begin{quote}{\em
Suppose that there is one piece of evidence $a_0$ for $\alpha$, and
another piece of evidence $b_0$ for $\beta$. Suppose also that a
construction for
\mbox{$(\alpha\limplies\beta)\lor(\beta\limplies\alpha)$} must be
communicated to both Jane Doe and Richard Roe. Suppose that Jane Doe
understands our name for $a_0$ as a correct name of evidence for
$\alpha$, but takes our name for $b_0$ to refer to different
nonevidence $b_{i\neq 0}$ depending on circumstances; Richard Roe
understands our name for $b_0$, but takes our name for $a_0$ to refer
to nonevidence $a_{j\neq0}$. No construction for
\mbox{$\alpha\limplies\beta$} can be communicated to Jane Doe in such
a way that she recognizes its correctness, and no construction for
\mbox{$\beta\limplies\alpha$} can be communicated to Richard Roe so
that he recognizes its correctness, so we cannot communicate to the
community of our colleagues constructive evidence for
$(\alpha\limplies\beta)\lor(\beta\limplies\alpha)$.
}\end{quote}

Relational realizability countermodels still lack the concreteness of
the truth-table countermodels, they still depend on metacircumstances
and the requirement that constructions be communicable in spite of
noise, and they must be infinite to disprove even the simple formula
$(\alpha\limplies\beta)\lor(\beta\limplies\alpha)$. To the good, they
share with L\"auchli countermodels the virtue of being single
potential realities, without subjunctive or contingent
components. And, they strengthen the intuitive force of L\"auchli
countermodels by demonstrating that no construction supporting an
unprovable formula $\gamma$ can be communicated in a way that
generates common knowledge of its correctness as a construction
supporting $\gamma$, even if we allow ambiguity as to the precise
identity of the construction.

\section{Proof of Soundness for Relational Realizability}
\label{sec:soundness}

We conjecture that the Heyting calculus is complete for relational
realizability semantics, and that the proof of completeness is
constructive. The proof of completeness is work in progress. We have
already proved soundness.

\begin{definition}
  \label{def:valid-sequent}
{\raggedright
  A sequent\/ \mbox{$\Gamma\proves\Psi$} is\/ {\em
  valid for relational realizability\/} if and only if, for
  every relational realizability model\/
  \mbox{$\model{M}=\tuple{\universe{D},\universe{U},\evidence{P},\noise{N}}$},
  (1) implies (2) below:
  \begin{enumerate}
  \item there is a finite subset\/ \mbox{${\cal A}\subseteq\bar{\universe{U}}$}
    such that, for each noise function\/ \mbox{$f\in\noise{N}$},
    and each \mbox{$\gamma\in\Gamma$}, there exists an\/
    \mbox{$A\in{\cal A}$} with
    \mbox{$\hat{f}_{\gamma}(A)\in\hat{\evidence{P}}(\gamma)$}
  \item there is a finite subset\/ \mbox{${\cal B}\subseteq\bar{\universe{U}}$}
    such that, for each noise function\/ \mbox{$f\in\noise{N}$},
    for some\/ \mbox{$\psi\in\Psi$}, there exists a\/
    \mbox{$B\in{\cal B}$} with
    \mbox{$\hat{f}_{\psi}(B)\in\hat{\evidence{P}}(\psi)$}
  \end{enumerate}

  Note that the condition above can be shown equivalent to: for
  every\/ $\model{M}$, if the conjunction of\/ $\Gamma$ holds in
  $\model{M}$, then the disjunction of\/ $\Psi$ holds in\/
  $\model{M}$.
}
\end{definition}

\begin{definition}
\label{def:realizing-sets}
{\raggedright
  Let\/ \mbox{$\model{M}=
    \tuple{\universe{D},\universe{U},\evidence{P},\noise{N}}$} be a
  relational realizability model,
  \mbox{$\noise{M}\subseteq\noise{N}$}, \mbox{$\alpha\in\PF$}, and\/
  \mbox{$A\in\hat{\universe{U}}_{\alpha}$}. Then\/
  \mbox{$\realize{\noise{M}}{\alpha}{A}=
  \setof{f\in\noise{M}}{\hat{f}_{\alpha}(A)\in\hat{\evidence{P}}(\alpha)}$}.
  Similarly, \mbox{$\realize{\noise{M}}{\Ind}{D}=
  \setof{f\in\noise{M}}{\hat{f}_{\Ind}(D)\in\hat{\evidence{P}}(\Ind)}$}.
  A subset\/
  \mbox{$\noise{P}\subseteq\noise{N}$} is a\/ {\em realizing subset for\/}
  $\model{M}$ if and only if there exist\/ \mbox{$\alpha\in\PF$} and\/
  \mbox{$A\in\universe{U}_{\alpha}$} such that\/
  \mbox{$\noise{P}=\realize{\noise{N}}{\alpha}{A}$},
  or there exists \mbox{$D\in\universe{D}$} such that
  \mbox{$\noise{P}=\realize{\noise{N}}{\Ind}{D}$}.
}
\end{definition}
\begin{lemma}
\label{lem:realizability-beth}
{\raggedright
  Let\/ \mbox{$\model{M}=
    \tuple{\universe{D},\universe{U},\evidence{P},\noise{N}}$} be a
  relational realizability model, $\eta$ an environment
  for\/ $\model{M}$.
  \begin{enumerate}
    \item \mbox{$\model{M},\eta\nmodels\alpha\land\beta$} if and only if\/
       \mbox{$\model{M},\eta\nmodels\alpha$} and\/
       \mbox{$\model{M},\eta\nmodels\beta$}.
    \item \mbox{$\model{M},\eta\nmodels\alpha\lor\beta$} if and only if
       there are two subsets\/
       \mbox{$\noise{N}_{\alpha},\noise{N}_{\beta}\subseteq\noise{N}$}
       such that\/
       \mbox{$\noise{N}_{\alpha}\cup\noise{N}_{\beta}=\noise{N}$},
       \mbox{$\tuple{\universe{D},\universe{U},
         \evidence{P},\noise{N}_{\alpha}},\eta\nmodels
       \alpha$}, and\/
       \mbox{$\tuple{\universe{D},\universe{U},
         \evidence{P},\noise{N}_{\beta}},\eta\nmodels
       \beta$}.
    \item \mbox{$\model{M},\eta\nmodels\alpha\limplies\beta$} if and only
        if, for every subset\/ \mbox{$\noise{M}\subseteq\noise{N}$},
        \mbox{$\tuple{\universe{D},\universe{U},
          \evidence{P},\noise{M}},\eta\nmodels\alpha$}
        implies
        \mbox{$\tuple{\universe{D},\universe{U},
          \evidence{P},\noise{M}},\eta\nmodels\beta$}.
    \item \mbox{$\model{M},\eta\nmodels\alpha\limplies\beta$} if and only
        if, for every\/ \mbox{$A\in\hat{\universe{U}}_{\alpha}$},
        \mbox{$\tuple{\universe{D},\universe{U},\evidence{P},
        \realize{\noise{M}}{\alpha}{A}},\eta\nmodels\beta$}.
    \item \mbox{$\model{M},\eta\nmodels\alpha\limplies\beta$} if and only
        if, for every\/ \mbox{$a\in\universe{U}_{\alpha}$},
        \mbox{$\tuple{\universe{D},\universe{U},\evidence{P},
        \realize{\noise{M}}{\alpha}{\{a\}}},\eta\nmodels\beta$}.
    \item \mbox{$\model{M},\eta\nmodels\forall x\sepdot\alpha$} if and
        only if, for every\/ \mbox{$\noise{M}\subseteq\noise{N}$} and
        every\/ \mbox{$D\in\hat{\universe{D}}$},
        \mbox{$\hat{f}_{\Ind}(D)\in\hat{\evidence{P}}(\Ind)$} implies\/
        \mbox{$\tuple{\universe{D},\universe{U},\evidence{P},\noise{M}},\eta
          \nmodels\subst{D}{x}{\alpha}$}.
    \item \mbox{$\model{M},\eta\nmodels\exists x\sepdot\alpha$} if and
       only if\/ there is a\/ \mbox{$D\in\hat{\universe{D}}$} such that\/
       \mbox{$\model{M},\eta\nmodels\subst{D}{x}{\alpha}$}.
    \item If there is a finite collection of subsets\/
      \mbox{$\noise{N}_1,\ldots,\noise{N}_m\subseteq\noise{N}$}
      such that\/
      \mbox{$\noise{N}_1\union\cdots\union\noise{N}_m=\noise{N}$}
      and for each\/ \mbox{$i\leq m$}
      \mbox{$\tuple{\universe{D},\universe{U},
        \evidence{P},\noise{N}_i},\eta\nmodels\alpha$},
      then\/
      \mbox{$\model{M},\eta\nmodels\alpha$}.
    \item If $\Gamma\proves\Delta$ is valid, and $\Delta=\{\delta_1,\ldots,\delta_n\}$, then 
  \end{enumerate}
}
  All of the equivalences above hold when the subets of\/
  $\noise{N}$ range over the realizing subsets for\/ $\model{M}$.
  Similarly, the equivalences hold when the subsets of\/ $\noise{N}$
  range over a {\em cover\/} class $C$, where each realizing subset is
  the finite union of sets in $C$.
\end{lemma}
{\raggedright
\paragraph{Proof:} In all of the proof below, the environment $\eta$
must be applied systematically. So, let $\alpha'=\eta(\alpha)$, and
$\beta'=\eta(\beta)$ to condense the notation.
\paragraph{1 ($\limplies$)}
  Assume \mbox{$\model{M},\eta\nmodels\alpha\land\beta$}.
  By Definitions~\ref{def:relational-closure}
  and~\ref{def:relational-theory}, there is a
  \mbox{$C\in\hat{\universe{U}}_{\alpha'\land\beta'}$} such that, for
  all \mbox{$f\in\noise{N}$}
  \mbox{$\hat{f}_{\alpha'\land\beta'}(C)\in\hat{\evidence{P}}
    (\alpha'\land\beta')$}.
  Let \mbox{$C=\{\tuple{A_1,B_1},\ldots,\tuple{A_n,B_n}\}$}.
  Define \mbox{$C_{\alpha}=\{A_1,\ldots,A_n\}$} and
  \mbox{$C_{\beta}=\{B_1,\ldots,B_n\}$}.
  Define \mbox{$A=\Union C_{\alpha}$}, \mbox{$B=\Union C_{\beta}$}.
  Since $C_{\alpha}$ is a finite set of finite subsets of
  $\universe{U}_{\alpha'}$, the union $A$ of $C_{\alpha}$ is also a
  finite subset of $\universe{U}_{\alpha'}$, that is,
  \mbox{$A\in\hat{\universe{U}}_{\alpha'}$}.
  For each \mbox{$f\in\noise{N}$},
  \mbox{$\hat{f}_{\alpha'\land\beta'}(C)\in
    \hat{\evidence{P}}(\alpha'\land\beta')$},
  so there is a tuple \mbox{$\tuple{A_i,B_i}$} such that
  \mbox{$f_{\alpha'\land\beta'}(\tuple{A_i,B_i})\in
    \evidence{P}(\alpha'\land\beta')$}.
  By Definition~\ref{def:relational-closure} of $f$ and $\hat{f}$,
  \mbox{$\hat{f}_{\alpha'}(A_i)\in\hat{\evidence{P}}(\alpha')$};
  applying the definition again, there is an \mbox{$a\in A_i$} such
  that \mbox{$f_{\alpha'}(a)\in\evidence{P}(\alpha')$}.
  But, \mbox{$a\in A$} as well, so
  \mbox{$\hat{f}_{\alpha'}(A)\in\hat{\evidence{P}}(\alpha')$}.
  A symmetric argument shows that
  \mbox{$B\in\hat{\universe{U}}_{\beta'}$} and
  \mbox{$\hat{f}_{\beta'}(B)\in\hat{\evidence{P}}(\beta')$}.
  Therefore, \mbox{$\model{M},\eta\nmodels A\colon\alpha$} and
  \mbox{$\model{M},\eta\nmodels B\colon\beta$}.

\paragraph{1 ($\limplied$)}
  Conversely, assume \mbox{$\model{M},\eta\nmodels
  A\colon\alpha$} and \mbox{$\model{M}\eta\nmodels A\colon\alpha$}.
  For each \mbox{$f\in\noise{N}$},
  \mbox{$\hat{f}_{\alpha'}(A)\in\hat{\evidence{P}}(\alpha')$} and
  \mbox{$\hat{f}_{\beta'}(B)\in\hat{\evidence{P}}(\beta')$}.
  So, \mbox{$\hat{f}_{\alpha'\land\beta'}(\{\tuple{A,B}\})=
    \{f_{\alpha'\land\beta'}(\tuple{A,B})\}=
    \{\tuple{\hat{f}_{\alpha'}(A),\hat{f}_{\beta'}(B)}\}\in
    \hat{\evidence{P}}(\alpha'\land\beta')$}.
  Therefore,
    \mbox{$\model{M},\eta\nmodels\{\tuple{A,B}\}\colon\alpha\land\beta$}.

\paragraph{2 ($\limplies$)}
  Assume \mbox{$\model{M},\eta\nmodels C\colon\alpha\lor\beta$}.
  By Definition~\ref{def:relational-theory}, for each
  \mbox{$f\in\noise{N}$},
  \mbox{$\hat{f}_{\alpha'\lor\beta'}(C)\in
    \hat{\evidence{P}}(\alpha'\lor\beta')$}.
  Write \mbox{$C=\{\tuple{0,A_1},\ldots,\tuple{0,A_m},
    \tuple{1,B_1},\ldots,\tuple{1,B_n}\}$}.
  Define \mbox{$A=\Union\{A_1,\ldots,A_m\}$},
    \mbox{$B=\Union\{B_1,\ldots,B_n\}$}.
  Let \mbox{$\noise{N}_{\alpha}=
  \setof{f\in\noise{N}}{\hat{f}_{\alpha'}(A_i)\in\hat{\evidence{P}}(\alpha')
  \mbox{ for some }i\leq m}$} and \mbox{$\noise{N}_{\beta}=
  \setof{f\in\noise{N}}{\hat{f}_{\beta'}(B_j)\in\hat{\evidence{P}}(\beta')
  \mbox{ for some }j\leq n}$}

  \paragraph{Claim:
    \mbox{$\tuple{\universe{D},\universe{U},
      \evidence{P},\noise{N}_{\alpha}}\nmodels
    A\colon\alpha$}.}
    Clearly, \mbox{$A\in\hat{\universe{U}}_{\alpha'}$}
    (same argument as in 3 above).
    For each \mbox{$f\in\noise{N}_{\alpha}$}, there
    is an \mbox{$A'\in C_{\alpha}$} such that
    \mbox{$\hat{f}_{\alpha'}(A')\in\hat{\evidence{P}}(\alpha')$}.
    Since \mbox{$A'\subseteq A$},
    \mbox{$\hat{f}_{\alpha'}(A)\in\hat{\evidence{P}}(\alpha')$}.

  \paragraph{Claim:
    \mbox{$\tuple{\universe{D},\universe{U},
      \evidence{P},\noise{N}_{\beta}}\nmodels
    B\colon\beta$}.}
   Symmetric to the argument above.

  \paragraph{Claim:
    \mbox{$\noise{N}_{\alpha}\union\noise{N}_{\beta}=\noise{N}$}.}
    Let \mbox{$f\in\noise{N}$}.
    By assumption,
    \mbox{$\hat{f}_{\alpha'\lor\beta'}(C)\in
     \hat{\evidence{P}}(\alpha'\lor\beta')$}.
    So, there is a \mbox{$c\in C$} such that
    \mbox{$f_{\alpha'\lor\beta'}(c)\in\evidence{P}(\alpha'\lor\beta')$}.
    $c$ must be of the form \mbox{$\tuple{0,A'}$} with
    \mbox{$\hat{f}_{\alpha'}(A')\in\hat{\evidence{P}}(\alpha')$}, or $c$ is of
    the form \mbox{$\tuple{1,B'}$}, with
    \mbox{$\hat{f}_{\beta'}(B')\in\hat{\evidence{P}}(\beta')$}.
    In the first case, \mbox{$f\in\noise{N}_{\alpha}$};
    in the second case, \mbox{$f\in\noise{N}_{\beta}$}.

\paragraph{2 ($\limplied$)}
  Assume \mbox{$\tuple{\universe{D},\universe{U},
    \evidence{P},\noise{N}_{\alpha}},\eta\nmodels
    A\colon\alpha$} and
  \mbox{$\tuple{\universe{D},\universe{U},
    \evidence{P},\noise{N}_{\beta}},\eta\nmodels
    B\colon\beta$}, where
  \mbox{$\noise{N}_{\alpha}\union\noise{N}_{\beta}=\noise{N}$}.
  Let \mbox{$f\in\noise{N}$} be arbitrary.
  \mbox{$\hat{f}_{\alpha'\lor\beta'}(\{\tuple{0,A},\tuple{1,B}\})=
    \{f_{\alpha'\lor\beta'}(\tuple{0,A}),f_{\alpha'\lor\beta'}(\tuple{1,B})\}=
    \{\tuple{0,\hat{f}_{\alpha'}(A)},\tuple{1,\hat{f}_{\beta'}(B)}\}$}
  If \mbox{$f\in\noise{N}_{\alpha}$}, then
  \mbox{$\hat{f}_{\alpha'}(A)\in\hat{\evidence{P}}(\alpha')$}, so
  \mbox{$f_{\alpha'\lor\beta'}(\tuple{0,A})\in
    \evidence{P}(\alpha'\lor\beta')$},
  so \mbox{$\hat{f}_{\alpha'\lor\beta'}(\{\tuple{0,A},\tuple{1,B}\})\in
  \hat{\evidence{P}}(\alpha'\lor\beta')$}.
  By definition, \mbox{$\tuple{\universe{D},\universe{U},
    \evidence{P},\noise{N}}\eta\nmodels
    \{\tuple{0,A},\tuple{1,B}\}\colon\alpha\lor\beta$}.
  A symmetric argument holds when \mbox{$f\in\noise{N}_{\beta}$}.

\paragraph{3 ($\limplies$)}
  Assume that \mbox{$\model{M},\eta\nmodels
  C\colon\alpha\limplies\beta$}, that
  \mbox{$\noise{M}\subseteq\noise{N}$}, and that
  \mbox{$\tuple{\universe{D},\universe{U},\evidence{P},\noise{M}}\nmodels
  A\colon\alpha$}.
  Let \mbox{$C=\{c_1,\ldots,c_n\}$}.
  For each\/ \mbox{$1\leq i\leq n$}, choose\/ $B_i$ such that\/
  \mbox{$A[c_i]B_i$} (there is such a\/ $B_i$ because\/ $c_i$ is
  entire from\/ $\hat{\universe{U}}_{\alpha'}$ to\/
  $\hat{\universe{U}}_{\beta'}$, and finite choice is allowed by
  Lemma~\ref{lem:choice}).
  Define \mbox{$B=B_1\union\cdots\union B_n$}.
  Let \mbox{$f\in\noise{N}$} be an arbitrary noise function.
  \mbox{$\hat{f}_{\alpha'\limplies\beta'}(C)\in
  \hat{\evidence{P}}(\alpha'\limplies\beta')$}, so for some\/
  \mbox{$c_i\in C$},
  \mbox{$f_{\alpha'\limplies\beta'}(c_i)\in
    \evidence{P}(\alpha'\limplies\beta')$}.
  By definition of\/ $f_{\alpha'\limplies\beta'}$,
  \mbox{$\hat{f}_{\alpha'}(A)[f_{\alpha'\limplies\beta'}(c_i)]
    \hat{f}_{\beta'}(B_i)$}.
  Since \mbox{$\hat{f}_{\alpha'}(A)\in\hat{\evidence{P}}(\alpha')$}, and
  since \mbox{$f_{\alpha'\limplies\beta'}(c_i)$} is reliable from\/
  \mbox{$\hat{\evidence{P}}(\alpha')$} to\/
  \mbox{$\hat{\evidence{P}}(\beta')$},
  \mbox{$\hat{f}_{\beta'}(B_i)\in\hat{\evidence{P}}(\beta')$}.
  Since\/ \mbox{$B_i\subseteq B$},
  \mbox{$\hat{f}_{\beta'}(B)\in\hat{\evidence{P}}(\beta')$} as well.
  So,
  \mbox{$\tuple{\universe{D},\universe{U},\evidence{P},\noise{M}},\eta\nmodels
  B\colon\beta$}.

\paragraph{3 ($\limplied$)}
  Conversely, assume that, for every subset
  \mbox{$\noise{M}\subseteq\noise{N}$}, if
  \mbox{$\tuple{\universe{D},\universe{U},
    \evidence{P},\noise{M}},\eta\nmodels\alpha$} then
  \mbox{$\tuple{\universe{D},\universe{U},
   \evidence{P},\noise{M}},\eta\nmodels\beta$}.
  Define\/ \mbox{$c\in\universe{U}_{\alpha'\limplies\beta'}$} by
  \mbox{$c=\setof{\tuple{A,B}}{\tuple{\universe{D},\universe{U},\evidence{P},
  \realize{\noise{N}}{\alpha'}{A}}\nmodels B\colon\beta}$}.
  The assumption guarantees that\/ $c$ is entire from\/
  $\hat{\universe{U}}_{\alpha'}$ to\/ $\hat{\universe{U}}_{\beta'}$
  (let\/ \mbox{$\noise{M}=\realize{\noise{N}}{\alpha'}{A}$}).
  Let\/ \mbox{$f\in\noise{N}$} be an arbitrary noise function, and let\/
  \mbox{$A\in\hat{\evidence{P}}(\alpha')$},
  \mbox{$B\in\hat{\universe{U}}_{\beta'}$} be arbitrary realizers such that
  \mbox{$A[f_{\alpha'\limplies\beta'}(c)]B$}.
  By definition of\/ $f_{\alpha'\limplies\beta'}$,
  \mbox{$\hat{f}^{-1}_{\alpha'}(A)[c]\hat{f}^{-1}_{\beta'}(B)$}
  ($f^{-1}$ is well-defined because noise is required to be injective).
  By the definition of\/ $c$ above, since\/
  \mbox{$f\in\realize{\noise{N}}{\alpha'}{\hat{f}^{-1}(A)}$},
  \mbox{$B=\hat{f}_{\beta'}(\hat{f}^{-1}_{\beta'}(B))\in
  \hat{\evidence{P}}(\beta')$}.
  So, \mbox{$f_{\alpha'\limplies\beta'}(c)$} is reliable from\/
  \mbox{$\hat{\evidence{P}}_{\alpha'}$} to\/
  \mbox{$\hat{\evidence{P}}_{\beta'}$}.
  Therefore, \mbox{$\model{M}\nmodels,\eta\{c\}\colon\alpha\limplies\beta$}.

\paragraph{4} Follows from inspection of the proof of 3.

\paragraph{5} Straightforward.

\paragraph{6 ($\limplies$)}
  Assume that\/ \mbox{$\model{M},\eta\nmodels
  R\colon\forall x\sepdot\alpha$}, \mbox{$\noise{M}\subseteq\noise{N}$},
  \mbox{$D\in\hat{\universe{D}}$}, and that\/
  \mbox{$\hat{f}_{\Ind}(D)\in\hat{\evidence{P}}(\Ind)$}.
  Then\/
  \mbox{$\tuple{\universe{D},\universe{U},\evidence{P},\noise{M}},\eta
          \nmodels R\colon\forall x\sepdot\alpha$}.
  Write\/ \mbox{$R=\{r_1,\ldots,r_n\}$}.
  For each\/ \mbox{$1\leq i\leq n$}, choose\/ $B_i$ such that\/
  \mbox{$D[r_i]B_i$} (there is such a\/ $B_i$ because\/ $r_i$ is
  entire from\/ $\hat{\universe{D}}$ to\/
  $\hat{\universe{U}}_{\subst{D}{x}{\alpha'}}$,
  and because finite choice is allowed by
  Lemma~\ref{lem:choice}).
  Define\/ \mbox{$B=B_1\union\cdots\union B_n$}.
  Let\/ \mbox{$f\in\noise{N}$} be an arbitrary noise function.
  \mbox{$\hat{f}_{\forall x \sepdot\alpha'}(R)\in
  \hat{\evidence{P}}(\forall x \sepdot\alpha')$}, so for some\/
  \mbox{$r_i\in R$},
  \mbox{$f_{\forall x \sepdot\alpha'}(r_i)\in
    \evidence{P}(\forall x \sepdot\alpha')$}.
  By definition of\/ $f_{\forall x \sepdot\alpha'}$,
  \mbox{$\hat{f}_{\Ind}(D)[f_{\forall x
  \sepdot\alpha'}(r_i)]\hat{f}_{\subst{D}{x}{\alpha'}}(B_i)$},
  hence\/ $\hat{f}_{\subst{D}{x}{\alpha'}}(B_i)
    \in\hat{\evidence{P}}(\subst{D}{x}{\alpha'})$.
  Since\/ \mbox{$B_i\subseteq B$}, we also have\/
  $\hat{f}_{\subst{D}{x}{\alpha'}}(B)\in
    \hat{\evidence{P}}(\subst{D}{x}{\alpha'})$.
  Therefore,
   \mbox{$\tuple{\universe{D},\universe{U},\evidence{P},\noise{M}},\eta
          \nmodels B:\subst{D}{x}{\alpha}$}.

\paragraph{6 ($\limplied$)}
  Conversely, assume that, for every subset\/
  \mbox{$\noise{M}\subseteq\noise{N}$}, and every\/
  \mbox{$D\in\hat{\universe{D}}$},
  if\/ \mbox{$\hat{f}_{\Ind}(D)\in\hat{\evidence{P}}(\Ind)$} then\/
        \mbox{$\tuple{\universe{D},\universe{U},\evidence{P},\noise{M}},\eta
          \nmodels\subst{D}{x}{\alpha}$}.
  Define\/ \mbox{$r\in\universe{U}_{\forall x\sepdot\alpha'}$} by\/
  \mbox{$r=\setof{\tuple{D,B}}{\tuple{\universe{D},\universe{U},\evidence{P},
  \realize{\noise{N}}{\Ind}{D}}\nmodels B\colon\subst{D}{x}{\alpha'}}$}.
  The assumption guarantees that\/ $r$ is entire from\/
  $\hat{\universe{D}}$ to\/  $\hat{\universe{U}}_{\subst{D}{x}{\alpha'}}$.
  Let\/ \mbox{$f\in\noise{N}$} be an arbitrary noise function, and let\/
  \mbox{$D\in\hat{\evidence{P}}(\Ind)$},
  \mbox{$B\in\hat{\universe{U}}_{\subst{D}{x}{\alpha'}}$}
  be arbitrary realizers such that\/
  \mbox{$D[f_{\forall x\sepdot\alpha'}(r)]B$}.
  By definition of\/ $f_{\forall x \sepdot\alpha'}$,
  \mbox{$\hat{f}^{-1}_{\Ind}(D)[r]\hat{f}^{-1}_{\subst{D}{x}{\alpha'}}(B)$}.
  By the definition of\/ $r$ above, since\/
  \mbox{$f\in\realize{\noise{N}}{\Ind}{\hat{f}^{-1}(D)}$},
  \mbox{$B=
   \hat{f}_{\subst{D}{x}{\alpha'}}(\hat{f}^{-1}_{\subst{D}{x}{\alpha'}}(B)
   )\in
  \hat{\evidence{P}}(\subst{D}{x}{\alpha'})$}.
  So, \mbox{$f_{\forall x \sepdot\alpha'}(r)$} is reliable from\/
  \mbox{$\hat{\evidence{P}}_{\Ind}$} to\/
  \mbox{$\hat{\evidence{P}}_{\subst{D}{x}{\alpha'}}$}.
  Therefore, \mbox{$\model{M},\eta\nmodels\{r\}\colon\forall x
  \sepdot\alpha$}.

\paragraph{7 ($\limplies$)}
  Assume \mbox{$\model{M},\eta\nmodels C\colon\exists x\sepdot\alpha$}.
  By Definition~\ref{def:relational-theory}, for each
  \mbox{$f\in\noise{N}$},
  \mbox{$\hat{f}_{\exists x\sepdot\alpha'}(C)\in
    \hat{\evidence{P}}(\exists x\sepdot\alpha')$}.
  Write \mbox{$C=\{\tuple{D_1,A_1},\ldots,\tuple{D_m,A_m}\}$}.
  Define \mbox{$D=\Union\{D_1,\ldots,D_m\}$},
    \mbox{$A=\Union\{A_1,\ldots,A_m\}$}.
  \mbox{$D\in\hat{\universe{D}}$} since each
    \mbox{$D_i\in\hat{\universe{D}}$}.
  Similarly, \mbox{$A\in\hat{\universe{A}}_{\alpha'}$}.
  For each \mbox{$f\in\noise{N}$},
    \mbox{$\hat{f}_{\exists x\colon\sepdot\alpha'}(C)\in
      \hat{\evidence{P}}(\exists x\colon\sepdot\alpha')$}.
  So, there is a tuple \mbox{$\tuple{D_i,A_i}\in C$} such that
    \mbox{$f_{\exists x\sepdot\alpha'}(\tuple{D_i,A_i})\in
      \evidence{P}(\exists x\sepdot\alpha')$}.
  So, \mbox{$\hat{f}_{\subst{D_i}{x}{\alpha'}}(A_i)\in
    \hat{\evidence{P}}(\subst{D_i}{x}{\alpha'})$}.
  Since \mbox{$D_i\subseteq D$} and \mbox{$A_i\subseteq A$},
    \mbox{$\hat{f}_{\subst{D}{x}{\alpha'}}(A)\in
      \hat{\evidence{P}}(\subst{D}{x}{\alpha'})$}.
  Therefore,
  \mbox{$\model{M},\eta\nmodels A\colon\subst{D}{x}{\alpha'}$}.

\paragraph{7 ($\limplied$)}
  Conversely, assume that
  \mbox{$\model{M},\eta\nmodels A\colon\subst{D}{x}{\alpha}$}.
  For each \mbox{$f\in\noise{N}$},
    \mbox{$\hat{f}_{\subst{D}{x}{\alpha'}}(A)\in
      \hat{\evidence{P}}(\subst{D}{x}{\alpha'})$}.
  So, \mbox{$\hat{f}_{\exists x\sepdot\alpha'}(\{\tuple{D,A}\})\in
      \hat{\evidence{P}}(\exists x\sepdot\alpha')$}.
  Therefore, \mbox{$\model{M},\eta\nmodels
    \{\tuple{D,A}\}\colon\exists x\sepdot\alpha$}.

\paragraph{8}
  If $\tuple{\universe{D},\universe{U},\evidence{P},\noise{N}_i},\eta\nmodels
  A_i\colon\alpha$ then $\model{M},\eta\nmodels\Union_i A_i\colon\alpha$.
}

\eop{Lemma~\ref{lem:realizability-beth}}

\begin{theorem}
  \label{thm:soundness}
{\raggedright
  If a sequent\/ \mbox{$\Gamma\proves\Psi$} is derivable, then it is valid.
}
\end{theorem}
{\raggedright
\paragraph{Proof:}
Straightforward induction on the length of the derivation, using
Lemma~\ref{lem:realizability-beth} at each step.
}
\eop{Theorem~\ref{thm:soundness}}
Lemma~\ref{lem:realizability-beth} may also be used to construct from
each relational realizability model an elementarily equivalent Beth
model. Let
$\model{M}=\tuple{\universe{D}_R,\universe{U},\evidence{P},\noise{N}}$
be a relational realizability model. Define the Beth
model~\cite{troelstra-van-dalen,grayson}
$\model{B}=\tuple{\universe{D}_B,\universe{W},\preceq,\nu,\Cov}$ by
$\universe{W}={\cal P}(\noise{N})$, $\universe{D}_B=\hat{\universe{D}_R}$.
The forcing relation is given by $\nu_{\world{w},\eta}(\alpha)$ if and
only if
$\tuple{\universe{D}_R,\universe{U},\evidence{P},\world{w}},\eta\nmodels
\alpha$. $\Cov\subseteq\universe{W}\times\appu{\universe{W}}$
is a binary predicate given by $\Cov(\world{w},{\cal S})$ if and only
if $\Union{\cal S}=\world{w}$. By Lemma~\ref{lem:realizability-beth}
clause 8, this is a legal cover predicate for a Beth model. It is
straightforward to show that $\model{B}$ is elementarily equivalent to
$\model{M}$.

\section{Directions for Further Research}

\begin{itemize}

\item Extend L\"auchli and relational realizability models to
higher-order languages, and prove soundness and completeness for
appropriate formal systems of proof. As the language gets more
powerful, the necessary conditions for uniform constructibility should
get stronger in order to characterize intuitively constructive truth.

\item Completeness guarantees that every valid formula is provable,
but it does not address the brevity, computational efficiency, or
other quality of a constructive proof besides the formula that is
proved. Adapt the characterization of definability in typed lambda
calculus~\cite{StatRel,MitchTCS} to L\"auchli and relational
realizability models. Investigate more expressive proof calculi that
prove the same theories as the Heyting calculus, but provide better
constructions in some technical sense such as brevity or computational
efficiency.

\item The now conventional  approach to giving semantics for modal
logics is to design models consisting of systems of possible worlds
with an accessibility relation~\cite{kripke:modal-semantics-I}. Modal
operators are defined to make assertions about the possible worlds
that are connected to the actual one (for example, knowledge is often
defined as truth in all accessible worlds). Another approach is to
interpret modal operators within realizability models as additional
constraints on the realizers. Design modal realizability models to
generate the traditional theories of various modal logics, and also
other theories that have not been explained by possible worlds. For
example, design models for the logic of knowledge that avoid the
well-known paradoxes of possible-worlds interpretations.

\item Make L\"auchli models classical by letting every set-theoretic object
in $\evidence{P}(\alpha)$ be a realizer for $\alpha$. Add two modal
operators, $\invar$ and $\inhab$. Define $\evidence{P}(\invar\alpha)$
to be the invariant objects in $\evidence{P}(\alpha)$, and
$\evidence{P}(\inhab\alpha)$ to be $\{0\}$ if $\evidence{P}(\alpha)$
contains an invariant, $\emptyset$ otherwise. In a reasonable sense,
$\invar\alpha$ expresses the constructive content of $\alpha$ within
classical logic, and $\inhab\alpha$ expresses the classical content of
$\alpha$ within constructive logic. What is the theory of this modal
system? Clearly $\invar\alpha$ is valid if and only if $\alpha$ is
constructively valid. Contrast this behavior with the usual encoding
of constructive logic into the classical modal logic of necessity,
where the necessity mode is added to every subformula of
$\alpha$~\cite{van-dalen,dummett:intuitionism}. Notice that $\alpha$
with $\invar$ at every subformula is valid if and only if $\alpha$ is
classically valid. The modal realizability approach appears to give a
very different combination of classical and constructive logic than
the well-known one based on necessity in possible worlds. In the new
view, constructive reasoning (where each entire construction is
invariant) is pinned between two different semantic interpretations of
classical reasoning: one requiring no invariance, and the other
requiring invariance at every level of the type hierarchy.

\item Characterize useful concepts of {\em relevant
implication\/}~\cite{anderson-belnap} in realizability models. For
example, in L\"auchli realizability models a candidate definition is
{\em $\alpha$ relevantly implies $\beta$ if and only if there is a
function from $\evidence{P}(\alpha)$ to $\evidence{P}(\beta)$ that is
an isomorphism on each orbit of $\evidence{P}(\alpha)$\/} (invariance
requires only a homomorphism). Or, in relational realizability models,
define relevant implication to require a relation on
$\hat{\universe{U}}(\alpha)$ to $\hat{\universe{U}(\beta)}$ that
reliably maps the complement
$\hat{\universe{U}}(\alpha)-\hat{\evidence{P}}(\alpha)$ to
$\hat{\universe{U}}(\beta)-\hat{\evidence{P}}(\beta)$, as well as
$\hat{\evidence{P}}(\alpha)$ to $\hat{\evidence{P}}(\beta)$.

\item Consider variations on the usual logical connectives. For
example, constructivists generally believe that $\alpha\lor\beta$
should be regarded as true only when there is a uniform construction
realizing either $\alpha$ or $\beta$, and we know which one is
realized. That is why $\evidence{P}(\alpha\lor\beta)$ is defined to be
the {\em marked\/} union of $\evidence{P}(\alpha)$ and
$\evidence{P}(\beta)$. What if we introduce another connective,
$\lambor$, with $\evidence{P}(\alpha\lambor\beta)=
\evidence{P}(\alpha)\union\evidence{P}(\beta)$?

\item Characterize precisely the Kripke models that are natural
translations of L\"auchli realizability models. This relates to
important open problems in the relation between group theory and
lattice theory.

\end{itemize}

\bibliographystyle{plain}
\bibliography{paper}

\end{document}