Statement List for Quantum Logic Explorer - 1001-1024 - Page 11 of 11
| Type | Label | Description |
|---|
| Statement |
|---|
| |
| Theorem | oadistc0 1001 |
Pre-distributive law.
|
| d
≤ ((a →2 b) ∩ (a
→2 c))
& ((a →2
c) ∩ ((a →2 b) ∩ ((b
∪ c)⊥ ∪ d))) ≤ (((a
→2 b) ∩ (b ∪ c)⊥ ) ∪ d)
⇒ ((a →2
b) ∩ ((b ∪ c)⊥ ∪ d)) = (((a
→2 b) ∩ (b ∪ c)⊥ ) ∪ d) |
| |
| Theorem | oadistc 1002 |
Distributive law.
|
| d
≤ ((a →2 b) ∩ (a
→2 c))
& ((a →2
b) ∩ ((b ∪ c)⊥ ∪ d)) ≤ (((a
→2 b) ∩ (b ∪ c)⊥ ) ∪ d)
⇒ ((a →2
b) ∩ ((b ∪ c)⊥ ∪ d)) = (((a
→2 b) ∩ (b ∪ c)⊥ ) ∪ ((a →2 b) ∩ d)) |
| |
| Theorem | oadistd 1003 |
OA distributive law.
|
| d
≤ (a →2 b)
& e ≤ ((b ∪ c)
→0 ((a →2
b) ∩ (a →2 c)))
& f ≤ ((b ∪ c)
→0 ((a →2
b) ∩ (a →2 c)))
& (d ∩ (a →2 c)) ≤ f
⇒ (d ∩
(e ∪ f)) = ((d ∩
e) ∪ (d ∩ f)) |
| |
| Theorem | 3oa2 1004 |
Alternate form for the 3-variable orthoarguesion law.
|
| ((a →1 c) ∩ (((a
→1 c) ∩ (b →1 c)) ∪ ((a⊥ →1 c) ∩ (b⊥ →1 c)))) ≤ (b
→1 c) |
| |
| Theorem | 3oa3 1005 |
3-variable orthoarguesion law expressed with the 3OA identity
abbreviation.
|
| ((a →1 c) ∩ (a
≡ c ≡OA b)) ≤ (b
→1 c) |
| |
| Axiom | ax-oal4 1006 |
Orthoarguesian law (4-variable version).
|
| a
≤ b⊥
& c ≤ d⊥
⇒ ((a ∪
b) ∩ (c ∪ d))
≤ (b ∪ (a ∩ (c
∪ ((a ∪ c) ∩ (b
∪ d))))) |
| |
| Theorem | oa4cl 1007 |
4-variable OA closed equational form)
|
| ((a ∪ (b
∩ a⊥ )) ∩
(c ∪ (d ∩ c⊥ ))) ≤ ((b ∩ a⊥ ) ∪ (a ∩ (c
∪ ((a ∪ c) ∩ ((b
∩ a⊥ ) ∪
(d ∩ c⊥ )))))) |
| |
| Theorem | oa43v 1008 |
Derivation of 3-variable OA from 4-variable OA.
|
| ((a →2 b) ∩ ((b
∪ c)⊥ ∪
((a →2 b) ∩ (a
→2 c)))) ≤ (a →2 c) |
| |
| Axiom | ax-oa6 1009 |
Orthoarguesian law (6-variable version).
|
| a
≤ b⊥
& c ≤ d⊥
& e ≤ f⊥
⇒ (((a ∪
b) ∩ (c ∪ d))
∩ (e ∪ f)) ≤ (b
∪ (a ∩ (c ∪ (((a
∪ c) ∩ (b ∪ d))
∩ (((a ∪ e) ∩ (b
∪ f)) ∪ ((c ∪ e)
∩ (d ∪ f))))))) |
| |
| Theorem | oa64v 1010 |
Derivation of 4-variable OA from 6-variable OA.
|
| a
≤ b⊥
& c ≤ d⊥
⇒ ((a ∪
b) ∩ (c ∪ d))
≤ (b ∪ (a ∩ (c
∪ ((a ∪ c) ∩ (b
∪ d))))) |
| |
| Theorem | oa63v 1011 |
Derivation of 3-variable OA from 6-variable OA.
|
| ((a →2 b) ∩ ((b
∪ c)⊥ ∪
((a →2 b) ∩ (a
→2 c)))) ≤ (a →2 c) |
| |
| Axiom | ax-4oa 1012 |
The proper 4-variable OA law.
|
| ((a →1 d) ∩ (((a
∩ b) ∪ ((a →1 d) ∩ (b
→1 d))) ∪ (((a ∩ c)
∪ ((a →1 d) ∩ (c
→1 d))) ∩ ((b ∩ c)
∪ ((b →1 d) ∩ (c
→1 d)))))) ≤ (b →1 d) |
| |
| Theorem | axoa4 1013 |
The proper 4-variable OA law.
|
| (a⊥ ∩ (a ∪ (b
∩ (((a ∩ b) ∪ ((a
→1 d) ∩ (b →1 d))) ∪ (((a
∩ c) ∪ ((a →1 d) ∩ (c
→1 d))) ∩ ((b ∩ c)
∪ ((b →1 d) ∩ (c
→1 d)))))))) ≤ d |
| |
| Theorem | axoa4b 1014 |
Proper 4-variable OA law variant.
|
| ((a →1 d) ∩ (a
∪ (b ∩ (((a ∩ b)
∪ ((a →1 d) ∩ (b
→1 d))) ∪ (((a ∩ c)
∪ ((a →1 d) ∩ (c
→1 d))) ∩ ((b ∩ c)
∪ ((b →1 d) ∩ (c
→1 d)))))))) ≤ d |
| |
| Theorem | oa6 1015 |
Derivation of 6-variable orthoarguesian law from 4-variable
version.
|
| a
≤ b⊥
& c ≤ d⊥
& e ≤ f⊥
⇒ (((a ∪
b) ∩ (c ∪ d))
∩ (e ∪ f)) ≤ (b
∪ (a ∩ (c ∪ (((a
∪ c) ∩ (b ∪ d))
∩ (((a ∪ e) ∩ (b
∪ f)) ∪ ((c ∪ e)
∩ (d ∪ f))))))) |
| |
| Theorem | axoa4a 1016 |
Proper 4-variable OA law variant.
|
| ((a →1 d) ∩ (a
∪ (b ∩ (((a ∩ b)
∪ ((a →1 d) ∩ (b
→1 d))) ∪ (((a ∩ c)
∪ ((a →1 d) ∩ (c
→1 d))) ∩ ((b ∩ c)
∪ ((b →1 d) ∩ (c
→1 d)))))))) ≤
(((a ∩ d) ∪ (b
∩ d)) ∪ (c ∩ d)) |
| |
| Theorem | axoa4d 1017 |
Proper 4-variable OA law variant.
|
| (a
∩ (((a ∩ b) ∪ ((a
→1 d) ∩ (b →1 d))) ∪ (((a
∩ c) ∪ ((a →1 d) ∩ (c
→1 d))) ∩ ((b ∩ c)
∪ ((b →1 d) ∩ (c
→1 d)))))) ≤ (b⊥ →1 d) |
| |
| Theorem | 4oa 1018 |
Variant of proper 4-OA.
|
| e
= (((a ∩ c) ∪ ((a
→1 d) ∩ (c →1 d))) ∩ ((b
∩ c) ∪ ((b →1 d) ∩ (c
→1 d))))
& f = (((a ∩ b)
∪ ((a →1 d) ∩ (b
→1 d))) ∪ e)
⇒ ((a →1
d) ∩ f) ≤ (b
→1 d) |
| |
| Theorem | 4oaiii 1019 |
Proper OA analog to Godowski/Greechie, Eq. III.
|
| e
= (((a ∩ c) ∪ ((a
→1 d) ∩ (c →1 d))) ∩ ((b
∩ c) ∪ ((b →1 d) ∩ (c
→1 d))))
& f = (((a ∩ b)
∪ ((a →1 d) ∩ (b
→1 d))) ∪ e)
⇒ ((a →1
d) ∩ f) = ((b
→1 d) ∩ f) |
| |
| Theorem | 4oath1 1020 |
Proper 4-OA theorem.
|
| e
= (((a ∩ c) ∪ ((a
→1 d) ∩ (c →1 d))) ∩ ((b
∩ c) ∪ ((b →1 d) ∩ (c
→1 d))))
& f = (((a ∩ b)
∪ ((a →1 d) ∩ (b
→1 d))) ∪ e)
⇒ ((a →1
d) ∩ f) = ((a
→1 d) ∩ (b →1 d)) |
| |
| Theorem | 4oagen1 1021 |
"Generalized" 4-OA.
|
| e
= (((a ∩ c) ∪ ((a
→1 d) ∩ (c →1 d))) ∩ ((b
∩ c) ∪ ((b →1 d) ∩ (c
→1 d))))
& f = (((a ∩ b)
∪ ((a →1 d) ∩ (b
→1 d))) ∪ e)
& g ≤ f
⇒ ((a →1
d) ∩ (g ∪ ((a
→1 d) ∩ (b →1 d)))) = ((a
→1 d) ∩ (b →1 d)) |
| |
| Theorem | 4oagen1b 1022 |
"Generalized" OA.
|
| e
= (((a ∩ c) ∪ ((a
→1 d) ∩ (c →1 d))) ∩ ((b
∩ c) ∪ ((b →1 d) ∩ (c
→1 d))))
& f = (((a ∩ b)
∪ ((a →1 d) ∩ (b
→1 d))) ∪ e)
& g ≤ f & h ≤ (a
→1 d)
⇒ (h ∩
(g ∪ ((a →1 d) ∩ (b
→1 d)))) = (h ∩ (b
→1 d)) |
| |
| Theorem | 4oadist 1023 |
OA Distributive law. This is equivalent to the 6-variable OA
law, as shown by theorem d6oa 977.
|
| e
= (((a ∩ c) ∪ ((a
→1 d) ∩ (c →1 d))) ∩ ((b
∩ c) ∪ ((b →1 d) ∩ (c
→1 d))))
& f = (((a ∩ b)
∪ ((a →1 d) ∩ (b
→1 d))) ∪ e)
& h ≤ (a →1 d)
& j ≤ f & k ≤ f
& (h ∩ (b →1 d)) ≤ k
⇒ (h ∩
(j ∪ k)) = ((h ∩
j) ∪ (h ∩ k)) |
| |
| Axiom | ax-newstateeq 1024 |
New equation that holds in Hilbert space, discovered by Pavicic and Megill
(unpublished).
|
| (((a →1 b) →1 (c →1 b)) ∩ ((a
→1 c) ∩ (b →1 a))) ≤ (c
→1 a) |
![[Lattice L46-7]Home Page](l46-7icon.gif){kind=small}
Home