# Carnap’s problem for intuitionistic propositional logic

Haotian Tong
Tsinghua University  Dag Westerståhl
Stockholm University
Tsinghua University
<EMAIL_ADDRESS>
###### Abstract

We show that intuitionistic propositional logic is _Carnap categorical_ : the
only interpretation of the connectives consistent with the intuitionistic
consequence relation is the standard interpretation. This holds relative to
the most well-known semantics with respect to which intuitionistic logic is
sound and complete; among them Kripke semantics, Beth semantics, Dragalin
semantics, and topological semantics. It also holds for algebraic semantics,
although categoricity in that case is different in kind from categoricity
relative to possible worlds style semantics.

> Keywords: intuitionistic logic, Carnap’s problem, nuclear semantics,
> algebraic semantics, logical constants, consequence relations, categoricity

> MSC: 00A30, 03B20, 06D20

##  1 Motivation and background

[5] worried about the existence of ‘non-normal’ interpretations of the
connectives in classical propositional logic ($\mathsf{CPC}$), i.e.
interpretations that were different from the usual truth tables but still
consistent with $\vdash_{\mathsf{CPC}}$. Though neglected during many decades,
the issue has been reopened in recent years. One reason was that non-normal
interpretations were seen to clash with inferentialist meaning theories
([14]). It has been countered that inferentialism is not really threatened by
non-normal interpretations (e.g. [11]), or that such interpretations are
avoided by a proper understanding of inference rules (e.g. [12]).

In this note we do not discuss the shape or the epistemological status of
rules, but follow the model-theoretic approach to Carnap’s problem initiated
in [3]. That is, a single-conclusion consequence relation $\vdash$ in a
logical language is _given_ (no matter in what way), and, relative to a
semantics which compositionally assigns _semantic values_ (set-theoretic
objects of various kinds) to formulas, one investigates to what extent the
meaning of the logical constants in that language is _fixed_ by consistency
with $\vdash$. This is a precise model-theoretic task.

A first observation, which as pointed out in [3] is hiding already in Carnap’s
1943 book, is that compositionality already rules out non-normal
interpretations of the connectives in $\mathsf{CPC}$, relative to the usual
two-valued semantics.111Compositionality is by now an accepted requirement on
formal semantics, but the idea was not around in 1943. The result as stated
presupposes that propositional atoms are treated as _variables_ , as we do
here. Otherwise, one would have to exclude by stipulation the non-standard
compositional interpretations making all sentences true, since these would
also be consistent with $\vdash_{\mathsf{CPC}}$.  More interestingly,
classical first-order consequence $\vdash_{\mathsf{IPC}}$ does _not_ by itself
fix the meaning of $\forall$, relative to a semantics interpreting quantifier
symbols as sets of subsets of the domain (unary generalized quantifiers), but
constrains it to be a _principal filter_. But if _permutation invariance_ is
also required, then the only consistent interpretation is the standard one:
$\vdash_{\mathsf{IPC}}$ forces $\forall x\varphi(x)$ to mean ‘for all $x$ in
the domain, $\varphi(x)$ holds’.

Carnap’s question can be asked for any consequence relation in any logical
language, relative to any formal semantics for that language. [4] deals with
Carnap’s problem in modal logic, and [16] discusses it for some logics with
generalized quantifiers.

Here we consider Carnap’s problem for intuitionistic propositional logic
($\mathsf{IPC}$). Relative to which formal semantics should we ask the
question? There is by now a plethora of semantics for which $\mathsf{IPC}$ is
sound and complete: Kripke semantics, Beth semantics, topological semantics,
algebraic semantics, …; ideally we would like an answer for all of them.

Actually, there are _two kinds_ of semantics for $\mathsf{IPC}$: the possible
worlds kind and the algebraic kind. The former assigns _subsets of a given
domain_ as semantic values of formulas. The latter doesn’t: semantic values
are just elements of the carrier of an algebra. We will see that categoricity
means something different in the two cases. In Section 2, we show that _Carnap
categoricity_ in fact holds for $\mathsf{IPC}$, relative to a large number of
possible worlds semantics, including the ones just mentioned: only the
standard interpretations are consistent with $\vdash_{\mathsf{IPC}}$. In
Section 3 we do the same for algebraic semantics. Section 4 concludes with
some discussion and open issues..

Our main reference for the semantics of $\mathsf{IPC}$ will be the article [2]
— BH19 in what follows — which surveys and compares a great variety of
intuitionistic semantics. In particular, the notion of _nuclear_ semantics
(introduced in [1]) plays a crucial role, as it does in this note. We largely
follow the notation and terminology in BH19, and refer to that article for
technical notions not explained here.

The propositional language will (with a few explicitly noted exceptions) be
generated by

.[]
$\varphi\;:=\;p\;|\;\bot\;|\;\varphi\land\varphi\;|\;\varphi\lor\varphi\;|\;\varphi\to\varphi\;\;\;\;\;(p\in\mathit{Prop})$

where $\mathit{Prop}$ is a denumerable set of propositional variables. So
$\neg\varphi:=\varphi\to\bot$. The single-conclusion consequence relation

.[] $\vdash_{\mathsf{IPC}}$

in this language is assumed to be familiar, as well as standard intuitionistic
Kripke semantics, with respect to which $\vdash_{\mathsf{IPC}}$ is sound and
complete.

##  2 Possible worlds semantics

What exactly is a possible worlds semantics for $\mathsf{IPC}$? Compare the
analogous question for basic modal logic. That question has a precise (if
initially somewhat surprising) answer: neighborhood semantics. The reason is
that, as shown in [3], when the semantic values of formulas are subsets of a
set $X$ of points (worlds, states, …), classical propositional logic _fixes
the meaning_ of the propositional connectives: negation is complement,
conjunction is intersection, etc.222In fact, this result is a special case of
Theorem 2.9 below; see Remark 2.11.  So the only operator left to interpret is
$\Box$, and if no requirements are placed on that interpretation, it must (by
compositionality) be a function from sets of points to sets of points. Thus,
(local) interpretations can be identified with pairs $(X,F)$, where
$F\\!:\mathcal{P}(X)\to\mathcal{P}(X)$, and these are exactly the neighborhood
frames.333See [4]. [13] is an introduction to neighborhood semantics for modal
logic.

In the case of $\mathsf{IPC}$ there are no further operators to interpret, but
surely there should be some constraints on the interpretation of the
connectives, since we are after all interested in _intuitionistic_
interpretations. Given the great variety of semantics for $\mathsf{IPC}$, it
is not obvious how to formulate a constraint that fits all.444All possible
worlds style semantics, that is, not algebraic semantics, to which we come in
the next section.  However, guided by the most well-known instances of such
semantics (see below), we suggest, somewhat stipulatively, that an
intuitionistic possible worlds semantics assigns _upward closed subsets_
(upsets) of partially ordered set (poset) $\mathcal{F}=(X,\leq)$ as semantic
values. This immediately rules out the classical interpretation of the
connectives (the complement of an upset is usually not an upset).

The elements of the poset can be thought of as _stages_ ; the rough idea being
that information obtained at a stage remains at all later stages. There are
numerous implementations and variations of this idea, by Kripke, Dummett, and
many others; see the detailed discussion in BH19 and the references therein.
But treating semantic values as upsets is common to most of them.

###  2.1 Nuclear interpretations

Let $\mathit{Up}(\mathcal{F})$ be the set of upsets in $\mathcal{F}=(X,\leq)$,
and for $U\subseteq X$, let $\uparrow\\!U$ be the set $\\{x\in X\\!:\exists
y\in U\\!:y\leq x\\}$. Also, for $x\in X$,
$\uparrow\\!x=\;\uparrow\\!\\{x\\}$; these are the _principal_ upsets (the
upsets are exactly the unions of principal upsets).

In algebraic terms, $(\mathit{Up}(\mathcal{F}),\emptyset,\cap,\cup,\to)$ is a
_complete Heyting algebra_ (see footnote 16) also called a _locale_ , where,
for $U,V\in\mathit{Up}(\mathcal{F})$,

.[] $U\to V=\\{x\in X\\!:\;\uparrow\\!x\cap U\subseteq V\\}$ 555More
precisely, it is a _spatial_ locale, since it comes from the open sets of a
topology; completeness is the property of being closed under arbitrary joins
(unions), which holds for all topologies. In this case the topology is rather
special (the _Alexandroff_ topology): the open sets are the upsets on a poset,
and these are also closed under arbitrary meets (intersections).

######  Definition 2.1 (intuitionistic interpretations and consistency)

Let a poset $\mathcal{F}=(X,\leq)$ be given.

  1. 1.

