1
$\begingroup$

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

  • 0
    @Tegiri: Your listed rules are not inconsistent: the$y$ havee a model with one element, all binar$y$ operations the obvious ones, and all nullar$y$ operations the unique element.2011-03-19

2 Answers 2

1

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 \ne 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\:.$

  • 0
    Here is automatic proof, which is identical to Bill's. The culprit was to go after correct goal! 1$0$^ x =$0$# label(non_clause) # label(goal). [goal]. 4 x ^ (x v y) = x. [assumption]. 10$0$^ x = 1. [assumption]. 11 0 ^ c1 != 0. [deny(1)]. 12 0 != 1. [copy(11),rewrite([10(3)]),flip(a)]. 30 0 = 1. [para(10(a,1),4(a,1)),flip(a)]. 31 $F. [resolve(30,a,12,a)].2011-03-21
0

Solved the remaining bit of the puzzle: GCD(0,8)≠0.

1 v x = x ⇒  1 v 0 = 0 0 ^ x = 0 ⇒  1 ^ 0 = 0   1 v 0 = 1 ^ 0 ⇒  1 = 0