I've been playing with the idea of a "double Lawvere theory" for mechanizing first order logical theories. I've been able to find only a tiny amount of detail online though and want feedback on whether the idea makes sense.
I think the basic idea might be phrased as a "Lawvere theory equipped with relations?"
Assume a double category with finite products $\text{T}^n$ as objects. The vertical category is Cartesian with respect to the product (Set like) and the horizontal category is dagger closed monoidal copy-delete with respect to product (Rel or Span like.) 2-cells are thin.
Assume constructive propositional logic operators for the horizontal category. Assume an adjoint to composition something like Kan extension of two relations $(Q/P)(a, b) = \forall x, P(x, a) \rightarrow Q(x, b)$.
Assume covariant $[ - \vert$ and contravariant $ \vert - ]$ maps from the vertical (Set-like) category to the horizontal (Rel-like) category.
Function symbols map to horizontal morphisms and relation symbols map to vertical morphisms.
For example, consider IZF. I'm mostly following https://plato.stanford.edu/entries/set-theory-constructive/axioms-CZF-IZF.html#axioms .
You might suppose a horizontal map for set membership $\in \colon \text{T} \nrightarrow \text{T} $ and vertical maps
- empty set $\emptyset \colon 1 \rightarrow \text{T}$
- infinity $\infty \colon 1 \rightarrow \text{T}$
- pairing $\text{pair} \colon \text{T}^2 \rightarrow \text{T}$
- union $\bigcup \colon \text{T} \rightarrow \text{T}$
- powerset $\text{pow}\colon \text{T} \rightarrow \text{T} $
- separation $\text{sep}\colon (1 \nrightarrow \text{T}) \rightarrow (\text{T} \rightarrow \text{T})$
- collection $\text{col}\colon (\text{T} \nrightarrow \text{T}) \rightarrow (\text{T} \rightarrow \text{T})$
Define subsets: $\mathop{\subseteq} = \mathop{\in}/\mathop{\in}$.
Define the successor set: $\text{S} = \text{pair} \circ \langle \text{id} , \text{pair} \circ \langle \text{id} , \text{id} \rangle \rangle$
I'd like to draw squares but phrasing the 2-cells as maps between relations you get
Extensionality: $\mathop{\subseteq} \wedge \mathop{\subseteq}^{\text{T}} \Leftrightarrow \text{id}$
Empty set: $\mathop{\in} \circ \vert \emptyset ] \Rightarrow \bot $
Pairing: $ \mathop{\in} \circ \vert \text{pair}] \Leftrightarrow \mathop{\in} \circ \vert \pi_1 ] \vee \mathop{\in} \circ \vert \pi_2 ]$
Powerset: $ \mathop{ \in} \circ \vert \text{pow} ] \Leftrightarrow \mathop{\subseteq} $
Infinity 1: $ \top \Rightarrow [\emptyset \vert \circ \mathop{\in} \circ \vert \infty ] $
Infinity 2: $\mathop{\in} \circ \vert \infty ] \Rightarrow [\text{S} \vert \circ \mathop{\in} \circ \vert \infty ]$
Union: $\mathop{\in} \circ \mathop{\in} \Leftrightarrow \mathop{\in} \circ \vert \mathop{\bigcup} ]$
I'm very confused on separation and induction. I think you want something like
Separation: $ \mathop{\in } \wedge \vert P \circ \text{tt} ] \Rightarrow \mathop{\in} \circ \vert \mathop{\text{sep}} P ]$
Induction: $ (\mathop{\in} \wedge [P \circ \text{tt}| \rightarrow \mathop{\in} \circ \vert P \circ \text{tt}]) \Rightarrow \mathop{\in} \circ \vert P \circ \text{tt}]$
I still can't figure out the axiom of collection.
I'm pretty sure I got some other stuff wrong as well. This feels great for computers and mechanization but it's a little teensy bit opaque. In the future I would look to compile down a higher level language to this sort of formulation.