# Curry-Howard-Lambek Correspondence for Intuitionistic Belief

Cosimo Perini Brogi

► To cite this version:

Cosimo Perini Brogi. Curry-Howard-Lambek Correspondence for Intuitionistic Belief. Studia Logica, 2021, 109 (6), pp.1441 - 1461. 10.1007/s11225-021-09952-3. hal-04599500

HAL Id: hal-04599500

https://hal.science/hal-04599500v1

Submitted on 1 Jul 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Curry–Howard–Lambek
Correspondence for
Intuitionistic Belief

**Abstract.** This paper introduces a *natural deduction calculus for intuitionistic logic of belief IEL<sup>-</sup>* which is easily turned into a *modal λ-calculus giving a computational semantics for deductions in IEL<sup>-</sup>. By using that interpretation, it is also proved that IEL<sup>-</sup> has *good proof-theoretic properties*. The correspondence between deductions and typed terms is then extended to a *categorical semantics* for identity of proofs in IEL<sup>-</sup> showing the general structure of such a modality for belief in an intuitionistic framework.

**Keywords:** Intuitionistic modal logic, Epistemic logic, Categorical proof theory, Modal type theory, Proofs-as-programs.

**Introduction**

Brouwer–Heyting–Kolmogorov (BHK) interpretation is based on a semantic reading of propositional variables as problems (or tasks), and of logical connectives as operations on *proofs*. In this way, it provides a semantics of mathematical statements in which the computational aspects of proving and refuting are highlighted.<fnref n="1" />

In spite of being named after L.E.J. Brouwer, this approach is rather away from the deeply philosophical attitude at the origin of intuitionism: In BHK interpretation, reasoning intuitionistically is similar to a safe mode of program execution which always terminates; on the contrary, according to the founders of intuitionism, at the basis of the mathematical activity there is a continuous mental process of construction of objects starting with the flow of time underlying the chain of natural numbers, and intuitionistic reasoning is what structures that process.<fnref n="2" />

<footnote n="1">¹The reader is referred to [16] for an introduction.</footnote>

<footnote n="2">²For instance, Dummett’s [6] advocates a purely philosophical justification of the whole current of intuitionistic mathematics.</footnote>
This reading of the mathematical activity is formally captured by Kripke semantics for intuitionistic logic [9]: Relational structures based on preorders capture the informal idea of a process of growth of knowledge in time which characterises the mental life of the mathematician.

It is worth-noting that the focuses of these semantics are quite different: BHK interpretation stresses the importance of the concept of proof in the semantics for intuitionistic logic; Kripke's approach highlights the epistemic process behind the provability of a statement.

In [2], Artemov and Protopopescu make use of the BHK interpretation to extend—in a sense—the epistemic realm of constructivism: In BHK interpretation we have an implicit notion of proof whose epistemic aspects are modelled by Kripke structures; the construction of a proof for a specific proposition that we carried out as a cumulative mental process gives us sufficient reason for (at least) believing that proposition. It is then possible to cover also traditional epistemic states of belief and knowledge within such a framework, once we recognise the correct clauses for corresponding modal operators: Proving A assures that A is true; proving □A is weaker, for we may believe in A even though we do not have a direct proof of A itself.

In [2] the starting point is thus a BHK interpretation of epistemic statements in which knowledge and belief are considered as (different) results of a process of verification. The general idea is that a proof of a (mathematical) statement is a most strict type of verification, and that verifying a statement is a sufficient condition for *believing* it. At the same time, *knowing* that a statement is true means, according to this intuitionistic reading, that this very statement cannot be false, since we have a verification of it.

Hence, the proposed intuitionistic account of epistemic states validates a principle of “constructivity of truth”

$$A \to \Box A$$

and of “intuitionistic factivity of knowledge”

$$\Box A \to \neg\neg A.$$

The latter principle appears particularly promising for applying this formal framework in a broader realm than mathematics: In [2] various informal justifications to the proposed account are indeed given, and those authors express the aim of giving new foundations to intuitionistic epistemology.

It appears clear, in any case, that both principles are validated by contemporary mathematical practice: When a statement A is proved, then its very proof can be checked by a human being both by ‘pencil and paper’ and by computer proof-assistants, so that the whole mathematical community
can believe/know that what has been given is a proof of A indeed. Also, intuitionistic factivity of knowledge states that whenever we know that A is true in a (constructive, but maybe) not specified sense—e.g. we do not have direct access to its proof—then A cannot be false, if we agree that knowledge is at least consistent belief. Again, this is common in general mathematical practice, when a theorem is known to hold even by those who cannot develop a proof of it by themselves.

In short, it seems that the BHK computational reading of the epistemic operator $\square$ provides a finer analysis of truth and of epistemic states from the constructive point of view.

In spite of this, the mentioned paper [2] covers only axiomatic calculi and Kripke semantics for intuitionistic epistemic logics, so that the stimulating question of considering the computational aspects of epistemic states remained informal and at a very beginning stage.

The present paper, on the contrary, is committed to giving a precise, formal analysis of the computational content of intuitionistic belief.

