Theorem List for Quantum Logic Explorer - 401-500   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremwbile 401 Biconditional to l.e. (Contributed by NM, 13-Oct-1997.)
(ab) = 1       (a2 b) = 1

Theoremwlebi 402 L.e. to biconditional. (Contributed by NM, 13-Oct-1997.)
(a2 b) = 1    &   (b2 a) = 1       (ab) = 1

Theoremwle2or 403 Disjunction of 2 l.e.'s. (Contributed by NM, 13-Oct-1997.)
(a2 b) = 1    &   (c2 d) = 1       ((ac) ≤2 (bd)) = 1

Theoremwle2an 404 Conjunction of 2 l.e.'s. (Contributed by NM, 13-Oct-1997.)
(a2 b) = 1    &   (c2 d) = 1       ((ac) ≤2 (bd)) = 1

Theoremwledi 405 Half of distributive law. (Contributed by NM, 13-Oct-1997.)
(((ab) ∪ (ac)) ≤2 (a ∩ (bc))) = 1

Theoremwledio 406 Half of distributive law. (Contributed by NM, 13-Oct-1997.)
((a ∪ (bc)) ≤2 ((ab) ∩ (ac))) = 1

Theoremwcom0 407 Commutation with 0. Kalmbach 83 p. 20. (Contributed by NM, 13-Oct-1997.)
C (a, 0) = 1

Theoremwcom1 408 Commutation with 1. Kalmbach 83 p. 20. (Contributed by NM, 13-Oct-1997.)
C (1, a) = 1

Theoremwlecom 409 Comparable elements commute. Beran 84 2.3(iii) p. 40. (Contributed by NM, 13-Oct-1997.)
(a2 b) = 1        C (a, b) = 1

Theoremwbctr 410 Transitive inference. (Contributed by NM, 13-Oct-1997.)
(ab) = 1    &    C (b, c) = 1        C (a, c) = 1

Theoremwcbtr 411 Transitive inference. (Contributed by NM, 13-Oct-1997.)
C (a, b) = 1    &   (bc) = 1        C (a, c) = 1

Theoremwcomorr 412 Weak commutation law. (Contributed by NM, 13-Oct-1997.)
C (a, (ab)) = 1

Theoremwcoman1 413 Weak commutation law. (Contributed by NM, 13-Oct-1997.)
C ((ab), a) = 1

Theoremwcomcom 414 Commutation is symmetric. Kalmbach 83 p. 22. (Contributed by NM, 13-Oct-1997.)
C (a, b) = 1        C (b, a) = 1

Theoremwcomcom2 415 Commutation equivalence. Kalmbach 83 p. 23. (Contributed by NM, 13-Oct-1997.)
C (a, b) = 1        C (a, b ) = 1

Theoremwcomcom3 416 Commutation equivalence. Kalmbach 83 p. 23. (Contributed by NM, 13-Oct-1997.)
C (a, b) = 1        C (a , b) = 1

Theoremwcomcom4 417 Commutation equivalence. Kalmbach 83 p. 23. (Contributed by NM, 13-Oct-1997.)
C (a, b) = 1        C (a , b ) = 1

Theoremwcomd 418 Commutation dual. Kalmbach 83 p. 23. (Contributed by NM, 13-Oct-1997.)
C (a, b) = 1       (a ≡ ((ab) ∩ (ab ))) = 1

Theoremwcom3ii 419 Lemma 3(ii) of Kalmbach 83 p. 23. (Contributed by NM, 13-Oct-1997.)
C (a, b) = 1       ((a ∩ (ab)) ≡ (ab)) = 1

Theoremwcomcom5 420 Commutation equivalence. Kalmbach 83 p. 23. (Contributed by NM, 13-Oct-1997.)
C (a , b ) = 1        C (a, b) = 1

Theoremwcomdr 421 Commutation dual. Kalmbach 83 p. 23. (Contributed by NM, 13-Oct-1997.)
(a ≡ ((ab) ∩ (ab ))) = 1        C (a, b) = 1

