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

Theoremgo2n6 901 12-variable Godowski equation derived from 6-variable one. The last hypothesis is the 6-variable Godowski equation.
gh    &   hi    &   ij    &   jk    &   km    &   mn    &   nu    &   uw    &   wx    &   xy    &   yz    &   zg    &   (((i2 g) ∩ (g2 y)) ∩ (((y2 w) ∩ (w2 n)) ∩ ((n2 k) ∩ (k2 i)))) ≤ (g2 i)       (((gh) ∩ (ij)) ∩ (((km) ∩ (nu)) ∩ ((wx) ∩ (yz)))) ≤ (hi)

Theoremgomaex3h1 902 Hypothesis for Godowski 6-var -> Mayet Example 3.
ab    &   g = a    &   h = b       gh

Theoremgomaex3h2 903 Hypothesis for Godowski 6-var -> Mayet Example 3.
bc    &   h = b    &   i = c       hi

Theoremgomaex3h3 904 Hypothesis for Godowski 6-var -> Mayet Example 3.
i = c    &   j = (cd)       ij

Theoremgomaex3h4 905 Hypothesis for Godowski 6-var -> Mayet Example 3.
r = ((p1 q) ∩ (cd))    &   j = (cd)    &   k = r       jk

Theoremgomaex3h5 906 Hypothesis for Godowski 6-var -> Mayet Example 3.
r = ((p1 q) ∩ (cd))    &   k = r    &   m = (p1 q)       km

Theoremgomaex3h6 907 Hypothesis for Godowski 6-var -> Mayet Example 3.
m = (p1 q)    &   n = (p1 q)       mn

Theoremgomaex3h7 908 Hypothesis for Godowski 6-var -> Mayet Example 3.
n = (p1 q)    &   u = (pq)       nu

Theoremgomaex3h8 909 Hypothesis for Godowski 6-var -> Mayet Example 3.
u = (pq)    &   w = q       uw

Theoremgomaex3h9 910 Hypothesis for Godowski 6-var -> Mayet Example 3.
w = q    &   x = q       wx

Theoremgomaex3h10 911 Hypothesis for Godowski 6-var -> Mayet Example 3.
q = ((ef) →1 (bc) )    &   x = q    &   y = (ef)       xy

Theoremgomaex3h11 912 Hypothesis for Godowski 6-var -> Mayet Example 3.
y = (ef)    &   z = f       yz

Theoremgomaex3h12 913 Hypothesis for Godowski 6-var -> Mayet Example 3.
fa    &   g = a    &   z = f       zg

Theoremgomaex3lem1 914 Lemma for Godowski 6-var -> Mayet Example 3.
cd       (c ∪ (cd) ) = d

Theoremgomaex3lem2 915 Lemma for Godowski 6-var -> Mayet Example 3.
ef       ((ef)f) = e

Theoremgomaex3lem3 916 Lemma for Godowski 6-var -> Mayet Example 3.
((p1 q) ∪ (pq)) = p

Theoremgomaex3lem4 917 Lemma for Godowski 6-var -> Mayet Example 3.
p = ((ab) →1 (de) )       ((ab) ∩ (de) ) ≤ p

Theoremgomaex3lem5 918 Lemma for Godowski 6-var -> Mayet Example 3.
ab    &   bc    &   cd    &   ef    &   fa    &   (((i2 g) ∩ (g2 y)) ∩ (((y2 w) ∩ (w2 n)) ∩ ((n2 k) ∩ (k2 i)))) ≤ (g2 i)    &   p = ((ab) →1 (de) )    &   q = ((ef) →1 (bc) )    &   r = ((p1 q) ∩ (cd))    &   g = a    &   h = b    &   i = c    &   j = (cd)    &   k = r    &   m = (p1 q)    &   n = (p1 q)    &   u = (pq)    &   w = q    &   x = q    &   y = (ef)    &   z = f       (((gh) ∩ (ij)) ∩ (((km) ∩ (nu)) ∩ ((wx) ∩ (yz)))) ≤ (hi)

Theoremgomaex3lem6 919 Lemma for Godowski 6-var -> Mayet Example 3.
ab    &   bc    &   cd    &   ef    &   fa    &   (((i2 g) ∩ (g2 y)) ∩ (((y2 w) ∩ (w2 n)) ∩ ((n2 k) ∩ (k2 i)))) ≤ (g2 i)    &   p = ((ab) →1 (de) )    &   q = ((ef) →1 (bc) )    &   r = ((p1 q) ∩ (cd))    &   g = a    &   h = b    &   i = c    &   j = (cd)    &   k = r    &   m = (p1 q)    &   n = (p1 q)    &   u = (pq)    &   w = q    &   x = q    &   y = (ef)    &   z = f       (((ab) ∩ (c ∪ (cd) )) ∩ (((r ∪ (p1 q)) ∩ ((p1 q) ∪ (pq))) ∩ ((qq) ∩ ((ef)f)))) ≤ (bc)