In order to establish some clear facts, a **natural deduction** system $IEL^-)$ for the intuitionistic logic of belief is developed and designed with the intent of translating it into a functional calculus of $IEL^-)$-deductions. In a sense, we define a formal counterpart of Artemov and Protopopescu's reading of the epistemic operator for belief by extending the Curry-Howard correspondence between intuitionistic natural deduction NJ and simple type theory, to a **modal $\lambda$-calculus** in which the modal connective on propositions behaves according to a single (term-)introduction rule.

Furthermore, we establish **normalization** for $IEL^-$ along with other **proof-theoretic properties**, and, in spite of its simple grammar, we show that there is a surprisingly rich **categorical structure** behind the calculus: Our $\lambda$-system for $IEL^-$-deductions is sound and complete w.r.t. the class of bi-cartesian closed categories equipped with a monoidal pointed endofunctor whose point is monoidal.

Therefore, by adopting the proofs-as-programs paradigm to give a precise meaning to the motto "belief-as-verification" we succeed in:

* Designing a natural deduction calculus $IEL^-$ for intuitionistic belief which is well-behaved from a proof-theoretic point of view;

* Proving that this calculus corresponds to a modal typed system in which every term has a unique normal form, and the epistemic modality acquires a precise functional interpretation;
◦ Developing a categorical semantics for intuitionistic belief which focuses on identity of proofs, and not simply on provability.

The paper is then organised as follows: In Section 1, the axiomatic calculus $IEL^-$ and its relational semantics are recalled. In Section 2, we introduce the natural deduction system $IEL^-$ and prove—syntactically—that it is logically equivalent to $IEL^-$. Then we investigate some of its proof-theoretic properties: We start by proving that detours can be eliminated from deductions by defining a $\lambda$-calculus with a modal operator which captures in a very natural way the behaviour of the epistemic modality on propositions; then we prove a canonicity lemma for this calculus of proof-terms, from which we derive syntactic proofs of the weak and standard disjunction property. Finally, in Section 3, we give a categorical semantics for $IEL^-$-deduction: After recalling the main lines of Curry-Howard-Lambek correspondence, we prove that deductions define—up to normalization—specific categorical structures which subsume Heyting algebras with operators and, at the same time, provide a proof-theoretic semantics for intuitionistic belief.

By means of these results we can also see that some claims in [2] concerning a type-theoretic reading of the epistemic operator as the truncation of types are not correct. The belief modality there defined is ‘weaker’ than $inh : Type \to Type$ because of its type-theoretic—hence syntactic—behaviour, validated also from a categorical—hence semantic—point of view: Types truncation equips bi-cartesian closed categories with an idempotent monad, while we show that the belief operator we are considering is a more general functor.<fnref n="3" />

# 1. Axiomatic Calculus for Intuitionistic Belief

Let's start by recalling the syntax and relational semantics for the logic of intuitionistic belief as introduced in [2].

## 1.1. System $IEL^-$

DEFINITION 1.1.1. $IEL^-$ is the axiomatic calculus given by:

• Axiom schemes for intuitionistic propositional logic;

• Axiom scheme $K : \Box(A \to B) \to \Box A \to \Box B$;

• Axiom scheme of co-reflection $A \to \Box A$;

<footnote n="3">³In fact even when thought of as a modal connective of our base language, the epistemic $\Box$ is not an idempotent operator.</footnote>
• Modus Pones $\frac{A \rightarrow B}{B}$ as the only inference rule.

We write $\Gamma \vdash_{\mathrm{IEL}^{-}} A$ when $A$ is derivable in $\mathrm{IEL}^{-}$ assuming the set of hypotheses $\Gamma$, and we write $\mathrm{IEL}^{-} \vdash A$ when $\Gamma = \emptyset$.

We immediately have

**PROPOSITION 1.1.2.** *The following properties hold:*

(i) *Necessitation rule* $\frac{A}{\Box A}$ is derivable in $\mathrm{IEL}^{-}$;

(ii) *The deduction theorem holds in IEL*⁻;

(iii) IEL⁻ is a normal intuitionistic modal system.

**PROOF.** See [2]. ■

<figure><img src="image_2.png" /></figure>

As stated before, this system axiomatizes the idea of belief as the result of verification within a framework in which truth corresponds to provability, accordingly to the Brouwer-Heyting-Kolmogorov interpretation of intuitionistic logic.<fnref n="4" /> Note also that, in this perspective, the co-reflection scheme is valid, while its converse does not hold: If A is true, then it has a proof, hence it is verified; but A can be verified without disclosing a specific proof, therefore the standard epistemic scheme $\Box A \rightarrow A$ is not valid under this interpretation.<fnref n="5" />

**1.2. Kripke Semantics for IEL**⁻

Turning to relational semantics, in [2] the following class of Kripke models is given.

**DEFINITION 1.2.1.** A model for $\mathrm{IEL}^{-}$ is a quadruple $\langle W, \leq, v, E \rangle$ where

• $\langle W, \leq, v \rangle$ is a standard model for intuitionistic propositional logic;

• $E$ is a binary ‘knowledge’ relation on $W$ such that:

· if $x \leq y$, then $xEy$; and

· if $x \leq y$ and $yEz$, then $xEz$; graphically we have

<figure><img src="image_3.png" /></figure>

<footnote n="4">⁴See e.g. [18].</footnote>