Theoremwcom3i 422 Lemma 3(i) of Kalmbach 83 p. 23. (Contributed by NM, 13-Oct-1997.)
((a ∩ (ab)) ≡ (ab)) = 1        C (a, b) = 1

Theoremwfh1 423 Weak structural analog of Foulis-Holland Theorem. (Contributed by NM, 13-Oct-1997.)
C (a, b) = 1    &    C (a, c) = 1       ((a ∩ (bc)) ≡ ((ab) ∪ (ac))) = 1

Theoremwfh2 424 Weak structural analog of Foulis-Holland Theorem. (Contributed by NM, 13-Oct-1997.)
C (a, b) = 1    &    C (a, c) = 1       ((b ∩ (ac)) ≡ ((ba) ∪ (bc))) = 1

Theoremwfh3 425 Weak structural analog of Foulis-Holland Theorem. (Contributed by NM, 13-Oct-1997.)
C (a, b) = 1    &    C (a, c) = 1       ((a ∪ (bc)) ≡ ((ab) ∩ (ac))) = 1

Theoremwfh4 426 Weak structural analog of Foulis-Holland Theorem. (Contributed by NM, 13-Oct-1997.)
C (a, b) = 1    &    C (a, c) = 1       ((b ∪ (ac)) ≡ ((ba) ∩ (bc))) = 1

Theoremwcom2or 427 Thm. 4.2 Beran p. 49. (Contributed by NM, 10-Nov-1998.)
C (a, b) = 1    &    C (a, c) = 1        C (a, (bc)) = 1

Theoremwcom2an 428 Thm. 4.2 Beran p. 49. (Contributed by NM, 10-Nov-1998.)
C (a, b) = 1    &    C (a, c) = 1        C (a, (bc)) = 1

Theoremwnbdi 429 Negated biconditional (distributive form) (Contributed by NM, 13-Oct-1997.)
((ab) ≡ (((ab) ∩ a ) ∪ ((ab) ∩ b ))) = 1

Theoremwlem14 430 Lemma for KA14 soundness. (Contributed by NM, 25-Oct-1997.)
(((ab ) ∪ a ) ∪ ((ab ) ∪ ((a ∩ ((ab ) ∩ (ab))) ∪ (a ∩ ((ab ) ∩ (ab)) )))) = 1

Theoremwr5 431 Proof of weak orthomodular law from weaker-looking equivalent, wom3 367, which in turn is derived from ax-wom 361. (Contributed by NM, 25-Oct-1997.)
(ab) = 1       ((ac) ≡ (bc)) = 1

0.2.4  Kalmbach axioms (soundness proofs) that require WOML

Theoremska2 432 Soundness theorem for Kalmbach's quantum propositional logic axiom KA2. (Contributed by NM, 10-Nov-1998.)
((ab) ∪ ((bc) ∪ (ac))) = 1

Theoremska4 433 Soundness theorem for Kalmbach's quantum propositional logic axiom KA4. (Contributed by NM, 9-Nov-1998.)
((ab) ∪ ((ac) ≡ (bc))) = 1

Theoremwom2 434 Weak orthomodular law for study of weakly orthomodular lattices. (Contributed by NM, 13-Nov-1998.)
a ≤ ((ab) ∪ ((ac) ≡ (bc)))

Theoremka4ot 435 3-variable version of weakly orthomodular law. It is proved from a weaker-looking equivalent, wom2 434, which in turn is proved from ax-wom 361. (Contributed by NM, 25-Oct-1997.)
((ab) ∪ ((ac) ≡ (bc))) = 1

0.2.5  Weak orthomodular law variants

Theoremwoml6 436 Variant of weakly orthomodular law. (Contributed by NM, 14-Nov-1998.)
((a1 b) ∪ (a2 b)) = 1

Theoremwoml7 437 Variant of weakly orthomodular law. (Contributed by NM, 14-Nov-1998.)
(((a2 b) ∩ (b2 a)) ∪ (ab)) = 1