Theoremgomaex3lem7 920 Lemma for Godowski 6-var -> Mayet Example 3.
ab    &   bc    &   cd    &   ef    &   fa    &   (((i2 g) ∩ (g2 y)) ∩ (((y2 w) ∩ (w2 n)) ∩ ((n2 k) ∩ (k2 i)))) ≤ (g2 i)    &   p = ((ab) →1 (de) )    &   q = ((ef) →1 (bc) )    &   r = ((p1 q) ∩ (cd))    &   g = a    &   h = b    &   i = c    &   j = (cd)    &   k = r    &   m = (p1 q)    &   n = (p1 q)    &   u = (pq)    &   w = q    &   x = q    &   y = (ef)    &   z = f       (((ab) ∩ d ) ∩ (((r ∪ (p1 q)) ∩ p ) ∩ e )) ≤ (bc)

Theoremgomaex3lem8 921 Lemma for Godowski 6-var -> Mayet Example 3.
ab    &   bc    &   cd    &   ef    &   fa    &   (((i2 g) ∩ (g2 y)) ∩ (((y2 w) ∩ (w2 n)) ∩ ((n2 k) ∩ (k2 i)))) ≤ (g2 i)    &   p = ((ab) →1 (de) )    &   q = ((ef) →1 (bc) )    &   r = ((p1 q) ∩ (cd))    &   g = a    &   h = b    &   i = c    &   j = (cd)    &   k = r    &   m = (p1 q)    &   n = (p1 q)    &   u = (pq)    &   w = q    &   x = q    &   y = (ef)    &   z = f       (((ab) ∩ (de) ) ∩ ((r ∪ (p1 q)) ∩ p )) ≤ (bc)

Theoremgomaex3lem9 922 Lemma for Godowski 6-var -> Mayet Example 3.
ab    &   bc    &   cd    &   ef    &   fa    &   (((i2 g) ∩ (g2 y)) ∩ (((y2 w) ∩ (w2 n)) ∩ ((n2 k) ∩ (k2 i)))) ≤ (g2 i)    &   p = ((ab) →1 (de) )    &   q = ((ef) →1 (bc) )    &   r = ((p1 q) ∩ (cd))    &   g = a    &   h = b    &   i = c    &   j = (cd)    &   k = r    &   m = (p1 q)    &   n = (p1 q)    &   u = (pq)    &   w = q    &   x = q    &   y = (ef)    &   z = f       (((ab) ∩ (de) ) ∩ (r ∪ (p1 q))) ≤ (bc)

Theoremgomaex3lem10 923 Lemma for Godowski 6-var -> Mayet Example 3.
ab    &   bc    &   cd    &   ef    &   fa    &   (((i2 g) ∩ (g2 y)) ∩ (((y2 w) ∩ (w2 n)) ∩ ((n2 k) ∩ (k2 i)))) ≤ (g2 i)    &   p = ((ab) →1 (de) )    &   q = ((ef) →1 (bc) )    &   r = ((p1 q) ∩ (cd))    &   g = a    &   h = b    &   i = c    &   j = (cd)    &   k = r    &   m = (p1 q)    &   n = (p1 q)    &   u = (pq)    &   w = q    &   x = q    &   y = (ef)    &   z = f       (((ab) ∩ (de) ) ∩ (r ∪ (p1 q))) ≤ ((bc) ∪ (ef) )

Theoremgomaex3 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.
ab    &   bc    &   cd    &   ef    &   fa    &   (((i2 g) ∩ (g2 y)) ∩ (((y2 w) ∩ (w2 n)) ∩ ((n2 k) ∩ (k2 i)))) ≤ (g2 i)    &   p = ((ab) →1 (de) )    &   q = ((ef) →1 (bc) )    &   r = ((p1 q) ∩ (cd))    &   g = a    &   i = c    &   k = r    &   n = (p1 q)    &   w = q    &   y = (ef)       (((ab) ∩ (de) ) ∩ ((((ab) →1 (de) ) →1 ((ef) →1 (bc) ) )1 (cd))) ≤ ((bc) ∪ (ef) )

0.3.11  OML Lemmas for studying orthoarguesian laws

Theoremoas 925 "Strengthening" lemma for studying the orthoarguesian law.
(a ∩ (ab)) ≤ c       ((a1 c) ∩ (ab)) ≤ c

Theoremoasr 926 Reverse of oas 925 lemma for studying the orthoarguesian law.
((a1 c) ∩ (ab)) ≤ c       (a ∩ (ab)) ≤ c

Theoremoat 927 Transformation lemma for studying the orthoarguesian law.
(a ∩ (ab)) ≤ c       b ≤ (a1 c)

Theoremoatr 928 Reverse transformation lemma for studying the orthoarguesian law.
b ≤ (a1 c)       (a ∩ (ab)) ≤ c

Theoremoau 929 Transformation lemma for studying the orthoarguesian law.
(a ∩ ((a1 c) ∪ b)) ≤ c       b ≤ (a1 c)

Theoremoaur 930 Transformation lemma for studying the orthoarguesian law.
b ≤ (a1 c)       (a ∩ ((a1 c) ∪ b)) ≤ c

Theoremoaidlem2 931 Lemma for identity-like OA law.
((d ∪ ((a1 c) ∩ (b1 c))) ∪ ((a1 c) →1 (b1 c))) = 1       ((a1 c) ∩ (d ∪ ((a1 c) ∩ (b1 c)))) ≤ (b1 c)