<footnote n="5">⁵See Williamson's system in [20] for an intuitionistic epistemic logic in which the standard epistemic principle is valid; however it is worth noting that this specific logic is not based on the BHK-semantics.</footnote>
• *v* extends to a forcing relation $\models$ such that

• $x \models \Box A$ iff $y \models A$ for all $y$ such that $xEy$.

A formula $A$ is true in a model iff it is forced by each world of that model; we write $\mathbb{I}EL^- \models A$ iff $A$ is true in each model for $\mathbb{I}EL^-$.

Note that this semantics assumes Kripke's original interpretation of intuitionistic reasoning as a growing knowledge—or discovery process—for an epistemic agent in which the relation $E$ defines an audit of ‘cognitively’ $\le$-accessible states in which the agent can commit a verification.

This semantics is adequate to the calculus:

**THEOREM 1.2.2.** *The following hold:*

(Soundness) If $\mathbb{I}EL^- \vdash A$, then $\mathbb{I}EL^- \models A$.

(Completeness) If $\mathbb{I}EL^- \models A$, then $\mathbb{I}EL^- \vdash A$.

**PROOF.** Soundness is proved by induction on the derivation of $A$.

Completeness is proved by a standard construction of a canonical model.

See [2] for the details.

<figure><img src="image_4.png" /></figure>

## 2. Natural Deduction for Intuitionistic Belief

We want to develop a semantics of proofs for the logic of intuitionistic belief. In order to do that, we now introduce a natural deduction system which is logically equivalent to $\mathbb{I}EL^-$, but which is also capable of a computational reading of the epistemic operator and of proofs involving this kind of modality.

Accordingly, the starting point is proving that the calculus $\mathbb{I}EL^-$ of natural deduction is sound and complete w.r.t. $\mathbb{I}EL^-$; then, we prove that proofs in $\mathbb{I}EL^-$ can be named by means of $\lambda$-terms as stated in the proofs-as-programs paradigm for intuitionistic logic also known as Curry-Howard correspondence. By using this formalism, we prove a normalization theorem for $\mathbb{I}EL^-$ stating that detours can be eliminated from all deductions. Afterwards, we present some results about the proof-theoretic behaviour of $\mathbb{I}EL^-$.

In the next section, we extend such a correspondence to category theory for showing the underlying structure of the operator for intuitionistic belief.
## 2.2. Normalization

In order to eliminate potential detours from IEL$^-$-deduction we introduce the following proof rewritings:

$$ (\iota) \qquad \begin{array}{ccc} \Gamma & & \Gamma \\ & \vdots & \\ \frac{\Box A \quad [A]}{\Box A} & \rightsquigarrow & \vdots \\ & \Box A \end{array} $$

$$ (\delta) \qquad \begin{array}{ccc} \Gamma & [\vec{A}]^1, \vec{C} & \Delta [B, \vec{D}]^2, \vec{E} \\ & \vdots & \vdots \\ \frac{\Box \vec{A} \quad B}{\Box B} & \Box \text{-intro:1} & \Box \vec{D} \quad F \\ & \Box F & \Box \text{-intro:2} \end{array} \rightsquigarrow $$

$$ \begin{array}{ccc} & [\vec{A}]^1, \vec{C} & \\ \Gamma & \Delta & B \\ & \vdots & \\ \frac{\Box \vec{A} \quad \Box \vec{D}}{\Box F} & F & \Box \text{-intro:1} \end{array} $$

Note that $(\iota)$ eliminates a useless application of $\Box$-intro, while $(\delta)$ collapses two $\Box$-intros into a single one.

**REMARK 1.** (Proofs-as-programs). Curry-Howard correspondence permits a functional reading of proofs in NJ, once one recognises the following mapping:

$$ f \equiv A \qquad \longmapsto \quad x_i^A, \qquad \text{where } i \text{ is the parcel of the hypothesis } A $$

$$ f \equiv \frac{f_1 \quad f_2}{A \wedge B} \qquad \longmapsto \quad \langle t^A, s^B \rangle, \qquad \text{where } t^A, s^B \text{ correspond to } f_1 \text{ and } f_2 \text{ resp.} $$

$$ f' \qquad \longmapsto \quad \pi_1.t^{A \times B}, \qquad \text{where } t^{A \times B} \text{ corresponds to } f' $$
Concerning the modality, we see that in the proof-term box
$[\vec{x} : \vec{A}].\vec{t} : \Box A$ in $(s : B) : \Box B$ for the $\Box$-intro rule, a term $s$ of type $B$—with
$\vec{x}$ of type $A_1, \dots, A_n$ among its free variables—is used along with terms $\vec{t}$
of type $\Box A_1, \dots, \Box A_n$ in order to obtain a term of type $\Box B$ not depending
on the variables $\vec{x}$.

Proof rewritings can be then expressed by imposing appropriate reduc-
tions of $\lambda$-terms:

$$
\mathbf{box}[x].t \text{ in } x >_\iota t
$$

$$
\mathbf{box}[x_1, \dots, x_{i-1}, x_i, x_{i+1}, \dots, x_n].(t_1, \dots, t_{i-1}, (\mathbf{box}[\vec{y}].\vec{s} \text{ in } t_i), t_{i+1}, \dots, t_n) \text{ in } r
$$

