# Prove distributive law in Hilbert system

Using the logical axioms of the Hilbert system

1. $\phi\to\phi$
2. $\phi\to(\psi\to\phi)$
3. $\left( \phi \to \left( \psi \rightarrow \xi \right) \right) \to \left( \left( \phi \to \psi \right) \to \left( \phi \to \xi \right) \right)$
4. $\left ( \lnot \phi \to \lnot \psi \right) \to \left( \psi \to \phi \right)$
5. $\alpha\to\beta\to\alpha\land\beta$
6. $\alpha\wedge\beta\to\alpha$
7. $\alpha\wedge\beta\to\beta$
8. $\alpha\to\alpha\vee\beta$
9. $\beta\to\alpha\vee\beta$
10. $(\alpha\to\gamma)\to (\beta\to\gamma) \to \alpha\vee\beta \to \gamma$

along with the inference rule modus ponens MP $\dfrac{\alpha,\alpha\to\beta}{\beta}$,

how can we prove the distributive law $p\wedge(q\vee r) \leftrightarrow(p\wedge q)\vee(p\wedge r)$? I'm sure I'm probably missing something quite obvious, but I can't see how any of these axioms can prove any disjunction at all.

• 8 and 9 allow you to prove disjunctions. If ↔ means logical equivalence though, you need more axioms to prove the distributive equivalence that you referenced. Commented Oct 24, 2017 at 1:43
• Though, one you have an equivalence axiom (you only need one actually), you basically can assume one side and prove the other via axiom 10. E. G. you have (q∨r). If q, then (p∧q), so the right. If r, then (p∧r), so the right. Then axiom 10 gets used to get to the right. From the right, if (p∧q), then q, so (q V r), thus the left. If (p∧r), then r, so (q V r), thus the right. Then use 10 to get to the left. (I've omitted some steps). Then from ((p→q)→((q→p)→(p↔q))) you have the equivalence. Commented Oct 24, 2017 at 1:58
• I view $p \leftrightarrow q$ as a shorthand of $p \to q \land q \to p$, where your rule would just be 5. Commented Oct 24, 2017 at 2:03
• @KennyLau I think that's possible. But, it could not be a shorthand also. Commented Oct 24, 2017 at 11:54
• @ziggurism Well, Wikipedia dropped the ball ... We could easily add an axiom 'Hilbert-style': $(\phi \rightarrow \psi) \rightarrow ((\psi \rightarrow \phi) \rightarrow (\phi \leftrightarrow \psi))$ Commented Oct 24, 2017 at 16:21

For the forward direction: you need to split the premise into $p$ and $q \lor r$, then use prove by cases (i.e. 10) on $q \lor r$ along with $p$.

01 p→q→(p∧q)                   5
02 p∧q→(p∧q)∨(p∧r)             8
03 (p∧q→(p∧q)∨(p∧r))→(q→p∧q→(p∧q)∨(p∧r)) 2
04 q→p∧q→(p∧q)∨(p∧r)           MP 02 03
05 (q→p∧q→(p∧q)∨(p∧r))→(q→p∧q)→(q→(p∧q)∨(p∧r)) 3
06 (q→p∧q)→(q→(p∧q)∨(p∧r))     MP 04 05
07 ((q→p∧q)→(q→(p∧q)∨(p∧r)))→p→(q→p∧q)→(q→(p∧q)∨(p∧r)) 2
08 p→(q→p∧q)→(q→(p∧q)∨(p∧r))   MP 06 07
09 (p→(q→p∧q)→(q→(p∧q)∨(p∧r)))→(p→(q→p∧q))→(p→(q→(p∧q)∨(p∧r))) 3
10 (p→q→p∧q)→(p→q→(p∧q)∨(p∧r)) MP 08 09
11 p→q→(p∧q)∨(p∧r)             MP 01 10

12 p→r→(p∧r)                   5
13 p∧r→(p∧q)∨(p∧r)             9
14 (p∧r→(p∧q)∨(p∧r))→(r→p∧r→(p∧q)∨(p∧r)) 2
15 r→p∧r→(p∧q)∨(p∧r)           MP 13 14
16 (r→p∧r→(p∧q)∨(p∧r))→(r→p∧r)→(r→(p∧q)∨(p∧r)) 3
17 (r→p∧r)→(r→(p∧q)∨(p∧r))     MP 15 16
18 ((r→p∧r)→(r→(p∧q)∨(p∧r)))→p→(r→p∧r)→(r→(p∧q)∨(p∧r)) 2
19 p→(r→p∧r)→(r→(p∧q)∨(p∧r))   MP 17 18
20 (p→(r→p∧r)→(r→(p∧q)∨(p∧r)))→(p→(r→p∧r))→(p→(r→(p∧q)∨(p∧r))) 3
21 (p→r→p∧r)→(p→r→(p∧q)∨(p∧r)) MP 19 20
22 p→r→(p∧q)∨(p∧r)             MP 12 21

23 (q→(p∧q)∨(p∧r))→(r→(p∧q)∨(p∧r))→(q∨r)→(p∧q)∨(p∧r) 10
24 ((q→(p∧q)∨(p∧r))→(r→(p∧q)∨(p∧r))→(q∨r)→(p∧q)∨(p∧r))→p→((q→(p∧q)∨(p∧r))→(r→(p∧q)∨(p∧r))→(q∨r)→(p∧q)∨(p∧r)) 2
25 p→((q→(p∧q)∨(p∧r))→(r→(p∧q)∨(p∧r))→(q∨r)→(p∧q)∨(p∧r)) MP 23 24
26 (p→(q→(p∧q)∨(p∧r))→(r→(p∧q)∨(p∧r))→(q∨r)→(p∧q)∨(p∧r))→(p→(q→(p∧q)∨(p∧r)))→(p→(r→(p∧q)∨(p∧r))→(q∨r)→(p∧q)∨(p∧r)) 3
27 (p→(q→(p∧q)∨(p∧r)))→(p→(r→(p∧q)∨(p∧r))→(q∨r)→(p∧q)∨(p∧r)) MP 25 26
28 p→(r→(p∧q)∨(p∧r))→(q∨r)→(p∧q)∨(p∧r) MP 11 27
29 (p→(r→(p∧q)∨(p∧r))→(q∨r)→(p∧q)∨(p∧r))→(p→(r→(p∧q)∨(p∧r)))→(p→(q∨r)→(p∧q)∨(p∧r)) 3
30 (p→(r→(p∧q)∨(p∧r)))→(p→(q∨r)→(p∧q)∨(p∧r)) MP 28 29
31 p→(q∨r)→(p∧q)∨(p∧r) MP 22 30

32 (p→(q∨r)→(p∧q)∨(p∧r))→p∧(q∨r)→p→(q∨r)→(p∧q)∨(p∧r) 2
33 p∧(q∨r)→p→(q∨r)→(p∧q)∨(p∧r) MP 31 32
34 (p∧(q∨r)→p→(q∨r)→(p∧q)∨(p∧r))→(p∧(q∨r)→p)→(p∧(q∨r)→(q∨r→(p∧q)∨(p∧r))) 3
35 (p∧(q∨r)→p)→(p∧(q∨r)→(q∨r→(p∧q)∨(p∧r))) MP 33 34
36 p∧(q∨r)→p 6
37 p∧(q∨r)→(q∨r→(p∧q)∨(p∧r)) MP 36 35

38 (p∧(q∨r)→(q∨r→(p∧q)∨(p∧r)))→(p∧(q∨r)→q∨r)→(p∧(q∨r)→(p∧q)∨(p∧r)) 3
39 (p∧(q∨r)→q∨r)→(p∧(q∨r)→(p∧q)∨(p∧r)) MP 37 38
40 p∧(q∨r)→q∨r 7
41 p∧(q∨r)→(p∧q)∨(p∧r) MP 39 40


Synopsis:

11 p→q→(p∧q)∨(p∧r)
22 p→r→(p∧q)∨(p∧r)
31 p→(q∨r)→(p∧q)∨(p∧r)
37 p∧(q∨r)→(q∨r→(p∧q)∨(p∧r))
41 p∧(q∨r)→(p∧q)∨(p∧r)


The backward direction is left as an exercise to the reader.

• Thank you Kenny. I followed all the steps, and agreed with each one, but am not sure I could've come up with them. I think studying the synopsis you wrote to try to get the big picture will be helpful. Thanks again. Commented Oct 24, 2017 at 18:42

Some Preliminaries
First: before answering the question, it will be useful to rename the axioms and adopt some conventions that will also sneak something (yet to be named) in to resolve this question and others like it: $$\begin{array}{ll} I:& a ⊃ a,\\ K:& a ⊃ b ⊃ a,\\ S:& (a ⊃ b ⊃ c) ⊃ (a ⊃ b) ⊃ a ⊃ c,\\ Z:& (¬a ⊃ ¬b) ⊃ b ⊃ a,\\ A:& a ⊃ b ⊃ a∧b,\\ π_0:& a∧b ⊃ a,\\ π_1:& a∧b ⊃ b,\\ σ_0:& a ⊃ a∨b,\\ σ_1:& b ⊃ a∨b,\\ O:& (a ⊃ c) ⊃ (b ⊃ c) ⊃ a∨b ⊃ c. \end{array}$$

Second: in here, and below, use $$⊃$$ for the conditional operator and adopt the conventions that it associates to the right, e.g. $$a ⊃ b ⊃ c = a ⊃ (b ⊃ c)$$ and that it binds more loosely than the other connectives, with $$¬$$ binding the strongest of all the connectives. For concreteness, we will write $$f: a$$ to state that $$f$$ is a proof of $$a$$. For modus ponens, if $$f: a ⊃ b$$ and $$g: a$$, then we write $$fg: b$$. Products associate to the left, e.g. $$fgh = (fg)h$$.

We can also define the following: $$\left(\begin{matrix}x: a\\y: b\end{matrix}\right) → (x, y) ≡ A x y: a ∧ b,\\ \left(\begin{matrix}f: a ⊃ c\\g: b ⊃ c\end{matrix}\right) → [f, g] ≡ O f g: a ∨ b ⊃ c.$$

Third: some key lemmas may then be established and written succinctly as follows: $$\begin{array}{rll} I &= S K K:& a ⊃ a,\\ B &= S (K S) K:& (b ⊃ c) ⊃ (a ⊃ b) ⊃ a ⊃ c,\\ C &= S (B B S) (K K):& (a ⊃ b ⊃ c) ⊃ b ⊃ a ⊃ c,\\ W &= S S (K I):& (a ⊃ a ⊃ b) ⊃ a ⊃ b,\\ T &= B (S I) K:& a ⊃ (a ⊃ b) ⊃ b,\\ U &= S I:& ((a ⊃ b) ⊃ a) ⊃ (a ⊃ b) ⊃ b. \end{array}$$

As an example and illustration, the proof is provided in line-by-line form for $$T = B (S I) K$$: $$\begin{array}{ll} B:& (e ⊃ d) ⊃ (a ⊃ e) ⊃ a ⊃ d,\\ S:& (c ⊃ a ⊃ b) ⊃ (c ⊃ a) ⊃ c ⊃ b,\\ I:& c ⊃ c,\\ S I:& (c ⊃ a) ⊃ c ⊃ b,\\ B (S I):& (a ⊃ e) ⊃ a ⊃ d,\\ K:& a ⊃ c ⊃ a,\\ B (S I) K:& a ⊃ d, \end{array}$$ where the requirement that the modus ponens fits for $$S I$$, $$B (S I)$$ and $$B (S I) K$$ imposes the following constraints: $$c = a ⊃ b,\quad e = c ⊃ a,\quad d = c ⊃ b,$$ so that the final result yields $$T = B (S I) K: a ⊃ d = a ⊃ (a ⊃ b) ⊃ b.$$

Fourth: an equivalence relation between proofs can be defined, where $$f = g$$ may occur for two proofs $$f$$ and $$g$$ that yield the same results. For instance, if $$x: a$$, while we also have $$I x: a$$. If $$f: a$$ and $$x: b$$, then $$K f x: a$$. Finally, if $$f: a ⊃ b ⊃ c$$, $$g: a ⊃ b$$ and $$x: a$$, then $$f x: b ⊃ c$$, $$g x: b$$, so that $$f x (g x): c$$, while we also have $$S f g x: c$$.

Other relations may be imposed for $$π_0$$, $$π_1$$ and $$A$$: if $$x: a$$, $$y: b$$, then $$(x,y): a ∧ b$$, $$π_0(x,y): a$$, $$π_1(x,y): b$$. If $$z: a ∧ b$$, then $$π_0 z: a$$, $$π_1 z: b$$ and $$(π_0 z, π_1 z): a ∧ b$$.

On this basis we may assert the following proof equivalences: $$I x = x,\quad K f x = f,\quad S f g x = f x (g x),\\ π_0(x,y) = x,\quad π_1(x,y) = y,\quad (π_0 z, π_1 z) = z\quad (z: a ∧ b),$$ the last one being constrained in its range of application.

Based on this, we have the following equivalence $$B f = S (K S) K f = K S f (K f) = S (K f),$$ as well as the following, which may be derived similarly: $$\begin{array}{rcl} U g &=& S I g,\\ W f &=& S f I,\\ T g &=& S I (K g),\\ B f g &=& S (K f) g,\\ C f g &=& S f (K g). \end{array}$$

With the inclusion of additional arguments, this can be further developed to the following: $$U g x = x (g x),\quad W f x = f x x,\quad T g x = x g,\quad B f g x = f (g x),\quad C f g x = f x g.$$

It is actually possible to go even further and define $$\left(\begin{matrix} f: b ⊃ c\\g: a ⊃ b \end{matrix}\right) → f ∘ g ≡ B f g: a ⊃ c$$ and assert additional equivalences such as $$f ∘ I = f = I ∘ f,\quad (f ∘ g) ∘ h = f ∘ g ∘ h = f ∘ (g ∘ h).$$ The corresponding equivalence rule, as one might expect: $$(f ∘ g) x = f (g x)$$, which is just the rule for $$B$$. One consequence of this is that $$f = f ∘ I = B f I = S (K f) I.$$

Fifth: what we need the most, here, is the Deduction Theorem, which states that given a proof $$φ(x): b$$ that depends on a stipulation $$x: a$$, there should exist a proof $$λx·φ(x): a ⊃ b$$, such that $$λx·φ(x)$$ is free of any occurrences of the stipulation/hypothetical $$x$$, such that $$(λx·φ(x))x = φ(x)$$. In fact, we can define it inductively over the structure of $$φ(x)$$ by: $$λx·x = I,\quad λx·a = K a,\quad λx·a x = a,\\ λx·u x = W a,\quad λx·u b = C a b,\quad λx·x b = T b,\\ λx·x v = U b,\quad λx·a v = B a b,\quad λx·u v = S a b,$$ where $$a$$ and $$b$$ are free of any occurrences of $$x$$ in them, $$u$$ and $$v$$ each have at least one occurrence of $$x$$ in them, but with $$u ≠ x ≠ v$$, with $$λx·u = a$$, $$λx·v = b$$, such that $$a x = u$$, and $$b x = v$$.

Yes, I sneaked in the Curry-Howard-Lambek Correspondence. The Deduction Theorem, in particular, corresponds to taking the "λ-abstractions", such as what was laid out above. There are other λ-abstraction algorithms, but this one will best suit our purposes.

We can go even further and work with structured stipulations/hypotheticals. For instance, if $$x: a$$ and $$y: b$$, with $$φ(x,y): c$$, then we may write $$λ(x,y)·φ(x,y) ≡ λz·φ(π_0z,π_1z): a ∧ b ⊃ c.$$

In particular, we have the following equivalences $$λ(x,y)·x = λz·π_0 z = π_0,\quad λ(x,y)·y = λz·π_1 z = π_1.$$

Finally, note that the term $$x x$$ cannot be made consistent with modus ponens, since this would require a proof of the form $$x: (((⋯) ⊃ a) ⊃ a) ⊃ a$$, yielding the proof $$x x: a$$. However, we could still add in $$D = λx·x x$$, just to round out the inductive construction of $$λx·φ(x)$$, and pretend it's well-defined, even though its proof would be $$D: (((⋯) ⊃ a) ⊃ a) ⊃ a$$. However, we're not going to need or use it anywhere.

Proof Of Distributivity I:
Now, with the preliminaries laid out, watch and see how fast the problem gets crunched.

First, to establish $$Δ_0: a ∧ (b ∨ c) ⊃ (a ∧ b) ∨ (a ∧ c),$$ let $$x: a,\quad y: b ∨ c,\quad v: b,\quad w: c.$$ Then $$(x,v): a ∧ b\quad→ σ_0(x,v): (a ∧ b) ∨ (a ∧ c)\quad→ υ_0 ≡ λv·σ_0(x,v): b ⊃ (a ∧ b) ∨ (a ∧ c),\\ (x,w): a ∧ c\quad→ σ_1(x,w): (a ∧ b) ∨ (a ∧ c)\quad→ υ_1 ≡ λw·σ_1(x,w): c ⊃ (a ∧ b) ∨ (a ∧ c).$$ Therefore, $$[υ_0,υ_1]: b ∨ c ⊃ (a ∧ b) ∨ (a ∧ c)\quad → [υ_0,υ_1] y: (a ∧ b) ∨ (a ∧ c).$$ Noting that $$(x,y): a ∧ (b ∨ c)$$, we have $$Δ_0 ≡ λ(x,y)·[υ_0,υ_1] y: a ∧ (b ∨ c) ⊃ (a ∧ b) ∨ (a ∧ c).$$

This can be worked out in detail $$υ_0 = λv·σ_0(x,v) = λv·σ_0(A x v) = B σ_0 (A x),\\ υ_1 = λw·σ_1(x,w) = λw·σ_1(A x w) = B σ_1 (A x),\\ λ(x,y)·[υ_0, υ_1] y = λ(x,y)·O υ_0 υ_1 y = λz·O \bar υ_0 \bar υ_1 (π_1 z),$$ where $$\bar υ_0 = B σ_0 (A (π_0 z)),\quad \bar υ_1 = B σ_1 (A (π_0 z)).$$ Their respective λ-abstractions may then be worked out: $$\bar τ_0 = λz·\bar υ_0 = B (B σ_0) (B A π_0) = (B σ_0) ∘ A ∘ π_0,\\ \bar τ_1 = λz·\bar υ_1 = B (B σ_1) (B A π_0) = (B σ_1) ∘ A ∘ π_0.$$ Therefore, $$λz·O \bar υ_0 \bar υ_1 (π_1 z) = S (λz·O \bar υ_0 \bar υ_1) π_1,\\ λz·O \bar υ_0 \bar υ_1 = S (λz·O \bar υ_0) \bar τ_1,\\ λz·O \bar υ_0 = B O \bar τ_0.\\$$ Thus, $$Δ_0 = λz·O \bar υ_0 \bar υ_1 (π_1 z) = S (S (B O \bar τ_0) \bar τ_1) π_1.$$

Expressed in pure $$SK$$ form, noting that $$B O = S (K O)$$, with other combinations of $$B$$ similarly eliminated: $$\bar τ_0 = S (K (S (K σ_0))) (S (K A) π_0),\\ \bar τ_1 = S (K (S (K σ_1))) (S (K A) π_0),\\ Δ_0 = S (S (S (K O) \bar τ_0) \bar τ_1) π_1.$$ If written in line-by-line form, the $$\bar τ$$'s each use 9 axioms, and the overall term $$Δ_0$$ use 6 more axioms, for a total of 24 axioms, connected by 23 modus ponens, for a total of 47 lines.

You can write out the lines, if you wish, but there's no reason to (other than to check for errors and validate the result), since everything you need is already contained in this formula.

Proof Of Distributivity II:
For the converse, we want $$Δ_1: (a ∧ b) ∨ (a ∧ c) ⊃ a ∧ (b ∨ c).$$

Let $$w: a,\quad x: b,\quad y: c.$$ Then, noting that $$(w,x): a ∧ b$$ and $$(w,y): a ∧ c$$, we have $$σ_0x: b ∨ c ⇒ (w,σ_0x): a ∧ (b ∨ c) ⇒ λ(w,x)·(w,σ_0x): a ∧ b ⊃ a ∧ (b ∨ c),\\ σ_1y: b ∨ c ⇒ (w,σ_1y): a ∧ (b ∨ c) ⇒ λ(w,y)·(w,σ_1y): a ∧ c ⊃ a ∧ (b ∨ c).$$ Thus $$Δ_1 = [λ(w,x)·(w,σ_0x), λ(w,y)·(w,σ_1y)]: (a ∧ b) ∨ (a ∧ c) ⊃ a ∧ (b ∨ c).$$

Working this out in detail, we get $$(w,σ_0x) = Aw(σ_0 x) ⇒ λ(w,x).(w, σ_0 x) = λz·A (π_0 z) (σ_0 (π_1 z)) = S (B A π_0) (B σ_0 π_1),\\ (w,σ_1y) = Aw(σ_1 y) ⇒ λ(w,y).(w, σ_1 y) = λz·A (π_0 z) (σ_1 (π_1 z)) = S (B A π_0) (B σ_1 π_1).$$ Thus $$Δ_1 = O (L_1 (B σ_0 π_1)) (L_1 (B σ_1 π_1))$$ where $$L_1 = S (B A π_0).$$ You can consolidate this, by noting that $$L_1 (B φ π_1) = L_1 (C B π_1 φ) = B L_1 (C B π_1) φ = L_2 φ,$$ where $$L_2 = B L_1 (C B π_1) = L_1 ∘ (C B π_1).$$ So, we can write $$Δ_1 = O (L_2 σ_0) (L_2 σ_1) = [L_2 σ_0, L_2 σ_1],$$ where $$L_2 = B (S (B A π_0)) (C B π_1) = (S (A ∘ π_0)) ∘ (C B π_1).$$

Reducing the $$BC$$ form to $$SK$$ form, we have: $$L_2 = S (K (S (S (K A) π_0))) (S (S (K S) K) (K π_1)).$$ That's 14 axioms and 13 modus ponens for 27 lines. Therefore, $$Δ_1$$ is 3 + 14 + 14 axioms, for a total of 31, and 30 modus ponens, for 61 lines. The proofs are a lot smaller when you factor out the lemmas $$L_1$$ and $$L_2$$, and use $$B$$ and $$C$$.

More Examples - The Curry Rule And Its Inverse.
Consider next the Curry Rule and its inverse: $$⋀: (a ∧ b ⊃ c) ⊃ a ⊃ b ⊃ c,\quad ⋁: (a ⊃ b ⊃ c) ⊃ a ∧ b ⊃ c.$$

For the Curry Rule, in cursory form, we have the following: $$f: a ∧ b ⊃ c,\quad x: a,\quad y: b,\\ (x,y): a ∧ b,\quad f (x,y): c,\\ λy·f(x,y): b ⊃ c,\quad λx·λy·f(x,y): a ⊃ b ⊃ c,\\ ⋀ ≡ λf·λx·λy·f(x,y): (a ∧ b ⊃ c) ⊃ a ⊃ b ⊃ c.$$

Worked out in detail, $$f(x,y) = f (A x y) = B f (A x) y = B (B f) A x y = C (B B B) A f x y,\\ ⋀ = C (B B B) A.$$

For the Inverse Curry Rule, we have the following development: $$g: a ⊃ b ⊃ c,\quad x: a,\quad y: b,\\ g x: b ⊃ c,\quad g x y: c,\quad (x,y): a ∧ b,\\ λ(x,y)·g x y = λz·g (π_0 z) (π_1 z): a ∧ b ⊃ c,\\ ⋁ ≡ λg·λ(x,y)·g x y: (a ⊃ b ⊃ c) ⊃ a ∧ b ⊃ c$$ When worked out in detail $$g (π_0 z) (π_1 z) = B g π_0 z (π_1 z) = S (B g π_0) π_1 z$$ this leads to $$λz·S (B g π_0) π_1 z = S (B g π_0) π_1,\\ S (B g π_0) π_1 = S (C B π_0 g) π_1 = B S (C B π_0) g π_1 = C (B S (C B π_0)) π_1 g,\\ ⋁ ≡ λg·S (B g π_0) π_1 = C (B S (C B π_0)) π_1$$

Other Examples: Formulas With Negation
Proofs involving negation are more difficult. But, a few worthy of note are $$V ≡ B Z K: ¬a ⊃ a ⊃ b,\quad N ≡ W (B Z V): ¬¬a ⊃ a,\quad N^{-1} ≡ Z N: a ⊃ ¬¬a.$$ Rules, such as $$(¬a ⊃ a) ⊃ a$$ or $$(a ⊃ b) ⊃ ¬a ∨ b$$, on the other hand, are harder to establish.

The name $$N^{-1}$$ isn't really justified, unless (or until) enough equivalence rules have been laid out for $$Z$$ to allow one to prove that $$N ∘ Z N = I$$ and that $$Z (Z (Z N ∘ N)) = I$$. The restricted form of the second identity is because $$Z N ∘ N: ¬¬a ⊃ ¬¬a$$ has a constraint on the propositions, which is undone by two applications of $$Z$$, while $$N ∘ Z N: a ⊃ a$$ is not constrained.

I don't know of any system of equational axioms that works with $$Z$$.