Theoremortha 438 Property of orthogonality. (Contributed by NM, 10-Mar-2002.)
ab       (ab) = 0

0.3  Orthomodular lattices

0.3.1  Orthomodular law

Axiomax-r3 439 Orthomodular law - when added to an ortholattice, it makes the ortholattice an orthomodular lattice. See r3a 440 for a more compact version. (Contributed by NM, 12-Aug-1997.)
(cc ) = ((ab ) ∪ (ab) )       a = b

Theoremr3a 440 Orthomodular law restated. (Contributed by NM, 12-Aug-1997.)
1 = (ab)       a = b

Theoremwed 441 Weak equivalential detachment (WBMP). (Contributed by NM, 10-Aug-1997.)
a = b    &   (ab) = (cd)       c = d

Theoremr3b 442 Orthomodular law from weak equivalential detachment (WBMP). (Contributed by NM, 10-Aug-1997.)
(cc ) = (ab)       a = b

Theoremlem3.1 443 Lemma used in proof of Thm. 3.1 of Pavicic 1993. (Contributed by NM, 12-Aug-1997.)
(ab) = b    &   (ba) = 1       a = b

Theoremlem3a.1 444 Lemma used in proof of Thm. 3.1 of Pavicic 1993. (Contributed by NM, 12-Aug-1997.)
(ab) = b    &   (ba) = 1       (ab) = a

Theoremoml 445 Orthomodular law. Compare Thm. 1 of Pavicic 1987. (Contributed by NM, 12-Aug-1997.)
(a ∪ (a ∩ (ab))) = (ab)

Theoremomln 446 Orthomodular law. (Contributed by NM, 2-Nov-1997.)
(a ∪ (a ∩ (ab))) = (ab)

Theoremomla 447 Orthomodular law. (Contributed by NM, 7-Nov-1997.)
(a ∩ (a ∪ (ab))) = (ab)

Theoremomlan 448 Orthomodular law. (Contributed by NM, 7-Nov-1997.)
(a ∩ (a ∪ (ab))) = (ab)

Theoremoml5 449 Orthomodular law. (Contributed by NM, 16-Nov-1997.)
((ab) ∪ ((ab) ∩ (bc))) = (bc)

Theoremoml5a 450 Orthomodular law. (Contributed by NM, 16-Nov-1997.)
((ab) ∩ ((ab) ∪ (bc))) = (bc)

0.3.2  Relationship analogues using OML (ordering; commutation)

Theoremoml2 451 Orthomodular law. Kalmbach 83 p. 22. (Contributed by NM, 27-Aug-1997.)
ab       (a ∪ (ab)) = b

Theoremoml3 452 Orthomodular law. Kalmbach 83 p. 22. (Contributed by NM, 27-Aug-1997.)
ab    &   (ba ) = 0       a = b

Theoremcomcom 453 Commutation is symmetric. Kalmbach 83 p. 22. (Contributed by NM, 27-Aug-1997.)
a C b       b C a

Theoremcomcom3 454 Commutation equivalence. Kalmbach 83 p. 23. (Contributed by NM, 27-Aug-1997.)
a C b       a C b

Theoremcomcom4 455 Commutation equivalence. Kalmbach 83 p. 23. (Contributed by NM, 27-Aug-1997.)
a C b       a C b

Theoremcomd 456 Commutation dual. Kalmbach 83 p. 23. (Contributed by NM, 27-Aug-1997.)
a C b       a = ((ab) ∩ (ab ))

Theoremcom3ii 457 Lemma 3(ii) of Kalmbach 83 p. 23. (Contributed by NM, 27-Aug-1997.)
a C b       (a ∩ (ab)) = (ab)

Theoremcomcom5 458 Commutation equivalence. Kalmbach 83 p. 23. (Contributed by NM, 27-Aug-1997.)
a C b       a C b