$$
>_{\delta} \mathbf{box}[x_1, \dots, x_{i-1}, \vec{y}, x_{i+1}, \dots, x_n].(t_1, \dots, t_{i-1}, \vec{s}, t_{i+1}, \dots, t_n) \text{ in } r[t_i/x_i]
$$

Assuming this reading of deductions as programs, normalization now be-
comes just the execution of a program written in our modal λ-calculus; it
assures then consistency of IEL⁻, being also useful to prove its analyticity,
and hence its decidability. Accordingly, the quest for normalizing natural
deduction systems is not limited to the proofs-as-programs paradigm, and
its origins are actually at the very core of proof theory: We refer the reader
to [12] and [19] for the technical and historical aspects of the research field,
respectively.

We write $\triangleright$ for the transitive closure of the relation obtained by combin-
ing $>_{\iota}$ and $>_{\delta}$, together with standard rewritings of $\lambda$-calculus as presented
in Remark 1. An algebra of $\lambda$-terms is then obtained by considering the re-
flexive, symmetric, transitive closure $\triangleq^-$ of $\triangleright$, i.e. by combining the reflexive,
symmetric, transitive closure $\stackrel{\iota}{=}^-$ and $\stackrel{\delta}{=}^-$ of $>_{\iota}$ and $>_{\delta}$, respectively, along with
standard rewriting rules for typed $\lambda$-calculus.⁶

We can now prove that every deduction in IEL⁻ can be uniquely reduced
to a proof containing no detours.

THEOREM 2.2.1. *Strong normalization holds for IEL<sup>-</sup>.*

PROOF. We define a translation$^7 |-|$ from the $\lambda$-calculus of IEL$^-$-deductions to typed $\lambda$-calculus with products, sums, empty and unit types:

<footnote>$^6$Note that $\stackrel{\iota}{=}^-$ is just a special case of $\stackrel{\delta}{=}^-$ . We decide to adopt this redundant system of rewriting since $\stackrel{\iota}{=}^-$ has a straightforward interpretation in category theory: See Section 3.2.</footnote>

<footnote>$^7$This function is introduced in [8] to prove detour-elimination for the implicational fragment of basic intuitionistic modal logic IK by reducing the problem to normalization of simple type theory. Here we adopt the mapping to consider also product, co-product, empty, and unit types, keeping the original strategy due to [4]. A different proof based on Tait’s computability method [15] should also be possible and is under development by the author.</footnote>
$$
\begin{align*}
|0| &::= 0 \\
|1| &::= 1 \\
|p| &::= p \\
|A \to B| &::= |A| \to |B| \\
|A \times B| &::= |A| \times |B| \\
|A + B| &::= |A| + |B| \\
|\Box A| &::= (|A| \to q) \to q \\
|x| &::= x \\
|c| &::= c \\
|E(t)| &::= E(|t|) \\
|U(t)| &::= U(|t|) \\
|\lambda x t| &::= \lambda x .|t| \\
|ts| &::= |t||s| \\
|(t, s)| &::= (|t|, |s|) \\
|\pi_i(t)| &::= \pi_i(|t|) \\
|C(t, x.t_1, y.t_2)| &::= C(|t|, x.|t_1|, y.|t_2|) \\
|\mathrm{in}_i(t)| &::= \mathrm{in}_i(|t|) \\
|\mathrm{box}[x_1, \dots, x_n].(t_1, \dots, t_n) \mathrm{in} s| &::= \lambda k .|t_1|(\lambda x_1.\dots|t_n|(\lambda x_n.k|s|)\dots)
\end{align*}
$$

where *q* is specific atom type. Then it is easy to see that $\sqsubseteq$ is preserved by this mapping: If $t \triangleright t'$ in one step, then $|t| \gg |t'|$, where $\gg$ indicates the usual relation made of $\beta\eta$-reductions with permutations. Therefore, since typed $\lambda$-calculus with products, sums, empty and unit types is strongly normalizing,<fnref n="8" /> so is our modal $\lambda$-calculus, and $IEL^-$ also. In other terms: If $IEL^-$ was not normalizing, then we would have an infinite $\triangleright$-reduction starting from, say, $t: A$. By the previous note, this would lead to an infinite $\gg$-reduction starting from $|t|:|A|$, contradicting strong normalization of typed $\lambda$-calculus with $\times, +, 1, 0$. ■

**LEMMA 2.2.2.** *The modal $\lambda$-calculus of $IEL^-$-deductions has the Church-Rosser property.*

**PROOF.** It is straightforward to prove weak Church-Rosser property for our calculus. By Theorem 2.2.1, the modal $\lambda$-calculus of $IEL^-$-deductions has the Church-Rosser property.<fnref n="9" /> ■

<footnote n="8">⁸See [7] and [1].</footnote>

<footnote n="9">⁹A proof of Newman’s result relating strong normalization and Church-Rosser property is given in [14, Prop. 3.6.2].</footnote>
**COROLLARY 2.2.3.** Every IEL$^-$-deduction reduces uniquely to a deduction without detours.

