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).