can GCD(0,8)≠1 be proven purely by lattice laws? Triggered by previous question, can one prove GCD(0,8)≠1 purely by lattice laws? Brute force Prover9/Mace4 assertions x ^ y = y ^ x. (x ^ y) ^ z = x ^ (y ^ z). x ^ (x v y) = x. x v y = y v x. (x v y) v z = x v (y v z). x v (x ^ y) = x. 1 v x = x. 1 ^ x = 1. 0 ^ x = 1. exhibit no [finite] model, which is indication that the system is inconsistent. I have trouble, however, understanding how to elevate this intuition into a formal proof (there is no goal).

Note $\rm\ x = 0\ $ in $\rm\ x \wedge (x \vee y)\ =\ x\ \ \Rightarrow\ \ 0\wedge (0\vee y)\ =\ 0\ \ $ contra $\rm\ \ 0\wedge x\ =\ 1\ \ $ (presuming $\rm\ 0 \
e 1\:$).

Alternatively, recall that the idempotent laws follows from the absorption laws, viz.

$$\rm x\wedge x\ =\ x\wedge (x\vee (x\wedge x))\ =\ x $$

Hence $\rm\ \ 0\wedge 0\ =\ 0\ \ $ contra $\rm\ \ 0\wedge x\ =\ 1\:.$