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

Theoremi1abs 801 An absorption law for 1 . (Contributed by NM, 21-Feb-2002.)
((a1 b) ∪ (ab)) = a

Theoremtest 802 Part of an attempt to crack a potential Kalmbach axiom. (Contributed by NM, 29-Dec-1997.)
(((c ∪ (ab )) ∩ (c ∩ (c ∪ (ab)))) ∪ ((c ∩ (ab)) ∪ (c ∩ (c ∪ (ab))))) = ((c ∪ (ab)) ∩ (c ∪ (ab)))

Theoremtest2 803 Part of an attempt to crack a potential Kalmbach axiom. (Contributed by NM, 29-Dec-1997.)
(ab) ≤ ((ab) ∪ ((c ∪ (ab)) ∩ (c ∪ (ab))))

0.3.9  Some 3-variable theorems

Theorem3vth1 804 A 3-variable theorem. Equivalent to OML. (Contributed by NM, 18-Oct-1998.)
((a2 b) ∩ (bc) ) ≤ (a2 c)

Theorem3vth2 805 A 3-variable theorem. Equivalent to OML. (Contributed by NM, 18-Oct-1998.)
((a2 b) ∩ (bc) ) = ((a2 c) ∩ (bc) )

Theorem3vth3 806 A 3-variable theorem. Equivalent to OML. (Contributed by NM, 18-Oct-1998.)
((a2 c) ∪ ((a2 b) ∩ (bc) )) = (a2 c)

Theorem3vth4 807 A 3-variable theorem. (Contributed by NM, 18-Oct-1998.)
((a2 b)2 (bc)) = ((a2 c)2 (bc))

Theorem3vth5 808 A 3-variable theorem. (Contributed by NM, 18-Oct-1998.)
((a2 b)2 (bc)) = (c ∪ ((a2 b) ∩ (c2 b)))

Theorem3vth6 809 A 3-variable theorem. (Contributed by NM, 18-Oct-1998.)
((a2 b)2 (bc)) = (((a2 b) ∩ (c2 b)) ∪ ((a2 c) ∩ (b2 c)))

Theorem3vth7 810 A 3-variable theorem. (Contributed by NM, 18-Oct-1998.)
((a2 b)2 (bc)) = (a2 (bc))

Theorem3vth8 811 A 3-variable theorem. (Contributed by NM, 18-Oct-1998.)
(a2 (bc)) = (((a2 b) ∩ (c2 b)) ∪ ((a2 c) ∩ (b2 c)))

Theorem3vth9 812 A 3-variable theorem. (Contributed by NM, 16-Nov-1998.)
((ab) →1 (c2 b)) = ((bc) →2 (a2 b))

Theorem3vcom 813 3-variable commutation theorem. (Contributed by NM, 19-Mar-1999.)
((a1 c) ∪ (b1 c)) C ((a1 c) ∩ (b1 c))

Theorem3vded11 814 A 3-variable theorem. Experiment with weak deduction theorem. (Contributed by NM, 25-Oct-1998.)
b ≤ (c1 (b1 a))       c ≤ (b1 a)

Theorem3vded12 815 A 3-variable theorem. Experiment with weak deduction theorem. (Contributed by NM, 25-Oct-1998.)
(a ∩ (c1 a)) ≤ (c1 (b1 a))    &   ca       c ≤ (b1 a)

Theorem3vded13 816 A 3-variable theorem. Experiment with weak deduction theorem. (Contributed by NM, 25-Oct-1998.)
(b ∩ (c1 a)) ≤ (c1 (b1 a))    &   ca       c ≤ (b1 a)

Theorem3vded21 817 A 3-variable theorem. Experiment with weak deduction theorem. (Contributed by NM, 31-Oct-1998.)
c ≤ ((a0 b) →0 (c2 b))    &   c ≤ (a0 b)       cb

Theorem3vded22 818 A 3-variable theorem. Experiment with weak deduction theorem. (Contributed by NM, 31-Oct-1998.)
c ≤ ( C (a, b) ∪ C (c, b))    &   ca    &   c ≤ (a0 b)       cb