An _intuitionistic interpretation of $\mathsf{IPC}$ on $\mathcal{F}$_ is a map
$I^{\mathcal{F}}$ from $\\{\bot,\land,\lor,\to\\}$ to functions of the
corresponding arity taking upsets to upsets, and a function
$I^{\mathcal{F},\mathit{at}}\\!:\mathit{Up}(\mathcal{F})\to\mathit{Up}(\mathcal{F})$
($\mathit{at}$ for ‘atom’).

  2. 2.

A _valuation on $\mathcal{F}$_ is a map
$v\\!:\mathit{Prop}\to\mathit{Up}(\mathcal{F})$.666There is no constraint on
$v$. But, as we will see, particular intuitionistic interpretations may
require all semantic values, even those of propositional atoms, to be a
special kind of upset. That’s the reason for including the function
$I^{\mathcal{F},\mathit{at}}$ in interpretations; see the next item.

  3. 3.

$I^{\mathcal{F}}$, $I^{\mathcal{F},\mathit{at}}$, and $v$ compositionally
assign a semantic value
$[\\![\varphi]\\!]^{I^{\mathcal{F}}}_{v}\in\mathit{Up}(\mathcal{F})$ of each
formula $\varphi$, as follows:

    1. (a)

$[\\![p]\\!]^{I^{\mathcal{F}}}_{v}=I^{\mathcal{F},\mathit{at}}(v(p))$

    2. (b)

