List of Syntax, Axioms (ax-) and
Definitions (df-)|
Ref | Expression (see link for any distinct variable requirements)
|
| wb 1 | wff
a = b |
| wle 2 | wff
a ≤ b |
| wc 3 | wff
a C b |
| wn 4 | term
a⊥ |
| tb 5 | term
(a ≡ b) |
| wo 6 | term
(a ∪ b) |
| wa 7 | term
(a ∩ b) |
| wp 8 | term
(a⊥ b) |
| wt 9 | term
1 |
| wf 10 | term
0 |
| wle2 11 | term
(a ≤2 b) |
| wi0 12 | term
(a →0 b) |
| wi1 13 | term
(a →1 b) |
| wi2 14 | term
(a →2 b) |
| wi3 15 | term
(a →3 b) |
| wi4 16 | term
(a →4 b) |
| wi5 17 | term
(a →5 b) |
| wid0 18 | term
(a ≡0 b) |
| wid1 19 | term
(a ≡1 b) |
| wid2 20 | term
(a ≡2 b) |
| wid3 21 | term
(a ≡3 b) |
| wid4 22 | term
(a ≡4 b) |
| wb3 23 | term
(a ↔3 b) |
| wo3 24 | term
(a ∪3 b) |
| wan3 25 | term
(a ∩3 b) |
| wid3oa 26 | term
(a ≡ c ≡OA b) |
| wid4oa 27 | term
(a ≡ c, d
≡OA b) |
| wcmtr 28 | term
C (a, b) |
| ax-a1 29 | a =
a⊥
⊥ |
| ax-a2 30 | (a
∪ b) = (b ∪ a) |
| ax-a3 31 | ((a
∪ b) ∪ c) = (a ∪
(b ∪ c)) |
| ax-a4 32 | (a
∪ (b ∪ b⊥ )) = (b ∪ b⊥ ) |
| ax-a5 33 | (a
∪ (a⊥ ∪ b)⊥ ) = a |
| ax-r1 34 | a =
b
⇒ b = a |
| ax-r2 35 | a =
b
& b = c
⇒ a = c |
| ax-r4 36 | a =
b
⇒ a⊥ = b⊥ |
| ax-r5 37 | a =
b
⇒ (a ∪ c) = (b ∪
c) |
| df-b 38 | (a
≡ b) = ((a⊥ ∪ b⊥ )⊥ ∪
(a ∪ b)⊥ ) |
| df-a 39 | (a
∩ b) = (a⊥ ∪ b⊥ )⊥ |
| df-t 40 | 1 = (a ∪ a⊥ ) |
| df-f 41 | 0 = 1⊥ |
| df-i0 42 | (a
→0 b) = (a⊥ ∪ b) |
| df-i1 43 | (a
→1 b) = (a⊥ ∪ (a ∩ b)) |
| df-i2 44 | (a
→2 b) = (b ∪ (a⊥ ∩ b⊥ )) |
| df-i3 45 | (a
→3 b) = (((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ (a⊥ ∪ b))) |
| df-i4 46 | (a
→4 b) = (((a ∩ b) ∪
(a⊥ ∩ b)) ∪ ((a⊥ ∪ b) ∩ b⊥ )) |
| df-i5 47 | (a
→5 b) = (((a ∩ b) ∪
(a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) |
| df-id0 48 | (a
≡0 b) = ((a⊥ ∪ b) ∩ (b⊥ ∪ a)) |
| df-id1 49 | (a
≡1 b) = ((a ∪ b⊥ ) ∩ (a⊥ ∪ (a ∩ b))) |
| df-id2 50 | (a
≡2 b) = ((a ∪ b⊥ ) ∩ (b ∪ (a⊥ ∩ b⊥ ))) |
| df-id3 51 | (a
≡3 b) = ((a⊥ ∪ b) ∩ (a
∪ (a⊥ ∩ b⊥ ))) |
| df-id4 52 | (a
≡4 b) = ((a⊥ ∪ b) ∩ (b⊥ ∪ (a ∩ b))) |
| df-o3 53 | (a
∪3 b) = (a⊥ →3 (a⊥ →3 b)) |
| df-a3 54 | (a
∩3 b) = (a⊥ ∪3 b⊥ )⊥ |
| df-b3 55 | (a
↔3 b) = ((a →3 b) ∩ (b
→3 a)) |
| df-id3oa 56 | (a
≡ c ≡OA b) = (((a
→1 c) ∩ (b →1 c)) ∪ ((a⊥ →1 c) ∩ (b⊥ →1 c))) |
| df-id4oa 57 | (a
≡ c, d ≡OA b) = ((a ≡
d ≡OA b) ∪ ((a
≡ d ≡OA c) ∩ (b
≡ d ≡OA c))) |
| df-le 121 | (a
≤2 b) = ((a ∪ b)
≡ b) |
| df-le1 122 | (a
∪ b) = b
⇒ a ≤ b |
| df-le2 123 | a
≤ b
⇒ (a ∪ b) = b |
| df-c1 124 | a
= ((a ∩ b) ∪ (a
∩ b⊥
)) ⇒ a C b |
| df-c2 125 | a C b
⇒ a = ((a ∩ b) ∪
(a ∩ b⊥ )) |
| df-cmtr 126 | C (a, b) =
(((a ∩ b) ∪ (a
∩ b⊥ )) ∪
((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))) |
| ax-wom 343 | (a⊥ ∪ (a ∩ b)) =
1 ⇒ (b ∪ (a⊥ ∩ b⊥ )) = 1 |
| ax-r3 421 | (c
∪ c⊥ ) = ((a⊥ ∪ b⊥ )⊥ ∪
(a ∪ b)⊥ )
⇒ a = b |
| ax-oadist 974 | 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)) |
| ax-3oa 978 | ((a →1 c) ∩ ((a
∩ b) ∪ ((a →1 c) ∩ (b
→1 c)))) ≤ (b →1 c) |
| ax-oal4 1006 | a
≤ b⊥
& c ≤ d⊥
⇒ ((a ∪ b) ∩ (c
∪ d)) ≤ (b ∪ (a ∩
(c ∪ ((a ∪ c) ∩
(b ∪ d))))) |
| ax-oa6 1009 | 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))))))) |
| ax-4oa 1012 | ((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) |
| ax-newstateeq 1024 | (((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