Theorem3vded3 819 A 3-variable theorem. Experiment with weak deduction theorem. (Contributed by NM, 24-Jan-1999.)
(c0 C (a, c)) = 1    &   (c0 a) = 1    &   (c0 (a0 b)) = 1       (c0 b) = 1

Theorem1oa 820 Orthoarguesian-like law with 1 instead of 0 but true in all OMLs. (Contributed by NM, 1-Nov-1998.)
((a2 b) ∩ ((bc) →1 ((a2 b) ∩ (a2 c)))) ≤ (a2 c)

Theorem1oai1 821 Orthoarguesian-like OM law. (Contributed by NM, 30-Dec-1998.)
((a1 c) ∩ ((ab)1 ((a1 c) ∩ (b1 c)))) ≤ (b1 c)

Theorem2oai1u 822 Orthoarguesian-like OM law. (Contributed by NM, 28-Feb-1999.)
((a1 c) ∩ (((a1 c) ∩ (b1 c))2 ((a1 c) ∩ (b1 c)))) ≤ (b1 c)

Theorem1oaiii 823 OML analog to orthoarguesian law of Godowski/Greechie, Eq. III with 1 instead of 0 . (Contributed by NM, 1-Nov-1998.)
((a2 b) ∩ ((bc) →1 ((a2 b) ∩ (a2 c)))) = ((a2 c) ∩ ((bc) →1 ((a2 b) ∩ (a2 c))))

Theorem1oaii 824 OML analog to orthoarguesian law of Godowski/Greechie, Eq. II with 1 instead of 0 . (Contributed by NM, 1-Nov-1998.)
(b ∩ ((a2 b) ∪ ((a2 c) ∩ ((bc) →1 ((a2 b) ∩ (a2 c)))))) ≤ a

Theorem2oalem1 825 Lemma for OA-like stuff with 2 instead of 0 . (Contributed by NM, 15-Nov-1998.)
((a2 b) ∪ ((bc) ∪ ((a2 b) ∩ (a2 c)))) = 1

Theorem2oath1 826 OA-like theorem with 2 instead of 0 . (Contributed by NM, 15-Nov-1998.)
((a2 b) ∩ ((bc) →2 ((a2 b) ∩ (a2 c)))) = ((a2 b) ∩ (a2 c))

Theorem2oath1i1 827 Orthoarguesian-like OM law. (Contributed by NM, 30-Dec-1998.)
((a1 c) ∩ ((ab)2 ((a1 c) ∩ (b1 c)))) = ((a1 c) ∩ (b1 c))

Theorem1oath1i1u 828 Orthoarguesian-like OM law. (Contributed by NM, 28-Feb-1999.)
((a1 c) ∩ (((a1 c) ∩ (b1 c))1 ((a1 c) ∩ (b1 c)))) = ((a1 c) ∩ (b1 c))

Theoremoale 829 Relation for studying OA. (Contributed by NM, 18-Nov-1998.)
((a2 b) ∩ ((bc) ∪ ((a2 b) ∩ (a2 c))) ) ≤ (a2 c)

Theoremoaeqv 830 Weakened OA implies OA). (Contributed by NM, 16-Nov-1998.)
((a2 b) ∩ ((bc) ∪ ((a2 b) ∩ (a2 c)))) ≤ ((bc) →2 ((a2 b) ∩ (a2 c)))       ((a2 b) ∩ ((bc) ∪ ((a2 b) ∩ (a2 c)))) ≤ (a2 c)

Theorem3vroa 831 OA-like inference rule (requires OM only). (Contributed by NM, 13-Nov-1998.)
((a2 b) ∩ ((bc) →0 ((a2 b) ∩ (a2 c)))) = 1       (a2 c) = 1

Theoremmlalem 832 Lemma for Mladen's OML. (Contributed by NM, 4-Nov-1998.)
((ab) ∩ (b1 c)) ≤ (a1 c)

Theoremmlaoml 833 Mladen's OML. (Contributed by NM, 4-Nov-1998.)
((ab) ∩ (bc)) ≤ (ac)

Theoremeqtr4 834 4-variable transitive law for equivalence. (Contributed by NM, 26-Jun-2003.)
(((ab) ∩ (bc)) ∩ (cd)) ≤ (ad)