$[\\![\\#(\varphi_{1},\ldots,\varphi_{n})]\\!]^{I^{\mathcal{F}}}_{v}=I^{\mathcal{F}}(\\#)([\\![\varphi_{1}]\\!]^{I^{\mathcal{F}}}_{v},\ldots,[\\![\varphi_{n}]\\!]^{I^{\mathcal{F}}}_{v})$

  4. 4.

$I^{\mathcal{F}}$ is _consistent with a consequence relation $\vdash$_ if,
whenever $\Gamma\vdash\varphi$, we have, for all valuations $v$ on
$\mathcal{F}$: .
$\bigcap_{\psi\in\Gamma}[\\![\psi]\\!]^{I^{\mathcal{F}}}_{v}\subseteq\>[\\![\varphi]\\!]^{I^{\mathcal{F}}}_{v}$

We take $\bigcap\emptyset=X$, so a special case of 4 is that if
$\>\vdash\varphi$, then for all $v$, .
$[\\![\varphi]\\!]^{I^{\mathcal{F}}}_{v}=X$

We can now see how familiar semantics for $\mathsf{IPC}$ each has a
corresponding kind of intuitionistic interpretation, and, among these, a
_standard_ interpretation. The starting point is the _nuclear_ semantics from
[1].

A _nucleus on $\mathit{Up}(\mathcal{F})$_ is a function $j$ from
$\mathit{Up}(\mathcal{F})$ to $\mathit{Up}(\mathcal{F})$ such that the
following holds for all $U,V\in\mathit{Up}(\mathcal{F})$:

  1. (i)

$U\subseteq jU$ (inflationarity)

  2. (ii)

$jjU\subseteq jU$ (idempotence)

  3. (iii)

$j(U\cap V)=jU\cap jV$ (multiplicativity)

$j$ is _dense_ if $j\emptyset=\emptyset$. This is an instance of the general
notion of a nucleus on a Heyting algebra, wich is defined analogously, with
$\cap$ replaced by $\land$, $\emptyset$ by 0, and $\subseteq$ by the partial
order $a\leq b\Leftrightarrow a\land b=a$.

It easily follows that $\subseteq$ in (ii) can be replaced by $=$, and that we
have:

  1. (iv)

$U\subseteq V$ implies $jU\subseteq jV$ (monotonicity)

We say that $U\in\mathit{Up}(\mathcal{F})$ is _fixed_ , if it is a fixpoint of
$j$, i.e. if $jU=U$. Let

.[] $\mathit{Up}(\mathcal{F})_{j}$

be the set of fixed elements of $\mathit{Up}(\mathcal{F})$. BH19 calls
$(\mathcal{F},j)$ a _nuclear frame_. Similarly, if $H$ is a Heyting algebra
and $j$ a nucleus on $H$, $(H,j)$ is a _nuclear algebra_.

######  Definition 2.2 (nuclear interpretations)

Let $j$ be a nucleus on $\mathit{Up}(\mathcal{F})$.

  1. 1.

A _nuclear interpretation_ (on $(\mathcal{F},j)$) is an intuitionistic
interpretation, written $I^{\mathcal{F},j}$, in which the connectives are
interpreted as functions taking fixed upsets to fixed upsets, and
$I^{\mathcal{F},j,\mathit{at}}=j$. Thus, semantic values, calculated as in
Definition 2.1:3, are fixed upsets. Valuations are as before functions from
$\mathit{Prop}$ to $\mathit{Up}(\mathcal{F})$.

  2. 2.

The _standard_ nuclear interpretation, $I^{\mathcal{F},j}_{\text{st}}$, is
defined as follows, for fixed upsets $U,V$:

    1. (a)

$I^{\mathcal{F},j}_{\text{st}}(\bot)=j\emptyset$

    2. (b)

$I^{\mathcal{F},j}_{\text{st}}(\land)(U,V)=U\cap V$

    3. (c)

$I^{\mathcal{F},j}_{\text{st}}(\lor)(U,V)=j(U\cup V)$

    4. (d)

$I^{\mathcal{F},j}_{\text{st}}(\to)(U,V)=\\{x\in X\\!:\;\uparrow\\!x\cap
U\subseteq V\\}$

That $I^{\mathcal{F},j}_{\text{st}}$ is indeed a nuclear interpretation, i.e.
that semantic values are fixed upsets, follows from a well-known fact about
Heyting algebras: if $j$ is a nucleus on a Heyting algebra $H$, then the
algebra $H_{j}$ of fixpoints of $j$ is again a Heyting algebra (and if $H$ is
a locale, so is $H_{j}$), with $0_{j}=j0$, $a\land_{j}b=a\land b$,
$a\lor_{j}b=j(a\lor b)$ (or $\bigvee_{j}A=j\bigvee\\!A$), and $a\to_{j}b=a\to
b$. In particular, if $U,V\in\mathit{Up}(\mathcal{F})_{j}$, then
$I^{\mathcal{F},j}_{\text{st}}(\to)(U,V)\in\mathit{Up}(\mathcal{F})_{j}$. Let

.[]
$\mathbf{Up}_{j}=(\mathit{Up}(\mathcal{F})_{j},\emptyset_{j},\cap_{j},\cup_{j},\to_{j})$

###  2.2 Examples

######  Example 2.3 (Kripke semantics)

Given $\mathcal{F}$, let $j_{k}$ be the identity function on
$\mathit{Up}(\mathcal{F})$. $j_{k}$ is clearly a nucleus. So _Kripke frames_
are nuclear frames of the form $(\mathcal{F},j_{k})$ (or simply
$\mathcal{F}$), and the _standard Kripke interpretation_
$I^{\mathcal{F},j_{k}}_{\text{st}}$ is now as in Definition 2.2, with
$j=j_{k}$. Clearly, these are exactly the usual truth conditions in Kripke
semantics for intuitionistic logic.

More generally, let a _Kripke interpretation on $\mathcal{F}$_ be a nuclear
interpretation $I^{\mathcal{F},j_{k}}$. Semantic values
$[\\![\varphi]\\!]^{I^{\mathcal{F},j_{k}}}_{v}$ are upsets (which are
trivially fixed), and
$[\\![p]\\!]^{I^{\mathcal{F},j_{k}}}_{v}=j_{k}v(p)=v(p)$.

######  Example 2.4 (Beth semantics)

There are several versions of Beth semantics, but here we follow BH19: a _Beth
frame_ is a poset $\mathcal{F}$ (rather than a tree), and a _path_ is chain in
$\mathcal{F}$ closed under upper bounds. So the nuclear setting applies
without change. Let, for $U\in\mathit{Up}(\mathcal{F})$,

. $j_{b}U=\\{x\in X\\!:\text{every path through $x$ intersects $U$}\\}$

Then one verfies that $j_{b}$ is a nucleus on $\mathit{Up}(\mathcal{F})$ — the
_Beth nucleus_ — and the _standard Beth interpretation_
$I^{\mathcal{F},j_{b}}_{\text{st}}$ is as in Definition 2.2 with $j=j_{b}$.
Thus, it differs from the standard Kripke interpretation only in the semantic
values of atoms and disjunctions.

In general, we define a _Beth interpretation on $\mathcal{F}$_ to be any
nuclear interpretation of the form $I^{\mathcal{F},j_{b}}$. Semantic values
are fixed upsets relative to $j_{b}$, and
$[\\![p]\\!]^{I^{\mathcal{F},j_{b}}}_{v}=j_{b}v(p)$.

######  Example 2.5 (Dragalin semantics)

Dragalin generalized Beth semantics by considering a more general notion of a
path, called a _development_ by Bezhanishvili and Holliday. Each $x\in X$ is a
associated with a set $D(x)$ of subsets of $X$ satifying certain conditions.
Dragalin proved that

.[] $j_{D}U=\\{x\in X\\!:\text{every development in $D(x)$ intersects $U$}\\}$

is a nucleus on $\mathit{Up}(\mathcal{F})$, so Dragalin semantics is an
instance of nuclear semantics. The importance of this kind of nuclear
semantics is seen from the result in [1] that _every_ locale can be realized
as the set of fixed upsets of a nuclear frame of the form
$(\mathcal{F},j_{D})$.

Just as before, one has the _standard Dragalin interpretation_ (see BH19), and
a notion of an arbitrary _Dragalin interpretation_.

######  Example 2.6 (topological semantics)

Topological semantics is the oldest formal semantics for $\mathsf{IPC}$, going
back to [17] and [18]. That it can be seen as an instance of nuclear semantics
follows from a special case of a theorem of Dragalin; for a proof of the
general case in the present setting see [1] (Theorem 2.8).

Let $\Omega(X)$ be a topology on $X$, i.e. $\Omega(X)$ is its set of
opens.777So $\Omega(X)\subseteq\mathcal{P}(X)$, $\emptyset,X\in\Omega(X)$, and
$\Omega(X)$ is closed under finite intersections and arbitrary unions.  Then
$\mathbf{\Omega}(X)=(\Omega(X),\emptyset,\cap,\cup,\to)$ is a complete Heyting
algebra, with

.[] $U\to V=\mathit{int}((X\\!-\\!U)\cup V)$

where $\mathit{int}$ is the _interior operation_ : for $Y\subseteq X$,

.[] $\mathit{int}(Y)=\bigcup\\{U\\!\in\Omega(X)\\!:\>U\subseteq Y\\}$

The open sets themselves need not be upsets of a partial order, but Dragalin’s
result is that $\mathbf{\Omega}(X)$ is _isomorphic_ to the fixed upsets of a
nuclear frame.

Let $\mathcal{F}$ be the poset $(\Omega(X)^{-},\supseteq)$, where
$\Omega(X)^{-}=\Omega(X)-\\{\emptyset\\}$ (so the upsets of $\mathcal{F}$ are
the downsets of $(\Omega(X)^{-},\subseteq)$). We use $A,B,\ldots$ for upsets
of $\mathcal{F}$, and $Z,U,V\ldots$ for open sets. Define:

.[] $jA=\;\uparrow\\!\bigcup A$

######  Theorem 2.7 (Dragalin)

$j$ is a dense nucleus on $\mathcal{F}$, and the function
$h(U)=\;\uparrow\\!U$ is an isomorphism from $\mathbf{\Omega}(X)$ to
$\mathbf{Up}(\mathcal{F})_{j}$.

So in this sense, a topology can be seen as a nuclear frame, defined via the
bijection $h$. Next, the _standard topological semantics_ on $\Omega(X)$ for
$\mathsf{IPC}$, originating from Stone and Tarski, is given by the
interpretation we write $I^{\Omega(X)}_{\text{st}}$, as follows. Valuations
are functions from _Prop_ to $\Omega(X)$, and semantic values are calculated
with the these functions:

. . $I^{\Omega(X)}_{\text{st}}(\bot)=\emptyset$ .̱
$I^{\Omega(X)}_{\text{st}}(\land)(U,V)=U\cap V$ .̱
$I^{\Omega(X)}_{\text{st}}(\lor)(U,V)=U\cup V$ .̱
$I^{\Omega(X)}_{\text{st}}(\to)(U,V)=\mathit{int}((X\\!-\\!U)\cup V)$

This is not an intuitionistic possible worlds semantics in the sense of
Definition 2.1, but _almost_. More precisely:

###### Lemma 2.8

If $\mathcal{F}$, $j$, and $h$ are as in Theorem 2.7, then, for all
$A,B\in\mathit{Up}(\mathcal{F})_{j}$,
$I^{\mathcal{F},j}_{\text{st}}(\land)(A,B)=h(I^{\Omega(X)}_{\text{st}}\\!(\land)(h^{-1}(A),h^{-1}(B)))$,
and similarly for the other connectives.

###### Proof.

The proof is a routine verification, using the density of $j$ for $\bot$, and,
for $\lor$ and $\to$, the following observation from the proof of Theorem 2.7:

. $jA=A\;$ iff $\;A$ is $\emptyset$ or $A=h(U)$ for some $U\in\Omega(X)^{-}$.

We omit the details. $\Box$

In analogy with the preceding examples, let us say that a _topological
interpretation of $\mathsf{IPC}$_ (on $\Omega(X)$) is a map $I^{\Omega(X)}$
from $\\{\bot,\land,\lor,\to\\}$ to functions of the corresponding arity
taking open sets to open sets. A _topological valuation_ is a map
$v\\!:\mathit{Prop} \to\Omega(X)$, and semantic values
$[\\![\varphi]\\!]^{I^{\Omega(X)}}_{v}$ are assigned compositionally just as
before. Also, consistency of such an interpretation with a consequence
relation is defined as before.

###  2.3 Carnap categoricity

$\vdash_{\mathsf{IPC}}$ is sound and complete with respect to all the
semantics discussed in the preceding subsection, relative to what we are here
calling the standard interpretations; see BH19 for proofs. However, our
interest is not completeness, but categoricity. For each particular semantics
mentioned above, we defined the notion of a (local) interpretation of the
connectives in that semantics, and described how semantic values relative to
such an interpretation are computed for each formula. We also specified, in
each case, the _standard_ interpretation.

The standard interpretations are all consistent with $\vdash_{\mathsf{IPC}}$.
But could there be _other_ interpretations, of the relevant kind, that are
_also_ consistent with $\vdash_{\mathsf{IPC}}$? This is Carnap’s question. We
now give a negative answer to that question.

###### Theorem 2.9

Let $(\mathcal{F},j)$ be a nuclear frame, and $I^{\mathcal{F},j}$ a nuclear
interpretation which is consistent with $\vdash_{\mathsf{IPC}}$. Then
$I^{\mathcal{F},j}=I^{\mathcal{F},j}_{\text{st}}$.

###### Proof.

We first show:

.[(a)] $I^{\mathcal{F},j}(\land)$ is standard.

Here and below, $U,V\in\mathit{Up}(\mathcal{F})_{j}$. Since $p\land
q\vdash_{\mathsf{IPC}}p$, we have $I^{\mathcal{F},j}(\land)(U,V)\subseteq U$.
Let us see in detail how this happens. Let $v$ be a valuation such that
$v(p)=U$ and $v(q)=V$. The requirement that
$v(p),v(q)\in\mathit{Up}(\mathcal{F})$ is satisfied. By the truth definition
(Definition 2.1:3) and consistency with $\vdash_{\mathsf{IPC}}$, we have

$[\\![p\land
q]\\!]^{I^{\mathcal{F},j}}_{v}\\!=I^{\mathcal{F},j}\\!(\land)([\\![p]\\!]^{I^{\mathcal{F},j}}_{v}\\!,[\\![q]\\!]^{I^{\mathcal{F},j}}_{v})=I^{\mathcal{F},j}\\!(\land)(jU,jV)=I^{\mathcal{F},j}(\land)(U,V)\subseteq[\\![p]\\!]^{I^{\mathcal{F},j}}_{v}\\!=U$

(note that $U$ and $V$ are fixpoints). Similarly,
$I^{\mathcal{F},j}(\land)(U,V)\subseteq V$. In the other direction, we use the
fact that $p,q\vdash_{\mathsf{IPC}}p\land q$ to see that $U\cap V\subseteq
I^{\mathcal{F},j}(\land)(U,V)$. Thus, $I^{\mathcal{F},j}(\land)(U,V)=U\cap
V=I^{\mathcal{F},j}_{\text{st}}(\land)(U,V)$. Next,

.[(b)] $I^{\mathcal{F},j}(\bot)$ is standard.

This follows from the fact that $\bot\vdash_{\mathsf{IPC}}p$: letting
$v(p)=\emptyset$, we obtain that
$I^{\mathcal{F},j}(\bot)\subseteq[\\![p]\\!]^{\mathcal{F},j}_{v}=j\emptyset$.
Since $\emptyset\subseteq I^{\mathcal{F},j}(\bot)$ we also have
$j\emptyset\subseteq jI^{\mathcal{F},j}(\bot)=I^{\mathcal{F},j}(\bot)$, by the
monotonicity of $j$ and the assumption that $I^{\mathcal{F},j}(\bot)$ is a
fixed upset. Thus,
$I^{\mathcal{F},j}(\bot)=j\emptyset=I^{\mathcal{F},j}_{\text{st}}(\bot)$. We
now establish some facts about the interpretation of $\to$.

.[(c)]
$I^{\mathcal{F},j}(\to)(U,V)\>\subseteq\>I^{\mathcal{F},j}_{\text{st}}(\to)(U,V)$

To see this, take $x\in I^{\mathcal{F},j}(\to)(U,V)$. In order to show that
$x\in
I^{\mathcal{F},j}_{\text{st}}(\to)(U,V)=I^{\mathcal{F}}_{\text{st}}(\to)(U,V)$,
we must show $\uparrow\\!x\cap\>U\subseteq V$. From the fact that $p,p\to
q\vdash_{\mathsf{IPC}}q$, we obtain, as should now be clear,

.[] $U\cap I^{\mathcal{F},j}(\to)(U,V)\>\subseteq\>V$

Take $y\in\;\uparrow\\!\\!x\cap\>U$. Since $y\geq x$ and
$I^{\mathcal{F},j}(\to)(U,V)$ is an upset, $y\in I^{\mathcal{F},j}(\to)(U,V)$.
So $y\in V$ follows, and (c) is proved.

.[(d)] $U\subseteq V\;$ iff $\;I^{\mathcal{F},j}(\to)(U,V)=X$

Suppose $U\subseteq V$, so $U\cap V=U$. Since $\vdash_{\mathsf{IPC}}p\land
q\to q$, we obtain, from consistency with $\vdash_{\mathsf{IPC}}$ and the fact
that $\land$ is standard, that $I^{\mathcal{F},j}(\to)(U\cap V,V)=X$, i.e.
that $I^{\mathcal{F},j}(\to)(U,V)=X$. In the other direction, suppose
$I^{\mathcal{F},j}(\to)(U,V)=X$. By (c),
$I^{\mathcal{F},j}_{\text{st}}(\to)(U,V)=X$. Then for all $x\in X$, $x\in
U\Rightarrow x\in V$ (since $x\leq x$), i.e. $U\subseteq V$. This proves (d).
We are now able to show:

.[(e)] $I^{\mathcal{F},j}(\lor)$ is standard.

From $p\vdash_{\mathsf{IPC}}p\lor q$ and $q\vdash_{\mathsf{IPC}}p\lor q$ we
obtain that $U\cup V\subseteq I^{\mathcal{F},j}(\lor)(U,V)$. By monotonicity
and since $I^{\mathcal{F},j}(\lor)(U,V)$ is a fixed upset, we have $j(U\cup
V)\subseteq jI^{\mathcal{F},j}(\lor)(U,V)=I^{\mathcal{F},j}(\lor)(U,V)$. In
the other direction, let $v$ be a valuation such that $v(p)=U$, $v(q)=V$, and
$v(r)=U\cup V$. (Note that $U\cup V$ is an upset, even though it need not be
fixed.888But we could equally well have taken $v(r)=j(U\cup V)$. ) Since
$U\subseteq U\cup V$, we have $jU\subseteq j(U\cup V)$, and so by (d),
$I^{\mathcal{F},j}(\to)(jU,j(U\cup V))=I^{\mathcal{F},j}(\to)(U,j(U\cup
V))=[\\![p\to r]\\!]^{I^{\mathcal{F},j}}_{v}=X$. Similarly, $[\\![q\to
r]\\!]^{I^{\mathcal{F},j}}_{v}=X$. Then, from consistency and the fact that

.[] $p\to r,q\to r,p\lor q\vdash_{\mathsf{IPC}}r$

we obtain $I^{\mathcal{F},j}(\lor)(U,V)\subseteq j(U\cup V)$. That is,
$I^{\mathcal{F},j}(\lor)(U,V)=j(U\cup
V)=I^{\mathcal{F},j}_{\text{st}}(\lor)(U,V)$, and (e) is proved. Finally, we
show:

.[(f)] $I^{\mathcal{F},j}(\to)$ is standard.

By (c), it suffices to show that
$I^{\mathcal{F},j}_{\text{st}}(\to)(U,V)\subseteq
I^{\mathcal{F},j}(\to)(U,V)$. Thus, take $x\in
I^{\mathcal{F},j}_{\text{st}}(\to)(U,V)$, i.e. $\uparrow\\!x\cap U\subseteq
V$. Using the multiplicativity and monotonicity of $j$, we have

.[] $j(\uparrow\\!x\cap U)=j\\!\\!\uparrow\\!x\cap jU=j\\!\\!\uparrow\\!x\cap
U\subseteq jV=V$

Let $v$ be such that $v(p)=\;\uparrow\\!\\!x$, $v(q)=U$, and $v(r)=V$. Thus,
since $\land$ is standard,

.[] $[\\![p\land q]\\!]^{I^{\mathcal{F},j}}_{v}=\>j\\!\\!\uparrow\\!x\cap
U\subseteq V=\,[\\![r]\\!]^{I^{\mathcal{F},j}}_{v}$

By (d), it follows that $[\\![p\land q\to r]\\!]^{I^{\mathcal{F},j}}_{v}=\,X$.
Since

.[] $p,p\land q\to r\vdash_{\mathsf{IPC}}q\to r$

we conclude that $j\\!\\!\uparrow\\!\\!x\subseteq
I^{\mathcal{F},j}(\to)(U,V)$. And since $x\in\>\uparrow\\!\\!x\subseteq
j\\!\\!\uparrow\\!\\!x$ (by inflationarity), we have that $x\in
I^{\mathcal{F},j}(\to)(U,V)$. That is,
$I^{\mathcal{F},j}(\to)(U,V)=I^{\mathcal{F},j}_{\text{st}}(\to)(U,V)$.

This concludes the proof that
$I^{\mathcal{F},j}=\,I^{\mathcal{F},j}_{\text{st}}$. $\Box$

###### Corollary 2.10

$\mathsf{IPC}$ is Carnap categorical with respect to any nuclear semantics,
such as Kripke semantics, Beth semantics, or Dragalin semantics. It is also
categorical with respect to topological semantics. Thus, the only
interpretation, of the respective kind, of the propositional connectives that
is consistent with $\vdash_{\mathsf{IPC}}$ is the standard interpretation.

###### Proof.

This is immediate from the theorem for nuclear semantics. For topological
semantics, let $\Omega(X)$ be a topology on $X$, and suppose the topological
interpretation $I^{\Omega(X)}$ is consistent with $\vdash_{\mathsf{IPC}}$. Let
$\mathcal{F}$, $j$, and $h$ be as in Theorem 2.7. Define a nuclear
interpretation $I^{\mathcal{F},j}$ as follows:
$I^{\mathcal{F},j}(\land)(A,B)=h(I^{\Omega(X)}(\land)(h^{-1}(A),h^{-1}(B)))$,
and similarly for the other connectives. Also, if
$v\\!:\mathit{Prop}\to\mathit{Up}(\mathcal{F})$, define the topological
valuation $v^{*}\\!:\mathit{Prop}\to\Omega(X)$ by $v^{*}(p)=h^{-1}(v(p))$. It
follows by an easy induction over formulas (using 2.6 for the atomic case)
that for every $\varphi$,

.[]
$[\\![\varphi]\\!]^{I^{\mathcal{F},j}}_{v}=\;h([\\![\varphi]\\!]^{I^{\Omega(X)}}_{v^{*}})$

Since $h$ is monotone ($U\subseteq V\Rightarrow h(U)\subseteq h(V)$), this
entails that $I^{\mathcal{F},j}$ is consistent with $\vdash_{\mathsf{IPC}}$.
Then we have:
$I^{\Omega(X)}(\land)(U,V)=h^{-1}(I^{\mathcal{F},j}(\land)(h(U),h(V)))$ (by
definition) $=h^{-1}(I^{\mathcal{F},j}_{\text{st}}(\land)(h(U),h(V)))$ (by the
theorem) $=I^{\Omega(X)}_{\text{st}}(\land)(U,V)$ (by Lemma 2.8). Similarly
for the other connectives. Thus, $I^{\Omega(X)}=\,I^{\Omega(X)}_{\text{st}}$.
$\Box$

###### Remark 2.11

The Carnap categoricity of $\mathsf{CPC}$ relative to classical possible
worlds semantics, proved in [3], is a special case of the result for
$\mathsf{IPC}$, since on posets that are sets of isolated points,
$\mathsf{IPC}$ and $\mathsf{CPC}$ coincide. In more detail: suppose $W$ is a
set of worlds and $I^{W}$ an interpretation of the connectives over $W$ — i.e.
$I^{W}$ assigns to each connective a function on $\mathcal{P}(W)$ of
appropriate arity — which is consistent with $\vdash_{\mathsf{CPC}}$. The
upsets of the poset $\mathcal{F}=(W,\\{(x,x)\\!:x\in W\\})$ are exactly the
subsets of $W$. Thus $I^{\mathcal{F}}=I^{W}$ is in fact a Kripke
interpretation, in the sense of Example 2.3, which is consistent with
$\vdash_{\mathsf{CPC}}$, hence with $\vdash_{\mathsf{IPC}}$. By the theorem,
$I^{\mathcal{F}}$ is standard, and so $I^{W}$ is standard (for example,
$I^{W}(\to)(U,V)=(W\\!-\\!U)\cup V$).

Similarly, letting $\mathcal{F}$ be a single reflexive point $\\{x\\}$, the
categoricity of $\mathsf{CPC}$ relative to classical 2-valued semantics,
mentioned in Section 1, also follows from Theorem 2.9: in this case the
interpretation functions are truth functions, and the truth values 0 and 1
correspond to the two upsets $\emptyset$ and $\\{x\\}$.

As the remark illustrates, the strength of the intuitionistic categoricity
theorem comes from its strictly local character: the result holds for _each_
nuclear frame, no matter how trivial.

The proof of Theorem 2.9 uses essentially the assumption that consistency with
$\vdash_{\mathsf{IPC}}$ means that 4 holds (for all $v$). One might be tempted
to suppose that since $\mathsf{IPC}$ satisfies the Deduction Theorem, it would
suffice that all $\mathsf{IPC}$-_theorems_ are valid (so that 4 holds for all
$v$). It is instructive to see why this is _not_ the case.

To begin, we can see where the proof breaks down. Suppose
$\psi\vdash_{\mathsf{IPC}}\varphi$. By the Deduction Theorem, we have
$\vdash_{\mathsf{IPC}}\varphi\to\psi$, so by the soundness assumption,
$[\\![\psi\to\varphi]\\!]^{I^{\mathcal{F},j}}_{v}=I^{\mathcal{F},j}(\to)([\\![\psi]\\!]^{I^{\mathcal{F},j}}_{v},[\\![\varphi]\\!]^{I^{\mathcal{F},j}}_{v})=X$
for all $v$. We wish to conclude that
$[\\![\psi]\\!]^{I^{\mathcal{F},j}}_{v}\subseteq[\\![\varphi]\\!]^{I^{\mathcal{F},j}}_{v}$.
This would follow from (d) in the proof, but (d) presupposes consistency in
the stronger sense. More precisely, (d) relies on (c), whose proof in turn
uses that from $p,p\to q\vdash_{\mathsf{IPC}}q$ we are able to conclude that,
for any fixed upsets $U,V$, we have $U\cap
I^{\mathcal{F},j}(\to)(U,V)\subseteq V$. But it should be fairly clear that
from $\vdash_{\mathsf{IPC}}p\to((p\to q)\to q)$, no such conclusion can be
drawn.

In fact, Wesley Holliday found a counter-example (_p.c_): a non-standard
interpretation of the connectives which validates all $\mathsf{IPC}$-theorems,
and hence is not consistent with $\vdash_{\mathsf{IPC}}$ in the sense of
Definition 2.1:4. With his kind permission, we present the example here.999The
example was originally intended to show that the stronger notion of
consistency is needed for the result in [3] about $\mathsf{CPC}$; see Remark
2.11. Here we have adapted it to $\mathsf{IPC}$.

######  Example 2.12 (Holliday)

Let $\Omega(X)$ be any topological space. We will define a topological
interpretation $I^{\Omega(X)}$ (see Example 2.6) such that (a) if
$\vdash_{\mathsf{IPC}}\varphi$ then for all valuations $v$ on $\Omega(X)$,
$[\\![\varphi]\\!]^{I^{\Omega(X)}}_{v}=X$, but (b) $I^{\Omega(X)}\neq
I^{\Omega(X)}_{\text{st}}$. This gives a generic topological counter-example.
For more concreteness, we can start with a Kripke frame $\mathcal{F}=(X,\leq)$
and let $\Omega(X)$ be the Alexandroff topology described in footnote 5. As
made clear in BH19, Sect. 2.3, Kripke semantics essentially _is_ topological
semantics based on Alexandroff spaces. It is easy to see that the counter-
example then becomes a non-standard Kripke interpretation
$I^{\mathcal{F},j_{k}}$ (see Example 2.3) which validates all theorems of
$\mathsf{IPC}$.

For this example it is easier to use $\neg,\land,\lor,\to$ as primitive
connectives. 2.7 is then replaced by

.[2.7′] $I^{\Omega(X)}_{\text{st}}(\neg)(U)=\mathit{int}(X-U)$

Recall the _closure_ operation $\mathit{cl}$, the dual of $\mathit{int}$:
$\mathit{cl}(Y)$ is the smallest closed set (set whose complement is open)
containing $Y$. An easy calculation shows

.
$[\\![\neg\neg\varphi]\\!]^{I^{\Omega(X)}_{\text{st}}}_{v}=\mathit{int}(\mathit{cl}([\\![\varphi]\\!]^{I^{\Omega(X)}_{\text{st}}}_{v}))$

and thus

.
$[\\![\neg\neg\neg\varphi]\\!]^{I^{\Omega(X)}_{\text{st}}}_{v}=\mathit{int}(X-\mathit{int}(\mathit{cl}([\\![\varphi]\\!]^{I^{\Omega(X)}_{\text{st}}}_{v})))$

Now define $I^{\Omega(X)}$ as follows.

. .
$I^{\Omega(X)}(\land)(U,V)=\mathit{int}(\mathit{cl}(U))\cap\mathit{int}(\mathit{cl}(V))$
.̱ $I^{\Omega(X)}(\neg)(U)=\mathit{int}(X-\mathit{int}(\mathit{cl}(U)))$ .̱
$I^{\Omega(X)}(\to)(U,V)=I^{\Omega(X)}(\neg)(I^{\Omega(X)}(\land)(I^{\Omega(X)}(\neg)(U),V))$
.̱
$I^{\Omega(X)}(\lor)(U,V)=I^{\Omega(X)}(\neg)(I^{\Omega(X)}(\land)(I^{\Omega(X)}(\neg)(U),I^{\Omega(X)}(\neg)(V)))$

Thus, we are putting double negations in front of negated formulas and the
conjuncts of conjunctions, whereas $\to$ and $\lor$ are defined classically
from $\land$ and $\neg$. Clearly, $I^{\Omega(X)}$ is non-standard: for
example, just find a space with open sets $U,V$ such that
$\mathit{int}(\mathit{cl}(U))\cap\mathit{int}(\mathit{cl}(V))\neq U\cap V$.

Now we use a particular _negative translation_ of classical into
intuitionistic propositional logic, defined as follows:

. . $g(p)=p$ .̱ $g(\varphi\land\psi)=\neg\neg g(\varphi)\land\neg\neg g(\psi)$
.̱ $g(\neg\varphi)=\neg\neg\neg g(\psi)$ .̱
$g(\varphi\to\psi)=\neg(g(\varphi)\land\neg g(\psi))$ .̱
$g(\varphi\lor\psi)=\neg(\neg g(\varphi)\land\neg g(\psi))$

Using well-known facts about negative translations, it is not hard to show
that

. $\models_{\mathsf{CPC}}\varphi\;$ iff
$\;\vdash_{\mathsf{IPC}}g(\varphi)$.101010$g$ is similar to the _Kolmogorov
translation_ , say, $G$, which puts a double negation in front of all
subformulas. One can show that if $\varphi$ is not an atom,
$\vdash_{\mathsf{IPC}}\\!g(\varphi)\leftrightarrow G(\varphi)$. It is well-
known that
$\vdash_{\mathsf{CPC}}\varphi\Leftrightarrow\;\,\vdash_{\mathsf{IPC}}G(\varphi)$,
and since no atom is a theorem, 2.12 follows. [7] is a survey of various
negative translations.

Finally, observe that $I^{\Omega(X)}$ interprets a formula $\varphi$ just as
$g(\varphi)$ is standardly interpreted in topological semantics. In other
words, for each topological valuation $v$ we have:

.
$[\\![\varphi]\\!]^{I^{\Omega(X)}}_{v}\\!=[\\![g(\varphi)]\\!]^{I^{\Omega(X)}_{\text{st}}}_{v}$

This is proved by a straightforward inductive argument, using the standard
topological truth definition and 2.12 – 2.12. Thus, if
$\vdash_{\mathsf{IPC}}\varphi$, then $\vdash_{\mathsf{CPC}}\varphi$, hence
$\vdash_{\mathsf{IPC}}g(\varphi)$ by 2.12, and so for any topological
valuation $v$, $[\\![g(\varphi)]\\!]^{I^{\Omega(X)}_{\text{st}}}_{v}=X$, which
by 2.12 entails that $[\\![\varphi]\\!]^{I^{\Omega(X)}}_{v}=X$. That is,
$I^{\Omega(X)}$ validates all $\mathsf{IPC}$ theorems.111111Indeed, it
validates all $\mathsf{CPC}$ theorems, by 2.12, and since the above argument
in fact works for all valuations $v\\!:\mathit{Prop} \to\mathcal{P}(X)$. As
Wesley Holliday pointed out, $I^{\Omega(X)}$ evaluates complex formulas using
the _double negation nucleus_ , i.e. in the Heyting algebra of _regular open_
sets (sets $U$ such that $U=\mathit{int}(\mathit{cl}(U)))$, which is a Boolean
algebra.

On the other hand, it is easy to see that $I^{\Omega(X)}$ is not consistent
with $\vdash_{\mathsf{IPC}}$. For example, one can have
$[\\![p]\\!]^{I^{\Omega(X)}}_{v}\\!=[\\![p\to
q]\\!]^{I^{\Omega(X)}}_{v}\\!=X$, while
$[\\![q]\\!]^{I^{\Omega(X)}}_{v}\\!\neq X$.

##  3 Algebraic semantics

Algebraic semantics for $\mathsf{IPC}$ standardly interprets the connectives
in a Heyting algebra
$\mathcal{A}=(A,0^{\mathcal{A}},1^{\mathcal{A}},\land^{\mathcal{A}},\lor^{\mathcal{A}},\to^{\mathcal{A}})$:
a valuation $v$ maps atoms to $A$, and semantic values
$[\\![\varphi]\\!]^{\mathcal{A}}_{v}$ in $A$ are given by the unique
homomorphism $\overline{v}$ from the syntax algebra to $\mathcal{A}$ that
extends $v$.121212In this section we take 1 ($\top$) to be in the signature
(as is commonly done).  Bezhanishvili and Holliday discuss the view that
algebraic semantics is just ‘syntax in disguise’ (quoted from [19], p. 358),
and that algebraic completeness of $\mathsf{IPC}$ via the usual Tarski-
Lindenbaum construction isn’t really illuminating about the intuitionistic
meaning of the connectives (BH19, end of sect. 2.1). They counter that when
Heyting algebras are defined order-theoretically, and $\leq$ is seen as
entailment, completeness with respect to Heyting algebras is in fact quite
illuminating.131313One might also note that completeness with respect to
‘concrete’ semantics, like Kripke semantics or topological semantics,
_follows_ from algebraic completeness via well-known representation theorems.
Arguably, however, the real work here lies in the representations theorems,
not in the Lindenbaum algebras of logical systems.

From the categoricity perspective, Carnap’s question for algebraic semantics
is conceptually somewhat different from the case of possible worlds semantics.
In the latter case, given, say, a nuclear frame, there are many different
putative interpretations of the connectives _on that frame_ , and we ask which
ones are consistent with $\vdash_{\mathsf{IPC}}$. Relative to an algebra
$\mathcal{A}$, on the other hand, the interpretation of $\to$, say, simply
_is_ $\to^{\mathcal{A}}$. That is, the algebra itself is the interpretation.

We ask, then: Are there _other_ algebras than Heyting algebras — the agreed-on
standard interpretations — consistent with $\vdash_{\mathsf{IPC}}$? It seems
plausible that the answer is No: consistency with $\vdash_{\mathsf{IPC}}$
forces the algebra to be Heyting.

The problem with this reasoning is that we haven’t said _which class of
algebras_ we are looking at: it would be circular to restrict attention to
Heyting algebras! It has to be algebras for which a suitable notion of
consistency with a consequence relation makes sense. For the record, we now
describe how this can be done. We hasten to add, however, that when it comes
to categoricity rather than completeness, the claim that algebraic semantics
is ‘syntax in disguise’ seems more convincing. This will be clear from the
proof of Theorem 3.3 below. But since Carnap’s question in this algebraic
context is new (as far as we know), we shall spell out the fairly obvious
answer.

###  3.1 Algebraic interpretations

The syntax algebra of propositional logic is a _term algebra_ with countably
many generators, which means that for _any_ algebra $\mathcal{A}$ of the same
signature, every map $v$ from propositional atoms to $A$ extends to a unique
homomorphism $\overline{v}$ to $\mathcal{A}$. But it would make no sense to
let every algebra of that signature be a putative interpretation of the
connectives. Interpretations are relative to a _semantics_ , and a semantics
needs at the very least a notion of _truth_. We could of course stipulate that
$\overline{v}(\varphi)=1^{\mathcal{A}}$ means that $\varphi$ is true in
$\mathcal{A}$ under $v$. But nothing can be done with that stipulation unless
we know more about the role of $1^{\mathcal{A}}$. For example, why not
$0^{\mathcal{A}}$ instead?

On the other hand, we want to make as few assumptions as possible. Without
further ado, here is a suggestion.

###### Definition 3.1

$\mathcal{A}=(A,0^{\mathcal{A}},1^{\mathcal{A}},\land^{\mathcal{A}},\lor^{\mathcal{A}},\to^{\mathcal{A}})$
is an _algebraic interpretation_ if $\leq^{\mathcal{A}}$ defined by
$a\leq^{\mathcal{A}}b\Leftrightarrow a\land^{\mathcal{A}}b=a$ is a partial
order with $1^{\mathcal{A}}$ as its largest element.

So we are putting some minimal requirements on $\mathcal{A}$ in order for it
to count as an interpretation, but note that we don’t require anything of
$0^{\mathcal{A}}$, $\lor^{\mathcal{A}}$, or $\to^{\mathcal{A}}$.141414Even
$\land^{\mathcal{A}}$ is not constrained much: idempotence
($a\land^{\mathcal{A}}a=a$) follows, since $\leq^{\mathcal{A}}$ is reflexive,
but not, for example, commutativity.

###  3.2 Consistency and categoricity

It remains to define what it means for an algebraic interpretation to be
consistent with a consequence relation. We are now working in what [10] calls
_$\leq$ -based algebraic semantics_, and the following definition is suggested
by Remark 2.14.7(i) in Humberstone’s book.

###### Definition 3.2

An algebraic interpretation $\mathcal{A}$ is _consistent with_ $\vdash$, if,
whenever $\psi_{1},\ldots,\psi_{n}\vdash\varphi$ holds, we have for all
valuations $v$ on $\mathcal{A}$ and all $c\in A$, that if
$c\leq^{\mathcal{A}}[\\![\psi_{i}]\\!]^{\mathcal{A}}_{v}$ for $i=1,\ldots,n$,
then $c\leq^{\mathcal{A}}[\\![\varphi]\\!]^{\mathcal{A}}_{v}$. 151515If there
are no assumptions, i.e. if $\vdash\varphi$, then the antecedent of the
requirement is vacuously satisfied for each $v$, and the consequent becomes
$[\\![\varphi]\\!]^{\mathcal{A}}_{v}=1^{\mathcal{A}}$.

It may seem more natural to require that if $c$ is the greatest lower bound of
$[\\![\psi_{1}]\\!]^{\mathcal{A}}_{v},\ldots,[\\![\psi_{n}]\\!]^{\mathcal{A}}_{v}$,
then $c\leq^{\mathcal{A}}[\\![\varphi]\\!]^{\mathcal{A}}_{v}$, and indeed this
is equivalent, provided greatest lower bounds _exist_. But Definition 3.1
doesn’t require them to exist, and the next result shows that such a
requirement is not necessary.

We now have a precise formulation of Carnap’s question for algebraic
semantics. The next fact gives the answer, here formulated for $\mathsf{CPC}$
as well.

###### Theorem 3.3

Let $\mathcal{A}$ be an algebraic interpretation.

  1. 1.

If $\mathcal{A}$ is consistent with $\vdash_{\mathsf{IPC}}$, then
$\mathcal{A}$ is a Heyting algebra.

  2. 2.

If $\mathcal{A}$ is consistent with $\vdash_{\mathsf{CPC}}$, then, defining
$a^{\prime\mathcal{A}}:=a\to^{\mathcal{A}}0^{\mathcal{A}}$, we have that
$(A,0^{\mathcal{A}},1^{\mathcal{A}},\land^{\mathcal{A}},\lor^{\mathcal{A}},^{\prime\mathcal{A}})$
is a Boolean algebra.

###### Proof.

Suppose $\mathcal{A}$ is an algebraic interpretation consistent with
$\vdash_{\mathsf{IPC}}$. So $\leq^{\mathcal{A}}$ defined by
$a\leq^{\mathcal{A}}b\Leftrightarrow a\land^{\mathcal{A}}b=a$ is a partial
order. In particular:

.[(i)] $a=b\;$ iff $\>a\leq^{\mathcal{A}}b$ and $b\leq^{\mathcal{A}}a$.

Now, to show that $\mathcal{A}$ is a Heyting algebra, we have to check that
each of the equations defining (the variety of) Heyting algebras is valid in
$\mathcal{A}$. But this is completely straightforward. Indeed, we have:

.[(ii)] For each defining equation $s=t$ of Heyting algebras there is a
valuation $v$ and formulas $\varphi,\psi$ such that $\overline{v}(\varphi)=s$,
$\overline{v}(\psi)=t$, and $\varphi\vdash_{\mathsf{IPC}}\psi$ and
$\psi\vdash_{\mathsf{IPC}}\varphi$.161616$\mathcal{A}$ is a Heyting algebra
iff
$(A,0^{\mathcal{A}},1^{\mathcal{A}},\land^{\mathcal{A}},\lor^{\mathcal{A}})$
is a bounded lattice and in addition the following equations are valid
(omitting superscripts):  $a\to a=1$ $a\land(a\to b)=a\land b$ $(a\to b)\land
b=b$ $\;a\to(b\land c)=(a\to b)\land(a\to c)$ To be more accurate, we should
have distinguished in (ii) between the syntactic equation $s=t$ in which $s,t$
are _terms_ , and the corresponding equality in $\mathcal{A}$, but we trust
our abuse of notation here is not a problem.

It then follows, from (i) and consistency with $\vdash_{\mathsf{IPC}}$, that
$\mathcal{A}$ is a Heyting algebra. As an example, let us check the defining
equation

.[(iii)] $a\land^{\mathcal{A}}(a\to^{\mathcal{A}}b)=a\land^{\mathcal{A}}b$

Let $v(p)=a$, $v(q)=b$, $\varphi=p\land(p\to q)$, and $\psi=p\land q$. Since
we have that $p\land(p\to q)\vdash_{\mathsf{IPC}}p\land q$, $p\land
q\vdash_{\mathsf{IPC}}p\land(p\to q)$, and $\overline{v}$ is a homomorphism,
the claim follows. As the example shows, we are merely translating familiar
laws of $\mathsf{IPC}$ into (in)equalities in $\mathcal{A}$, which are valid
by the consistency requirement.

Finally, suppose $\mathcal{A}$ is consistent with $\vdash_{\mathsf{CPC}}$. The
defining equations of Heyting algebras are still valid. It only remains to
show (dropping superscripts) that $a\land a^{\prime}=0$ and $a\lor
a^{\prime}=1$. The first is a consequence of (iii) and the fact that $a\land
0=0$. The second identity is the Law of Excluded Middle. $\Box$

###### Remark 3.4

Just as for possible worlds semantics, to enforce that all algebraic
interpretations consistent with $\vdash_{\mathsf{IPC}}$ are standard
(Heyting), it is not enough to require that all $\mathsf{IPC}$-_theorems_ are
valid. The proof of Theorem 3.3 doesn’t work if we cannot conclude from
$\psi\vdash_{\mathsf{IPC}}\varphi$ that (for all $v$)
$[\\![\psi]\\!]^{\mathcal{A}}_{v}\leq^{\mathcal{A}}[\\![\varphi]\\!]^{\mathcal{A}}_{v}$.
In fact, the following counter-example can be found in BH19.

If $(H,j)$ is a nuclear algebra (see just before Definition 2.2), BH19 defines
the algebra $D(H,j)$ of the same signature to be just like $(H,j)$, except
that $a\to^{j}b=_{\text{def}}a\to jb$. Algebras of this form are called
_Dummett algebras_ in BH19.171717Dummett algebras have an interesting
connection to a proposal in [6] to explain the significance of Beth semantics
in terms of a distinction between a formula being _verified_ and _assertible_
at a stage $x$ (BH19, end of Sect. 3.2).  They need not be Heyting algebras —
Bezhanishvili and Holliday give a simple example — but they of course qualify
as algebraic interpretations. However, BH19 also proves that the formulas
valid in all Dummett algebras are _exactly_ the theorems of $\mathsf{IPC}$
(their Theorem 3.25). Thus, by Theorem 3.3, non-Heyting Dummett algebras are
not consistent with $\vdash_{\mathsf{IPC}}$.

##  4 Discussion

We find it rather remarkable that $\mathsf{IPC}$ is Carnap categorical. Many
scholars think that the intuitionistic meaning of the connectives is best
captured by the informal Brouwer-Heyting-Kolmogorov explanation, and that the
various formal semantics with respect to which $\mathsf{IPC}$ is sound and
complete fail in various degrees to do justice to that explanation. For
example, the BHK explanation of the meaning of $\to$ uses notions like ‘proof’
and ‘construction’: a proof of $\varphi\to\psi$ is a construction that takes
any proof of $\varphi$ to a proof of $\psi$. Nuclear semantics involves no
similar notions. Nor does it rely on facts about verification or assertion,
although one can argue quite convincingly, as BH19 does building on Dummett
and others, that some instances of nuclear semantics _represent_ such facts
quite accurately.

###  4.1 Carnap’s question and the meaning of the connectives

However, Carnap’s question, as we construe it here, is a model-theoretic
question. If you will, it is about the _extension_ of the meaning of the
connectives. And then, relative to certain set-theoretic objects taken to be
_semantic values_ of sentences (the ‘extensional part’ of sentence meanings),
there is nothing more to say about those extensions than how they determine
the semantic value of a complex sentence from the semantic values of its
(immediate) constituents. In possible worlds semantics for intuitionistic
logic, the values are certain upward closed subsets of some poset, and the
connectives must be interpreted as functions on those values. And what we find
remarkable is that in every nuclear semantics (as well as topological
semantics), however the nucleus $j$ selects appropriate semantic values, the
consequence relation $\vdash_{\mathsf{IPC}}$ _uniquely fixes_ , among all the
in principle available options, the functions interpreting the connectives on
those values.

Similarly, though less surprisingly, for algebraic semantics. Facing the
extensive literature on algebraic semantics for intuitionistic logic, someone
might naively ask: Why Heyting algebras? Aren’t there other possible algebraic
interpretations? Or, in the classical case: Why Boolean algebras? The answer
you are most likely to get will be in terms of facts about completeness. But
such facts don’t determine unique classes of algebras. $\mathsf{IPC}$ is sound
and complete for the class $\mathcal{H}$ of all Heyting algebras, _and_ the
class of all finite Heyting algebras, _and_ the singleton class of the locale
corresponding to the Euclidean topology on the real line, to take just a few
examples. Similarly for $\mathsf{CPC}$ and Boolean algebras. The answer to the
naive question given by Theorem 3.3, on the other hand, is straightforward: if
you want your algebra to be consistent with $\vdash_{\mathsf{IPC}}$
($\vdash_{\mathsf{CPC}}$), it has to be Heyting (Boolean).

One might object that $\mathcal{H}$ is the _largest_ class with respect to
which $\mathsf{IPC}$ is sound and complete, and in that sense fixed by
$\mathsf{IPC}$. Yes, but Theorem 3.3 shows that completeness is not the issue:
$\mathcal{H}$ is the largest class with respect to which $\mathsf{IPC}$ is
_sound_ , if soundness is taken to be consistency with
$\vdash_{\mathsf{IPC}}$. Completeness is an additional, presumably deeper
fact, but irrelevant to Carnap’s question. Indeed, going beyond propositional
logic, there are logics which are _not_ complete but still Carnap categorical:
the meaning of the logical constants is still fixed by the standard
consequence relation — a case in point is the logic
$\mathcal{L}(\mathcal{Q}_{0})$, which is classical first-order logic with the
additional quantifier ‘there are infinitely many’.181818This was observed by
the second author, and is stated and generalized in [16]. The set of valid
sentences in $\mathcal{L}(\mathcal{Q}_{0})$ is not recursively enumerable.

###  4.2 Other logics, other settings

Here are some final thoughts and open questions.

1. We have considered Carnap’s problem for $\mathsf{IPC}$, but the same question could be asked for related logics. Not intermediate logics — propositional logics between $\mathsf{IPC}$ and $\mathsf{CPC}$ — their categoricity follows from that of $\mathsf{IPC}$. But one could look at weaker logics. An interesting question brought up by Wesley Holliday (_p.c._) concerns the role of implication. Note that in our proof of Theorem 2.9, showing that $\lor$ is standard required some facts about the interpretation of $\to$ to be established first. What if we drop implication from the language, and consider $\vdash_{\mathsf{IPC}}$ restricted to the language with $\\{\neg,\land,\lor\\}$? (We need $\neg$ as a primitive since it can no longer be defined in terms of $\to$ and $\bot$.) In a natural deduction system for $\mathsf{IPC}$ (that takes $\neg$ as primitive), this logic, say $\mathsf{IPC}^{*}$, is axiomatized by simply dropping the introduction and elimination rules for $\to$.191919As Wesley Holliday pointed out, this follows since with the remaining rules one can prove that the Lindenbaum-Tarski algebra is a pseudocomplemented distributive lattice, and [15] proved that $\mathsf{IPC}^{*}$ is the logic of pseudocomplemented distributive lattices.  In view of the remarks just made, it would be natural to ask Carnap’s question for $\vdash_{\mathsf{IPC}^{*}}$.

[9] studies an even weaker logic in the $\\{\neg,\land,\lor\\}$-language,
$\vdash_{\mathsf{F}}$, which has restrictions on the $\lor$E and $\neg$I
rules.202020He presents it with a Fitch style natural deduction system, where
the added constraint becomes a requirement on the Reiteration rule.
$\vdash_{\mathsf{F}}$ is also extended to a first-order language with the
quantifiers $\forall$ and $\exists$ (but without $\to$ and $=$).  Among other
things, distributivity no longer holds:
$\varphi\land(\psi\lor\theta)\not\vdash_{\mathsf{F}}(\varphi\land\psi)\lor(\varphi\land\theta)$.212121Failure
of distributivity is a characteristic of quantum logic, but Holliday argues
that it also accords with certain facts about natural language semantics, in
particular facts about epistemic modals.  He shows how $\vdash_{\mathsf{F}}$
can be seen as a neutral base logic, from which intuitionistic logic, and
versions of the _orthologic_ studied in [8], and classical logic, can be
obtained by suitable additions or changes to the rules, or by corresponding
constraints in the algebraic or the relational semantics he provides for
$\vdash_{\mathsf{F}}$. So already Carnap’s question for $\vdash_{\mathsf{F}}$
makes a lot of sense.

Similarly, one could consider the $\\{\neg,\land,\to\\}$-fragment of
$\mathsf{IPC}$, or even smaller fragments.

2. A related natural question is if there is a proper fragment of $\mathsf{IPC}$ in the original $\\{\bot,\land,\lor,\to\\}$-language which is Carnap categorical. Looking at the $\mathsf{IPC}$-consequences needed in the proof of Theorem 2.9, it does seem that all the natural deduction rules, or all the $\mathsf{IPC}$ axioms in a standard Hilbert style axiomatization, are indeed used, but that is of course not a proof. If no such proper fragment exists, that would be a kind of functional completeness property of $\mathsf{IPC}$.

3. Can Theorem 2.9 be generalized to arbitrary intuitionistic interpretations as specified in Definition 2.1? This concerns in particular the function $I^{\mathcal{F},\mathit{at}}$ which (as Denis Bonnay pointed out to us) could be seen as the interpretation of an invisible logical constant preceding all atoms. Does categoricity extend to that constant? A more precise question: if $I^{\mathcal{F}}$ is consistent with $\vdash_{\mathsf{IPC}}$, under what circumstances would $I^{\mathcal{F},\mathit{at}}$ have to be a nucleus?

4. We end with another set of questions, not related specifically to intuitionistic logic but the general setting in which Carnap’s question has been posed. We have so far simply followed the lead of [3] and other papers in considering consequence relations $\vdash$ where the first argument is a (possibly empty) _set_ of formulas and the second is a _formula_ ; the set-fmla setting in Humberstone’s terminology. One could look at other settings, like fmla (no premises), set-set, fmla-fmla, or seq-fmla (with a sequence of premises). As we have seen, the categoricity results would differ significantly. We think set-fmla most naturally corresponds to intuitive ideas about ‘what follows from what’, but one would like a better argument for why the others are less suitable. Or, less contentiously, an overview of what the results would be in those settings.222222Note that the solution proposed in [5] to the existence of non-normal interpretations was to use the set-set framework instead.

In this context, here is final more concrete issue. In all categoricity
results (in our sense) that we are aware of, it is practically immediate that
any interpretation consistent with the relevant consequence relation $\vdash$
must interpret conjunction ($\land$) standardly. It is the other logical
constants that need some work (except for $\bot$ if _Ex Falso_ holds). But one
could argue that this is built into our definition of consistency with
$\vdash$ in Definition 2.1:4: it is the _intersection_ of the values of the
premises that must be included in the value of the conclusion. This guarantees
that $U\cap V\subseteq I(\land)(U,V)$; the converse inclusion is just from
single-premise $\land$-elimination.

This choice should at least be motivated. Is it necessary? One approach could
be to see what happens in the fmla-fmla setting: does it too force $\land$ to
be standard? The answer seems to be No in a general possible worlds
environment; at least if interpretations now have the form
$\mathcal{F}=(X,\mathcal{C},\subseteq)$, where $\mathcal{C}$ is any subset of
$\mathcal{P}(X)$, and semantic values are required to stay in $\mathcal{C}$.
It is easy to find such $\mathcal{C}$ such that $I^{\mathcal{F}}$ is ‘fmla-
fmla-consistent’ with $\vdash$ — in the sense that if $\psi\vdash\varphi$ then
for all valuations $v$,
$[\\![\psi]\\!]^{I^{\mathcal{F}}}_{v}\subseteq[\\![\varphi]\\!]^{I^{\mathcal{F}}}_{v}$
— but $I^{\mathcal{F}}(\land)$ is _not_ intersection. On the other hand, if
$\mathcal{C}$ is required to be closed under intersections, then
$I^{\mathcal{F}}(\land)$ will be intersection.

We feel these issues need more thought, but leave them for future work.

### Acknowledgements

We thank Valentin Goranko and Lloyd Humberstone for helpful comments at a
(much) earlier stage of this work, and Johan van Benthem, Denis Bonnay, and
Wesley Holliday for careful and constructive remarks on the present paper.
Special thanks to Wes for allowing us to present his Example 2.12.

## References

  * [1] Guram Bezhanishvili and Wesley H. Holliday  “Locales, nuclei, and Dragalin frames”  In _Advances in Modal Logic, vol. 11_ London: College Publications, 2016, pp. 177–196
  * [2] Guram Bezhanishvili and Wesley H. Holliday  “A semantic hierarchy for intuitionistic logic”  In _Indagationes Mathematicae_ 30.3, 2019, pp. 403–469
  * [3] Denis Bonnay and Dag Westerståhl  “Compositionality solves Carnap’s Problem”  In _Erkenntnis_ 81.4, 2016, pp. 721–739
  * [4] Denis Bonnay and Dag Westerståhl  “Carnap’s Problem for modal logic (online version)”  In _Review of Symbolic Logic_ , 2021
  * [5] Rudolf Carnap  “ _Formalization of Logic_ ”  In _vol. 2 of Studies in Semantics_ Cambridge, Mass.: Cambridge University Press, 1943
  * [6] Michael Dummett  “Elements of Intuitionism, 2nd ed.”  Oxford: Clarendon Press, 2000
  * [7] Gilda Ferreira and Paulo Oliva  “On various negative translations”  In _Logic, Construction, Computation_ De Gruyter, 2012
  * [8] Robert Goldblatt  “Semantic analysis of orthologic”  In _Journal of Philosophical Logic_ 3.1, 1974, pp. 19–35
  * [9] Wesley H. Holliday  “A fundamental non-classical logic”, arXiv, 2022  URL: https://arxiv.org/abs/2207.06993
  * [10] Lloyd Humberstone  “The Connectives”  Cambridge MA: MIT Press, 2011
  * [11] J. Murzi and O. Hjortland  “Inferentialism and the categoricity problem: Reply to Raatikainen”  In _Analysis_ 69(3), 2009, pp. 480–488
  * [12] Julien Murzi and Brett Topey  “Categoricity by convention”  In _Philosophical Studies_ 178.10, 2021, pp. 3391–3420
  * [13] Eric Pacuit  “Neighborhood Semantics for Modal Logic”  Springer, 2017
  * [14] Panu Raatikainen  “On the rules of inference and the meaning of logical constants”  In _Analysis_ 68(4), 2008, pp. 282–287
  * [15] Jordi Rebagliato and Ventura Verdú  “On the algebraization of some Gentzen systems”  In _Fundamenta Informaticae_ 18.2–4, 1993, pp. 319–338
  * [16] Sebastian Speitel  “Logical Constants between Inference and Reference”, 2020
  * [17] M. Stone  “Topological representation of distributive lattices and Brouwerian logics”  In _$\check{C}\\!$ asopis pro p$\check{e}\\!$stování matematiky a fysiky_ 67.1, 1937, pp. 1–25
  * [18] Alfred Tarski  “Der Aussagenkalkül und die Topologie”  In _Fundamenta Mathematicae_ 31.1, 1938, pp. 103–134. English tr. in [tarski56]pp. 421–454
  * [19] Johan van Benthem  “Correspondence theory”  In _Handbook of Philosophical Logic, vol. III, 2nd edition_ Dordrecht: Springer, 2001, pp. 326–408