Theoremcomcom6 459 Commutation equivalence. Kalmbach 83 p. 23. (Contributed by NM, 26-Nov-1997.)
a C b       a C b

Theoremcomcom7 460 Commutation equivalence. Kalmbach 83 p. 23. (Contributed by NM, 26-Nov-1997.)
a C b       a C b

Theoremcomor1 461 Commutation law. (Contributed by NM, 9-Nov-1997.)
(ab) C a

Theoremcomor2 462 Commutation law. (Contributed by NM, 9-Nov-1997.)
(ab) C b

Theoremcomorr2 463 Commutation law. (Contributed by NM, 26-Nov-1997.)
b C (ab)

Theoremcomanr1 464 Commutation law. (Contributed by NM, 26-Nov-1997.)
a C (ab)

Theoremcomanr2 465 Commutation law. (Contributed by NM, 26-Nov-1997.)
b C (ab)

Theoremcomdr 466 Commutation dual. Kalmbach 83 p. 23. (Contributed by NM, 27-Aug-1997.)
a = ((ab) ∩ (ab ))       a C b

Theoremcom3i 467 Lemma 3(i) of Kalmbach 83 p. 23. (Contributed by NM, 28-Aug-1997.)
(a ∩ (ab)) = (ab)       a C b

Theoremdf2c1 468 Dual 'commutes' analogue for analogue of =. (Contributed by NM, 20-Sep-1998.)
a = ((ab) ∩ (ab ))       a C b

Theoremfh1 469 Foulis-Holland Theorem. (Contributed by NM, 29-Aug-1997.)
a C b    &   a C c       (a ∩ (bc)) = ((ab) ∪ (ac))

Theoremfh2 470 Foulis-Holland Theorem. (Contributed by NM, 29-Aug-1997.)
a C b    &   a C c       (b ∩ (ac)) = ((ba) ∪ (bc))

Theoremfh3 471 Foulis-Holland Theorem. (Contributed by NM, 29-Aug-1997.)
a C b    &   a C c       (a ∪ (bc)) = ((ab) ∩ (ac))

Theoremfh4 472 Foulis-Holland Theorem. (Contributed by NM, 29-Aug-1997.)
a C b    &   a C c       (b ∪ (ac)) = ((ba) ∩ (bc))

Theoremfh1r 473 Foulis-Holland Theorem. (Contributed by NM, 23-Nov-1997.)
a C b    &   a C c       ((bc) ∩ a) = ((ba) ∪ (ca))

Theoremfh2r 474 Foulis-Holland Theorem. (Contributed by NM, 23-Nov-1997.)
a C b    &   a C c       ((ac) ∩ b) = ((ab) ∪ (cb))

Theoremfh3r 475 Foulis-Holland Theorem. (Contributed by NM, 23-Nov-1997.)
a C b    &   a C c       ((bc) ∪ a) = ((ba) ∩ (ca))

Theoremfh4r 476 Foulis-Holland Theorem. (Contributed by NM, 23-Nov-1997.)
a C b    &   a C c       ((ac) ∪ b) = ((ab) ∩ (cb))

Theoremfh2c 477 Foulis-Holland Theorem. (Contributed by NM, 20-Sep-1998.)
a C b    &   a C c       (b ∩ (ca)) = ((bc) ∪ (ba))

Theoremfh4c 478 Foulis-Holland Theorem. (Contributed by NM, 20-Sep-1998.)
a C b    &   a C c       (b ∪ (ca)) = ((bc) ∩ (ba))

Theoremfh1rc 479 Foulis-Holland Theorem. (Contributed by NM, 10-Mar-2002.)
a C b    &   a C c       ((cb) ∩ a) = ((ca) ∪ (ba))

Theoremfh2rc 480 Foulis-Holland Theorem. (Contributed by NM, 20-Sep-1998.)
a C b    &   a C c       ((ca) ∩ b) = ((cb) ∪ (ab))