Theoremoaidlem2g 932 Lemma for identity-like OA law (generalized).
((c ∪ (ab)) ∪ (a1 b)) = 1       (a ∩ (c ∪ (ab))) ≤ b

Theoremoa6v4v 933 6-variable OA to 4-variable OA.
(((ab) ∩ (cd)) ∩ (ef)) ≤ (b ∪ (a ∩ (c ∪ (((ac) ∩ (bd)) ∩ (((ae) ∩ (bf)) ∪ ((ce) ∩ (df)))))))    &   e = 0    &   f = 1       ((ab) ∩ (cd)) ≤ (b ∪ (a ∩ (c ∪ ((ac) ∩ (bd)))))

Theoremoa4v3v 934 4-variable OA to 3-variable OA (Godowski/Greechie Eq. IV).
db    &   ec    &   ((db) ∩ (ec)) ≤ (b ∪ (d ∩ (e ∪ ((de) ∩ (bc)))))    &   d = (a2 b)    &   e = (a2 c)       (b ∩ ((a2 b) ∪ ((a2 c) ∩ ((bc) ∪ ((a2 b) ∩ (a2 c)))))) ≤ ((b ∩ (a2 b)) ∪ (c ∩ (a2 c)))

Theoremoal42 935 Derivation of Godowski/Greechie Eq. II from Eq. IV.
(b ∩ ((a2 b) ∪ ((a2 c) ∩ ((bc) ∪ ((a2 b) ∩ (a2 c)))))) ≤ ((b ∩ (a2 b)) ∪ (c ∩ (a2 c)))       (b ∩ ((a2 b) ∪ ((a2 c) ∩ ((bc) ∪ ((a2 b) ∩ (a2 c)))))) ≤ a

Theoremoa23 936 Derivation of OA from Godowski/Greechie Eq. II.
(c ∩ ((a2 c) ∪ ((a2 b) ∩ ((cb) ∪ ((a2 c) ∩ (a2 b)))))) ≤ a       ((a2 b) ∩ ((bc) ∪ ((a2 b) ∩ (a2 c)))) ≤ (a2 c)

Theoremoa4lem1 937 Lemma for 3-var to 4-var OA.
ab    &   cd       (ab) ≤ ((ac)2 b)

Theoremoa4lem2 938 Lemma for 3-var to 4-var OA.
ab    &   cd       (cd) ≤ ((ac)2 d)

Theoremoa4lem3 939 Lemma for 3-var to 4-var OA.
ab    &   cd       ((ab) ∩ (cd)) ≤ ((bd) ∪ (((ac)2 b) ∩ ((ac)2 d)))

Theoremdistoah1 940 Satisfaction of distributive law hypothesis.
d = (a2 b)    &   e = ((bc) →1 ((a2 b) ∩ (a2 c)))    &   f = ((bc) →2 ((a2 b) ∩ (a2 c)))       d ≤ (a2 b)

Theoremdistoah2 941 Satisfaction of distributive law hypothesis.
d = (a2 b)    &   e = ((bc) →1 ((a2 b) ∩ (a2 c)))    &   f = ((bc) →2 ((a2 b) ∩ (a2 c)))       e ≤ ((bc) →0 ((a2 b) ∩ (a2 c)))

Theoremdistoah3 942 Satisfaction of distributive law hypothesis.
d = (a2 b)    &   e = ((bc) →1 ((a2 b) ∩ (a2 c)))    &   f = ((bc) →2 ((a2 b) ∩ (a2 c)))       f ≤ ((bc) →0 ((a2 b) ∩ (a2 c)))

Theoremdistoah4 943 Satisfaction of distributive law hypothesis.
d = (a2 b)    &   e = ((bc) →1 ((a2 b) ∩ (a2 c)))    &   f = ((bc) →2 ((a2 b) ∩ (a2 c)))       (d ∩ (a2 c)) ≤ f

Theoremdistoa 944 Derivation in OM of OA, assuming OA distributive law oadistd 1023.
d = (a2 b)    &   e = ((bc) →1 ((a2 b) ∩ (a2 c)))    &   f = ((bc) →2 ((a2 b) ∩ (a2 c)))    &   (d ∩ (ef)) = ((de) ∪ (df))       ((a2 b) ∩ ((bc) ∪ ((a2 b) ∩ (a2 c)))) ≤ (a2 c)

Theoremoa3to4lem1 945 Lemma for orthoarguesian law (Godowski/Greechie 3-variable to 4-variable proof).
ab    &   cd    &   g = ((ab) ∪ (cd))       b ≤ (a1 g)

Theoremoa3to4lem2 946 Lemma for orthoarguesian law (Godowski/Greechie 3-variable to 4-variable proof).
ab    &   cd    &   g = ((ab) ∪ (cd))       d ≤ (c1 g)

Theoremoa3to4lem3 947 Lemma for orthoarguesian law (Godowski/Greechie 3-variable to 4-variable proof).
ab    &   cd    &   g = ((ab) ∪ (cd))       (a ∩ (b ∪ (d ∩ ((ac) ∪ (bd))))) ≤ (a ∩ ((a1 g) ∪ ((c1 g) ∩ ((ac) ∪ ((a1 g) ∩ (c1 g))))))