**PROOF.** By Theorem 2.2.1 and Lemma 2.2.2, any term of the modal $\lambda$-calculus of IEL$^-$-deductions has a unique normal form. ■

**2.3. Further Proof-Theoretic Properties**

Knowing that IEL$^-$-deductions normalise, it is possible to investigate further on the relevant aspects of our system from the perspective of proof theory.

Following [7], we will say that a deduction (or, equivalently, a proof-term) is **neutral**, iff it is a hypothesis, or its last rule is an elimination rule (E-rule, for short).

We immediately have the following

**LEMMA 2.3.1.** In any normal and neutral deduction $\Gamma \vdash_{IEL^-} C$, $\Gamma \neq \emptyset$.

**PROOF.** Straightforward induction on the height of the deduction. ■

By the previous lemma we can easily prove canonicity of proof-terms:

**LEMMA 2.3.2.** (Canonicity). If IEL$^-$ $\vdash$ A is normal, then the last rule of the deduction is the appropriate introduction rule.

**PROOF.** By Lemma 2.3.1, since $\Gamma = \emptyset$ here, and the deduction is normal, its last rule cannot be an E-rule. ■

It is now straightforward to apply the canonicity lemma in order to obtain the following results:

**COROLLARY 2.3.3.** (Disjunction Property). If IEL$^-$ $\vdash$ $A \lor B$, then IEL$^-$ $\vdash$ A or IEL$^-$ $\vdash$ B.

**COROLLARY 2.3.4.** Reflection rule is admissible in IEL$^-$: If IEL$^-$ $\vdash$ $\Box A$, then IEL$^-$ $\vdash$ A.

**COROLLARY 2.3.5.** (Weak Disjunction Property). If IEL$^-$ $\vdash$ $\Box(A \lor B)$, then IEL$^-$ $\vdash$ $\Box A$ or IEL$^-$ $\vdash$ $\Box B$.

Another interesting question is whether IEL$^-$ satisfies the subformula property.<fnref n="10" /> In the present paper, we are mainly focused on the computational aspects of the intuitionistic modality for belief, and that property would be relevant to these aims only for it implies the decidability of the calculus. We

<footnote n="10">¹⁰We are extremely grateful to an anonymous reviewer for pointing to this aspect of the structural behaviour of the system.</footnote>
have already developed the main lines of a general proof for the property, and obtained some preliminary results for answering positively the question (modulo minor tweaks); however, proving that the principle holds indeed for IEL⁻ involve checking many minor details, which make the intermediate proofs quite long. We prefer then to discuss the status of this principle in another work (in preparation) focused on the structural properties of our system.

### 3. Categorical Semantics for Intuitionistic Belief

If λ-calculus gives a computational semantics of proofs in NJ—and, as we showed in the previous section, in IEL⁻ also—category theory furnishes the tools for an ‘algebraic’ semantics which is *proof relevant*—i.e. contrary to traditional algebraic semantics based on Heyting algebras and to relational semantics based on Kripke models, it focuses on the very notion of proof, distinguishing between different deductions of the same formula.

In this perspective, the correspondence between proofs and programs is extended to consider arrows in categories which have enough structure to capture the behaviour of logical operators. The so-called Curry-Howard-Lambek correspondence can be then summarized by the following table

<table><thead><tr><th>Logic</th><th>Type theory</th><th>Category theory</th></tr></thead><tbody><tr><td>Proposition</td><td>Type</td><td>Object</td></tr><tr><td>Proof</td><td>Term</td><td>Arrow</td></tr><tr><td>Theorem</td><td>Inhabitant</td><td>Element-arrow</td></tr><tr><td>Conjunction</td><td>Product type</td><td>Product</td></tr><tr><td>True</td><td>Unit type</td><td>Terminal object</td></tr><tr><td>Implication</td><td>Function type</td><td>Exponential</td></tr><tr><td>Disjunction</td><td>Sum type</td><td>Coproduct</td></tr><tr><td>False</td><td>Empty type</td><td>Initial object</td></tr></tbody></table>

Here we see that cartesian product models conjunction, and exponential models implication. Any category having products and exponentials for any of its objects is called **cartesian closed (CCCat)**; moreover, if it has also coproducts—modelling disjunction—it is called **bi-cartesian closed (bi-CCCat)**: ⊤ and ⊥ correspond to empty product – the terminal object 1 – and empty coproduct – the initial object 0—respectively. The reader is referred to the classic [10] for the details of such completeness result.

For our calculus, in order to capture the behaviour of the epistemic modality, some more structure is required: In the following subsections some basic
definitions are recalled and then used to provide IEL⁻ with an adequate categorical semantics.

**3.1. Monoidal Functors, Pointed Functors, and Monoidal Natural Transformations**

**DEFINITION 3.1.1.** Given a CCCat $\mathcal{C}$, a **monoidal** endofunctor consists of a functor $\mathfrak{F} : \mathcal{C} \to \mathcal{C}$ together with

* a natural transformation

$$m_{A,B} : \mathfrak{F}A \times \mathfrak{F}B \to \mathfrak{F}(A \times B);$$

* a morphism

$$m_1 : 1 \to \mathfrak{F}1,$$

preserving the monoidal structure of $\mathcal{C}$.<fnref n="11" />

