Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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

share|improve this question
    
Do you have x ^ x = x from your laws ? –  mercio Mar 18 '11 at 21:20
    
@chandok: Yes, it is redundant. –  Tegiri Nenashi Mar 18 '11 at 21:28
    
Is 0 v x = 1 correct? –  Myself Mar 19 '11 at 1:24
    
That is what the original thread suggested. It has been refuted together with another option: 0 v x = 1. The correct version is 0 v x = x and, predictably, Mace4 generates 2 element model. I'm interested, however disproving the wrong assertion 0 v x = 1. I tried putting its negation into Prover9 goal, still Prover9 doesn't seem to be able to derive it. –  Tegiri Nenashi Mar 19 '11 at 1:36
    
@Tegiri: You either have things backward, or you are viewing the divisibility order backwards, with $a|b$ meaning $b\leq a$... –  Arturo Magidin Mar 19 '11 at 2:00
show 3 more comments

2 Answers

up vote 1 down vote accepted

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

share|improve this answer
    
Just to clarify: you are using $0$ and $1$ to denote the corresponding integers, and not to denote the infimum and supremum of the lattice, correct? –  Arturo Magidin Mar 19 '11 at 21:21
    
No, the above is in the equational theory that the OP gave. –  Bill Dubuque Mar 19 '11 at 21:37
    
@Bill: Right: so that $0$ denotes the usual $0$, not the least element of the lattice. (His theory includes, e.g., $1\lor x = x$, which of course means that "1" does not represent the maximum, as is standard in 01-lattices). –  Arturo Magidin Mar 19 '11 at 21:39
    
@Arturo: Possible models are not relevant to the above equational proof (other than the assumption that $\rm\ 0 \ne 1\:$). –  Bill Dubuque Mar 19 '11 at 21:57
    
I tried absorption and even distributivity, but this rather simple proof escaped me. Thank you. –  Tegiri Nenashi Mar 21 '11 at 19:21
show 1 more comment

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
share|improve this answer
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.