Theoremoa3to4lem4 948 Lemma for orthoarguesian law (Godowski/Greechie 3-variable to 4-variable proof).
ab    &   cd    &   g = ((ab) ∪ (cd))    &   (a ∩ ((a1 g) ∪ ((c1 g) ∩ ((ac) ∪ ((a1 g) ∩ (c1 g)))))) ≤ ((ag) ∪ (cg))       (a ∩ (b ∪ (d ∩ ((ac) ∪ (bd))))) ≤ g

Theoremoa3to4lem5 949 Lemma for orthoarguesian law (Godowski/Greechie 3-variable to 4-variable proof).
((ab) ∩ (cd)) ≤ (a ∪ (b ∩ (d ∪ ((ac) ∩ (bd)))))       ((ba) ∩ (dc)) ≤ (a ∪ (b ∩ (d ∪ ((bd) ∩ (ac)))))

Theoremoa3to4lem6 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.
ab    &   cd    &   g = ((ab ) ∪ (cd ))    &   e = a    &   f = c    &   (e ∩ ((e1 g) ∪ ((f1 g) ∩ ((ef) ∪ ((e1 g) ∩ (f1 g)))))) ≤ ((eg) ∪ (fg))       ((ab) ∩ (cd)) ≤ (a ∪ (b ∩ (d ∪ ((ac) ∩ (bd)))))

Theoremoa3to4 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.
ab    &   cd    &   g = ((ba ) ∪ (dc ))    &   e = b    &   f = d    &   (e ∩ ((e1 g) ∪ ((f1 g) ∩ ((ef) ∪ ((e1 g) ∩ (f1 g)))))) ≤ ((eg) ∪ (fg))       ((ab) ∩ (cd)) ≤ (b ∪ (a ∩ (c ∪ ((ac) ∩ (bd)))))

Theoremoa6todual 952 Conventional to dual 6-variable OA law.
(((ab ) ∩ (cd )) ∩ (ef )) ≤ (b ∪ (a ∩ (c ∪ (((ac ) ∩ (bd )) ∩ (((ae ) ∩ (bf )) ∪ ((ce ) ∩ (df )))))))       (b ∩ (a ∪ (c ∩ (((ac) ∪ (bd)) ∪ (((ae) ∪ (bf)) ∩ ((ce) ∪ (df))))))) ≤ (((ab) ∪ (cd)) ∪ (ef))

Theoremoa6fromdual 953 Dual to conventional 6-variable OA law.
(b ∩ (a ∪ (c ∩ (((ac ) ∪ (bd )) ∪ (((ae ) ∪ (bf )) ∩ ((ce ) ∪ (df ))))))) ≤ (((ab ) ∪ (cd )) ∪ (ef ))       (((ab) ∩ (cd)) ∩ (ef)) ≤ (b ∪ (a ∩ (c ∪ (((ac) ∩ (bd)) ∩ (((ae) ∩ (bf)) ∪ ((ce) ∩ (df)))))))

Theoremoa6fromdualn 954 Dual to conventional 6-variable OA law.
(b ∩ (a ∪ (c ∩ (((ac) ∪ (bd)) ∪ (((ae) ∪ (bf)) ∩ ((ce) ∪ (df))))))) ≤ (((ab) ∪ (cd)) ∪ (ef))       (((ab ) ∩ (cd )) ∩ (ef )) ≤ (b ∪ (a ∩ (c ∪ (((ac ) ∩ (bd )) ∩ (((ae ) ∩ (bf )) ∪ ((ce ) ∩ (df )))))))

Theoremoa6to4h1 955 Satisfaction of 6-variable OA law hypothesis.
b = (a1 g)    &   d = (c1 g)    &   f = (e1 g)       ab

Theoremoa6to4h2 956 Satisfaction of 6-variable OA law hypothesis.
b = (a1 g)    &   d = (c1 g)    &   f = (e1 g)       cd

Theoremoa6to4h3 957 Satisfaction of 6-variable OA law hypothesis.
b = (a1 g)    &   d = (c1 g)    &   f = (e1 g)       ef

Theoremoa6to4 958 Derivation of 4-variable proper OA law, assuming 6-variable OA law.
b = (a1 g)    &   d = (c1 g)    &   f = (e1 g)    &   (((ab ) ∩ (cd )) ∩ (ef )) ≤ (b ∪ (a ∩ (c ∪ (((ac ) ∩ (bd )) ∩ (((ae ) ∩ (bf )) ∪ ((ce ) ∩ (df )))))))       ((a1 g) ∩ (a ∪ (c ∩ (((ac) ∪ ((a1 g) ∩ (c1 g))) ∪ (((ae) ∪ ((a1 g) ∩ (e1 g))) ∩ ((ce) ∪ ((c1 g) ∩ (e1 g)))))))) ≤ (((ag) ∪ (cg)) ∪ (eg))

Theoremoa4b 959 Derivation of 4-OA law variant.
((a1 g) ∩ (a ∪ (c ∩ (((ac) ∪ ((a1 g) ∩ (c1 g))) ∪ (((ae) ∪ ((a1 g) ∩ (e1 g))) ∩ ((ce) ∪ ((c1 g) ∩ (e1 g)))))))) ≤ (((ag) ∪ (cg)) ∪ (eg))       ((a1 g) ∩ (a ∪ (c ∩ (((ac) ∪ ((a1 g) ∩ (c1 g))) ∪ (((ae) ∪ ((a1 g) ∩ (e1 g))) ∩ ((ce) ∪ ((c1 g) ∩ (e1 g)))))))) ≤ g