These are called **structure morphisms** of $\mathfrak{F}$.

It is quite easy to see that a monoidal endofunctor on the category of logical formulas induces a modal operator satisfying K-scheme, as proved in [5].

**DEFINITION 3.1.2.** Given any category $\mathcal{C}$, an endofunctor $\mathfrak{F} : \mathcal{C} \to \mathcal{C}$ is **pointed** iff there exists a natural transformation

$$\pi : \mathrm{Id}_\mathcal{C} \Rightarrow \mathfrak{F} \\ \pi_A : A \to \mathfrak{F}A$$

$$\begin{tikzcd}
A \arrow[r, "\pi_A"] & \mathfrak{F}A \\
f \arrow[u] \arrow[r, "\pi_B"] & \mathfrak{F}B
\end{tikzcd}$$

$\pi$ is called the **point** of $\mathfrak{F}$.

In the present setting, a pointed endofunctor on the category of logical formulas ‘represents’ the co-reflection scheme.

Since we want to give a semantics of proofs—and not simply of derivability—in IEL⁻, we need a further notion from category theory.

<footnote n="11">¹¹See [11] for the corresponding commuting diagrams and the definition of monoidal category.</footnote>
**DEFINITION 3.1.3.** Given a monoidal category $\mathcal{C}$, and monoidal endofunctors $\mathfrak{F}, \mathfrak{G} : \mathcal{C} \to \mathcal{C}$, a natural transformation $\kappa : \mathfrak{F} \Rightarrow \mathfrak{G}$ is **monoidal** when the following commute:

$$ \begin{tikzcd} \mathfrak{F}A \times \mathfrak{F}B \arrow[r, "m_{A,B}^\mathfrak{F}"] \arrow[d, "\kappa_A \times \kappa_B"] & \mathfrak{F}(A \times B) \arrow[d, "\kappa_A \times B"] \\ \mathfrak{G}A \times \mathfrak{G}B \arrow[r, "m_{A,B}^\mathfrak{G}"] & \mathfrak{G}(A \times B) \arrow[d, "\kappa_A \times B"] \end{tikzcd} $$

and

$$ \begin{tikzcd} 1 \arrow[r, "m_1^{\mathfrak{F}}"] & \mathfrak{F}(1) \arrow[d, "\kappa_1"] \\ \parallel \arrow[r, "m_1^{\mathfrak{G}}"] & \mathfrak{G}(1) \arrow[d, "\kappa_1"] \\ 1 \arrow[r, "m_1^{\mathfrak{G}}"] & \mathfrak{G}(1) \end{tikzcd} $$

## 3.2. Categorical Completeness

Finally, we introduce the models by which we want to capture $\text{IEL}^-$.

**DEFINITION 3.2.1.** An $\text{IEL}^-$-category is given by a bi-CCCat $\mathcal{C}$ together with a monoidal pointed endofunctor $\mathcal{R}$ whose point $\kappa$ is monoidal.

Now we can check adequacy of these models.

**THEOREM 3.2.2.** (Soundness). Let $\mathcal{C}$ be an $\text{IEL}^-$-category. Then there is a canonical interpretation $\llbracket - \rrbracket$ of $\text{IEL}^-$ in $\mathcal{C}$ such that

* a formula $A$ is mapped to a $\mathcal{C}$-object $\llbracket A \rrbracket$;

* a deduction $t$ of $A_1, \dots, A_n \vdash_{\text{IEL}^-} B$ is mapped to an arrow $\llbracket t \rrbracket : \llbracket A_1 \rrbracket \times \dots \times \llbracket A_n \rrbracket \to \llbracket B \rrbracket$;

* for any two deductions $t$ and $s$ which are equal modulo $\square$, we have $\llbracket t \rrbracket = \llbracket s \rrbracket$.

**PROOF.** By structural induction on $f : \mathcal{A} \vdash_{\text{IEL}^-} B$. The intuitionistic cases are interpreted according to the remarks about bi-CCCats at the beginning of this section. We overload the notation using $\langle \Box, m, \kappa \rangle$ for the monoidal pointed endofunctor of $\mathcal{C}$, its structure morphisms, and its point.

The deduction

$$ \frac{f_1 : \Gamma_1 \vdash \Box A_1 \quad \dots \quad f_n : \Gamma_n \vdash \Box A_n \quad \dots \quad g : [A_1, \dots, A_n], C_1, \dots, C_m \vdash B}{\Box B} $$
is mapped to

$$ (\Box[\mathfrak{g}]) \circ m_{[[A_1]], \dots, [[A_n]], [[C_1]], \dots, [[C_m]]} \circ [f_1] \times \dots \times [f_n] \times \kappa_{[[C_1]]} \times \dots \times \kappa_{[[C_m]]}, $$

where $m_{X_1, \dots, X_n}$ is defined inductively as

$$ m_{X_1, \dots, X_{n-1}, X_n} := m_{X_1 \times \dots \times X_{n-1}, X_n} \circ (m_{X_1, \dots, X_{n-1}}) \times \mathrm{id}_{\Box X_n}. $$

It is straightforward to check that $\stackrel{\wedge}{\delta}$ holds in the category $\mathcal{C}$ by functoriaity of $\Box$.