Theoremsac 835 Theorem showing "Sasaki complement" is an operation. (Contributed by NM, 3-Jan-1999.)
(a1 c) = (b1 c)       (a1 c) = (b1 c)

Theoremsa5 836 Possible axiom for a "Sasaki algebra" for orthoarguesian lattices. (Contributed by NM, 3-Jan-1999.)
(a1 c) ≤ (b1 c)       (b1 c) ≤ ((a1 c) ∪ c)

Theoremsalem1 837 Lemma for attempt at Sasaki algebra. (Contributed by NM, 4-Jan-1999.)
(((a1 b) ∪ b) →1 b) = (a2 b)

Theoremsadm3 838 Weak DeMorgan's law for attempt at Sasaki algebra. (Contributed by NM, 4-Jan-1999.)
(((a1 c) ∩ (b1 c)) →1 c) ≤ ((a1 c) ∪ (b1 c))

Theorembi3 839 Chained biconditional. (Contributed by NM, 2-Mar-2000.)
((ab) ∩ (bc)) = (((ab) ∩ c) ∪ ((ab ) ∩ c ))

Theorembi4 840 Chained biconditional. (Contributed by NM, 25-Jun-2003.)
(((ab) ∩ (bc)) ∩ (cd)) = ((((ab) ∩ c) ∩ d) ∪ (((ab ) ∩ c ) ∩ d ))

Theoremimp3 841 Implicational product with 3 variables. Theorem 3.20 of "Equations, states, and lattices..." paper. (Contributed by NM, 3-Mar-2000.)
((a2 b) ∩ (b1 c)) = ((ab ) ∪ (bc))

Theoremorbi 842 Disjunction of biconditionals. (Contributed by NM, 5-Jul-2000.)
((ac) ∪ (bc)) = (((a2 c) ∪ (b2 c)) ∩ ((c1 a) ∪ (c1 b)))

Theoremorbile 843 Disjunction of biconditionals. (Contributed by NM, 5-Jul-2000.)
((ac) ∪ (bc)) ≤ (((ab) →2 c) ∩ (c1 (ab)))

Theoremmlaconj4 844 For 4GO proof of Mladen's conjecture, that it follows from Eq. (3.30) in OA-GO paper. (Contributed by NM, 8-Jul-2000.)
((de) ∩ ((ec ) ∪ (dc))) ≤ (dc)    &   d = (ab)    &   e = (ab)       ((ab) ∩ ((ac) ∪ (bc))) ≤ (ac)

Theoremmlaconj 845 For 5GO proof of Mladen's conjecture. (Contributed by NM, 20-Jan-2002.)
((ab) ∩ ((ac) ∪ (bc))) ≤ ((((a1 (ab)) ∩ ((ab) →1 ((ab) ∪ c))) ∩ ((((ab) ∪ c) →1 c) ∩ (c1 (ab)))) ∩ ((ab) →1 a))

Theoremmlaconj2 846 For 5GO proof of Mladen's conjecture. Hypothesis is 5GO law consequence. (Contributed by NM, 6-Jul-2000.)
((((a1 (ab)) ∩ ((ab) →1 ((ab) ∪ c))) ∩ ((((ab) ∪ c) →1 c) ∩ (c1 (ab)))) ∩ ((ab) →1 a)) ≤ (ac)       ((ab) ∩ ((ac) ∪ (bc))) ≤ (ac)

Theoremi1orni1 847 Complemented antecedent lemma. (Contributed by NM, 6-Aug-2001.)
((a1 b) ∪ (a1 b)) = 1

Theoremnegantlem1 848 Lemma for negated antecedent identity. (Contributed by NM, 6-Aug-2001.)
(a1 c) = (b1 c)       a C (b1 c)

Theoremnegantlem2 849 Lemma for negated antecedent identity. (Contributed by NM, 6-Aug-2001.)
(a1 c) = (b1 c)       a ≤ (b1 c)

Theoremnegantlem3 850 Lemma for negated antecedent identity. (Contributed by NM, 6-Aug-2001.)
(a1 c) = (b1 c)       (ac) ≤ (b1 c)

Theoremnegantlem4 851 Lemma for negated antecedent identity. (Contributed by NM, 6-Aug-2001.)
(a1 c) = (b1 c)       (a1 c) ≤ (b1 c)