Theoremoa4to6lem1 960 Lemma for orthoarguesian law (4-variable to 6-variable proof).
ab    &   cd    &   ef    &   g = (((ab) ∪ (cd)) ∪ (ef))       b ≤ (a1 g)

Theoremoa4to6lem2 961 Lemma for orthoarguesian law (4-variable to 6-variable proof).
ab    &   cd    &   ef    &   g = (((ab) ∪ (cd)) ∪ (ef))       d ≤ (c1 g)

Theoremoa4to6lem3 962 Lemma for orthoarguesian law (4-variable to 6-variable proof).
ab    &   cd    &   ef    &   g = (((ab) ∪ (cd)) ∪ (ef))       f ≤ (e1 g)

Theoremoa4to6lem4 963 Lemma for orthoarguesian law (4-variable to 6-variable proof).
ab    &   cd    &   ef    &   g = (((ab) ∪ (cd)) ∪ (ef))       (b ∩ (a ∪ (c ∩ (((ac) ∪ (bd)) ∪ (((ae) ∪ (bf)) ∩ ((ce) ∪ (df))))))) ≤ ((a1 g) ∩ (a ∪ (c ∩ (((ac) ∪ ((a1 g) ∩ (c1 g))) ∪ (((ae) ∪ ((a1 g) ∩ (e1 g))) ∩ ((ce) ∪ ((c1 g) ∩ (e1 g))))))))

Theoremoa4to6dual 964 Lemma for orthoarguesian law (4-variable to 6-variable proof).
ab    &   cd    &   ef    &   g = (((ab) ∪ (cd)) ∪ (ef))    &   ((a1 g) ∩ (a ∪ (c ∩ (((ac) ∪ ((a1 g) ∩ (c1 g))) ∪ (((ae) ∪ ((a1 g) ∩ (e1 g))) ∩ ((ce) ∪ ((c1 g) ∩ (e1 g)))))))) ≤ g       (b ∩ (a ∪ (c ∩ (((ac) ∪ (bd)) ∪ (((ae) ∪ (bf)) ∩ ((ce) ∪ (df))))))) ≤ g

Theoremoa4to6 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.
ab    &   cd    &   ef    &   g = (((ab ) ∪ (cd )) ∪ (ef ))    &   h = a    &   j = c    &   k = e    &   ((h1 g) ∩ (h ∪ (j ∩ (((hj) ∪ ((h1 g) ∩ (j1 g))) ∪ (((hk) ∪ ((h1 g) ∩ (k1 g))) ∩ ((jk) ∪ ((j1 g) ∩ (k1 g)))))))) ≤ g       (((ab) ∩ (cd)) ∩ (ef)) ≤ (b ∪ (a ∩ (c ∪ (((ac) ∩ (bd)) ∩ (((ae) ∩ (bf)) ∪ ((ce) ∩ (df)))))))

Theoremoa4btoc 966 Derivation of 4-OA law variant.
((a1 g) ∩ (a ∪ (c ∩ (((ac) ∪ ((a1 g) ∩ (c1 g))) ∪ (((ae) ∪ ((a1 g) ∩ (e1 g))) ∩ ((ce) ∪ ((c1 g) ∩ (e1 g)))))))) ≤ g       (a ∩ (a ∪ (c ∩ (((ac) ∪ ((a1 g) ∩ (c1 g))) ∪ (((ae) ∪ ((a1 g) ∩ (e1 g))) ∩ ((ce) ∪ ((c1 g) ∩ (e1 g)))))))) ≤ g

Theoremoa4ctob 967 Derivation of 4-OA law variant.
(a ∩ (a ∪ (c ∩ (((ac) ∪ ((a1 g) ∩ (c1 g))) ∪ (((ae) ∪ ((a1 g) ∩ (e1 g))) ∩ ((ce) ∪ ((c1 g) ∩ (e1 g)))))))) ≤ g       ((a1 g) ∩ (a ∪ (c ∩ (((ac) ∪ ((a1 g) ∩ (c1 g))) ∪ (((ae) ∪ ((a1 g) ∩ (e1 g))) ∩ ((ce) ∪ ((c1 g) ∩ (e1 g)))))))) ≤ g

Theoremoa4ctod 968 Derivation of 4-OA law variant.
(a ∩ (a ∪ (b ∩ (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d)))))))) ≤ d       (b ∩ (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d)))))) ≤ (a1 d)

Theoremoa4dtoc 969 Derivation of 4-OA law variant.
(b ∩ (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d)))))) ≤ (a1 d)       (a ∩ (a ∪ (b ∩ (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d)))))))) ≤ d

Theoremoa4dcom 970 Lemma commuting terms.
(b ∩ (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d)))))) = (b ∩ (((ba) ∪ ((b1 d) ∩ (a1 d))) ∪ (((bc) ∪ ((b1 d) ∩ (c1 d))) ∩ ((ac) ∪ ((a1 d) ∩ (c1 d))))))

0.3.12  5OA law

