can be derived from AX together with V2 and V3. To simplify notation, I write ⊢ ϕ
′if the formula ϕ
′
can be derived from AX, and ⊢
+ ϕ
′if ϕ
′can be derived from AX + {V2, V3}.

I first need a technical lemma.

Lemma A.1 ⊢ (ϕ1  ϕ2 ∧ ϕ2  ϕ3) ⇒ (ϕ1 ∨ ϕ2)  ϕ3. Proof: By A1, ⊢ ϕ2  ϕ2, and by A4, ϕ1  ϕ2 ∧ ϕ2  ϕ2 ⇒ (ϕ1 ∨ ϕ2)  ψ. Thus,
⊢ (ϕ1  ϕ2) ⇒ (ϕ1 ∨ ϕ2)  ϕ2. (1)
Next observe that it easily follows from A1 and A4 that (a) ⊢ (ϕ1 ∧ ¬ϕ2)  (ϕ2 ⇒ ϕ3) (since
(ϕ1 ∧ ¬ϕ2) ⇒ (ϕ2 ⇒ ϕ3) is a tautology) and (b) ⊢ (ϕ2  ϕ3) ⇒ ϕ2  (ϕ2 ⇒ ϕ3) (since ϕ3 ⇒ (ϕ2 ⇒ ϕ3) is a tautology). By A4, RA1, and the observation that ((ϕ1∧¬ϕ2)∨ϕ2) ⇔ (ϕ1∨ϕ2)
is a tautology, we can conclude that
⊢ (ϕ2  ϕ3) ⇒ ((ϕ1 ∨ ϕ2)  (ϕ2 ⇒ ϕ3)). (2)
Let ψ be the formula (ϕ1  ϕ2 ∧ ϕ2  ϕ3). From (1) and (2), it follows that
⊢ ψ ⇒ ((ϕ1 ∨ ϕ2)  ϕ2) ∧ (ϕ1 ∨ ϕ2)  (ϕ2 ⇒ ϕ3)).

Applying A2 and RA1, it follows that
⊢ ψ ⇒ ((ϕ1 ∨ ϕ2)  ϕ3, as desired.

Now the proof is easy. By Lemma A.1, it follows that
⊢ (X1 = 1  X2 = 1) ∧ (X2 = 1  X3 **= 1)** ⇒
(X1 = 1 ∨ X2 = 1)  X3 = 1.

Applying the lemma again, we get that
⊢ (X1 = 1 ∨ X2 = 1)  X3 = 1 ∧ (X3 = 1  X1 **= 0)** ⇒
(X1 = 1 ∨ X2 = 1 ∨ X3 = 1)  X1 = 0.

Let ψ
′ be an abbreviation for X1 = 1∨ X2 = 1∨ X3 = 1. Thus, ⊢ ϕ ⇒ (ψ
′  X1 **= 0)**. An analogous argument shows that ⊢ ϕ ⇒ ψ
′  X2 **= 0)** and ⊢ ϕ ⇒ (ψ
′  X3 **= 0)**. By A2, we have that
⊢ ϕ ⇒ (ψ
′  (X1 = 0 ∧ X2 = 0 ∧ X3 **= 0)**. (3)
By V2, we have that ⊢
+ ψ
′ ⇒ (X1 6= 0 ∨ X2 6= 0 ∨ X3 6**= 0)**. Thus, by A1 and RA2, we have that
⊢
+ ϕ ⇒ (ψ
′  (X1 6= 0 ∧ X2 6= 0 ∧ X3 6**= 0)**. (4)
By A2, RA1, (3), and (4), we have that
⊢
+ ϕ ⇒ (ψ
′  **false**).

By V3, it follows that ⊢
+ ¬ϕ, as desired.

Note that all the axioms in AX other than A4 can be expressed using the language Luniq (provided that the formulas ϕ and ψ mentioned in these axioms are taken to be conjunctions of primitive propositions or just single primitive propositions, as appropriate). It is easy to check that all these axioms are valid in Tuniq, as are V2 and V3. Since ϕ is satisfiable in Tuniq, ¬ϕ cannot be proved from
(AX − {A4}) ∪ {V2,V3}.