Theoremnegant 852 Negated antecedent identity. (Contributed by NM, 6-Aug-2001.)
(a1 c) = (b1 c)       (a1 c) = (b1 c)

Theoremnegantlem5 853 Negated antecedent identity. (Contributed by NM, 6-Aug-2001.)
(a1 c) = (b1 c)       (ac ) = (bc )

Theoremnegantlem6 854 Negated antecedent identity. (Contributed by NM, 6-Aug-2001.)
(a1 c) = (b1 c)       (ac ) = (bc )

Theoremnegantlem7 855 Negated antecedent identity. (Contributed by NM, 6-Aug-2001.)
(a1 c) = (b1 c)       (ac) = (bc)

Theoremnegantlem8 856 Negated antecedent identity. (Contributed by NM, 6-Aug-2001.)
(a1 c) = (b1 c)       (ac) = (bc)

Theoremnegant0 857 Negated antecedent identity. (Contributed by NM, 6-Aug-2001.)
(a1 c) = (b1 c)       (a0 c) = (b0 c)

Theoremnegant2 858 Negated antecedent identity. (Contributed by NM, 6-Aug-2001.)
(a1 c) = (b1 c)       (a2 c) = (b2 c)

Theoremnegantlem9 859 Negated antecedent identity. (Contributed by NM, 6-Aug-2001.)
(a1 c) = (b1 c)       (a3 c) ≤ (b3 c)

Theoremnegant3 860 Negated antecedent identity. (Contributed by NM, 6-Aug-2001.)
(a1 c) = (b1 c)       (a3 c) = (b3 c)

Theoremnegantlem10 861 Lemma for negated antecedent identity. (Contributed by NM, 6-Aug-2001.)
(a1 c) = (b1 c)       (a4 c) ≤ (b4 c)

Theoremnegant4 862 Negated antecedent identity. (Contributed by NM, 6-Aug-2001.)
(a1 c) = (b1 c)       (a4 c) = (b4 c)

Theoremnegant5 863 Negated antecedent identity. (Contributed by NM, 6-Aug-2001.)
(a1 c) = (b1 c)       (a5 c) = (b5 c)

Theoremneg3antlem1 864 Lemma for negated antecedent identity. (Contributed by NM, 7-Aug-2001.)
(a3 c) = (b3 c)       (ac) ≤ (b1 c)

Theoremneg3antlem2 865 Lemma for negated antecedent identity. (Contributed by NM, 7-Aug-2001.)
(a3 c) = (b3 c)       a ≤ (b1 c)

Theoremneg3ant1 866 Lemma for negated antecedent identity. (Contributed by NM, 7-Aug-2001.)
(a3 c) = (b3 c)       (a1 c) = (b1 c)

Theoremelimconslem 867 Lemma for consequent elimination law. (Contributed by NM, 3-Mar-2002.)
(a1 c) = (b1 c)    &   (ac) ≤ (bc )       a ≤ (bc )

Theoremelimcons 868 Consequent elimination law. (Contributed by NM, 3-Mar-2002.)
(a1 c) = (b1 c)    &   (ac) ≤ (bc )       ab

Theoremelimcons2 869 Consequent elimination law. (Contributed by NM, 12-Mar-2002.)
(a1 c) = (b1 c)    &   (a ∩ (c ∩ (b1 c))) ≤ (b ∪ (c ∪ (a1 c) ))       ab

Theoremcomanblem1 870 Lemma for biconditional commutation law. (Contributed by NM, 1-Dec-1999.)
((ac) ∩ (bc)) = (((ac) ∪ ((ab) ∩ c)) ∩ (b1 c))

Theoremcomanblem2 871 Lemma for biconditional commutation law. (Contributed by NM, 1-Dec-1999.)
((ab) ∩ ((ac) ∩ (bc))) = ((ab) ∩ c)

Theoremcomanb 872 Biconditional commutation law. (Contributed by NM, 1-Dec-1999.)
(ab) C ((ac) ∩ (bc))

Theoremcomanbn 873 Biconditional commutation law. (Contributed by NM, 1-Dec-1999.)
(ab ) C ((ac) ∩ (bc))

