An intuitionistic set-theoretical model of fully dependent CC$^{\boldsymbol\omega}$

Abstract

Werner’s set-theoretical model is one of the simplest models of CIC. It combines a functional view of predicative universes with a collapsed view of the impredicative sort “ ${\tt Prop}$ ”. However, this model of ${\tt Prop}$ is so coarse that the principle of excluded middle $P \lor \neg P$ holds. Following our previous work, we interpret ${\tt Prop}$ into a topological space (a special case of Heyting algebra) to make the model more intuitionistic without sacrificing simplicity. We improve on that work by providing a full interpretation of dependent product types, using Alexandroff spaces. We also extend our approach to inductive types by adding support for ${\mathsf{list}}$ s.

1. Introduction

There are various models of type theory. Werner’s set-theoretical model (Werner 1997) provides an intuitive model of CIC. It combines a functional view of predicative universes with a collapsed view of the impredicative sort ${\tt Prop}$ . However, this model of ${\tt Prop}$ is so coarse that the principle of excluded middle $P \lor \neg P$ holds in it.

In this paper, we construct a set-theoretical model of CC $^\omega$ in which the principle of excluded middle does not hold, making it closer to completeness.

CC (the Calculus of Constructions, Coquand and Huet 1988) is a pure type system (Barendregt 1991) with two sorts, impredicative ${\ast}$ and predicative $\Box$ . CC $^\omega$ replaces $\Box$ by a cumulative hierarchy of predicative sorts ${\tt Type}_i$ . CIC (the Calculus of Inductive Constructions) adds inductive types to CC $^\omega$ .

Werner (1997) provided a remarkably simple model of CIC. In this model, $\lambda x\,:\,A.t$ is interpreted by a set-theoretical function for predicative sorts. Yet such a simple approach is known to fail for impredicative sorts as it runs afoul of Reynolds’ paradox (Reynolds 1984). Therefore, the model for ${\tt Prop}$ is two-valued. Hence, the principle of excluded middle is valid in this model, making it classical. Later, Miquel and Werner (2003) have shown that proving the soundness of this model was not as easy as it seems, but this does not change the simplicity of the model itself. This simple approach is to be contrasted with Luo’s model of ECC (CC $^\omega$ extended with strong sums $\Sigma x : A.B$ ) which uses $\omega$ -sets (Luo 1991), syntactic models based on combinatory logic (Geuvers 2001; Stefanova and Geuvers 1995), or more recent models such as categorical models (Jacobs 2001; Streicher 1991) or models based on homotopy theory (Univalent Foundations Program 2013). This is the drawback of simplicity: while Werner’s approach avoids many complications of more precise models, it is at times counter-intuitive, as it completely ignores the intuitionistic aspect of CC $^\omega$ .

Our goal has been to recover the intuitionistic part of CC $^\omega$ without increasing the complexity of the model. Barras (2010) provided a first way to do it, by interpreting CC $^\omega$ in IZF (intuitionistic Zermelo–Fraenkel set theory, Aczel and Rathjen 2010) rather than ZF. While this is an interesting result, and the fact it is backed by a fully formalized proof is very impressive, this requires one to work in the radically different world of IZF, where it is difficult to express meta-reasoning about the expressiveness of the language. For this reason, we prefer to stay inside classical set theory ZF, but we change the interpretation of ${\tt Prop}$ to be some topological space. The open sets of a topological space form a Heyting algebra. Heyting algebras are used when constructing models of intuitionistic logic, but usually their elements are not understood as sets. In our model, proofs shall be interpreted as elements of denotations of propositions, hence these denotations must be sets, and the order must be set inclusion. Using topological spaces solves this problem.

This leaves the question of how to interpret proofs, in a way that makes the whole interpretation coherent. In our previous work (Sato and Garrigue 2016), propositions were already interpreted as open sets, but proofs were interpreted by a fixed value, that had to be included in all true propositions. This choice was too inflexible to accomodate propositions parameterized over proofs, which we had to reject. While this type of parameterization is rare, it is for instance required to express proof-irrelevance as a proposition. In this paper, we are able to lift this restriction by shifting the interpretation to Alexandroff spaces (Arenas 1999), and making the interpretation of proofs a function of the context valuation. Alexandroff spaces act as parameters to the model, their choice making it more or less precise. For instance, if we use the trivial topological space $(X, \mathcal{O}(X))$ where $X = \{\cdot\}$ is a singleton and $\mathcal{O}(X)=\{\varnothing, X\}$ , we obtain a model of classical logic, which is the coarsest one.

Our model is still proof irrelevant, as it does not depend on the the proof term itself. As a result, this model does validate some propositions that are not provable, in particular logical proof irrelevance, hence it does not reach completeness. However, this is sufficient to exclude many classical propositions such as the principle of excluded middle $P \lor \neg P$ or the linearity axiom $(P \rightarrow Q) \lor (Q \rightarrow P)$ .

Note that, in this paper, we choose a slightly restricted version of CC $^\omega$ , which omits subsumption between universes ${\tt Prop}$ and ${\tt Type}_i$ . Subsumption between the predicative universes ${\tt Type}_i$ poses no problem, but our model of propositions is too different to allow subsumption between ${\tt Prop}$ and ${\tt Type}_i$ . Werner (2008) omitted this same subsumption in his exploration of proof irrelevance.

This model can also be extended to inductive types. To demonstrate it, we define a model of ${\mathsf{list}}$ s, with principles for recursion (in ${\tt Type}_0$ ) and induction (in ${\tt Prop}$ ), and extend our soundness proof to those. This is one more step in the direction of a model for the full CIC.

In Section 2, we define the language of the type system CC^ω. In Section 3, we give our set-theoretical interpretation of CC^ω and prove its soundness. In Section 4, we study some properties of this model. For instance, we show that it satisfies proof irrelevance, and that the excluded middle cannot be derived from the linearity axiom in CC^ω. In Section 5, we extend our interpretation to inductive types. Finally, we conclude and discuss some future directions.

2. Typing of CC^ω

2.1 Definition of CC^ω

We define the type system CC^ω as follows. The only deviation from the standard presentation is that our version has no subsumption between ${\tt Prop}$ and ${\tt Type}_i$ .

Definition 1 (Term). Let V be an infinite set of variables.

• • For all $x \in V$ , x is a term with free variables $\operatorname{fv}(x)=\{x\}$ .

• • If $t_1$ and $t_2$ are terms, then $t_1 \; t_2$ is a term with free variables $\operatorname{fv}(t_1) \cup \operatorname{fv}(t_2)$ .

• • If t and T are terms, and $x \in V$ then, $\lambda x : T. t$ is a term with free variables $\operatorname{fv}(T) \cup (\!\operatorname{fv}(t) \setminus \{x\})$ .

• • If $T_1$ and $T_2$ are terms, and $x \in V$ then $\forall x : T_1. T_2$ is a term with free variables $\operatorname{fv}(T_1) \cup (\!\operatorname{fv}(T_2) \setminus \{x\})$ .

• • The symbols ${\tt Prop}$ and ${\tt Type}_i$ (for $i = 0,1,2,...$ ) are terms with free variables $\varnothing$ .

• • ${\tt Prop}$ and ${\tt Type}_i$ are called sorts. ${\tt Prop}$ is called the impredicative sort and it represents the type of all propositions.

Definition 2 (Context)

• • [] is a context with domain $\operatorname{dom}([]) = \varnothing$ .

• • If $\Gamma$ is a context, and T is a term and $x \in V\setminus \operatorname{dom}(\Gamma)$ , then $\Gamma ;\; (x : T)$ is a context with domain $\operatorname{dom}(\Gamma)\cup\{x\}$ .

Figure 1 contains the typing rules of CC^ω. The metavariables $s, s_1, s_2$ denote sorts. In rule (PI-Type), either $s_1 = s_2$ or one of them is ${\tt Prop}$ . The equality $=_{\beta}$ denotes beta equality and $B[x \backslash v]$ denotes substitution. Here are their definitions. We assume that $\alpha$ -conversion occurs when needed.

Figure 1. Typing rules of CC^ω.

Definition 3 (Substitution). Let t and v be terms and x be a variable. The substitution $t[x \backslash v]$ , which means v replaces x in t, is defined inductively as follows:

1. (i) If y is a variable, then $y[x \backslash v] = \begin{cases}v & (y=x) \\ y & (otherwise),\end{cases}$

2. (ii) $(t_1 t_2)[x \backslash v] = (t_1[x \backslash v]) (t_2[x \backslash v])$ ,

3. (iii) $(\lambda x' : T.t')[x \backslash v] = \lambda x' : (T[x \backslash v]). t'[x \backslash v]$

   when $x'\notin\operatorname{fv}(v)\cup\{x\}$ ,

