An implicative structure is an ample generalization of complete Heyting algebras introduced by Alexandre Miquel in (Miquel β20a).

Implicative structures are used to define implicative algebras, with are implicative structures equipped with a βseparatorβ, which generalizes a filter for an Heyting algebra. From an implicative algebra, one can then construct an implicative tripos, a construction which is the real motivation behind implicative structures and algebras.

These triposes end up generalizing many others, constructed from complete Heyting algebras, partial combinatory algebras, ordered combinatory algebras, and Krivine structures, thus unifying the methodology of realizability theory. More strikingly, Miquel proved all triposes over $\mathbf{Set}$ are implicative triposes (Miquelβ20b).

An **implicative structure** is a complete meet semilattice $(\mathcal{A}, \leq)$ equipped with a right-continuous monotone operation $\to : \mathcal{A}^{op} \times \mathcal{A} \to \mathcal{A}$.

Explicitly, this means $\mathcal{A}$ is a poset with all meets, and $\to$ satisfies two axioms:

- for all $a' \leq a, b \leq b' \in \mathcal{A}$, $(a \to b) \leq (a' \to b')$,
- for all $a \in \mathcal{A}, B \subseteq \mathcal{A}$, $a \to \bigwedge_{b \in B} b = \bigwedge_{b \in B} (a \to b)$

We donβt assume $\to$ to also be left-continuous (i.e. commute with $\bigvee$ in the first argument, which comes out as a $\bigwedge$ because of the antimonotonicity), though in most examples $\to$ satisfies this additional property.

Two observations follow immediately from this definition:

- A complete semi-lattice is, at the end of the day, the same thing as a complete lattice since $\bigvee A = \bigwedge (\mathcal{A}\setminus A)$, where $A \subseteq \mathcal{A}$.
- By the adjoint functor theorem for posets, $a \to -$ has a left adjoint $- \otimes a : \mathcal{A} \to \mathcal{A}$. In this sense, implicative structures generalize Heyting algebras by weakening the requirement that $- \otimes a = - \wedge a$. In fact, we have no requirement whatsoever on $- \otimes a$, which makes $\to$ a much weaker operation than $\Rightarrow$, at least on paper.

Hence an alternative definition of implicative structure is:

An implicative structure is a complete lattice $\mathcal{A}$ equipped with a left-continuous, monotone operation $\otimes : \mathcal{A} \times \mathcal{A} \to \mathcal{A}$.

In this form, it is easy to see this as broadly generalizing posetal Benabou cosmoi, more commonly known as quantales. In fact implicative structures are quantales, but for the fact that $\otimes$ doesnβt satisfy the axioms of a monoidal operation on $\mathcal{A}$.

This is interesting since cosmoi are βgood enrichment basesβ for *categories*, while implicative structures are βgood enrichment basesβ for *sets*.

- implicative algebra
- realizability
- forcing
- tripos, in particular implicative tripos

- Alexandre Miquel,
*Implicative algebras: a new foundation for realizability and forcing*, Mathematical Structures in Computer Science 30 (5): 458β510. (doi). - Alexandre Miquel. 2020.
*Implicative Algebras II: Completeness w.r.t. Set-Based Triposes*. arXiv. https://doi.org/10.48550/arXiv.2011.09085. (arxiv)

Last revised on May 26, 2023 at 12:34:35. See the history of this page for a list of all contributions to it.