Theoremoa8todual 971 Conventional to dual 8-variable OA law.
(((ab ) ∩ (cd )) ∩ ((ef ) ∩ (gh ))) ≤ (b ∪ (a ∩ (c ∪ ((((ac ) ∩ (bd )) ∩ (((ag ) ∩ (bh )) ∪ ((cg ) ∩ (dh )))) ∩ ((((ae ) ∩ (bf )) ∩ (((ag ) ∩ (bh )) ∪ ((eg ) ∩ (fh )))) ∪ (((ce ) ∩ (df )) ∩ (((cg ) ∩ (dh )) ∪ ((eg ) ∩ (fh )))))))))       (b ∩ (a ∪ (c ∩ ((((ac) ∪ (bd)) ∪ (((ag) ∪ (bh)) ∩ ((cg) ∪ (dh)))) ∪ ((((ae) ∪ (bf)) ∪ (((ag) ∪ (bh)) ∩ ((eg) ∪ (fh)))) ∩ (((ce) ∪ (df)) ∪ (((cg) ∪ (dh)) ∩ ((eg) ∪ (fh))))))))) ≤ (((ab) ∪ (cd)) ∪ ((ef) ∪ (gh)))

Theoremoa8to5 972 Orthoarguesian law 5OA converted from 8 to 5 variables.
(((ab ) ∩ (cd )) ∩ ((ef ) ∩ (gh ))) ≤ (b ∪ (a ∩ (c ∪ ((((ac ) ∩ (bd )) ∩ (((ag ) ∩ (bh )) ∪ ((cg ) ∩ (dh )))) ∩ ((((ae ) ∩ (bf )) ∩ (((ag ) ∩ (bh )) ∪ ((eg ) ∩ (fh )))) ∪ (((ce ) ∩ (df )) ∩ (((cg ) ∩ (dh )) ∪ ((eg ) ∩ (fh )))))))))    &   b = (a1 j)    &   d = (c1 j)    &   f = (e1 j)    &   h = (g1 j)       ((a1 j) ∩ (a ∪ (c ∩ ((((ac) ∪ ((a1 j) ∩ (c1 j))) ∪ (((ag) ∪ ((a1 j) ∩ (g1 j))) ∩ ((cg) ∪ ((c1 j) ∩ (g1 j))))) ∪ ((((ae) ∪ ((a1 j) ∩ (e1 j))) ∪ (((ag) ∪ ((a1 j) ∩ (g1 j))) ∩ ((eg) ∪ ((e1 j) ∩ (g1 j))))) ∩ (((ce) ∪ ((c1 j) ∩ (e1 j))) ∪ (((cg) ∪ ((c1 j) ∩ (g1 j))) ∩ ((eg) ∪ ((e1 j) ∩ (g1 j)))))))))) ≤ (((aj) ∪ (cj)) ∪ ((ej) ∪ (gj)))

0.3.13  "Godowski/Greechie" form of proper 4-OA

Theoremoa4to4u 973 A "universal" 4-OA. The hypotheses are the standard proper 4-OA and substitutions into it.
((e1 d) ∩ (e ∪ (f ∩ (((ef) ∪ ((e1 d) ∩ (f1 d))) ∪ (((eg) ∪ ((e1 d) ∩ (g1 d))) ∩ ((fg) ∪ ((f1 d) ∩ (g1 d)))))))) ≤ (((ed) ∪ (fd)) ∪ (gd))    &   e = (a1 d)    &   f = (b1 d)    &   g = (c1 d)       ((a1 d) ∩ ((a1 d) ∪ ((b1 d) ∩ ((((a1 d) ∩ (b1 d)) ∪ ((a1 d) ∩ (b1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d)))))))) ≤ ((((a1 d) ∩ (a1 d)) ∪ ((b1 d) ∩ (b1 d))) ∪ ((c1 d) ∩ (c1 d)))

Theoremoa4to4u2 974 A weaker-looking "universal" proper 4-OA.
((e1 d) ∩ (e ∪ (f ∩ (((ef) ∪ ((e1 d) ∩ (f1 d))) ∪ (((eg) ∪ ((e1 d) ∩ (g1 d))) ∩ ((fg) ∪ ((f1 d) ∩ (g1 d)))))))) ≤ (((ed) ∪ (fd)) ∪ (gd))    &   e = (a1 d)    &   f = (b1 d)    &   g = (c1 d)       ((a1 d) ∩ ((a1 d) ∪ ((b1 d) ∩ ((((a1 d) ∩ (b1 d)) ∪ ((a1 d) ∩ (b1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d)))))))) ≤ d

Theoremoa4uto4g 975 Derivation of "Godowski/Greechie" 4-variable proper OA law variant from "universal" variant oa4to4u2 974.
((b1 d) ∩ ((b 1 d) ∪ ((a 1 d) ∩ ((((b1 d) ∩ (a1 d)) ∪ ((b 1 d) ∩ (a 1 d))) ∪ ((((b1 d) ∩ (c1 d)) ∪ ((b 1 d) ∩ (c 1 d))) ∩ (((a1 d) ∩ (c1 d)) ∪ ((a 1 d) ∩ (c 1 d)))))))) ≤ d    &   h = (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d))))       ((a1 d) ∩ (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ h)) ≤ (b1 d)