The relation $\stackrel{\wedge}{\delta}$ is also valid by naturality of $m$ and $\kappa$: The reader is invited to check that $\kappa$ must be monoidal in order to model correctly the following special case<fnref n="12" />

$$ \begin{array}{ccc} \begin{array}{c} \Gamma_1 \\ \vdots \\ \frac{A_1}{\Box A_1} \end{array} & \begin{array}{c} \Gamma_n \\ \vdots \\ \frac{A_n}{\Box A_n} \end{array} & \begin{array}{c} [A_1, \dots, A_n]^1, C_1, \dots, C_m \\ \vdots \\ B \end{array} \\ \begin{array}{c} \Box B \\ \vdots \\ A_1 \end{array} & \begin{array}{c} \Gamma_1 \\ \vdots \\ \Box B \end{array} & \begin{array}{c} \Gamma_n \\ \vdots \\ C_1, \dots, C_m \end{array} \end{array} \stackrel{\wedge}{\delta} \begin{array}{c} \Box A_1 \\ \vdots \\ A_1 \end{array} \quad \begin{array}{c} \Box B \\ \vdots \\ B \end{array} \end{array} \quad \begin{array}{c} \Box \end{array} $$

It remains to show that this interpretation is also complete.

**THEOREM 3.2.3. (Completeness).** If the interpretation of two IEL$^-$-deductions is equal in all IEL$^-$-categories, then the two deductions are equal modulo $\Box$.

**PROOF.** We proceed by constructing a term model for the modal $\lambda$-calculus for IEL$^-$-deductions. Consider the following category $\mathcal{M}$:

* its objects are formulae;

* an arrow $f: A \to B$ is an IEL$^-$-deduction of $B$ from $A$ modulo $\Box$;

* identities are given by assuming a hypothesis;

<footnote n="12">¹²Everything reduces to long categorical calculations.</footnote>
• composition is given by transitivity of deductions.

Then $\mathcal{M}$ has a bi-cartesian closed structure given by the properties of conjunction, implication, and disjunction in NJ.

Moreover, the modal operator $\Box$ induces a functor $\mathfrak{K}$ by mapping $A$ to $\Box A$, and

<figure><img src="image_5.png" /></figure>

which preserves identities by $\overset{\text{i}}{\simeq}$, and preserves composition as a special case of $\overset{\text{d}}{\simeq}$.

The structure morphism is given by

<figure><img src="image_6.png" /></figure>

whose properties follow as a special case of $\overset{\text{d}}{\simeq}$.

The point is given by $\frac{A}{\Box A}$ and its characteristic property is given as a special case of $\overset{\text{d}}{\simeq}$. Finally, such a point is monoidal by $\overset{\text{d}}{\simeq}$ up to $\wedge$-detours.

Then if an equation between interpreted $\mathbf{IEL}^{-}$-deductions holds in all $\mathbf{IEL}^{-}$-categories, then it holds also in $\mathcal{M}$, so that those deductions are equal w.r.t. $\overset{\Box}{\simeq}$.

■

**REMARK 2.** (Belief and truncation). In [3], truncation—there called “bracket types”—is defined in a first order calculus with types, and showed to behave like a monad. Similarly, in [13], ($n$-)truncation is defined as a monadic idempotent modality within the framework of homotopy type theory.

We have just seen that despite the truncation does eliminate all computational significance to an inhabitant of a type—turning then a *proof of a proposition into a simple verification of that statement*—the belief modality defined in [2] *does not* correspond to that operator on types.

Actually, after considering the potential applications of $\mathbf{IEL}^{(-)}$ prospected by Artemov and Protopopescu outside the realm of mathematical statements, that should be not surprising at all: The categorical semantics of $\mathbf{IEL}^{-}$-deductions subsumes the interpretation of truncation as an idempotent monad, since such a functor is just a special case of monoidal pointed endofunctor with monoidal point.
It might be interesting thus to consider the relationship between truncation and the belief modality from a purely syntactic perspective, by comparing the structural properties of a potential simple type theory with bracket types and our modal λ-calculus for intuitionistic belief.<fnref n="13" />

Conclusion

Our original intent has been to make precise the computational significance of the motto “belief-as-verification” which leads in [2] to the introduction of epistemic modalities in the framework of BHK interpretation. In particular, despite some claims contained in that paper, we were not sure how to relate the belief operator with type truncation.

In the present paper, we have addressed these questions and have developed a ‘proof-theoretically tractable’ system for intuitionistic belief that can be easily turned into a modal λ-calculus, showing that the epistemic operator behaves differently from truncation.

Moreover, by extending some results concerning categorical semantics for the basic intuitionistic modal logic IK in [5] and [8], we developed a proof-theoretic semantics for intuitionistic belief based on monoidal pointed endofunctors with monoidal points on bi-CCCats. Even from this ‘categorical’ perspective, the modal operator differs from type-theoretic truncation, so that the reading of belief as the result of verification seems to be just a heuristic interpretation of that specific modality.

Having established so, some general questions naturally arise:

* How could be the original motivation of co-reflection scheme $A \to \Box A$— i.e. the interpretation of $\Box$ as a verification operator on propositions— correctly captured, from a computational point of view, by intuitionistic logic of belief?