4. (iv) $(\forall x' : T_1 . T_2)[x \backslash v] = \forall x' : (T_1[x \backslash v]) . (T_2[x \backslash v])$

   when $x'\notin\operatorname{fv}(v)\cup\{x\}$ ,

5. (v) $s[x \backslash v] = s$ where s is a sort.

Definition 4 (Beta Equality). Let $=_{\beta}$ be the smallest equivalence relation such that the following conditions hold.

1. (i) $(\lambda x : A. t) \; a =_{\beta} t[x \backslash a]$ .

2. (ii) If $t_1 =_{\beta} t_1'$ and $t_2 =_{\beta} t_2'$ , then $t_1 t_2 =_{\beta} t_1' t_2'$ .

3. (iii) If $t =_{\beta} t'$ and $A =_{\beta} A'$ , then $\lambda x : A. t =_{\beta} \lambda x : A' t'$ .

4. (iv) If $A =_{\beta} A'$ and $B =_{\beta} B'$ , then $\forall x : A. B =_{\beta} \forall x : A' B'$ .

Now that we have defined ’s terms and typing rules, we show the following three lemmas that will be used in proofs. They can be proved by induction over the typing rules above.

Lemma 5 (Uniqueness of Typing) If $\Gamma \vdash t : A$ and $\Gamma \vdash t : B$ are derivable, then either $A =_{\beta} B$ , or $A =_\beta \forall x_1:A_1,\dots,\forall x_n:A_n,{\tt Type}_i$ and $B =_\beta \forall x_1:A_1,\dots,\forall x_n:A_n,{\tt Type}_j$ .

Lemma 6 (Substitution) If $\Gamma \vdash u : U$ and $\Gamma ;\; (x : U) ;\; \Delta \vdash t : T$ are derivable then $\Gamma ;\; \Delta[x \backslash u] \vdash t[x \backslash u] : T[x \backslash u]$ is also derivable.

Lemma 7 (Extended Weakening) If $\Gamma_1 ;\; \Gamma_2 \vdash t : T$ is derivable, then $\Gamma_1 ;\; \Delta ;\; \Gamma_2 \vdash t : T$ is also derivable when $\Gamma_1 ;\; \Delta ;\; \Gamma_2$ is well-formed, i.e. when $\Gamma_1 ;\; \Delta ;\; \Gamma_2 \vdash {\tt Type}_i : {\tt Type}_{i+1}$ is derivable.

Lemma 8 (Condensing Lemma) If $\Gamma ;\; (x : A) ;\; \Delta \vdash t : T$ is derivable and x does not occurs in $\Delta$ , t and T, then $\Gamma ;\; \Delta \vdash t : T$ is derivable.

Proof. See Jiménez (1999).

2.2 Propositional terms and proof terms

In CC^ω, propositions are types that belong to the impredicative sort ${\tt Prop}$ , and proofs are terms of types that represent propositions. Next, we give a definition of propositions and proofs through syntactic derivability. Rather than introducing an explicitly sorted type system like in Miquel and Werner (2003), we will prove that these definitions are stable under substitution, weakening, and reduction, so that we can safely use them when defining our interpretation.

Definition 9.

1. (1) Propositional Term

   A term P is called a propositional term for $\Gamma$ iff $\Gamma \vdash P : {\tt Prop}$ is derivable.

2. (2) Proof Term

   A term p is called a proof term for $\Gamma$ iff $\Gamma \vdash p : P$ is derivable for some P that is a propositional term for $\Gamma$ . P is then called a provable propositional term for $\Gamma$ .

Lemma 10 (Proof and propositional terms)

1. (i) We assume that $P_1$ and $P_2$ are well typed under the same context $\Gamma$ . If $P_1$ is a propositional term for $\Gamma$ and $P_1 =_\beta P_2$ , then $P_2$ is also a propositional term for $\Gamma$ .

2. (ii) We assume that $p_1$ and $p_2$ are well typed under the same context $\Gamma$ . If $p_1$ is a proof term for $\Gamma$ and $p_1 =_\beta p_2$ , then $p_2$ is also a proof term for $\Gamma$ .

3. (iii) We assume that $\Gamma \vdash u : \forall x : A.B$ and $\Gamma \vdash v : A$ are derivable. If u is a proof term for $\Gamma$ , then $u \; v$ is also a proof term for $\Gamma$ .

4. (iv) If t is a proof term for $\Gamma ;\; (x : A)$ and $\lambda x : A.t$ is well typed under $\Gamma$ , then $\lambda x : A.t$ is also a proof term for $\Gamma$ .

5. (v) If t is a proof term for $\Gamma$ , then there does not exist a term T such that $\Gamma \vdash t : T$ and $\Gamma \vdash T : {\tt Type}_i$ are both derivable.

Proof terms and propositional terms are preserved under substitution. The following lemmas express this fact.

Lemma 11. If $\Gamma \vdash t : T$ is derivable, then $\Gamma \vdash T : s$ for some sort s.

Lemma 12. We assume that $\Gamma \vdash u : U$ is derivable and p is well typed under $\Gamma ;\; (x : U) ;\; \Delta$ .

1. (i) If p is a proof (resp. propositional) term for the context $\Gamma ;\; (x : U) ;\; \Delta$ , then $p[x \backslash u]$ is a proof (resp. propositional) term for the context $\Gamma; \Delta[x \backslash u]$ .

2. (ii) If p is not a proof term for the context $\Gamma ;\; (x : U) ;\; \Delta$ , then $p[x \backslash u]$ is not a proof term for the context $\Gamma ;\; \Delta[x \backslash u]$ .

Proof. (i) is clear by Lemma 6 We will show (ii). Since p is well typed, there exists a type T such that

\[ \Gamma ;\; (x : U) ;\; \Delta \vdash p : T \]

and by Lemma 11 there exists a sort s such that

\[ \Gamma ;\; (x : U) ;\; \Delta \vdash T : s \]

Since p is not a proof term for the context $\Gamma ;\; (x : U) ;\; \Delta$ , we have that $s \neq {\tt Prop}$ , and as a result there exists an index i such that $s = {\tt Type}_i$ . Hence by Lemma 6,

\begin{eqnarray*} \Gamma ;\; \Delta[x \backslash u] &\vdash& p[x \backslash u] : T[x \backslash u] \\ \Gamma ;\; \Delta[x \backslash u] &\vdash& T[x \backslash u] : {\tt Type}_i \end{eqnarray*}

hold. If there exists a term P such that

\begin{eqnarray*} \Gamma ;\; \Delta[x \backslash u] &\vdash& p[x \backslash u] : P \\ \Gamma ;\; \Delta[x \backslash u] &\vdash& P : {\tt Prop}, \end{eqnarray*}

it implies a contradiction by Lemma 10 (v).

Note that the fact that P is not a propositional term for $\Gamma ;\; (x : U) ;\; \Delta$ does not imply that $P[x \backslash u]$ is not a propositional term for $\Gamma ;\; \Delta[x \backslash u]$ in general. Here is a counterexample.

\begin{eqnarray*} \Gamma ;\; (U : {\tt Type}_i) ;\; ( P : U ) &\vdash& P : U \\ \Gamma &\vdash& {\tt Prop} : {\tt Type}_i\end{eqnarray*}

In this case, P is not a propositional term. However $P[U \backslash {\tt Prop}] = P$ is a propositional term under $\Gamma ;\; (P : {\tt Prop})$ .

Lemma 13. We assume that p is well typed under $\Gamma_1 ;\; \Gamma_2$ and $\Gamma_1 ;\; \Delta ;\; \Gamma_2$ . p is a proof (resp. propositional) term for the context $\Gamma_1 ;\; \Gamma_2$ if and only if p is a proof (resp. propositional) term for the context $\Gamma_1; \Delta;\; \Gamma_2$ .

The function $\textbf{PT}_{\Gamma,x}(A,B)$ maps two types A and B into the string symbols $\{\mathsf{PP}, \mathsf{TP}, \mathsf{PT}, \mathsf{TT}\}$ according to their sorts. Its goal is to give different interpretations to $\forall x : A.B$ .

Definition 14 (Product Type) We assume that $\Gamma \vdash A : s_1$ and $\Gamma ;\; (x : A) \vdash B : s_2$ are derivable where $s_1$ , $s_2$ are sorts. We define:

\begin{equation*} \textbf{PT}_{\Gamma,x}(A,B) := \begin{cases} \mathsf{PP} & (s_1, s_2) = ({\tt Prop}, {\tt Prop}) \\ \mathsf{TP} & (s_1, s_2) = ({\tt Type}_i, {\tt Prop}) \\ \mathsf{PT} & (s_1, s_2) = ({\tt Prop}, {\tt Type}_i) \\ \mathsf{TT} & (s_1, s_2) = ({\tt Type}_i, {\tt Type}_j) \end{cases} \end{equation*}

Again, $\textbf{PT}_{\Gamma,x}(A,B)$ is stable under substitution and weakening.

Lemma 15.

1. (i) If A and B are typable under $\Gamma;\; (x : U) ;\; \Delta$ and $\Gamma \vdash u : U$ is derivable, then $\textbf{PT}_{(\Gamma; (x : U) ;\; \Delta),a}(A,B) = \textbf{PT}_{(\Gamma; \Delta[x \backslash u]),a}(A[x \backslash u],B[x \backslash u])$ holds.

2. (ii) If A and B are typable under $\Gamma_1 ;\; \Gamma_2$ and $\Gamma_1;\; \Delta ;\; \Gamma_2$ , then $\textbf{PT}_{(\Gamma_1 ;\; \Delta ;\; \Gamma_2),a}(A,B) = \textbf{PT}_{(\Gamma_1 ;\; \Gamma_2),a}(A,B)$ holds.

Proof.

1. (i) When $\textbf{PT}_{\Gamma; (x : U) ;\; \Delta,a}(A,B) = \mathsf{PP}$ , A is a proposition for $(\Gamma ;\; (x : U) ;\; \Delta)$ and B is a proposition for $(\Gamma ;\; (x : U) ;\; \Delta ;\; (a : A))$ . By Lemma 12, $A[x \backslash u]$ is a proposition for $(\Gamma ;\; \Delta[x \backslash u])$ and $B[x \backslash u]$ is also a proposition for $(\Gamma ;\; \Delta[x \backslash u] ;\; (a : A[x \backslash u]))$ . Hence, the statement holds in this case. When $\textbf{PT}_{\Gamma ;\; (x : U) ;\; \Delta,a}(A,B) = \mathsf{TP}$ , $\Gamma ;\; \Delta[x \backslash u] \vdash A[x \backslash u] : {\tt Type}_i$ is derivable. The remaining case is similar.

2. (ii) It is clearly proved by applying the result of (i) in this lemma, since variables in $\Delta$ do not appear in $\Gamma_2$ and terms A and B.

2.3 Logical symbols

Lastly, here are some notations allowing to use other logical symbols (Barendregt 1992). We shall use them to prove the adequacy of our model with respect to intuitionistic logic.

Definition 16.

\begin{align*} A \rightarrow B &:= \forall x : A. B \hspace{8ex} (\text{when } x \notin fv(B)), \\ \bot &:= \forall P : {\tt Prop}. P, \\ \neg A &:= A \rightarrow \bot, \\ A \land B &:= \forall P : {\tt Prop}. (A \rightarrow B \rightarrow P) \rightarrow P, \\ A \lor B &:= \forall P : {\tt Prop}. (A \rightarrow P) \rightarrow (B \rightarrow P) \rightarrow P, \\ \exists x:A.Q &:= \forall P : {\tt Prop}. (\forall x : A. (Q \rightarrow P)) \rightarrow P, \\ A \leftrightarrow B &:= (A \rightarrow B) \land (B \rightarrow A), \\ x =_A y &:= \forall Q : (A \rightarrow {\tt Prop}). Q \; x \rightarrow Q \; y. \end{align*}

3. Interpretation

3.1 Preparation of the interpretation

3.1.1 Heyting algebras

Several interpretations of type theory have been proposed such as using $\omega$ -sets (Luo 1991) or coherent spaces (Girard 1989). In this paper, we use Heyting algebras (MacLane and Moerdijk 1992; van Dalen 1984) for propositions. Heyting algebras provide models of intuitionistic logic. The open sets of a topological space can be given the structure of a Heyting algebra (see Lemma 18), and as such provide models of intuitionistic logic too (van Dalen 1984). We give a definition of lattice and Heyting algebra as follows.

Definition 17 (Lattices and Heyting algebras). Let $(A,\le\!)$ be a partially ordered set (i.e. reflexive, antisymmetric, and transitive). $(A,\le\!)$ is called a Lattice when any two elements a and b of A have a supremum “ $a \sqcup b$ ” and an infimum “ $a \sqcap b,$ ” which are called join and meet. We use the lattice operation symbols join ‘ $\sqcup$ ’ and meet ‘ $\sqcap$ ’ instead of ‘ $\lor$ ’ and ‘ $\land$ ’, since we use the latter as logical symbols. A lattice is also called a complete lattice if every subset S of A has a supremum “ $\bigsqcup S$ ” and an infimun ‘ ’. A complete lattice has a minimum element $\mathbb{O} := \bigsqcup \varnothing$ and a maximum element . If a (complete) lattice has an exponential operator $a^b$ such that

\begin{equation*} x \le z^y \Leftrightarrow x \sqcap y \le z \end{equation*}

holds, then we call it a (complete) Heyting Algebra.

The following lemma shows that topological spaces are both Heyting algebras and complete lattices.

Lemma 18. Any topological space $(X, \mathcal{O}(X))$ is a complete Heyting algebra.

Proof. Let $a \le b$ be $a \subset b$ , and define each operation as follows:

The following lemma states well-known properties of complete Heyting algebras.

Lemma 19. Let $(A,\leq\!)$ be a complete Heyting algebra. Then the following conditions hold.

(1)

(2)

(3)

(4)

(5)

(6)

(7)

(8)

(9)

(10)

3.1.2 Alexandroff spaces

Following in the steps of our previous work (Sato and Garrigue 2016), our interpretation avoids the Reynolds’ Paradox by not looking inside proof terms. In that previous work, this was done by interpreting all proof terms as a single point, the reference point. Soundness then required this reference point to be included in the interpretation of all propositions in the context, which forced us to restrict the type system.

In this paper, a proof term is again interpreted into an element of an open set. However, we make the interpretation of proofs a function of the context, which allows us to overcome this restriction. For soundness to stand, we must then assume that the proof we interpret uses all proofs in the context, which means that its interpretation should be smaller, in some “dependency order,” than their interpretations. For this we need to introduce an order on the elements of our topological space and ensure that there is always an infimum. Alexandroff spaces (Arenas 1999) allow us to define such an order on points, so that we just need to require the existence of the infimum.

Definition 20 (Alexandroff Space). A topological space $(X, \mathcal{O}(X))$ is an Alexandroff space iff the intersection of any tribe of open set is also an open set, i.e.

\begin{equation*} \bigcap S \in \mathcal{O}(X) \quad \textrm{for any}S \subset \mathcal{O}(X) \end{equation*}

The definition of Alexandroff space can also be given by the following equivalent statement.

Lemma 21 (Minimal Neighborhood) A topological space $(X, \mathcal{O}(X))$ is an Alexandroff space iff any point has a minimal neighborhood. The minimal neighborhood of the point x is denoted by $\downarrow x$ .

These are the basic definitions for Alexandroff spaces. However, to prove our soundness theorem later, we need more conditions. We state those as well behaved Alexandroff spaces.

Definition 22 (Well Behaved Alexandroff Space) An Alexandroff space $(X, \mathcal{O}(X))$ is well behaved if the following conditions hold.

• • For any finite subset $\{t_1, t_2, \cdots, t_n\}$ of X, we can choose a point $t \in X$ such that

  \begin{equation*} \downarrow t_1 \; \cap \; \downarrow t_2 \; \cap \cdots \cap \; \downarrow t_n = \; \downarrow t \end{equation*}
  holds. We write such a point t as $\inf\{t_1, t_2, \cdots , t_n\}$ .

• • There exists an element $\bot_X \in X$ such that any inhabited open set contains it, i.e.

  \begin{equation*} \forall O \in \mathcal{O}(X), O\;\textrm{is inhabited} \Rightarrow \bot_X \in O. \end{equation*}

To clarify the use of the notation of the minimal neighborhood $\downarrow x$ and $\bot_X$ , let us discuss a preordered (i.e. reflexivity and transitivity hold) set generated from an Alexandroff space. Let $\leq$ be the relation on X defined as follows.

\begin{equation*} a \leq b \quad \stackrel{\operatorname{def}}{=} \quad \forall O \in \mathcal{O}(X), b \in O \Rightarrow a \in O\end{equation*}

The relation $\leq$ is a preorder. Moreover, if this Alexandroff space is a $T_0$ space (i.e. it fulfills the $T_0$ separation axiom), then the generated preorder $(X, \leq\!)$ becomes an order (the antisymmetry condition holds). If the relation $(X, \leq\!)$ generated from an Alexandroff space forms an ordered set, then the followings hold.

\begin{eqnarray*} \downarrow x &=& \{ t \in X \mid t \leq x\} \\ \bot_X &=& \min X\end{eqnarray*}

Using an ordered Alexandroff space for X allows us to give multiple interpretations of proofs in the typing context, whereas in our previous work (Sato and Garrigue 2016) we used a fixed point $p \in X$ . This fixed point was required to satisfy a point condition, which was no other than the existence of a minimal neighborhood, satisfied by every point in an Alexandroff space.

3.1.3 Dependent function and universes

Definition 23 (Dependent Function). Let A be a set, and B(a) be a set with parameter $a \in A$ . We define the set of dependent functions as follows

\begin{equation*} \prod_{a \in A}B(a) := \left\{f \subset \coprod_{a \in A}B(a) \; | \; \forall a \in A, \exists ! b \in B(a), (a, b) \in f\right\} \end{equation*}

that is the set of functions whose graphs are included in

\begin{equation*} \coprod_{a \in A} B(a) := \{(x,y) \in A \times \bigcup_{a \in A}B(a) \; | \; y \in B(x) \}. \end{equation*}

Next, we introduce Grothendieck universes, which are closed under dependent-function construction, and which we will use to interprete the sort ${\tt Type}_i$ .

Definition 24 (Grothendieck Universe). We define a ith Grothendieck Universe $\mathcal{U}_i$ (for i any natural number) as

\begin{equation*} \mathcal{U}_i := V_{\lambda_i}, \end{equation*}

where a set $V_\alpha$ , with an ordinal number $\alpha$ , is recursively defined as follows

\begin{eqnarray*} V_0 &=& \varnothing, \\ V_{\alpha + 1} &=& \mathcal{P}(V_\alpha), \\ V_\alpha &=& \bigcup_{\beta < \alpha} V_\beta \quad \mbox{(when $\alpha$ is a limit ordinal)}, \end{eqnarray*}

and $\lambda_i$ is the ith inaccessible cardinal.

The class of all universes is well founded for the relation $\in$ . We write $\mathcal{U}_i$ as the ith universe. Note that $\mathcal{U}_i$ is so large that it cannot be constructed in ZFC without assuming an inaccessible cardinal. Our interpretation uses $\mathcal{U}_i$ for all $i \in \textbf{N}$ . The following lemma is necessary when proving soundness.

Lemma 25. The followings hold for any i.

1. (i) $A \in \mathcal{U}_i$ implies $A \subset \mathcal{U}_i$ .

2. (ii) $A \in \mathcal{U}_i$ and $B_\alpha \in \mathcal{U}_i$ for all $\alpha \in A$ imply $\displaystyle\prod_{\alpha \in A}B_\alpha \in \mathcal{U}_i$ .

3. (iii) $x \in \mathcal{U}_i$ and $y \subset x$ imply $y \in \mathcal{U}_i$ .

4. (iv) $\mathcal{U}_i \subset \mathcal{U}_{i+1}$ .

3.2 Interpretation of the judgments

In this model, a type T is interpreted into a set , and a context $x_1 : T_1 ;\; x_2 : T_2 ;\; \cdots ;\; x_n : T_n$ is interpreted into a dependent tuple; in particular, when there are no dependent types in the context, it is a tuple in ${{[\![T_1]\!]}} \times {{[\![T_2]\!]}} \times \cdots \times {{[\![T_n]\!]}} $ .

First, we define the interpretation of application and product types. The interpretation of application depends on whether the argument is a proof term or not, and may be undefined. We shall later prove that every time we use it, we actually have $\mathsf{app}_{\Gamma,v}(f,a) = f(a)$ .

Definition 26.

Now, we define the (partial) interpretations of contexts ${{[\![\hbox{---}]\!]}} $ and judgments ${{[\![\hbox{---} \vdash \hbox{---}]\!]}} $ . The former is by induction on the length of the context and the latter by induction on the structure of terms. Note that the interpretation of judgments does not rely on the interpretation of contexts.

Definition 27 (interpretation). Let $(X, \mathcal{O}(X)) \in \mathcal{U}_0$ be a well-behaved Alexandroff space.

1. (i) Definition of the interpretation of a context ${{[\![\Gamma]\!]}} $

   \begin{eqnarray*} {{[\![[]]\!]}} &:=& \{()\} \\ {{[\![\Gamma ;\; (x:A)]\!]}} &:=& \{(\gamma, \alpha) \mid \gamma \in {{[\![\Gamma]\!]}} \; \textrm{and} \; \alpha \in {{[\![\Gamma \vdash A]\!]}} (\gamma) \} \\ &=& \coprod_{\gamma \in {{[\![\Gamma]\!]}} } {{[\![\Gamma \vdash A]\!]}} (\gamma) \end{eqnarray*}
   where () represents the empty sequence.

2. (ii) Definition of the interpretation of a judgment ${{[\![\Gamma \vdash t]\!]}} $ If t is a proof term for $\Gamma = (x_1 : T_1) ;\; \cdots ;\; (x_n : T_n)$ , then

   \begin{equation*} {{[\![\Gamma \vdash t]\!]}} (\gamma) := \lfloor \gamma \rfloor \end{equation*}
   where
   \begin{equation*} \lfloor \gamma_1, \gamma_2, \cdots, \gamma_n \rfloor := \; \inf \{ \gamma_i \mid x_i \mbox{ is a proof under } \Gamma \}. \end{equation*}
   Otherwise, if $\Gamma \vdash t : T$ is derivable and T is not a proposition for $\Gamma$ , then
   

For simplicity, we write ${{[\![T]\!]}} $ for ${{[\![[]\vdash T]\!]}} ()$ , when the context is empty.

When defined, the interpretation of a context ${{[\![\Gamma]\!]}} $ is a set of sequences $\gamma$ whose length is the length of $\Gamma$ , and ${{[\![\Gamma \vdash t]\!]}} $ is a function whose domain is ${{[\![\Gamma]\!]}} $ , and which returns some set ${{[\![\Gamma \vdash t]\!]}} (\gamma)$ – soundness will tell us that if $\Gamma \vdash t : T$ , then ${{[\![\Gamma \vdash t]\!]}} (\gamma) \in {{[\![\Gamma \vdash T]\!]}} (\gamma)$ .

Concerning Definitions 26 and 27, most cases are similar to Werner’s interpretation, and we explained $\mathsf{app}_{\Gamma,v}$ above, so we only explain the interpretations of proof terms and PI-Types $\forall x : A.B$ .

The interpretation of a proof term ${{[\![\Gamma \vdash p]\!]}} (\gamma)$ is the minimum element of the set of proof values in $\gamma$ . Since each of these values belong to the interpretations of propositions in the context, which are open sets in our Alexandroff space, this minimum element belongs to all of them. This will allow us to prove that any proof variable belongs to the interpretation of its type, which is key to the soundness theorem.

$\mathsf{prod}_\mathsf{X}$ has four cases, according to $\mathsf{X} = \textbf{PT}_{\Gamma,x}(A,B)$ . When $\mathsf{X} = \mathsf{PP}$ , we use the Heyting algebra representation of this implication. If x does not appear in B, the interpretation of ${{[\![\Gamma \vdash \forall x : A.B]\!]}} $ is $\mathcal{B}^\mathcal{A}$ , which represents the logical implication $A \Rightarrow B$ , as will be proved in Corollary 28. If x appears in B, we still have the same meaning, since $\mathcal{B}(\alpha)$ does not depend on $\alpha$ , as will be proved in Lemma 31. This definition also works if $\mathcal{A}$ is empty, as the empty meet is X, and $X^\emptyset$ is X again (the top element of the lattice). In our previous work, $\alpha$ was required to be the (fixed) interpretation of a proof term, meaning that we could not interpret the case where $\mathcal{A}$ was not empty, but did not contain the reference point used for proof terms. Here we do not have such a problem, as the interpretation of proof terms is a function of the context; thanks to the interpretation with well behaved Alexandroff spaces, there is always a value small enough to serve as proof term.

When $\mathsf{X} = \mathsf{TP}$ , the interpretation of ${{[\![\Gamma \vdash \forall x : A.B]\!]}} $ represents universal quantification, and again we use the infinite meet operator of the complete Heyting algebra to express it.

When $\mathsf{X} = \mathsf{PT}$ , the interpretation of ${{[\![\Gamma \vdash \forall x : A.B]\!]}} $ becomes a set theoretical constant function. Functions whose argument are proofs should be constant functions since our model is proof-irrelevant. Note that here again, it follows from Lemma 31 that ${\mathcal B}(\alpha)$ shall not depend on $\alpha$ .

In the last case, when $\mathsf{X} = \mathsf{TT}$ , the representation becomes a set theoretical dependent function.

As soon as one component is $\mathsf{undefined}$ the whole interpretation is $\mathsf{undefined}$ . Thanks to Corollary 28 which is a consequence of the Soundness Theorem 33, $\mathsf{undefined}$ never appears, and implication and application can be defined in a straightforward way.

Corollary 28.

• • If $\Gamma \vdash t$ is well typed, then ${{[\![\Gamma \vdash t]\!]}} $ is a total function whose domain is ${{[\![\Gamma]\!]}} $ .

• • If $\textbf{PT}_{\Gamma,x}(A,B)=\mathsf{PP}$ and ${{[\![\Gamma \vdash A]\!]}} (\gamma) \neq \varnothing$ , then

  \begin{equation*} {{[\![\Gamma \vdash \forall x : A.B]\!]}} (\gamma) = {\biggl({{[\![\Gamma ;\; (x : A) \vdash B]\!]}} (\gamma, \alpha)\biggr)}^{{{[\![\Gamma \vdash A]\!]}} (\gamma)} \end{equation*}
  holds for any $\alpha \in {{[\![\Gamma \vdash A]\!]}} (\gamma)$ .

• • If $\textbf{PT}_{\Gamma,x}(A,B)=\mathsf{PP}$ and ${{[\![\Gamma \vdash A]\!]}} (\gamma) = \varnothing$ , then

  \begin{equation*} {{[\![\Gamma \vdash \forall x : A.B]\!]}} (\gamma) = X \end{equation*}
  holds.

• • If $\Gamma \vdash t_1 \; t_2$ is well typed and $t_1$ is not a proof term for $\Gamma$ , then ${{[\![\Gamma \vdash t_1]\!]}} (\gamma)$ is a function whose domain contains ${{[\![\Gamma \vdash t_2]\!]}} (\gamma)$ and

  \begin{equation*} {{[\![\Gamma \vdash t_1 \; t_2]\!]}} (\gamma) = {{[\![\Gamma \vdash t_1]\!]}} (\gamma)\biggl({{[\![\Gamma \vdash t_2]\!]}} (\gamma)\biggr) \end{equation*}
  holds.

3.3 Soundness

We can now start our soundness proof with the weakening and substitution lemmas. They show that our interpretation is well behaved.

Lemma 29 (interpretation of weakening). If t is not a proof term, then the following equation holds

\begin{equation*}{{[\![\Gamma_1 ;\; \Gamma_2 \vdash t]\!]}} (\gamma_1, \gamma_2) = {{[\![\Gamma_1 ;\; (x' : A') ;\; \Gamma_2 \vdash t]\!]}} (\gamma_1, \alpha', \gamma_2)\end{equation*}

when both sides are well defined.

Proof. See Appendix A.

Our substitution lemma is similar to those in Werner (1997) and Miquel and Werner (2003).

Lemma 30 (interpretation of substitution). We assume $\Gamma \vdash u : U$ is derivable. If $\Gamma ;\; (x : U) ;\; \Delta$ is well formed and

\begin{equation*} (\gamma, {{[\![\Gamma \vdash u]\!]}} (\gamma), \delta) \in {{[\![\Gamma;\; (x : U) ;\; \Delta]\!]}} \end{equation*}

holds (with all interpretations defined), then

\begin{equation*} (\gamma, \delta) \in {{[\![\Gamma;\; \Delta[x \backslash u]]\!]}} \end{equation*}

holds. Moreover, in

\begin{equation*} {{[\![\Gamma;\; (x:U) ;\; \Delta \vdash t]\!]}} (\gamma, {{[\![\Gamma \vdash u]\!]}} (\gamma),\delta) = {{[\![\Gamma ;\; \Delta[x \backslash u] \vdash t[x \backslash u]]\!]}} (\gamma,\delta) \end{equation*}

the right-hand side is defined whenever the left-hand side is, and the equation holds for all t and T such that $\Gamma ;\; (x : U) ;\; \Delta \vdash t : T$ is derivable.

Proof. See Appendix B.

While propositions can be interpreted by sets with multiple values, our interpretation is still proof-irrelevant, as the interpretation of terms of sort Type does not depend on the parameters of sort Prop. This simplifies the proof of the next lemma.

Lemma 31 (semantic proof irrelevance) We assume that A’ is a propositional term for $\Gamma$ and t is not a proof term under $\Gamma ;\; (x' : A') ;\; \Delta$ . If

\begin{eqnarray*} (\gamma, p_1, \delta) &\in& {{[\![\Gamma ;\; (x' : A') ;\; \Delta]\!]}} \\ (\gamma, p_2, \delta) &\in& {{[\![\Gamma ;\; (x' : A') ;\; \Delta]\!]}} \end{eqnarray*}

hold, then

\begin{equation*} {{[\![\Gamma ;\; (x' : A') ;\; \Delta \vdash t : T]\!]}} (\gamma, p_1, \delta) = {{[\![\Gamma ;\; (x' : A') ;\; \Delta \vdash t : T]\!]}} (\gamma, p_2, \delta) \end{equation*}

holds.

Proof. See Appendix C.

Theorem 32 (soundness of beta equality) If $t_1 =_\beta t_2$ , and $\Gamma \vdash t_1 : T, \Gamma \vdash t_2 : T$ are derivable, then ${{[\![\Gamma \vdash t_1]\!]}} (\gamma) = {{[\![\Gamma \vdash t_2]\!]}} (\gamma)$ when both sides are well defined.

Proof. If $t_1$ is a proof term, then $t_2$ is also a proof term by Lemma 10, hence the statement holds. If not, it is sufficient to only prove that ${{[\![\Gamma \vdash (\lambda x :U. t) \; u]\!]}} (\gamma) = {{[\![\Gamma \vdash t[x \backslash u]]\!]}} (\gamma)$ holds. If $(\lambda x : U. t) u$ is well typed under $\Gamma$ , then $\Gamma \vdash u : U$ is derivable. If u is not a proof term, then

\begin{eqnarray*} && {{[\![\Gamma \vdash (\lambda x : U.t) \; u]\!]}} (\gamma) \\ &=& {{[\![\Gamma \vdash \lambda x : U.t]\!]}} (\gamma)\bigl({{[\![\Gamma \vdash u]\!]}} (\gamma)\bigr) \\ &=& {{[\![\Gamma ;\; (x : U) \vdash t]\!]}} (\gamma, {{[\![\Gamma \vdash u]\!]}} (\gamma)) \\ &=& {{[\![\Gamma \vdash t[x \backslash u]]\!]}} (\gamma) \end{eqnarray*}

holds by Lemma 30. If u is a proof term, then ${{[\![\Gamma \vdash \lambda x : U. t]\!]}} (\gamma)$ is a function whose domain contains ${{[\![\Gamma \vdash u]\!]}} (\gamma)$ by definition of the interpretation. Therefore, ${{[\![\Gamma ;\; (x : U) \vdash t]\!]}} (\gamma, {{[\![\Gamma \vdash u]\!]}} (\gamma))$ is also well defined. Hence,

\begin{align*} & \quad {{[\![\Gamma \vdash (\lambda x : U.t) \; u]\!]}} (\gamma) \\ &= {{[\![\Gamma \vdash \lambda x : U.t]\!]}} (\gamma)(\bot_X) \\ &= {{[\![\Gamma ;\; (x : U) \vdash t]\!]}} (\gamma, \bot_X) \\ &= {{[\![\Gamma ;\; (x : U) \vdash t]\!]}} (\gamma, {{[\![\Gamma \vdash u]\!]}} (\gamma)) \\ &= {{[\![\Gamma \vdash t[x \backslash u]]\!]}} (\gamma) \end{align*}

holds by Lemmas 30 and 31. Hence, the statement holds.

We are now ready to prove the soundness of this type system.

Theorem 33 (soundness). We assume $\gamma \in {{[\![\Gamma]\!]}} $ . If $\Gamma \vdash t : T$ is derivable, then ${{[\![\Gamma \vdash t]\!]}} (\gamma) \in {{[\![\Gamma \vdash T]\!]}} (\gamma)$ .

Proof. See Appendix D.

4. Properties of the Model

4.1 Interpretation of logical symbols

The following theorem explicits the interpretation of logical symbols from Definition 16. It demonstrates the logical adequacy of the interpretation.

Theorem 34 (interpretation of logical symbols). Here, let A and B be propositional terms and T be any (propositional or non propositional) term.

1. (i) ${{[\![\Gamma \vdash A \to B]\!]}} (\gamma) = {{[\![\Gamma \vdash B]\!]}} (\gamma)^{{{[\![\Gamma \vdash A]\!]}} (\gamma)}$

2. (ii) ${{[\![\Gamma \vdash \bot]\!]}} (\gamma) = \varnothing$

3. (iii) ${{[\![\Gamma \vdash A \land B]\!]}} (\gamma) = ({{[\![\Gamma \vdash A]\!]}} (\gamma)) \sqcap ({{[\![\Gamma \vdash B]\!]}} (\gamma))$

4. (iv) ${{[\![\Gamma \vdash A \lor B]\!]}} (\gamma) = ({{[\![\Gamma \vdash A]\!]}} (\gamma)) \sqcup ({{[\![\Gamma \vdash B]\!]}} (\gamma))$

5. (v)

6. (vi) When T is not a propositional term: ${{[\![\Gamma \vdash \exists x : T. B]\!]}} (\gamma) = \bigsqcup_{\alpha \in {{[\![\Gamma \vdash T]\!]}} (\gamma)} {{[\![\Gamma ;\; (x : T) \vdash B]\!]}} (\gamma, \alpha)$

7. (vii)

   1. a. ${{[\![\Gamma \vdash x =_T y]\!]}} (\gamma) = X$ iff ${{[\![\Gamma \vdash x]\!]}} (\gamma) = {{[\![\Gamma \vdash y]\!]}} (\gamma)$

   2. b. ${{[\![\Gamma \vdash x =_T y]\!]}} (\gamma) = \varnothing$ iff ${{[\![\Gamma \vdash x]\!]}} (\gamma) \neq {{[\![\Gamma \vdash y]\!]}} (\gamma)$

8. (viii)

   1. a. ${{[\![\Gamma \vdash A =_{\tt Prop} B]\!]}} (\gamma) \subset {{[\![\Gamma \vdash A \leftrightarrow B]\!]}} (\gamma)$

   2. b. ${{[\![\Gamma \vdash A \leftrightarrow B]\!]}} (\gamma) = X$ implies ${{[\![\Gamma \vdash A =_{\tt Prop} B]\!]}} (\gamma) = X$

Proof. See Appendix E

Here some consequences of Theorem 34.

Corollary 35.

1. (1) ${{[\![\Gamma \vdash x =_T y \lor x \neq_T y]\!]}} (\gamma) = X$

2. (2) ${{[\![\Gamma \vdash A \leftrightarrow B]\!]}} (\gamma) = X$ iff ${{[\![\Gamma \vdash A =_{\tt Prop} B]\!]}} (\gamma) = X$ .

3. (3) ${{[\![\Gamma \vdash A \leftrightarrow B]\!]}} (\gamma) = \varnothing$ implies ${{[\![\Gamma \vdash A =_{\tt Prop} B]\!]}} (\gamma) = \varnothing$

Note that the reverse of (3) in Corollary 35 is not true in general, i.e. there are cases such that ${{[\![\Gamma \vdash A \leftrightarrow B]\!]}} (\gamma) \neq \varnothing$ holds while ${{[\![\Gamma \vdash A=_{\tt Prop} B]\!]}} (\gamma) = \varnothing$ holds. This fact means that the propositional extensionality axiom does not always hold in this model, as detailed later.

4.2 Interpretation of excluded middle and linearity

Our original goal was to provide intuitionistic models of CC $^\omega$ . We will see here that by changing the topological space used by the interpretation, one can change the validity of axioms.

4.2.1 Classical model

We start with the simplest case. Let us consider the trivial topological space, whose base set is the singleton $\{ \varnothing \}$ .

\begin{eqnarray*} X &:=& \{ \varnothing \} \\ \mathcal{O}(X) &:=& \{\varnothing, \{\varnothing\}\} = \{0,1\}\end{eqnarray*}

This topological space is a well-behaved Alexandroff space and coincides with Werner’s model (Werner 1997). However, this model is so coarse that it represents classical logic, since the principle of excluded middle holds.

If we want to be more discriminating, we need more open sets in $\mathcal{O}(X)$ .

4.2.2 Models disproving excluded middle

Now, let us consider the next simplest topological space, which contains another element.

\begin{eqnarray*} X &:=& \{\varnothing, \{\varnothing\}\} \\ \mathcal{O}(X) &:=& \{\varnothing, \{\varnothing\}, \{\varnothing, \{\varnothing\}\}\} = \{0, 1, 2\}\end{eqnarray*}

Although this model stays simple, its topological space is fine enough to avoid the principle of excluded middle, since the following statement holds.

\begin{equation*} 2 \notin {{[\![\forall P : {\tt Prop}. P \lor \neg P]\!]}} = 1.\end{equation*}

This statement is derived by using the following equations.

\[ \neg 0 = 2 \hspace{4ex} \neg 1 = 0 \hspace{4ex} \neg 2 = 0 \]

By our soundness theorem, this proves that the principle of excluded middle cannot be deduced in CC^ω.

Yet this model is not fully intutionistic as the linearity axiom $(P \rightarrow Q) \lor (Q \rightarrow P)$ holds, since we have the following fact by Table 1.

Table 1: Value of $y^x$ for $X=\{\varnothing,\{\varnothing\}\}$

The above remark is actually interesting because it shows that we can use this model to prove non trivial facts, for instance that the excluded middle cannot be deduced from the linearity axiom in . Indeed,

\begin{equation*} {{[\![(\forall P : {\tt Prop}. \forall Q : {\tt Prop}. (P \rightarrow Q) \lor (Q \rightarrow P)) \rightarrow (\forall P : {\tt Prop}. P \lor \neg P) ]\!]}} = 1.\end{equation*}

By our soundness theorem, this equation means that there is no term proving the above implication in CC ^ω .

4.2.3 Models disproving linearity

By adding more elements we can refine the model further. Let $(X, \mathcal{O}(X))$ be the Alexandroff space

\begin{eqnarray*} X &:=& \{b, l, r, t\} \\ \mathcal{O}(X) &=& \{\varnothing, \{b\}, \{b, l\}, \{b, r\}, \{b, l, r\}, X\} \\ &\equiv& \{\varnothing, \alpha, \beta, \gamma, \delta, X\}\end{eqnarray*}

In this model, $(P \rightarrow Q) \lor (Q \rightarrow P)$ does not hold, since we have the following fact by Table 2.

\begin{equation*} t \notin {{[\![\forall P : {\tt Prop}. \forall Q : {\tt Prop}. (P \rightarrow Q) \lor (Q \rightarrow P)]\!]}} = \alpha\end{equation*}

Table 2: Value of $y^x$ for $X=\{b, l , r, t\}$

4.3 Interpretation of logical proof irrelevance

A general form of proof irrelevance, which does not depend on the type of the result, can be expressed as a logical formula, using the propositional encoding for equality:

\begin{equation*} \vdash \forall P : {\tt Prop}. \forall p_1, p_2 : P. ~ p_1 =_P p_2.\end{equation*}

Proposition 36 (interpretation of proof irrelevance) The logical formula for proof irrelevance is valid for any Alexandroff space.

Proof. We shall prove that for any topological space $(X, \mathcal{O}(X))$ , the interpretation of this formula is X. First note that, for any valuation $\gamma$ ,

\[{{[\![P : {\tt Prop} ;\; p_1 : P ;\; p_2 : P \vdash p_1]\!]}} (\gamma) = \lfloor \gamma \rfloor = {{[\![P : {\tt Prop} ;\; p_1 : P ;\; p_2 : P \vdash p_2]\!]}} (\gamma). \]

By using (vii) from Theorem 34, we have

\[ {{[\![P : {\tt Prop} ;\; p_1 : P ;\; p_2 : P \vdash p_1 =_P p_2]\!]}} (\gamma) = X.\]

As a result,

Note that semantic proof irrelevance (Lemma 31) and logical proof irrelevance (Proposition 36) are quite different. The former is about equality of interpretations of non-proof terms under different valuations, while the latter uses the equality of interpretations of proof terms under the same valuation. As a result, their proofs are independent.

4.4 Interpretation of propositional extensionality

As a notable property, propositional extensionality does not hold in general in our model.

The classical model, which was presented in Section 4.2.1, validates propositional extensionality, but any model disproving the excluded middle invalidates it.

Let us recall the model of Section 4.2.2. We assume that $\Gamma \vdash A : {\tt Prop}$ and $\Gamma \vdash B : {\tt Prop}$ are derivable and

\begin{eqnarray*} {{[\![\Gamma \vdash A]\!]}} (\gamma) &=& 1 \\ {{[\![\Gamma \vdash B]\!]}} (\gamma) &=& 2\end{eqnarray*}

hold. In this case,

\begin{eqnarray*} {{[\![\Gamma \vdash A \leftrightarrow B]\!]}} (\gamma) &=& {{[\![\Gamma \vdash B]\!]}} (\gamma)^{{{[\![\Gamma \vdash A]\!]}} (\gamma)} \sqcap {{[\![\Gamma \vdash A]\!]}} (\gamma)^{{{[\![\Gamma \vdash B]\!]}} (\gamma)} \\ &=& 1\end{eqnarray*}

holds. Since ${{[\![\Gamma \vdash A]\!]}} (\gamma) \neq {{[\![\Gamma \vdash B]\!]}} (\gamma)$ , then we have ${{[\![\Gamma \vdash A =_{\tt Prop} B]\!]}} (\gamma) = 0$ . Therefore,

\begin{eqnarray*} {{[\![\Gamma \vdash (A \leftrightarrow B) \to A =_{\tt Prop} B]\!]}} (\gamma) &=& 0^1 \\ &=& 0\end{eqnarray*}

holds by (9) in Lemma 19. Hence, propositional extensionality does not hold in this model.

More generally, the followings holds.

Proposition 37. In any nonclassical model, i.e. any model which has more than 2 open sets, the following holds.

\begin{equation*} {{[\![\vdash \forall P_1 P_2 : {\tt Prop}. (P_1 \leftrightarrow P_2) \to P_1 =_{\tt Prop} P_2]\!]}} = \varnothing \end{equation*}

Proof.

Here, we can choose $S_1 = {\downarrow{\bot}}$ and $S_2 = X$ . Since $S_1$ is then the smallest nonempty open set and $S_2$ the biggest, they cannot be equal as it would contradict the existence of at least 3 open sets. Since $X^{(\downarrow \bot)} \sqcap {(\downarrow{\bot})}^X \neq \varnothing$ , the interpretation equals to $\varnothing$ .

4.5 Interpretation of the axiom of choice

If we choose ZFC as ambient logic for our interpretation, then it validates the Axiom of Choice for any topological space $(X, \mathcal{O}(X))$ . That is, if $\Gamma \vdash A : {\tt Type}_i$ , $\Gamma \vdash B : {\tt Type}_j$ , and $\Gamma \vdash R : A \to B \to {\tt Prop}$ are derivable, then

\begin{equation*} {{[\![\Gamma \vdash \forall x : A. \exists y : B. R \; x \; y \to \exists f : A \to B. \forall x : A. R \; x \; (f \; x)]\!]}} (\gamma) = X\end{equation*}

holds. Now, let us consider the interpretation of the Axiom of Choice. We pose:

\begin{eqnarray*} S &:=& {{[\![\Gamma \vdash A]\!]}} (\gamma) \\ T &:=& {{[\![\Gamma \vdash B]\!]}} (\gamma) \\ \Theta &:=& {{[\![\Gamma \vdash R]\!]}} (\gamma).\end{eqnarray*}

Then we have:

Under ZFC set theory,

is true. Therefore, the Axiom of Choice is valid by Lemma 19 (7).

This may look surprising as Diaconescu’s Theorem states that, in set theory, the Axiom of Choice implies the excluded middle.

However, it has been observed that to prove the excluded middle, one needs in general more properties: propositional extensionality and functional extentionality (Forster 2021; van den Berg 2007). In our model, functional extensionality is still valid, but propositional extensionality is not valid, as mentioned in Section 4.4. Hence, we obtain a model in which the Axiom of Choice is valid without necessarily implying the excluded middle.

5. Interpretation of Inductive Types

Until now, we have discussed the interpretation of CC $^\omega$ . However, Coq’s type system is not CC $^\omega$ but CIC, which is CC $^\omega$ extended with (co)inductive types. In this paper, we do not give a general definition of inductive types, but we present some examples of inductive definitions. Here, we introduce a new type system CC $^\omega_\mathsf{list}$ , which is CC $^\omega$ with the $\mathsf{list}$ type.

5.1 Typing rule of CC $^\omega_\mathsf{list}$

To construct the new type system CC $^\omega_\mathsf{list}$ , we add new terms and typing rules to CC $^\omega$ . Here, we give five new terms, $\mathsf{list}, \mathsf{nil}, \mathsf{cons}, \mathsf{list\_rec},$ and $\mathsf{list\_ind}$ , and also give new typing rules for the $\mathsf{list}$ type in Figure 2.

Figure 2. New typing rules of CC $^\omega_\mathsf{list}$ .

Now, we define the beta equality for CC $^\omega_\mathsf{list}$ .

Definition 38 (Beta Equality for CC $^\omega_\mathsf{list}$ ) Let $=_{\beta'}$ be the smallest equivalence relation such that the following conditions hold.

1. (i) $(\lambda x : A. t) \; a =_{\beta'} t[x \backslash a]$ .

2. (ii) If $t_1 =_{\beta'} t_1'$ and $t_2 =_{\beta'} t_2'$ , then $t_1 t_2 =_{\beta'} t_1' t_2'$ .

3. (iii) If $t =_{\beta'} t'$ and $A =_{\beta'} A'$ , then $\lambda x : A. t =_{\beta'} \lambda x : A' t'$ .

4. (iv) If $A =_{\beta'} A'$ and $B =_{\beta'} B'$ , then $\forall x : A. B =_{\beta'} \forall x : A' B'$ .

5. (v) $\mathsf{list\_rec} \; A \; F \; t_1 \; t_2 \; (\mathsf{nil} \; A) =_{\beta'} t_1$

6. (vi) $\mathsf{list\_rec} \; A \; F \; t_1 \; t_2 \; (\mathsf{cons} \; A \; a \; l) =_{\beta'} t_2 \; a \; l \; (\mathsf{list\_rec} \; A \; F \; t_1 \; t_2 \; l)$

7. (vii) $\mathsf{list\_ind} \; A \; F \; t_1 \; t_2 \; (\mathsf{nil} \; A) =_{\beta'} t_1$

8. (viii) $\mathsf{list\_ind} \; A \; F \; t_1 \; t_2 \; (\mathsf{cons} \; A \; a \; l) =_{\beta'} t_2 \; a \; l \; (\mathsf{list\_ind} \; A \; F \; t_1 \; t_2 \; l)$

Now that we defined CC $^\omega_\mathsf{list}$ ’s terms and typing rules, we can define some familiar operators over $\mathsf{list}$ type, such as membership operator ‘ $\mathsf{in}$ ’ for instance.

\begin{eqnarray*} && \mathsf{in} : \forall A : {\tt Type}_0. A \rightarrow \mathsf{list} \; A \rightarrow {\tt Prop} := \\ && \quad \lambda A : {\tt Type}_0 . \; \lambda a : A. \; \lambda l : \mathsf{list} A . \\ && \qquad (\mathsf{list\_rec} \; A \; (\lambda \_ : \mathsf{list} \; A. \; {\tt Prop}) \\ && \qquad\quad \textrm{False} \\ && \qquad\quad ( \; \lambda x : A. \; \lambda \_ : \mathsf{list} \; A. \; \lambda \mathsf{ind} : {\tt Prop}. \; x = a \lor \mathsf{ind} \; ) \\ && \qquad\quad l )\end{eqnarray*}

We can then derive the following equalities from Definition 38.

• • $\mathsf{in} \; A \; a \; (\mathsf{nil} \; A) =_{\beta'} \textrm{False}$

• • $\mathsf{in} \; A \; a \; (\mathsf{cons} \; A \; x \; l) =_{\beta'} x = a \lor \mathsf{in} \; A \; a \; l$

5.2 Interpretation

Here, we define an interpretation of CC $^\omega_\mathsf{list}$ . The interpretation of ${\mathsf{list}}$ s is obtained through an initial algebra construction. We fix an arbitrary element denoted by the dot symbol “ $\cdot$ ” to interpret the unit type. We can then define the interpretations of $\mathsf{list}$ , $\mathsf{nil}$ , $\mathsf{cons}$ , $\mathsf{list\_rec}$ and $\mathsf{list\_ind}$ as follows.

1. (I) Interpretation of $\mathsf{list}$ .

   First, we define the Kleene closure $S^*$ of a set S as follows.

   \begin{equation*} S^* := \bigcup_{n \in \omega} S^n \end{equation*}
   where $S^n$ is an n-tuple of S, i.e.
   \begin{eqnarray*} S^0 &:=& \{ (0, \cdot) \} \\ S^{n+1} &:=& \{(1, (a, l)) \mid a \in S \; \textrm{and} \; l \in S^n\}. \end{eqnarray*}
   Then $\mathsf{list}$ is interpreted as a function building the Kleene closure of a set.
   \begin{equation*} {{[\![\Gamma \vdash \mathsf{list}]\!]}} (\gamma) := \{(S, S^*) \mid S \in \mathcal{U}_0 \} \end{equation*}
   We can easily check that
   \begin{equation*} {{[\![\Gamma \vdash \mathsf{list}]\!]}} (\gamma) \in {{[\![\Gamma \vdash {\tt Type}_0 \rightarrow {\tt Type}_0]\!]}} (\gamma) \end{equation*}
   holds for any $\gamma \in {{[\![\Gamma]\!]}} $ .

2. (II) Interpretation of $\mathsf{nil}$ .

   $\mathsf{nil}$ is interpreted by the constant function returning “ $(0,\cdot)$ ”.

   \begin{equation*} {{[\![\Gamma \vdash \mathsf{nil}]\!]}} (\gamma) := \{(S, (0, \cdot)) \mid S \in \mathcal{U}_0\}, \end{equation*}
   We can again easily check that
   \begin{equation*} {{[\![\Gamma \vdash \mathsf{nil}]\!]}} (\gamma) \in {{[\![\Gamma \vdash \forall A : {\tt Type}_0, \mathsf{list} A]\!]}} (\gamma) \end{equation*}
   holds since $(0,\cdot) \in S^*$ for any set S.

3. (III) Interpretation of $\mathsf{cons}$ .

   First, we define $\mathsf{cons}_S$ as follows

   \begin{equation*} \mathsf{cons}_S := \{(s, (l, (1, s, l))) \mid s \in S \; \textrm{and} \; l \in S^*\} \end{equation*}
   for any set S. We can easily check that
   \begin{equation*} \mathsf{cons}_S \in S \rightarrow S^* \rightarrow S^* \end{equation*}
   holds. Now, we can define the interpretation of $\mathsf{cons}$ as follows.
   \begin{equation*} {{[\![\Gamma \vdash \mathsf{cons}]\!]}} (\gamma) := \{(S, \mathsf{cons}_S) \mid S \in \mathcal{U}_0\} \end{equation*}
   We can again easily check that
   \begin{equation*} {{[\![\Gamma \vdash \mathsf{cons}]\!]}} (\gamma) \in {{[\![\Gamma \vdash \forall A : {\tt Type}_0, A \rightarrow \mathsf{list} \; A \; \rightarrow \mathsf{list} \; A ]\!]}} (\gamma) \end{equation*}
   holds.

4. (IV) Interpretation of $\mathsf{list\_rec}$ .

   Given a function $T : S^* \rightarrow \mathcal{U}_0$ , we define the dependent function $\textrm{rec}^{(n)}_{t, f} \in \prod_{l \in S^n} T(l)$ by recursion on natural numbers.

   \begin{eqnarray*} \textrm{rec}^{(0)}_{t, f} &:=& \{ ((0, \cdot), t) \} \\ \textrm{rec}^{(n+1)}_{t, f} &:=& \{ ((1, (a, l)), f(a)(l)(\textrm{rec}^{(n)}_{t,f}(l))) \mid a \in S \; \textrm{and} \; l \in S^n \} \end{eqnarray*}
   where t is an element of $T((0,\cdot))$ and f is a dependent function
   \begin{equation*} f \in \prod_{a \in S} \prod_{l \in S^*} \Bigl( T(l) \rightarrow T((1,(a, l))) \Bigr). \end{equation*}
   Next, we define $\textrm{rec}_{t, f} \in \prod_{l \in S^*} T(l)$ as follows.
   \begin{equation*} \textrm{rec}_{t,f} := \bigcup_{n \in \omega} \textrm{rec}^{(n)}_{t,f} \end{equation*}

   Finally, we define $\mathsf{list\_rec}$ as follows.

   \begin{eqnarray*} {{[\![\Gamma \vdash \mathsf{list\_rec}]\!]}} (\gamma) &:=& \{ (S, (T, (t, (f, \textrm{rec}_{t, f})))) \mid \\ && \qquad S \in \mathcal{U}_0 \\ && \qquad T \in S^{*} \rightarrow \mathcal{U}_0 \\ && \qquad t \in T((0,\cdot)) \\ && \qquad f \in \prod_{a \in S} \prod_{l \in S^*} \Bigl( T(l) \rightarrow T((1,(a, l))) \Bigr) \} \end{eqnarray*}
   We can again easily check that
   check this
   holds.

5. (v) Interpretation of $\mathsf{list\_ind}$ .

   The interpretation of $\mathsf{list\_ind}$ is much simpler. Since $\mathsf{list\_ind}$ is a proof term, its interpretation must be

   \begin{equation*} {{[\![\Gamma \vdash \mathsf{list\_ind}]\!]}} (\gamma) := \lfloor \gamma \rfloor. \end{equation*}
   For the soundness theorem, we shall prove that
   check here
   holds. This is a corollary of Lemma 40.

It remains to prove the soundness of CC $^\omega_\mathsf{list}$ .

Theorem 39 (soundness for CC $^\omega_\mathsf{list}$ ).

1. (1) If $t_1 =_{\beta'} t_2$ holds and $\Gamma \vdash t_1 : T$ and $\Gamma \vdash t_2 : T$ are derivable, then ${{[\![\Gamma \vdash t_1]\!]}} (\gamma) = {{[\![\Gamma \vdash t_2]\!]}} (\gamma)$ holds.

2. (2) If $\Gamma \vdash t : T$ is derivable in CC $^\omega_\mathsf{list}$ , then ${{[\![\Gamma \vdash t]\!]}} (\gamma) \in {{[\![\Gamma \vdash T]\!]}} (\gamma)$ holds.

To prove (1), we need a CC $^\omega_\mathsf{list}$ version of Lemmas 10 and 30. They can be proved similary as for CC $^\omega$ . To prove (2), we need the following lemma that states the soundness of induction on ${\mathsf{list}}$ s.

Lemma 40.

check here

where X is the whole topological space $(X, \mathcal{O}(X))$ .

Proof. Let S be a set and $\psi \in S^{*} \to \mathcal{O}(X)$ be a function. We define the set of open sets $T^{\psi}_{n}$ as

\begin{eqnarray*} T^{\psi}_{0} &:=& \{ \psi(0, \cdot) \} \\ T^{\psi}_{n+1} &:=& T^{\psi}_n \cup \{ \psi(1, (a, l))^{\psi(l)} \mid a \in S \; \textrm{and} \; l \in S^n\}. \end{eqnarray*}

For any $n \in \omega$ and $l \in S^n$ , holds by induction on natural numbers. Let $T^{\psi}$ be their union

\begin{equation*} T^{\psi} := \bigcup_{n \in \omega} T^{\psi}_n. \end{equation*}

Since $T^{\psi}_n \subset T^{\psi}$ , therefore holds, hence we have for any $l \in S^{*}$ . Therefore, we also have .

Now, let us calculate the first equation:

To calculate it, we use (1) and (7) from Lemma 19.

6 Conclusion and Future Work

We could construct an intuitionistic set-theoretical model of CC^ω, which allowed us to prove that PEM and the linearity axiom do not hold in CC^ω. This model is not complete with respect to plain CC^ω, since it is proof-irrelevant.

This model combines an impredicative interpretation of propositional terms and a predicative interpretation of nonpropositional terms as in Miquel and Werner (2003).

Since one of our goals is to provide a model for Coq, we need to extend our model to all of CIC. This requires working on several extensions:

1. • CIC adds subsumption between ${\tt Prop}$ and ${\tt Type}_i$ .

   \[\frac{\Gamma \vdash A : {\tt Prop}}{\Gamma \vdash A : {\tt Type}_i}\]
   In fact, this rule breaks Lemmas 12 and 15. As a result, Theorem 32, soundness of beta equality, does not hold, as we show here.

Let $\mathcal{I}$ be $\lambda T : {\tt Type}_i. T \to T$ . In a set-theoretical interpretation, ${{[\![\mathcal{I}]\!]}} $ must be a function $A \mapsto \{f \mid f : A \to A\}$ . However, for any propositional term P, the term $\mathcal{I} P$ is a tautology, and its interpretation is X, which leads to conflicting interpretations as ${{[\![\mathcal{I}]\!]}} ({{[\![P]\!]}} ) = {{[\![P]\!]}} \to {{[\![P]\!]}} \neq X$ . Using an idea from Aczel (1998), Lee and Werner (2011), and Timany and Sozeau (2017) avoided this problem in an elegant way, by giving a uniform interpretation of propositional and non-propositional terms. They define the encoding functions $\mathsf{app}$ and $\mathsf{lam}$ as follows.

\begin{eqnarray*} \mathsf{app} (u,x) &:=& \{ z \mid (x, z) \in u\} \\ \mathsf{lam} (f) &:=& \bigcup_{(x,y) \in f} \{(x,z) \mid z \in y\}\end{eqnarray*}

These satisfy the expected property $\mathsf{app}(\mathsf{lam}(f),x) = f(x)$ . Using the classical interpretation ${{[\![{\tt Prop}]\!]}} = \{\varnothing,\{\varnothing\}\}$ , the interpretation of the product type $\forall x: A.B$ becomes $\{\mathsf{lam}(f) \mid f \in \prod_{x \in A} B(x)\} \in{{[\![{\tt Prop}]\!]}} $ . It evaluates to $\{\varnothing\}$ iff $B(x) = \{\varnothing\}$ for all $x \in A$ .

Unfortunately, this solution does not apply to intuitionistic settings, since ${{[\![{\tt Prop}]\!]}} $ should contain more elements, making such a simple encoding impossible. We believe that searching for a non uniform encoding is a more resonable direction.

1. • Finally, CIC adds inductive and co-inductive type definitions, and they both can live in the impredicative universe ${\tt Prop}$ . The model in Lee and Werner (2011) supports generic inductive definitions through their set theoretical interpretation in a predicative universe as it was defined by Dybjer (2000), using Aczel’s $\Phi$ -closed set approach (Aczel and Rathjen 2010). However, they do not extend this interpretation to the impredicative case. We have not yet investigated how to handle generic inductive definitions, co-inductive defintions, and impredicative inductive definitions in our model.