Theoremoa4gto4u 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.
((e1 d) ∩ (((ef) ∪ ((e1 d) ∩ (f1 d))) ∪ (((eg) ∪ ((e1 d) ∩ (g1 d))) ∩ ((fg) ∪ ((f1 d) ∩ (g1 d)))))) ≤ (f1 d)    &   f = (a1 d)    &   e = (b1 d)    &   g = (c1 d)       ((a1 d) ∩ ((a1 d) ∪ ((b1 d) ∩ ((((a1 d) ∩ (b1 d)) ∪ ((a1 d) ∩ (b1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d)))))))) ≤ d

Theoremoa4uto4 977 Derivation of standard 4-variable proper OA law from "universal" variant oa4to4u2 974.
((a1 d) ∩ ((a1 d) ∪ ((b1 d) ∩ ((((a1 d) ∩ (b1 d)) ∪ ((a1 d) ∩ (b1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d)))))))) ≤ d       ((a1 d) ∩ (a ∪ (b ∩ (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d)))))))) ≤ d

0.3.14  Some 3-OA inferences (derived under OM)

Theoremoa3-2lema 978 Lemma for 3-OA(2). Equivalence with substitution into 4-OA.
((a1 c) ∩ (a ∪ (b ∩ (((ab) ∪ ((a1 c) ∩ (b1 c))) ∪ (((a ∩ 0) ∪ ((a1 c) ∩ (0 →1 c))) ∩ ((b ∩ 0) ∪ ((b1 c) ∩ (0 →1 c)))))))) = ((a1 c) ∩ (a ∪ (b ∩ ((ab) ∪ ((a1 c) ∩ (b1 c))))))

Theoremoa3-2lemb 979 Lemma for 3-OA(2). Equivalence with substitution into 4-OA.
((a1 c) ∩ (a ∪ (b ∩ (((ab) ∪ ((a1 c) ∩ (b1 c))) ∪ (((ac) ∪ ((a1 c) ∩ (c1 c))) ∩ ((bc) ∪ ((b1 c) ∩ (c1 c)))))))) = ((a1 c) ∩ (a ∪ (b ∩ ((ab) ∪ ((a1 c) ∩ (b1 c))))))

Theoremoa3-6lem 980 Lemma for 3-OA(6). Equivalence with substitution into 4-OA.
((a1 c) ∩ (a ∪ (b ∩ (((ab) ∪ ((a1 c) ∩ (b1 c))) ∪ (((a ∩ 1) ∪ ((a1 c) ∩ (1 →1 c))) ∩ ((b ∩ 1) ∪ ((b1 c) ∩ (1 →1 c)))))))) = ((a1 c) ∩ (a ∪ (b ∩ (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c))))))

Theoremoa3-3lem 981 Lemma for 3-OA(3). Equivalence with substitution into 6-OA dual.
(a ∩ (a ∪ (b ∩ (((ab) ∪ (ab )) ∪ (((a ∩ 1) ∪ (ac)) ∩ ((b ∩ 1) ∪ (bc))))))) = (a ∩ (a ∪ (b ∩ ((ab) ∪ ((a1 c) ∩ (b1 c))))))

Theoremoa3-1lem 982 Lemma for 3-OA(1). Equivalence with substitution into 6-OA dual.
(1 ∩ (0 ∪ (a ∩ (((0 ∩ a) ∪ (1 ∩ (a1 c))) ∪ (((0 ∩ b) ∪ (1 ∩ (b1 c))) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c)))))))) = (a ∩ ((a1 c) ∪ ((b1 c) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c))))))

Theoremoa3-4lem 983 Lemma for 3-OA(4). Equivalence with substitution into 6-OA dual.
(a ∩ (a ∪ (b ∩ (((ab) ∪ (ab )) ∪ (((ac) ∪ (a ∩ 1)) ∩ ((bc) ∪ (b ∩ 1))))))) = (a ∩ (a ∪ (b ∩ ((ab) ∪ ((a1 c) ∩ (b1 c))))))

Theoremoa3-5lem 984 Lemma for 3-OA(5). Equivalence with substitution into 6-OA dual.
((a1 c) ∩ (a ∪ (c ∩ (((ac) ∪ ((a1 c) ∩ 1)) ∪ (((ab) ∪ ((a1 c) ∩ (b1 c))) ∩ ((cb) ∪ (1 ∩ (b1 c)))))))) = ((a1 c) ∩ (a ∪ (c ∩ ((a1 c) ∪ ((b1 c) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c))))))))

Theoremoa3-u1lem 985 Lemma for a "universal" 3-OA. Equivalence with substitution into 6-OA dual.
(1 ∩ (c ∪ ((a1 c) ∩ (((c ∩ (a1 c)) ∪ (1 ∩ (a1 c))) ∪ (((c ∩ (b1 c)) ∪ (1 ∩ (b1 c))) ∩ (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c)))))))) = (c ∪ ((a1 c) ∩ ((a1 c) ∪ ((b1 c) ∩ (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c)))))))

