An *implicative algebra* is an implicative structure equipped with a filter-like subset called a *separator*.

Recall an implicative structure is a generalized complete Heyting algebra in which the implication $\to$ is only required to be right continuous and not necessarily right adjoint to the meet.

The separator is defined in such a way as to induce a quotient which makes the implicative structure into a bona-fide Heyting algebra. It is in this sense that a separator is like a (ultra)filter, whose primary purpose is to be used to define quotients which usually restore some property.

Given the completeness result in (Miquelβ20b), we can say implicative algebras are to ($\mathbf{Set}$-)triposes what complete Heyting algebras (equivalently, locales) are to Grothendieck toposes.

Let $(\mathcal{A}, \leq, \to)$ be an implicative structure.

A **separator** of $\mathcal{A}$ is a subset $S \subseteq \mathcal{A}$ such that

- $S$ is upwards closed: for all $a \leq b \in \mathcal{A}$, $a \in S$ implies $b \in S$.
- $S$ is closed under βmodus ponensβ: for all $a, b \in \mathcal{A}$, $a \in S$ and $a \to b \in S$ implies $b \in S$.
- $S$ contains the following elements:$K = \bigwedge_{a,b \in \mathcal{A}} (a \to b \to a),$$S = \bigwedge_{a,b,c \in \mathcal{A}} ((a \to b \to c) \to (a \to b) \to a \to c)$

In the case $\mathcal{A}$ is actually an Heyting algebra, separators coincide with filters.

Let $S$ be a separator of $\mathcal{A}$. Then we can define a relation on $\mathcal{A}$:

$a \vdash_S b \quad \text{iff}\quad (a \to b) \in S.$

This relation is a preorder, and its posetal reflection is an Heyting algebra with implication given by:

$[a] \Rightarrow [b] := [a \to b].$

This is Proposition 3.2.1 in (Miquelβ20).

The Heyting algebra obtained from an implicative algebra is called its **induced Heyting algebra**, denoted $(\mathcal{A}/S, \leq_S)$. It is proven in (Miquelβ20) that this operation is functorial .

When $\mathcal{A}$ is an Heyting algebra to begin with, $(\mathcal{A}/S, \leq_S)$ is the quotient induced by $S$, seen as a filter.

- filter
- complete Heyting algebra
- realizability
- forcing
- tripos, in particular implicative tripos

Last revised on April 30, 2023 at 04:26:16. See the history of this page for a list of all contributions to it.