Theorem List for Quantum Logic Explorer - 801-900 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | i1abs 801 |
An absorption law for .
|
|
|
Theorem | test 802 |
Part of an attempt to crack a potential Kalmbach axiom.
|
|
|
Theorem | test2 803 |
Part of an attempt to crack a potential Kalmbach axiom.
|
|
|
0.3.9 Some 3-variable theorems
|
|
Theorem | 3vth1 804 |
A 3-variable theorem. Equivalent to OML.
|
|
|
Theorem | 3vth2 805 |
A 3-variable theorem. Equivalent to OML.
|
|
|
Theorem | 3vth3 806 |
A 3-variable theorem. Equivalent to OML.
|
|
|
Theorem | 3vth4 807 |
A 3-variable theorem.
|
|
|
Theorem | 3vth5 808 |
A 3-variable theorem.
|
|
|
Theorem | 3vth6 809 |
A 3-variable theorem.
|
|
|
Theorem | 3vth7 810 |
A 3-variable theorem.
|
|
|
Theorem | 3vth8 811 |
A 3-variable theorem.
|
|
|
Theorem | 3vth9 812 |
A 3-variable theorem.
|
|
|
Theorem | 3vcom 813 |
3-variable commutation theorem.
|
|
|
Theorem | 3vded11 814 |
A 3-variable theorem. Experiment with weak deduction theorem.
|
|
|
Theorem | 3vded12 815 |
A 3-variable theorem. Experiment with weak deduction theorem.
|
|
|
Theorem | 3vded13 816 |
A 3-variable theorem. Experiment with weak deduction theorem.
|
|
|
Theorem | 3vded21 817 |
A 3-variable theorem. Experiment with weak deduction theorem.
|
|
|
Theorem | 3vded22 818 |
A 3-variable theorem. Experiment with weak deduction theorem.
|
|
|
Theorem | 3vded3 819 |
A 3-variable theorem. Experiment with weak deduction theorem.
|
|
|
Theorem | 1oa 820 |
Orthoarguesian-like law with instead of but true in all
OMLs.
|
|
|
Theorem | 1oai1 821 |
Orthoarguesian-like OM law.
|
|
|
Theorem | 2oai1u 822 |
Orthoarguesian-like OM law.
|
|
|
Theorem | 1oaiii 823 |
OML analog to orthoarguesian law of Godowski/Greechie, Eq. III with
instead of
.
|
|
|
Theorem | 1oaii 824 |
OML analog to orthoarguesian law of Godowski/Greechie, Eq. II with
instead of
.
|
|
|
Theorem | 2oalem1 825 |
Lemma for OA-like stuff with instead of .
|
|
|
Theorem | 2oath1 826 |
OA-like theorem with instead of .
|
|
|
Theorem | 2oath1i1 827 |
Orthoarguesian-like OM law.
|
|
|
Theorem | 1oath1i1u 828 |
Orthoarguesian-like OM law.
|
|
|
Theorem | oale 829 |
Relation for studying OA.
|
|
|
Theorem | oaeqv 830 |
Weakened OA implies OA).
|
|
|
Theorem | 3vroa 831 |
OA-like inference rule (requires OM only).
|
|
|
Theorem | mlalem 832 |
Lemma for Mladen's OML.
|
|
|
Theorem | mlaoml 833 |
Mladen's OML.
|
|
|
Theorem | eqtr4 834 |
4-variable transitive law for equivalence.
|
|
|
Theorem | sac 835 |
Theorem showing "Sasaki complement" is an operation.
|
|
|
Theorem | sa5 836 |
Possible axiom for a "Sasaki algebra" for orthoarguesian lattices.
|
|
|
Theorem | salem1 837 |
Lemma for attempt at Sasaki algebra.
|
|
|
Theorem | sadm3 838 |
Weak DeMorgan's law for attempt at Sasaki algebra.
|
|
|
Theorem | bi3 839 |
Chained biconditional.
|
|
|
Theorem | bi4 840 |
Chained biconditional.
|
|
|
Theorem | imp3 841 |
Implicational product with 3 variables. Theorem 3.20 of "Equations,
states, and lattices..." paper.
|
|
|
Theorem | orbi 842 |
Disjunction of biconditionals.
|
|
|
Theorem | orbile 843 |
Disjunction of biconditionals.
|
|
|
Theorem | mlaconj4 844 |
For 4GO proof of Mladen's conjecture, that it follows from Eq. (3.30)
in OA-GO paper.
|
|
|
Theorem | mlaconj 845 |
For 5GO proof of Mladen's conjecture.
|
|
|
Theorem | mlaconj2 846 |
For 5GO proof of Mladen's conjecture. Hypothesis is 5GO law
consequence.
|
|
|
Theorem | i1orni1 847 |
Complemented antecedent lemma.
|
|
|
Theorem | negantlem1 848 |
Lemma for negated antecedent identity.
|
|
|
Theorem | negantlem2 849 |
Lemma for negated antecedent identity.
|
|
|
Theorem | negantlem3 850 |
Lemma for negated antecedent identity.
|
|
|
Theorem | negantlem4 851 |
Lemma for negated antecedent identity.
|
|
|
Theorem | negant 852 |
Negated antecedent identity.
|
|
|
Theorem | negantlem5 853 |
Negated antecedent identity.
|
|
|
Theorem | negantlem6 854 |
Negated antecedent identity.
|
|
|
Theorem | negantlem7 855 |
Negated antecedent identity.
|
|
|
Theorem | negantlem8 856 |
Negated antecedent identity.
|
|
|
Theorem | negant0 857 |
Negated antecedent identity.
|
|
|
Theorem | negant2 858 |
Negated antecedent identity.
|
|
|
Theorem | negantlem9 859 |
Negated antecedent identity.
|
|
|
Theorem | negant3 860 |
Negated antecedent identity.
|
|
|
Theorem | negantlem10 861 |
Lemma for negated antecedent identity.
|
|
|
Theorem | negant4 862 |
Negated antecedent identity.
|
|
|
Theorem | negant5 863 |
Negated antecedent identity.
|
|
|
Theorem | neg3antlem1 864 |
Lemma for negated antecedent identity.
|
|
|
Theorem | neg3antlem2 865 |
Lemma for negated antecedent identity.
|
|
|
Theorem | neg3ant1 866 |
Lemma for negated antecedent identity.
|
|
|
Theorem | elimconslem 867 |
Lemma for consequent elimination law.
|
|
|
Theorem | elimcons 868 |
Consequent elimination law.
|
|
|
Theorem | elimcons2 869 |
Consequent elimination law.
|
|
|
Theorem | comanblem1 870 |
Lemma for biconditional commutation law.
|
|
|
Theorem | comanblem2 871 |
Lemma for biconditional commutation law.
|
|
|
Theorem | comanb 872 |
Biconditional commutation law.
|
|
|
Theorem | comanbn 873 |
Biconditional commutation law.
|
|
|
Theorem | mhlemlem1 874 |
Lemma for Lemma 7.1 of Kalmbach, p. 91.
|
|
|
Theorem | mhlemlem2 875 |
Lemma for Lemma 7.1 of Kalmbach, p. 91.
|
|
|
Theorem | mhlem 876 |
Lemma 7.1 of Kalmbach, p. 91.
|
|
|
Theorem | mhlem1 877 |
Lemma for Marsden-Herman distributive law.
|
|
|
Theorem | mhlem2 878 |
Lemma for Marsden-Herman distributive law.
|
|
|
Theorem | mh 879 |
Marsden-Herman distributive law. Lemma 7.2 of Kalmbach, p. 91.
|
|
|
Theorem | marsdenlem1 880 |
Lemma for Marsden-Herman distributive law.
|
|
|
Theorem | marsdenlem2 881 |
Lemma for Marsden-Herman distributive law.
|
|
|
Theorem | marsdenlem3 882 |
Lemma for Marsden-Herman distributive law.
|
|
|
Theorem | marsdenlem4 883 |
Lemma for Marsden-Herman distributive law.
|
|
|
Theorem | mh2 884 |
Marsden-Herman distributive law. Corollary 3.3 of Beran, p. 259.
|
|
|
Theorem | mlaconjolem 885 |
Lemma for OML proof of Mladen's conjecture,
|
|
|
Theorem | mlaconjo 886 |
OML proof of Mladen's conjecture.
|
|
|
Theorem | distid 887 |
Distributive law for identity.
|
|
|
Theorem | mhcor1 888 |
Corollary of Marsden-Herman Lemma.
|
|
|
Theorem | oago3.29 889 |
Equation (3.29) of "Equations, states, and lattices..." paper. This
shows
that it holds in all OMLs, not just 4GO.
|
|
|
Theorem | oago3.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.
|
|
|
Theorem | cancellem 891 |
Lemma for cancellation law eliminating consequent.
|
|
|
Theorem | cancel 892 |
Cancellation law eliminating consequent.
|
|
|
Theorem | kb10iii 893 |
Exercise 10(iii) of Kalmbach p. 30 (in a rewritten form).
|
|
|
Theorem | e2ast2 894 |
Show that the E*2 derivative on p. 23 of
Mayet, "Equations holding in
Hilbert lattices" IJTP 2006, holds in all OMLs.
|
|
|
Theorem | e2astlem1 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.
|
|
|
0.3.10 OML Lemmas for studying Godowski
equations.
|
|
Theorem | govar 896 |
Lemma for converting n-variable Godowski equations to 2n-variable
equations.
|
|
|
Theorem | govar2 897 |
Lemma for converting n-variable to 2n-variable Godowski equations.
|
|
|
Theorem | gon2n 898 |
Lemma for converting n-variable to 2n-variable Godowski equations.
|
|
|
Theorem | go2n4 899 |
8-variable Godowski equation derived from 4-variable one. The last
hypothesis is the 4-variable Godowski equation.
|
|
|
Theorem | gomaex4 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.
|
|