Theoremfh3rc 481 Foulis-Holland Theorem. (Contributed by NM, 6-Aug-2001.)
a C b    &   a C c       ((cb) ∪ a) = ((ca) ∩ (ba))

Theoremfh4rc 482 Foulis-Holland Theorem. (Contributed by NM, 20-Sep-1998.)
a C b    &   a C c       ((ca) ∪ b) = ((cb) ∩ (ab))

Theoremcom2or 483 Thm. 4.2 Beran p. 49. (Contributed by NM, 7-Nov-1997.)
a C b    &   a C c       a C (bc)

Theoremcom2an 484 Thm. 4.2 Beran p. 49. (Contributed by NM, 7-Nov-1997.)
a C b    &   a C c       a C (bc)

Theoremcombi 485 Commutation theorem for Sasaki implication. (Contributed by NM, 25-Oct-1998.)
a C (ab)

Theoremnbdi 486 Negated biconditional (distributive form) (Contributed by NM, 30-Aug-1997.)
(ab) = (((ab) ∩ a ) ∪ ((ab) ∩ b ))

Theoremoml4 487 Orthomodular law. (Contributed by NM, 25-Oct-1997.)
((ab) ∩ a) ≤ b

Theoremoml6 488 Orthomodular law. (Contributed by NM, 3-Jan-1999.)
(a ∪ (b ∩ (ab ))) = (ab)

Theoremgsth 489 Gudder-Schelp's Theorem. Beran, p. 262, Thm. 4.1. (Contributed by NM, 20-Sep-1998.)
a C b    &   b C c    &   a C (bc)       (ab) C c

Theoremgsth2 490 Stronger version of Gudder-Schelp's Theorem. Beran, p. 263, Thm. 4.2. (Contributed by NM, 20-Sep-1998.)
b C c    &   a C (bc)       (ab) C c

Theoremgstho 491 "OR" version of Gudder-Schelp's Theorem. (Contributed by NM, 19-Oct-1998.)
b C c    &   a C (bc)       (ab) C c

Theoremgt1 492 Part of Lemma 1 from Gaisi Takeuti, "Quantum Set Theory". (Contributed by NM, 2-Dec-1998.)
a = (bc)    &   bd    &   cd       a C d

0.3.3  Commutator (orthomodular lattice theorems)

Theoremcmtr1com 493 Commutator equal to 1 commutes. Theorem 2.11 of Beran, p. 86. (Contributed by NM, 24-Jan-1999.)
C (a, b) = 1       a C b

Theoremcomcmtr1 494 Commutation implies commutator equal to 1. Theorem 2.11 of Beran, p. 86. (Contributed by NM, 24-Jan-1999.)
a C b        C (a, b) = 1

Theoremi0cmtrcom 495 Commutator element 0 commutator implies commutation. (Contributed by NM, 24-Jan-1999.)
(a0 C (a, b)) = 1       a C b

0.3.4  Kalmbach conditional

Theoremi3bi 496 Kalmbach implication and biconditional. (Contributed by NM, 5-Nov-1997.)
((a3 b) ∩ (b3 a)) = (ab)

Theoremi3or 497 Kalmbach implication OR builder. (Contributed by NM, 26-Dec-1997.)
((ab) ∪ ((ac) →3 (bc))) = 1

Theoremdf2i3 498 Alternate definition for Kalmbach implication. (Contributed by NM, 7-Nov-1997.)
(a3 b) = ((ab ) ∪ ((ab) ∩ (a ∪ (ab))))

Theoremdfi3b 499 Alternate Kalmbach conditional. (Contributed by NM, 6-Aug-2001.)
(a3 b) = ((ab) ∩ ((a ∪ (ab )) ∪ (ab)))

Theoremdfi4b 500 Alternate non-tollens conditional. (Contributed by NM, 6-Aug-2001.)
(a4 b) = ((ab) ∩ ((b ∪ (ba )) ∪ (ba)))

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1217
 Copyright terms: Public domain < Previous  Next >