6. Deductive sets [0030]
Since the overall problem with $PZ$ is to allow for a deduction theory (cf. §5), Lambek-Scott proposed in (Lambek & Scott, 1981) to understand $PZ$ as a deductive set, i.e. a set $E$ equipped with a relation $\vdash \subseteq (\mathcal{P}_\text{f}E)\times E$ called deduction, satisfying the following axioms: If $(L,\le)$ is a complete lattice, we can obtain a deduction structure $\vdash$ as follows:
$$
\begin{align*}
\{x_1,\dots,x_n\} \vdash y & \iff \bigvee x_i\ge y\\
& \iff \bigvee x_i = y\lor \bigvee x_i
\end{align*}
$$
Bibliography
-
Lambek, J., & Scott, P. J. (1981). Algebraic aspects of topos theory. Cahiers De Topologie Et Géométrie Différentielle Catégoriques, 22(2), 129–140. http://www.numdam.org/item/CTGDC_1981__22_2_129_0/Details