Quantum Logic Explorer - mmtheorems3

Jump to page: 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-1024

Statement List for Quantum Logic Explorer - 201-300 - Page 3 of 11

Type	Label	Description
Statement
Theorem	wcon3 201	Weak contraposition.
(a⊥ ≡ b) = 1    ⇒   (a ≡ b⊥ ) = 1
Theorem	wlem3.1 202	Weak analogue to lemma used in proof of Th. 3.1 of Pavicic 1993.
(a ∪ b) = b    &   (b⊥ ∪ a) = 1    ⇒   (a ≡ b) = 1
Theorem	woml 203	Theorem structurally similar to orthomodular law but does not require R3.
((a ∪ (a⊥ ∩ (a ∪ b))) ≡ (a ∪ b)) = 1
Theorem	wwoml2 204	Weak orthomodular law.
a ≤ b    ⇒   ((a ∪ (a⊥ ∩ b)) ≡ b) = 1
Theorem	wwoml3 205	Weak orthomodular law.
a ≤ b    &   (b ∩ a⊥ ) = 0    ⇒   (a ≡ b) = 1
Theorem	wwcomd 206	Commutation dual (weak). Kalmbach 83 p. 23.
a⊥ C b    ⇒   a = ((a ∪ b) ∩ (a ∪ b⊥ ))
Theorem	wwcom3ii 207	Lemma 3(ii) (weak) of Kalmbach 83 p. 23.
b⊥ C a    ⇒   (a ∩ (a⊥ ∪ b)) = (a ∩ b)
Theorem	wwfh1 208	Foulis-Holland Theorem (weak).
b C a    &   c C a    ⇒   ((a ∩ (b ∪ c)) ≡ ((a ∩ b) ∪ (a ∩ c))) = 1
Theorem	wwfh2 209	Foulis-Holland Theorem (weak).
a C b    &   c⊥ C a    ⇒   ((b ∩ (a ∪ c)) ≡ ((b ∩ a) ∪ (b ∩ c))) = 1
Theorem	wwfh3 210	Foulis-Holland Theorem (weak).
b⊥ C a    &   c⊥ C a    ⇒   ((a ∪ (b ∩ c)) ≡ ((a ∪ b) ∩ (a ∪ c))) = 1
Theorem	wwfh4 211	Foulis-Holland Theorem (weak).
a⊥ C b    &   c C a    ⇒   ((b ∪ (a ∩ c)) ≡ ((b ∪ a) ∩ (b ∪ c))) = 1
Theorem	womao 212	Weak OM-like absorption law for ortholattices.
(a⊥ ∩ (a ∪ (a⊥ ∩ (a ∪ b)))) = (a⊥ ∩ (a ∪ b))
Theorem	womaon 213	Weak OM-like absorption law for ortholattices.
(a ∩ (a⊥ ∪ (a ∩ (a⊥ ∪ b)))) = (a ∩ (a⊥ ∪ b))
Theorem	womaa 214	Weak OM-like absorption law for ortholattices.
(a⊥ ∪ (a ∩ (a⊥ ∪ (a ∩ b)))) = (a⊥ ∪ (a ∩ b))
Theorem	womaan 215	Weak OM-like absorption law for ortholattices.
(a ∪ (a⊥ ∩ (a ∪ (a⊥ ∩ b)))) = (a ∪ (a⊥ ∩ b))
Theorem	anorabs2 216	Absorption law for ortholattices.
(a ∩ (b ∪ (a ∩ (b ∪ c)))) = (a ∩ (b ∪ c))
Theorem	anorabs 217	Absorption law for ortholattices.
(a⊥ ∩ (b ∪ (a⊥ ∩ (a ∪ b)))) = (a⊥ ∩ (a ∪ b))
Theorem	ska2a 218	Axiom KA2a in Pavicic and Megill, 1998
(((a ∪ c) ≡ (b ∪ c)) ≡ ((c ∪ a) ≡ (c ∪ b))) = 1
Theorem	ska2b 219	Axiom KA2b in Pavicic and Megill, 1998
(((a ∪ c) ≡ (b ∪ c)) ≡ ((a⊥ ∩ c⊥ )⊥ ≡ (b⊥ ∩ c⊥ )⊥ )) = 1
Theorem	ka4lemo 220	Lemma for KA4 soundness (OR version) - uses OL only.
((a ∪ b) ∪ ((a ∪ c) ≡ (b ∪ c))) = 1
Theorem	ka4lem 221	Lemma for KA4 soundness (AND version) - uses OL only.
((a ∩ b)⊥ ∪ ((a ∩ c) ≡ (b ∩ c))) = 1
Theorem	sklem 222	Soundness lemma.
a ≤ b    ⇒   (a⊥ ∪ b) = 1
Theorem	ska1 223	Soundness theorem for Kalmbach's quantum propositional logic axiom KA1.
(a ≡ a) = 1
Theorem	ska3 224	Soundness theorem for Kalmbach's quantum propositional logic axiom KA3.
((a ≡ b)⊥ ∪ (a⊥ ≡ b⊥ )) = 1
Theorem	ska5 225	Soundness theorem for Kalmbach's quantum propositional logic axiom KA5.
((a ∩ b) ≡ (b ∩ a)) = 1
Theorem	ska6 226	Soundness theorem for Kalmbach's quantum propositional logic axiom KA6.
((a ∩ (b ∩ c)) ≡ ((a ∩ b) ∩ c)) = 1
Theorem	ska7 227	Soundness theorem for Kalmbach's quantum propositional logic axiom KA7.
((a ∩ (a ∪ b)) ≡ a) = 1
Theorem	ska8 228	Soundness theorem for Kalmbach's quantum propositional logic axiom KA8.
((a⊥ ∩ a) ≡ ((a⊥ ∩ a) ∩ b)) = 1
Theorem	ska9 229	Soundness theorem for Kalmbach's quantum propositional logic axiom KA9.
(a ≡ a⊥ ⊥ ) = 1
Theorem	ska10 230	Soundness theorem for Kalmbach's quantum propositional logic axiom KA10.
((a ∪ b)⊥ ≡ (a⊥ ∩ b⊥ )) = 1
Theorem	ska11 231	Soundness theorem for Kalmbach's quantum propositional logic axiom KA11.
((a ∪ (a⊥ ∩ (a ∪ b))) ≡ (a ∪ b)) = 1
Theorem	ska12 232	Soundness theorem for Kalmbach's quantum propositional logic axiom KA12.
((a ≡ b) ≡ (b ≡ a)) = 1
Theorem	ska13 233	Soundness theorem for Kalmbach's quantum propositional logic axiom KA13.
((a ≡ b)⊥ ∪ (a⊥ ∪ b)) = 1
Theorem	skr0 234	Soundness theorem for Kalmbach's quantum propositional logic axiom KR0.
a = 1    &   (a⊥ ∪ b) = 1    ⇒   b = 1
Theorem	wlem1 235	Lemma for 2-variable WOML proof.
((a ≡ b)⊥ ∪ ((a →1 b) ∩ (b →1 a))) = 1
Theorem	ska15 236	Soundness theorem for Kalmbach's quantum propositional logic axiom KA15.
((a →3 b)⊥ ∪ (a⊥ ∪ b)) = 1
Theorem	skmp3 237	Soundness proof for KMP3.
a = 1    &   (a →3 b) = 1    ⇒   b = 1
Theorem	lei3 238	L.e. to Kalmbach implication.
a ≤ b    ⇒   (a →3 b) = 1
Theorem	mccune2 239	E2 - OL theorem proved by EQP
(a ∪ ((a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b))) ∪ (a⊥ ∩ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))))) = 1
Theorem	mccune3 240	E3 - OL theorem proved by EQP
((((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ (a⊥ ∪ b)))⊥ ∪ (a⊥ ∪ b)) = 1
Theorem	i3n1 241	Equivalence for Kalmbach implication.
(a⊥ →3 b⊥ ) = (((a ∩ b⊥ ) ∪ (a ∩ b)) ∪ (a⊥ ∩ (a ∪ b⊥ )))
Theorem	ni31 242	Equivalence for Kalmbach implication.
(a →3 b)⊥ = (((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ )))
Theorem	i3id 243	Identity for Kalmbach implication.
(a →3 a) = 1
Theorem	li3 244	Introduce Kalmbach implication to the left.
a = b    ⇒   (c →3 a) = (c →3 b)
Theorem	ri3 245	Introduce Kalmbach implication to the right.
a = b    ⇒   (a →3 c) = (b →3 c)
Theorem	2i3 246	Join both sides with Kalmbach implication.
a = b    &   c = d    ⇒   (a →3 c) = (b →3 d)
Theorem	ud1lem0a 247	Introduce →1 to the left.
a = b    ⇒   (c →1 a) = (c →1 b)
Theorem	ud1lem0b 248	Introduce →1 to the right.
a = b    ⇒   (a →1 c) = (b →1 c)
Theorem	ud1lem0ab 249	Join both sides of hypotheses with →1 .
a = b    &   c = d    ⇒   (a →1 c) = (b →1 d)
Theorem	ud2lem0a 250	Introduce →2 to the left.
a = b    ⇒   (c →2 a) = (c →2 b)
Theorem	ud2lem0b 251	Introduce →2 to the right.
a = b    ⇒   (a →2 c) = (b →2 c)
Theorem	ud3lem0a 252	Introduce Kalmbach implication to the left.
a = b    ⇒   (c →3 a) = (c →3 b)
Theorem	ud3lem0b 253	Introduce Kalmbach implication to the right.
a = b    ⇒   (a →3 c) = (b →3 c)
Theorem	ud4lem0a 254	Introduce →4 to the left.
a = b    ⇒   (c →4 a) = (c →4 b)
Theorem	ud4lem0b 255	Introduce →4 to the right.
a = b    ⇒   (a →4 c) = (b →4 c)
Theorem	ud5lem0a 256	Introduce →5 to the left.
a = b    ⇒   (c →5 a) = (c →5 b)
Theorem	ud5lem0b 257	Introduce →5 to the right.
a = b    ⇒   (a →5 c) = (b →5 c)
Theorem	i1i2 258	Correspondence between Sasaki and Dishkant conditionals.
(a →1 b) = (b⊥ →2 a⊥ )
Theorem	i2i1 259	Correspondence between Sasaki and Dishkant conditionals.
(a →2 b) = (b⊥ →1 a⊥ )
Theorem	i1i2con1 260	Correspondence between Sasaki and Dishkant conditionals.
(a →1 b⊥ ) = (b →2 a⊥ )
Theorem	i1i2con2 261	Correspondence between Sasaki and Dishkant conditionals.
(a⊥ →1 b) = (b⊥ →2 a)
Theorem	i3i4 262	Correspondence between Kalmbach and non-tollens conditionals.
(a →3 b) = (b⊥ →4 a⊥ )
Theorem	i4i3 263	Correspondence between Kalmbach and non-tollens conditionals.
(a →4 b) = (b⊥ →3 a⊥ )
Theorem	i5con 264	Converse of →5 .
(a →5 b) = (b⊥ →5 a⊥ )
Theorem	0i1 265	Antecedent of 0 on Sasaki conditional.
(0 →1 a) = 1
Theorem	1i1 266	Antecedent of 1 on Sasaki conditional.
(1 →1 a) = a
Theorem	i1id 267	Identity law for Sasaki conditional.
(a →1 a) = 1
Theorem	i2id 268	Identity law for Dishkant conditional.
(a →2 a) = 1
Theorem	ud1lem0c 269	Lemma for unified disjunction.
(a →1 b)⊥ = (a ∩ (a⊥ ∪ b⊥ ))
Theorem	ud2lem0c 270	Lemma for unified disjunction.
(a →2 b)⊥ = (b⊥ ∩ (a ∪ b))
Theorem	ud3lem0c 271	Lemma for unified disjunction.
(a →3 b)⊥ = (((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ )))
Theorem	ud4lem0c 272	Lemma for unified disjunction.
(a →4 b)⊥ = (((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∩ b⊥ ) ∪ b))
Theorem	ud5lem0c 273	Lemma for unified disjunction.
(a →5 b)⊥ = (((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ (a ∪ b))
Theorem	bina1 274	Pavicic binary logic ax-a1 analog.
(a →3 a⊥ ⊥ ) = 1
Theorem	bina2 275	Pavicic binary logic ax-a2 analog.
(a⊥ ⊥ →3 a) = 1
Theorem	bina3 276	Pavicic binary logic ax-a3 analog.
(a →3 (a ∪ b)) = 1
Theorem	bina4 277	Pavicic binary logic ax-a4 analog.
(b →3 (a ∪ b)) = 1
Theorem	bina5 278	Pavicic binary logic ax-a5 analog.
(b →3 (a ∪ a⊥ )) = 1
Theorem	wql1lem 279	Classical implication inferred from Sakaki implication.
(a →1 b) = 1    ⇒   (a⊥ ∪ b) = 1
Theorem	wql2lem 280	Classical implication inferred from Dishkant implication.
(a →2 b) = 1    ⇒   (a⊥ ∪ b) = 1
Theorem	wql2lem2 281	Lemma for →2 WQL axiom.
((a ∪ c) →2 (b ∪ c)) = 1    ⇒   ((a ∪ (b ∪ c))⊥ ∪ (b ∪ c)) = 1
Theorem	wql2lem3 282	Lemma for →2 WQL axiom.
(a →2 b) = 1    ⇒   ((a ∩ b⊥ ) →2 a⊥ ) = 1
Theorem	wql2lem4 283	Lemma for →2 WQL axiom.
(((a ∩ b⊥ ) ∪ (a ∩ b)) →2 (a⊥ ∪ (a ∩ b))) = 1    &   ((a →1 b) ∪ (a ∩ b⊥ )) = 1    ⇒   (a →1 b) = 1
Theorem	wql2lem5 284	Lemma for →2 WQL axiom.
(a →2 b) = 1    ⇒   ((b⊥ ∩ (a ∪ b)) →2 a⊥ ) = 1
Theorem	wql1 285	The 2nd hypothesis is the first →1 WQL axiom. We show it implies the WOM law.
(a →1 b) = 1    &   ((a ∪ c) →1 (b ∪ c)) = 1    &   c = b    ⇒   (a →2 b) = 1
Theorem	oaidlem1 286	Lemma for OA identity-like law.
(a ∩ b) ≤ c    ⇒   (a⊥ ∪ (b →1 c)) = 1
Theorem	womle2a 287	An equivalent to the WOM law.
(a ∩ (a →2 b)) ≤ ((a →2 b)⊥ ∪ (a →1 b))    ⇒   ((a →2 b)⊥ ∪ (a →1 b)) = 1
Theorem	womle2b 288	An equivalent to the WOM law.
((a →2 b)⊥ ∪ (a →1 b)) = 1    ⇒   (a ∩ (a →2 b)) ≤ ((a →2 b)⊥ ∪ (a →1 b))
Theorem	womle3b 289	Implied by the WOM law.
((a →1 b)⊥ ∪ (a →2 b)) = 1    ⇒   (a ∩ (a →1 b)) ≤ ((a →1 b)⊥ ∪ (a →2 b))
Theorem	womle 290	An equality implying the WOM law.
(a ∩ (a →1 b)) = (a ∩ (a →2 b))    ⇒   ((a →2 b)⊥ ∪ (a →1 b)) = 1
Theorem	nomb41 291	Lemma for "Non-Orthomodular Models..." paper.
(a ≡4 b) = (b ≡1 a)
Theorem	nomb32 292	Lemma for "Non-Orthomodular Models..." paper.
(a ≡3 b) = (b ≡2 a)
Theorem	nomcon0 293	Lemma for "Non-Orthomodular Models..." paper.
(a ≡0 b) = (b⊥ ≡0 a⊥ )
Theorem	nomcon1 294	Lemma for "Non-Orthomodular Models..." paper.
(a ≡1 b) = (b⊥ ≡2 a⊥ )
Theorem	nomcon2 295	Lemma for "Non-Orthomodular Models..." paper.
(a ≡2 b) = (b⊥ ≡1 a⊥ )
Theorem	nomcon3 296	Lemma for "Non-Orthomodular Models..." paper.
(a ≡3 b) = (b⊥ ≡4 a⊥ )
Theorem	nomcon4 297	Lemma for "Non-Orthomodular Models..." paper.
(a ≡4 b) = (b⊥ ≡3 a⊥ )
Theorem	nomcon5 298	Lemma for "Non-Orthomodular Models..." paper.
(a ≡ b) = (b⊥ ≡ a⊥ )
Theorem	nom10 299	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
(a →0 (a ∩ b)) = (a →1 b)
Theorem	nom11 300	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
(a →1 (a ∩ b)) = (a →1 b)