Theoremmhlemlem1 874 Lemma for Lemma 7.1 of Kalmbach, p. 91. (Contributed by NM, 10-Mar-2002.)
(ab) ≤ (cd)       (((ab) ∪ c) ∩ (a ∪ (cd))) = (ac)

Theoremmhlemlem2 875 Lemma for Lemma 7.1 of Kalmbach, p. 91. (Contributed by NM, 10-Mar-2002.)
(ab) ≤ (cd)       (((ab) ∪ d) ∩ (b ∪ (cd))) = (bd)

Theoremmhlem 876 Lemma 7.1 of Kalmbach, p. 91. (Contributed by NM, 10-Mar-2002.)
(ab) ≤ (cd)       ((ac) ∩ (bd)) = ((ab) ∪ (cd))

Theoremmhlem1 877 Lemma for Marsden-Herman distributive law. (Contributed by NM, 10-Mar-2002.)
a C b    &   c C b       ((ab) ∩ (bc)) = ((ab ) ∪ (bc))

Theoremmhlem2 878 Lemma for Marsden-Herman distributive law. (Contributed by NM, 10-Mar-2002.)
a C c    &   a C d    &   b C c    &   b C d       (((ac) ∩ (cb )) ∩ ((bd) ∩ (ad ))) = (((ac ) ∩ (bd )) ∪ ((cb ) ∩ (da )))

Theoremmh 879 Marsden-Herman distributive law. Lemma 7.2 of Kalmbach, p. 91. (Contributed by NM, 10-Mar-2002.)
a C c    &   a C d    &   b C c    &   b C d       ((ac) ∩ (bd)) = (((ab) ∪ (ad)) ∪ ((cb) ∪ (cd)))

Theoremmarsdenlem1 880 Lemma for Marsden-Herman distributive law. (Contributed by NM, 26-Feb-2002.)
a C b    &   b C c    &   c C d    &   d C a       ((ab) ∩ (ad )) = ((a ∩ (ab)) ∪ (d ∩ (ab)))

Theoremmarsdenlem2 881 Lemma for Marsden-Herman distributive law. (Contributed by NM, 26-Feb-2002.)
a C b    &   b C c    &   c C d    &   d C a       ((cd) ∩ (bc )) = (((bc) ∪ (cd)) ∪ (bd))

Theoremmarsdenlem3 882 Lemma for Marsden-Herman distributive law. (Contributed by NM, 26-Feb-2002.)
a C b    &   b C c    &   c C d    &   d C a       (((bc) ∪ (cd)) ∩ (bd )) = 0

Theoremmarsdenlem4 883 Lemma for Marsden-Herman distributive law. (Contributed by NM, 26-Feb-2002.)
a C b    &   b C c    &   c C d    &   d C a       (((ab) ∪ (ad )) ∩ (bd)) = 0

Theoremmh2 884 Marsden-Herman distributive law. Corollary 3.3 of Beran, p. 259. (Contributed by NM, 10-Mar-2002.)
a C b    &   b C c    &   c C d    &   d C a       ((ab) ∩ (cd)) = (((ac) ∪ (ad)) ∪ ((bc) ∪ (bd)))

Theoremmlaconjolem 885 Lemma for OML proof of Mladen's conjecture, (Contributed by NM, 10-Mar-2002.)
((ac) ∪ (bc)) ≤ ((c ∩ (ab)) ∪ (c ∩ (ab )))

Theoremmlaconjo 886 OML proof of Mladen's conjecture. (Contributed by NM, 10-Mar-2002.)
((ab) ∩ ((ac) ∪ (bc))) ≤ (ac)

Theoremdistid 887 Distributive law for identity. (Contributed by NM, 17-Mar-2002.)
((ab) ∩ ((ac) ∪ (bc))) = (((ab) ∩ (ac)) ∪ ((ab) ∩ (bc)))

Theoremmhcor1 888 Corollary of Marsden-Herman Lemma. (Contributed by NM, 26-Jun-2003.)
((((a1 b) ∩ (b2 c)) ∩ (c1 d)) ∩ (d2 a)) = (((ab) ∩ (bc)) ∩ (cd))

Theoremoago3.29 889 Equation (3.29) of "Equations, states, and lattices..." paper. This shows that it holds in all OMLs, not just 4GO. (Contributed by NM, 22-Jun-2003.)
((a1 b) ∩ ((b2 c) ∩ (c1 a))) ≤ (ac)