Theoremoa3-u2lem 986 Lemma for a "universal" 3-OA. Equivalence with substitution into 6-OA dual.
((a1 c) ∩ ((a1 c) ∪ (c ∩ ((((a1 c) ∩ c) ∪ ((a1 c) ∩ 1)) ∪ ((((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c))) ∩ ((c ∩ (b1 c)) ∪ (1 ∩ (b1 c)))))))) = ((a1 c) ∩ ((a1 c) ∪ (c ∩ ((a1 c) ∪ ((b1 c) ∩ (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c))))))))

Theoremoa3-6to3 987 Derivation of 3-OA variant (3) from (6).
((a1 c) ∩ (a ∪ (b ∩ (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c)))))) ≤ c       (a ∩ (a ∪ (b ∩ ((ab) ∪ ((a1 c) ∩ (b1 c)))))) ≤ c

Theoremoa3-2to4 988 Derivation of 3-OA variant (4) from (2).
((a1 c) ∩ (a ∪ (b ∩ ((ab) ∪ ((a1 c) ∩ (b1 c)))))) ≤ c       (a ∩ (a ∪ (b ∩ ((ab) ∪ ((a1 c) ∩ (b1 c)))))) ≤ c

Theoremoa3-2wto2 989 Derivation of 3-OA variant from weaker version.
(a ∩ (a ∪ (b ∩ ((ab) ∪ ((a1 c) ∩ (b1 c)))))) ≤ c       ((a1 c) ∩ (a ∪ (b ∩ ((ab) ∪ ((a1 c) ∩ (b1 c)))))) ≤ c

Theoremoa3-2to2s 990 Derivation of 3-OA variant from weaker version.
((a1 d) ∩ (a ∪ (b ∩ ((ab) ∪ ((a1 d) ∩ (b1 d)))))) ≤ d    &   d = ((ac) ∪ (bc))       ((a1 c) ∩ (a ∪ (b ∩ ((ab) ∪ ((a1 c) ∩ (b1 c)))))) ≤ ((ac) ∪ (bc))

Theoremoa3-u1 991 Derivation of a "universal" 3-OA. The hypothesis is a substitution instance of the proper 4-OA.
((c1 c) ∩ (c ∪ ((a1 c) ∩ (((c ∩ (a1 c)) ∪ ((c1 c) ∩ ((a1 c) →1 c))) ∪ (((c ∩ (b1 c)) ∪ ((c1 c) ∩ ((b1 c) →1 c))) ∩ (((a1 c) ∩ (b1 c)) ∪ (((a1 c) →1 c) ∩ ((b1 c) →1 c)))))))) ≤ c       (c ∪ ((a1 c) ∩ ((a1 c) ∪ ((b1 c) ∩ (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c))))))) ≤ c

Theoremoa3-u2 992 Derivation of a "universal" 3-OA. The hypothesis is a substitution instance of the proper 4-OA.
(((a1 c) →1 c) ∩ ((a1 c) ∪ (c ∩ ((((a1 c) ∩ c) ∪ (((a1 c) →1 c) ∩ (c1 c))) ∪ ((((a1 c) ∩ (b1 c)) ∪ (((a1 c) →1 c) ∩ ((b1 c) →1 c))) ∩ ((c ∩ (b1 c)) ∪ ((c1 c) ∩ ((b1 c) →1 c)))))))) ≤ c       ((a1 c) ∩ ((a1 c) ∪ (c ∩ ((a1 c) ∪ ((b1 c) ∩ (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c)))))))) ≤ c

Theoremoa3-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.
((a1 c) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c)))) ≤ (b1 c)       (c ∩ ((b1 c) ∪ ((a1 c) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c)))))) ≤ (b1 c)

0.4  Derivation of 4-variable proper OA from OA distributive law

Axiomax-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.
e = (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d))))    &   f = (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ e)    &   h ≤ (a1 d)    &   jf    &   kf    &   (h ∩ (b1 d)) ≤ k       (h ∩ (jk)) = ((hj) ∪ (hk))

Theoremd3oa 995 Derivation of 3-OA from OA distributive law.
f = ((ab) ∪ ((a1 c) ∩ (b1 c)))       ((a1 c) ∩ f) ≤ (b1 c)

Theoremd4oa 996 Variant of proper 4-OA proved from OA distributive law.
e = ((ab) ∪ ((a1 d) ∩ (b1 d)))    &   f = (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d))))       ((a1 d) ∩ (ef)) ≤ (b1 d)

Theoremd6oa 997 Derivation of 6-variable orthoarguesian law from OA distributive law.
ab    &   cd    &   ef       (((ab) ∩ (cd)) ∩ (ef)) ≤ (b ∪ (a ∩ (c ∪ (((ac) ∩ (bd)) ∩ (((ae) ∩ (bf)) ∪ ((ce) ∩ (df)))))))

0.5  Orthoarguesian laws

0.5.1  3-variable orthoarguesian law

Axiomax-3oa 998 3-variable consequence of the orthoarguesion law.
((a1 c) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c)))) ≤ (b1 c)

Theoremoal2 999 Orthoarguesian law - 2 version.
((a2 b) ∩ ((bc) ∪ ((a2 b) ∩ (a2 c)))) ≤ (a2 c)

Theoremoal1 1000 Orthoarguesian law - 1 version derived from 1 version.
((a1 c) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c)))) ≤ (b1 c)

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-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1215
 Copyright terms: Public domain < Previous  Next >