Theorem List for Quantum Logic Explorer - 901-1000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | go2n6 901 |
12-variable Godowski equation derived from 6-variable one. The last
hypothesis is the 6-variable Godowski equation.
|
|
|
Theorem | gomaex3h1 902 |
Hypothesis for Godowski 6-var -> Mayet Example 3.
|
|
|
Theorem | gomaex3h2 903 |
Hypothesis for Godowski 6-var -> Mayet Example 3.
|
|
|
Theorem | gomaex3h3 904 |
Hypothesis for Godowski 6-var -> Mayet Example 3.
|
|
|
Theorem | gomaex3h4 905 |
Hypothesis for Godowski 6-var -> Mayet Example 3.
|
|
|
Theorem | gomaex3h5 906 |
Hypothesis for Godowski 6-var -> Mayet Example 3.
|
|
|
Theorem | gomaex3h6 907 |
Hypothesis for Godowski 6-var -> Mayet Example 3.
|
|
|
Theorem | gomaex3h7 908 |
Hypothesis for Godowski 6-var -> Mayet Example 3.
|
|
|
Theorem | gomaex3h8 909 |
Hypothesis for Godowski 6-var -> Mayet Example 3.
|
|
|
Theorem | gomaex3h9 910 |
Hypothesis for Godowski 6-var -> Mayet Example 3.
|
|
|
Theorem | gomaex3h10 911 |
Hypothesis for Godowski 6-var -> Mayet Example 3.
|
|
|
Theorem | gomaex3h11 912 |
Hypothesis for Godowski 6-var -> Mayet Example 3.
|
|
|
Theorem | gomaex3h12 913 |
Hypothesis for Godowski 6-var -> Mayet Example 3.
|
|
|
Theorem | gomaex3lem1 914 |
Lemma for Godowski 6-var -> Mayet Example 3.
|
|
|
Theorem | gomaex3lem2 915 |
Lemma for Godowski 6-var -> Mayet Example 3.
|
|
|
Theorem | gomaex3lem3 916 |
Lemma for Godowski 6-var -> Mayet Example 3.
|
|
|
Theorem | gomaex3lem4 917 |
Lemma for Godowski 6-var -> Mayet Example 3.
|
|
|
Theorem | gomaex3lem5 918 |
Lemma for Godowski 6-var -> Mayet Example 3.
|
|
|
Theorem | gomaex3lem6 919 |
Lemma for Godowski 6-var -> Mayet Example 3.
|
|
|
Theorem | gomaex3lem7 920 |
Lemma for Godowski 6-var -> Mayet Example 3.
|
|
|
Theorem | gomaex3lem8 921 |
Lemma for Godowski 6-var -> Mayet Example 3.
|
|
|
Theorem | gomaex3lem9 922 |
Lemma for Godowski 6-var -> Mayet Example 3.
|
|
|
Theorem | gomaex3lem10 923 |
Lemma for Godowski 6-var -> Mayet Example 3.
|
|
|
Theorem | gomaex3 924 |
Proof of Mayet Example 3 from 6-variable Godowski equation. R. Mayet,
"Equational bases for some varieties of orthomodular lattices
related to
states," Algebra Universalis 23 (1986), 167-195.
|
|
|
0.3.11 OML Lemmas for studying orthoarguesian
laws
|
|
Theorem | oas 925 |
"Strengthening" lemma for studying the orthoarguesian law.
|
|
|
Theorem | oasr 926 |
Reverse of oas 925 lemma for studying the orthoarguesian law.
|
|
|
Theorem | oat 927 |
Transformation lemma for studying the orthoarguesian law.
|
|
|
Theorem | oatr 928 |
Reverse transformation lemma for studying the orthoarguesian law.
|
|
|
Theorem | oau 929 |
Transformation lemma for studying the orthoarguesian law.
|
|
|
Theorem | oaur 930 |
Transformation lemma for studying the orthoarguesian law.
|
|
|
Theorem | oaidlem2 931 |
Lemma for identity-like OA law.
|
|
|
Theorem | oaidlem2g 932 |
Lemma for identity-like OA law (generalized).
|
|
|
Theorem | oa6v4v 933 |
6-variable OA to 4-variable OA.
|
|
|
Theorem | oa4v3v 934 |
4-variable OA to 3-variable OA (Godowski/Greechie Eq. IV).
|
|
|
Theorem | oal42 935 |
Derivation of Godowski/Greechie Eq. II from Eq. IV.
|
|
|
Theorem | oa23 936 |
Derivation of OA from Godowski/Greechie Eq. II.
|
|
|
Theorem | oa4lem1 937 |
Lemma for 3-var to 4-var OA.
|
|
|
Theorem | oa4lem2 938 |
Lemma for 3-var to 4-var OA.
|
|
|
Theorem | oa4lem3 939 |
Lemma for 3-var to 4-var OA.
|
|
|
Theorem | distoah1 940 |
Satisfaction of distributive law hypothesis.
|
|
|
Theorem | distoah2 941 |
Satisfaction of distributive law hypothesis.
|
|
|
Theorem | distoah3 942 |
Satisfaction of distributive law hypothesis.
|
|
|
Theorem | distoah4 943 |
Satisfaction of distributive law hypothesis.
|
|
|
Theorem | distoa 944 |
Derivation in OM of OA, assuming OA distributive law oadistd 1023.
|
|
|
Theorem | oa3to4lem1 945 |
Lemma for orthoarguesian law (Godowski/Greechie 3-variable to 4-variable
proof).
|
|
|
Theorem | oa3to4lem2 946 |
Lemma for orthoarguesian law (Godowski/Greechie 3-variable to 4-variable
proof).
|
|
|
Theorem | oa3to4lem3 947 |
Lemma for orthoarguesian law (Godowski/Greechie 3-variable to 4-variable
proof).
|
|
|
Theorem | oa3to4lem4 948 |
Lemma for orthoarguesian law (Godowski/Greechie 3-variable to
4-variable proof).
|
|
|
Theorem | oa3to4lem5 949 |
Lemma for orthoarguesian law (Godowski/Greechie 3-variable to 4-variable
proof).
|
|
|
Theorem | oa3to4lem6 950 |
Orthoarguesian law (Godowski/Greechie 3-variable to 4-variable). The
first 2 hypotheses are those for 4-OA. The next 3 are variable
substitutions into 3-OA. The last is the 3-OA. The proof uses OM logic
only.
|
|
|
Theorem | oa3to4 951 |
Orthoarguesian law (Godowski/Greechie 3-variable to 4-variable). The
first 2 hypotheses are those for 4-OA. The next 3 are variable
substitutions into 3-OA. The last is the 3-OA. The proof uses OM logic
only.
|
|
|
Theorem | oa6todual 952 |
Conventional to dual 6-variable OA law.
|
|
|
Theorem | oa6fromdual 953 |
Dual to conventional 6-variable OA law.
|
|
|
Theorem | oa6fromdualn 954 |
Dual to conventional 6-variable OA law.
|
|
|
Theorem | oa6to4h1 955 |
Satisfaction of 6-variable OA law hypothesis.
|
|
|
Theorem | oa6to4h2 956 |
Satisfaction of 6-variable OA law hypothesis.
|
|
|
Theorem | oa6to4h3 957 |
Satisfaction of 6-variable OA law hypothesis.
|
|
|
Theorem | oa6to4 958 |
Derivation of 4-variable proper OA law, assuming 6-variable OA law.
|
|
|
Theorem | oa4b 959 |
Derivation of 4-OA law variant.
|
|
|
Theorem | oa4to6lem1 960 |
Lemma for orthoarguesian law (4-variable to 6-variable proof).
|
|
|
Theorem | oa4to6lem2 961 |
Lemma for orthoarguesian law (4-variable to 6-variable proof).
|
|
|
Theorem | oa4to6lem3 962 |
Lemma for orthoarguesian law (4-variable to 6-variable proof).
|
|
|
Theorem | oa4to6lem4 963 |
Lemma for orthoarguesian law (4-variable to 6-variable proof).
|
|
|
Theorem | oa4to6dual 964 |
Lemma for orthoarguesian law (4-variable to 6-variable proof).
|
|
|
Theorem | oa4to6 965 |
Orthoarguesian law (4-variable to 6-variable proof). The first 3
hypotheses are those for 6-OA. The next 4 are variable substitutions
into 4-OA. The last is the 4-OA. The proof uses OM logic only.
|
|
|
Theorem | oa4btoc 966 |
Derivation of 4-OA law variant.
|
|
|
Theorem | oa4ctob 967 |
Derivation of 4-OA law variant.
|
|
|
Theorem | oa4ctod 968 |
Derivation of 4-OA law variant.
|
|
|
Theorem | oa4dtoc 969 |
Derivation of 4-OA law variant.
|
|
|
Theorem | oa4dcom 970 |
Lemma commuting terms.
|
|
|
0.3.12 5OA law
|
|
Theorem | oa8todual 971 |
Conventional to dual 8-variable OA law.
|
|
|
Theorem | oa8to5 972 |
Orthoarguesian law 5OA converted from 8 to 5 variables.
|
|
|
0.3.13 "Godowski/Greechie" form of proper
4-OA
|
|
Theorem | oa4to4u 973 |
A "universal" 4-OA. The hypotheses are the standard proper 4-OA and
substitutions into it.
|
|
|
Theorem | oa4to4u2 974 |
A weaker-looking "universal" proper 4-OA.
|
|
|
Theorem | oa4uto4g 975 |
Derivation of "Godowski/Greechie" 4-variable proper OA law variant
from
"universal" variant oa4to4u2 974.
|
|
|
Theorem | oa4gto4u 976 |
A "universal" 4-OA derived from the Godowski/Greechie form. The
hypotheses are the Godowski/Greechie form of the proper 4-OA and
substitutions into it.
|
|
|
Theorem | oa4uto4 977 |
Derivation of standard 4-variable proper OA law from "universal"
variant
oa4to4u2 974.
|
|
|
0.3.14 Some 3-OA inferences (derived under
OM)
|
|
Theorem | oa3-2lema 978 |
Lemma for 3-OA(2). Equivalence with substitution into 4-OA.
|
|
|
Theorem | oa3-2lemb 979 |
Lemma for 3-OA(2). Equivalence with substitution into 4-OA.
|
|
|
Theorem | oa3-6lem 980 |
Lemma for 3-OA(6). Equivalence with substitution into 4-OA.
|
|
|
Theorem | oa3-3lem 981 |
Lemma for 3-OA(3). Equivalence with substitution into 6-OA dual.
|
|
|
Theorem | oa3-1lem 982 |
Lemma for 3-OA(1). Equivalence with substitution into 6-OA dual.
|
|
|
Theorem | oa3-4lem 983 |
Lemma for 3-OA(4). Equivalence with substitution into 6-OA dual.
|
|
|
Theorem | oa3-5lem 984 |
Lemma for 3-OA(5). Equivalence with substitution into 6-OA dual.
|
|
|
Theorem | oa3-u1lem 985 |
Lemma for a "universal" 3-OA. Equivalence with substitution into 6-OA
dual.
|
|
|
Theorem | oa3-u2lem 986 |
Lemma for a "universal" 3-OA. Equivalence with substitution into 6-OA
dual.
|
|
|
Theorem | oa3-6to3 987 |
Derivation of 3-OA variant (3) from (6).
|
|
|
Theorem | oa3-2to4 988 |
Derivation of 3-OA variant (4) from (2).
|
|
|
Theorem | oa3-2wto2 989 |
Derivation of 3-OA variant from weaker version.
|
|
|
Theorem | oa3-2to2s 990 |
Derivation of 3-OA variant from weaker version.
|
|
|
Theorem | oa3-u1 991 |
Derivation of a "universal" 3-OA. The hypothesis is a substitution
instance of the proper 4-OA.
|
|
|
Theorem | oa3-u2 992 |
Derivation of a "universal" 3-OA. The hypothesis is a substitution
instance of the proper 4-OA.
|
|
|
Theorem | oa3-1to5 993 |
Derivation of an equivalent of the second "universal" 3-OA U2 from an
equivalent of the first "universal" 3-OA U1. This shows that
U2 is
redundant in a system containg U1. The hypothesis is theorem
oal1 1000.
|
|
|
0.4 Derivation of 4-variable proper OA from OA
distributive law
|
|
Axiom | ax-oadist 994 |
OA Distributive law. In this section, we postulate this temporary axiom
(intended not to be used outside of this section) for the OA
distributive law, and derive from it the 6-OA, in theorem d6oa 997.
This
together with the derivation of the distributive law in theorem
4oadist 1044 shows that the OA distributive law is
equivalent to the
6-OA.
|
|
|
Theorem | d3oa 995 |
Derivation of 3-OA from OA distributive law.
|
|
|
Theorem | d4oa 996 |
Variant of proper 4-OA proved from OA distributive law.
|
|
|
Theorem | d6oa 997 |
Derivation of 6-variable orthoarguesian law from OA distributive law.
|
|
|
0.5 Orthoarguesian laws
|
|
0.5.1 3-variable orthoarguesian law
|
|
Axiom | ax-3oa 998 |
3-variable consequence of the orthoarguesion law.
|
|
|
Theorem | oal2 999 |
Orthoarguesian law - version.
|
|
|
Theorem | oal1 1000 |
Orthoarguesian law - version derived from version.
|
|