* Does the possible extension IEL of IEL⁻ obtained by adding the elimination rule $\frac{\Gamma \vdash \Box A}{\Gamma \vdash \neg\neg A}$ recover the intuitionistic reading of epistemic states as results of verification in a formal way—i.e. as type-theoretic truncation?

<footnote n="13">¹³As stated before, truncation has been considered only in a first-order context—i.e. working within dependent types. It should be possible, however, to define truncation for simple types by imposing further reductions to terms of the system mimicking the rules involving (intensional) equality in bracketed types.</footnote>
In our opinion, these problems are strongly related: In fact, it seems plausible that the additional elimination rule provides **IEL** with an adjunction between □ and ¬¬ which has still to be checked and deserves a fine grained analysis and comparison with type truncation.

Moreover, it might be interesting to consider similar modalities in different settings, including first order logic and linear logics.

**Acknowledgements.** These results were obtained during my first year of PhD studies at DiMa of University of Genoa. After discussing a preliminary version of categorical semantics for intuitionistic belief during the Logic and Philosophy of Science Seminar of University of Florence in May 2019, I had the great opportunity to present more refined results during the poster session of The Proof Society Summer School in September 2019: My gratitude goes to all logicians of the Computational Foundry of Swansea University who hosted the event, along with the invited lecturers and the participants. In particular, I wish to thank Reuben Rowe for an enlightening discussion on the way to Rhossili about the behaviour of the □ in my formal system. A sincere acknowledgement goes to an anonymous reviewer for suggesting further investigations on the proof theory of the calculus I originally presented to this journal: Her/His comments have been very important for structuring the final version of this work.

**Funding** Open access funding provided by Università degli Studi di Genova within the CRUI-CARE Agreement.

**Open Access.** This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article's Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article's Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.

**Publisher's Note** Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

**References**

[1] AKAMA, Y., On Mints' reduction for ccc-calculus, in *International Conference on Typed Lambda Calculi and Applications*, Springer, 1993, pp. 1-12.
[2] ARTEMOV, S., and T. PROTOPOPESCU, Intuitionistic epistemic logic, *The Review of Symbolic Logic* 9(2):266–298, 2016.

[3] AWODEY, S., and A. BAUER, Propositions as [types], *Journal of Logic and Computation* 14(4):447–471, 2004

[4] DE GROOTE, P., On the strong normalisation of intuitionistic natural deduction with permutation-conversions, *Information and Computation* 178(2):441–464, 2002.

[5] DE PAIVA, V., and E. RITTER, Basic constructive modality, in J.-Y. Beziau, and M. E. Coniglio, (eds.), *Logic without Frontiers: Festschrift for Walter Alexandre Carnielli on the occasion of his 60th Birthday*, College Publications, 2011, pp. 411–428.

[6] DUMMETT, M., *Elements of intuitionism*, Oxford University Press, 2000.

[7] GIRARD, J.-Y., P. TAYLOR, and Y. LAFONT, *Proofs and types*, Cambridge University Press, 1989.

[8] KAKUTANI, Y., Calculi for intuitionistic normal modal logic, arXiv preprint arXiv:1606.03180, 2016.

[9] KRIPKE, S. A., Semantical analysis of intuitionistic logic i, in *Studies in Logic and the Foundations of Mathematics*, vol. 40, Elsevier, 1965, pp. 92–130.

[10] LAMBEK, J., and P. J. SCOTT, *Introduction to higher-order categorical logic*, vol. 7, Cambridge University Press, 1988.

[11] MAC LANE, S., *Categories for the working mathematician*, vol. 5, Springer Science & Business Media, 2013.

[12] NEGREI, S., J. VON PLATO, and A. RANTA, *Structural proof theory*, Cambridge University Press, 2008.

[13] RIJKE, E., M. SHULMAN, and B. SPITTERS, Modalities in homotopy type theory, arXiv preprint arXiv:1706.07526, 2017.

[14] SØRENSEN, M. H., and P. URZYCZYN, *Lectures on the Curry-Howard isomorphism*, vol. 149 of *Studies in Logic and the Foundations of Mathematics*, Elsevier, 2006.

[15] TAIT, W. W., Intensional interpretations of functionals of finite type i, *The Journal of Symbolic Logic* 32(2):198–212, 1967.

[16] TROELSTRA, A., *Principles of Intuitionism*, Springer, 1969.

[17] VAN DALEN, D., *Logic and Structure*, 4th edn., Springer, 2008.

[18] VAN DALEN, D., and A. TROELSTRA, *Constructivism in Mathematics. An Introduction I*, vol. 121 of *Studies in Logic and the Foundations of Mathematics*, Elsevier, 1988.

[19] VON PLATO, J., The development of proof theory, in Edward N. Zalta, (ed.), *The Stanford Encyclopedia of Philosophy*, winter 2018 edn., Metaphysics Research Lab, Stanford University, 2018.

[20] WILLIAMSON, T., On intuitionistic modal epistemic logic, *Journal of Philosophical Logic* 21(1):63–89, 1992.
C. PERINI BROGI
Department of Mathematics
University of Genoa
Via Dodecanneso 35
16146 Genova
Italy
perinibrogi@dima.unige.it