Theoremoago3.21x 890 4-variable extension of Equation (3.21) of "Equations, states, and lattices..." paper. This shows that it holds in all OMLs, not just 4GO. (Contributed by NM, 26-Jun-2003.)
((((a5 b) ∩ (b5 c)) ∩ (c5 d)) ∩ (d5 a)) = (((ab) ∩ (bc)) ∩ (cd))

Theoremcancellem 891 Lemma for cancellation law eliminating 1 consequent. (Contributed by NM, 21-Feb-2002.)
((d ∪ (a1 c)) →1 c) = ((d ∪ (b1 c)) →1 c)       (d ∪ (a1 c)) ≤ (d ∪ (b1 c))

Theoremcancel 892 Cancellation law eliminating 1 consequent. (Contributed by NM, 21-Feb-2002.)
((d ∪ (a1 c)) →1 c) = ((d ∪ (b1 c)) →1 c)       (d ∪ (a1 c)) = (d ∪ (b1 c))

Theoremkb10iii 893 Exercise 10(iii) of Kalmbach p. 30 (in a rewritten form). (Contributed by NM, 9-Jan-2004.)
b ≤ (a1 c)       c ≤ (a1 b)

Theoreme2ast2 894 Show that the E*2 derivative on p. 23 of Mayet, "Equations holding in Hilbert lattices" IJTP 2006, holds in all OMLs. (Contributed by NM, 24-Jun-2006.)
ab    &   cd    &   ac       ((ab) ∩ (cd)) ≤ ((bd) ∪ (ac) )

Theoreme2astlem1 895 Lemma towards a possible proof that E*2 on p. 23 of Mayet, "Equations holding in Hilbert lattices" IJTP 2006, holds in all OMLs. (Contributed by NM, 25-Jun-2006.)
ab    &   cd    &   ra    &   ac    &   cr       (((ab) ∩ (cd)) ∩ ((ac) ∪ r)) = ((a ∪ (b ∩ (cr))) ∩ (c ∪ (d ∩ (ar))))

0.3.10  OML lemmas for studying Godowski equations

Theoremgovar 896 Lemma for converting n-variable Godowski equations to 2n-variable equations. (Contributed by NM, 19-Nov-1999.)
ab    &   bc       ((ab) ∩ (a2 c)) ≤ (bc)

Theoremgovar2 897 Lemma for converting n-variable to 2n-variable Godowski equations. (Contributed by NM, 19-Nov-1999.)
ab    &   bc       (ab) ≤ (c2 a)

Theoremgon2n 898 Lemma for converting n-variable to 2n-variable Godowski equations. (Contributed by NM, 19-Nov-1999.)
ab    &   bc    &   ((c2 a) ∩ d) ≤ (a2 c)    &   ed       ((ab) ∩ e) ≤ (bc)

Theoremgo2n4 899 8-variable Godowski equation derived from 4-variable one. The last hypothesis is the 4-variable Godowski equation. (Contributed by NM, 19-Nov-1999.)
ab    &   bc    &   cd    &   de    &   ef    &   fg    &   gh    &   ha    &   (((c2 a) ∩ (a2 g)) ∩ ((g2 e) ∩ (e2 c))) ≤ (a2 c)       (((ab) ∩ (cd)) ∩ ((ef) ∩ (gh))) ≤ (bc)

Theoremgomaex4 900 Proof of Mayet Example 4 from 4-variable Godowski equation. R. Mayet, "Equational bases for some varieties of orthomodular lattices related to states," Algebra Universalis 23 (1986), 167-195. (Contributed by NM, 19-Nov-1999.)
ab    &   bc    &   cd    &   de    &   ef    &   fg    &   gh    &   ha    &   (((a2 g) ∩ (g2 e)) ∩ ((e2 c) ∩ (c2 a))) ≤ (g2 a)    &   (((e2 c) ∩ (c2 a)) ∩ ((a2 g) ∩ (g2 e))) ≤ (c2 e)       ((((ab) ∩ (cd)) ∩ ((ef) ∩ (gh))) ∩ ((ah) →1 (de) )) = 0

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