[Lattice L46-7]Home PageHome Quantum Logic Explorer
Theorem List (p. 3 of 13)
< Previous  Next >
Bad symbols? Try the
GIF version.

Mirrors  >  Metamath Home Page  >  QLE Home Page  >  Theorem List Contents       This page: Page List

Theorem List for Quantum Logic Explorer - 201-300   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremwa5c 201 Absorption law.
((a ∩ (ab)) ≡ a) = 1
 
Theoremwcon 202 Contraposition law.
((ab) ≡ (ab )) = 1
 
Theoremwancom 203 Commutative law.
((ab) ≡ (ba)) = 1
 
Theoremwanass 204 Associative law.
(((ab) ∩ c) ≡ (a ∩ (bc))) = 1
 
Theoremwwbmp 205 Weak weak equivalential detachment (WBMP).
a = 1    &   (ab) = 1       b = 1
 
Theoremwwbmpr 206 Weak weak equivalential detachment (WBMP).
b = 1    &   (ab) = 1       a = 1
 
Theoremwcon1 207 Weak contraposition.
(ab ) = 1       (ab) = 1
 
Theoremwcon2 208 Weak contraposition.
(ab ) = 1       (ab) = 1
 
Theoremwcon3 209 Weak contraposition.
(ab) = 1       (ab ) = 1
 
Theoremwlem3.1 210 Weak analogue to lemma used in proof of Th. 3.1 of Pavicic 1993.
(ab) = b    &   (ba) = 1       (ab) = 1
 
Theoremwoml 211 Theorem structurally similar to orthomodular law but does not require R3.
((a ∪ (a ∩ (ab))) ≡ (ab)) = 1
 
Theoremwwoml2 212 Weak orthomodular law.
ab       ((a ∪ (ab)) ≡ b) = 1
 
Theoremwwoml3 213 Weak orthomodular law.
ab    &   (ba ) = 0       (ab) = 1
 
Theoremwwcomd 214 Commutation dual (weak). Kalmbach 83 p. 23.
a C b       a = ((ab) ∩ (ab ))
 
Theoremwwcom3ii 215 Lemma 3(ii) (weak) of Kalmbach 83 p. 23.
b C a       (a ∩ (ab)) = (ab)
 
Theoremwwfh1 216 Foulis-Holland Theorem (weak).
b C a    &   c C a       ((a ∩ (bc)) ≡ ((ab) ∪ (ac))) = 1
 
Theoremwwfh2 217 Foulis-Holland Theorem (weak).
a C b    &   c C a       ((b ∩ (ac)) ≡ ((ba) ∪ (bc))) = 1
 
Theoremwwfh3 218 Foulis-Holland Theorem (weak).
b C a    &   c C a       ((a ∪ (bc)) ≡ ((ab) ∩ (ac))) = 1
 
Theoremwwfh4 219 Foulis-Holland Theorem (weak).
a C b    &   c C a       ((b ∪ (ac)) ≡ ((ba) ∩ (bc))) = 1
 
Theoremwomao 220 Weak OM-like absorption law for ortholattices.
(a ∩ (a ∪ (a ∩ (ab)))) = (a ∩ (ab))
 
Theoremwomaon 221 Weak OM-like absorption law for ortholattices.
(a ∩ (a ∪ (a ∩ (ab)))) = (a ∩ (ab))
 
Theoremwomaa 222 Weak OM-like absorption law for ortholattices.
(a ∪ (a ∩ (a ∪ (ab)))) = (a ∪ (ab))
 
Theoremwomaan 223 Weak OM-like absorption law for ortholattices.
(a ∪ (a ∩ (a ∪ (ab)))) = (a ∪ (ab))
 
Theoremanorabs2 224 Absorption law for ortholattices.
(a ∩ (b ∪ (a ∩ (bc)))) = (a ∩ (bc))
 
Theoremanorabs 225 Absorption law for ortholattices.
(a ∩ (b ∪ (a ∩ (ab)))) = (a ∩ (ab))
 
Theoremska2a 226 Axiom KA2a in Pavicic and Megill, 1998
(((ac) ≡ (bc)) ≡ ((ca) ≡ (cb))) = 1
 
Theoremska2b 227 Axiom KA2b in Pavicic and Megill, 1998
(((ac) ≡ (bc)) ≡ ((ac ) ≡ (bc ) )) = 1
 
Theoremka4lemo 228 Lemma for KA4 soundness (OR version) - uses OL only.
((ab) ∪ ((ac) ≡ (bc))) = 1
 
Theoremka4lem 229 Lemma for KA4 soundness (AND version) - uses OL only.
((ab) ∪ ((ac) ≡ (bc))) = 1
 
0.1.6  Kalmbach axioms (soundness proofs) that are true in all ortholattices
 
Theoremsklem 230 Soundness lemma.
ab       (ab) = 1
 
Theoremska1 231 Soundness theorem for Kalmbach's quantum propositional logic axiom KA1.
(aa) = 1
 
Theoremska3 232 Soundness theorem for Kalmbach's quantum propositional logic axiom KA3.
((ab) ∪ (ab )) = 1
 
Theoremska5 233 Soundness theorem for Kalmbach's quantum propositional logic axiom KA5.
((ab) ≡ (ba)) = 1
 
Theoremska6 234 Soundness theorem for Kalmbach's quantum propositional logic axiom KA6.
((a ∩ (bc)) ≡ ((ab) ∩ c)) = 1
 
Theoremska7 235 Soundness theorem for Kalmbach's quantum propositional logic axiom KA7.
((a ∩ (ab)) ≡ a) = 1
 
Theoremska8 236 Soundness theorem for Kalmbach's quantum propositional logic axiom KA8.
((aa) ≡ ((aa) ∩ b)) = 1
 
Theoremska9 237 Soundness theorem for Kalmbach's quantum propositional logic axiom KA9.
(aa ) = 1
 
Theoremska10 238 Soundness theorem for Kalmbach's quantum propositional logic axiom KA10.
((ab) ≡ (ab )) = 1
 
Theoremska11 239 Soundness theorem for Kalmbach's quantum propositional logic axiom KA11.
((a ∪ (a ∩ (ab))) ≡ (ab)) = 1
 
Theoremska12 240 Soundness theorem for Kalmbach's quantum propositional logic axiom KA12.
((ab) ≡ (ba)) = 1
 
Theoremska13 241 Soundness theorem for Kalmbach's quantum propositional logic axiom KA13.
((ab) ∪ (ab)) = 1
 
Theoremskr0 242 Soundness theorem for Kalmbach's quantum propositional logic axiom KR0.
a = 1    &   (ab) = 1       b = 1
 
Theoremwlem1 243 Lemma for 2-variable WOML proof.
((ab) ∪ ((a1 b) ∩ (b1 a))) = 1
 
Theoremska15 244 Soundness theorem for Kalmbach's quantum propositional logic axiom KA15.
((a3 b) ∪ (ab)) = 1
 
Theoremskmp3 245 Soundness proof for KMP3.
a = 1    &   (a3 b) = 1       b = 1
 
Theoremlei3 246 L.e. to Kalmbach implication.
ab       (a3 b) = 1
 
Theoremmccune2 247 E2 - OL theorem proved by EQP
(a ∪ ((a ∩ ((ab ) ∩ (ab))) ∪ (a ∩ ((ab) ∪ (ab ))))) = 1
 
Theoremmccune3 248 E3 - OL theorem proved by EQP
((((ab) ∪ (ab )) ∪ (a ∩ (ab))) ∪ (ab)) = 1
 
Theoremi3n1 249 Equivalence for Kalmbach implication.
(a3 b ) = (((ab ) ∪ (ab)) ∪ (a ∩ (ab )))
 
Theoremni31 250 Equivalence for Kalmbach implication.
(a3 b) = (((ab ) ∩ (ab)) ∩ (a ∪ (ab )))
 
Theoremi3id 251 Identity for Kalmbach implication.
(a3 a) = 1
 
Theoremli3 252 Introduce Kalmbach implication to the left.
a = b       (c3 a) = (c3 b)
 
Theoremri3 253 Introduce Kalmbach implication to the right.
a = b       (a3 c) = (b3 c)
 
Theorem2i3 254 Join both sides with Kalmbach implication.
a = b    &   c = d       (a3 c) = (b3 d)
 
Theoremud1lem0a 255 Introduce 1 to the left.
a = b       (c1 a) = (c1 b)
 
Theoremud1lem0b 256 Introduce 1 to the right.
a = b       (a1 c) = (b1 c)
 
Theoremud1lem0ab 257 Join both sides of hypotheses with 1 .
a = b    &   c = d       (a1 c) = (b1 d)
 
Theoremud2lem0a 258 Introduce 2 to the left.
a = b       (c2 a) = (c2 b)
 
Theoremud2lem0b 259 Introduce 2 to the right.
a = b       (a2 c) = (b2 c)
 
Theoremud3lem0a 260 Introduce Kalmbach implication to the left.
a = b       (c3 a) = (c3 b)
 
Theoremud3lem0b 261 Introduce Kalmbach implication to the right.
a = b       (a3 c) = (b3 c)
 
Theoremud4lem0a 262 Introduce 4 to the left.
a = b       (c4 a) = (c4 b)
 
Theoremud4lem0b 263 Introduce 4 to the right.
a = b       (a4 c) = (b4 c)
 
Theoremud5lem0a 264 Introduce 5 to the left.
a = b       (c5 a) = (c5 b)
 
Theoremud5lem0b 265 Introduce 5 to the right.
a = b       (a5 c) = (b5 c)
 
Theoremi1i2 266 Correspondence between Sasaki and Dishkant conditionals.
(a1 b) = (b2 a )
 
Theoremi2i1 267 Correspondence between Sasaki and Dishkant conditionals.
(a2 b) = (b1 a )
 
Theoremi1i2con1 268 Correspondence between Sasaki and Dishkant conditionals.
(a1 b ) = (b2 a )
 
Theoremi1i2con2 269 Correspondence between Sasaki and Dishkant conditionals.
(a1 b) = (b2 a)
 
Theoremi3i4 270 Correspondence between Kalmbach and non-tollens conditionals.
(a3 b) = (b4 a )
 
Theoremi4i3 271 Correspondence between Kalmbach and non-tollens conditionals.
(a4 b) = (b3 a )
 
Theoremi5con 272 Converse of 5 .
(a5 b) = (b5 a )
 
Theorem0i1 273 Antecedent of 0 on Sasaki conditional.
(0 →1 a) = 1
 
Theorem1i1 274 Antecedent of 1 on Sasaki conditional.
(1 →1 a) = a
 
Theoremi1id 275 Identity law for Sasaki conditional.
(a1 a) = 1
 
Theoremi2id 276 Identity law for Dishkant conditional.
(a2 a) = 1
 
Theoremud1lem0c 277 Lemma for unified disjunction.
(a1 b) = (a ∩ (ab ))
 
Theoremud2lem0c 278 Lemma for unified disjunction.
(a2 b) = (b ∩ (ab))
 
Theoremud3lem0c 279 Lemma for unified disjunction.
(a3 b) = (((ab ) ∩ (ab)) ∩ (a ∪ (ab )))
 
Theoremud4lem0c 280 Lemma for unified disjunction.
(a4 b) = (((ab ) ∩ (ab )) ∩ ((ab ) ∪ b))
 
Theoremud5lem0c 281 Lemma for unified disjunction.
(a5 b) = (((ab ) ∩ (ab )) ∩ (ab))
 
Theorembina1 282 Pavicic binary logic ax-a1 analog.
(a3 a ) = 1
 
Theorembina2 283 Pavicic binary logic ax-a2 analog.
(a 3 a) = 1
 
Theorembina3 284 Pavicic binary logic ax-a3 analog.
(a3 (ab)) = 1
 
Theorembina4 285 Pavicic binary logic ax-a4 analog.
(b3 (ab)) = 1
 
Theorembina5 286 Pavicic binary logic ax-a5 analog.
(b3 (aa )) = 1
 
Theoremwql1lem 287 Classical implication inferred from Sakaki implication.
(a1 b) = 1       (ab) = 1
 
Theoremwql2lem 288 Classical implication inferred from Dishkant implication.
(a2 b) = 1       (ab) = 1
 
Theoremwql2lem2 289 Lemma for 2 WQL axiom.
((ac) →2 (bc)) = 1       ((a ∪ (bc)) ∪ (bc)) = 1
 
Theoremwql2lem3 290 Lemma for 2 WQL axiom.
(a2 b) = 1       ((ab ) →2 a ) = 1
 
Theoremwql2lem4 291 Lemma for 2 WQL axiom.
(((ab ) ∪ (ab)) →2 (a ∪ (ab))) = 1    &   ((a1 b) ∪ (ab )) = 1       (a1 b) = 1
 
Theoremwql2lem5 292 Lemma for 2 WQL axiom.
(a2 b) = 1       ((b ∩ (ab)) →2 a ) = 1
 
Theoremwql1 293 The 2nd hypothesis is the first 1 WQL axiom. We show it implies the WOM law.
(a1 b) = 1    &   ((ac) →1 (bc)) = 1    &   c = b       (a2 b) = 1
 
Theoremoaidlem1 294 Lemma for OA identity-like law.
(ab) ≤ c       (a ∪ (b1 c)) = 1
 
Theoremwomle2a 295 An equivalent to the WOM law.
(a ∩ (a2 b)) ≤ ((a2 b) ∪ (a1 b))       ((a2 b) ∪ (a1 b)) = 1
 
Theoremwomle2b 296 An equivalent to the WOM law.
((a2 b) ∪ (a1 b)) = 1       (a ∩ (a2 b)) ≤ ((a2 b) ∪ (a1 b))
 
Theoremwomle3b 297 Implied by the WOM law.
((a1 b) ∪ (a2 b)) = 1       (a ∩ (a1 b)) ≤ ((a1 b) ∪ (a2 b))
 
Theoremwomle 298 An equality implying the WOM law.
(a ∩ (a1 b)) = (a ∩ (a2 b))       ((a2 b) ∪ (a1 b)) = 1
 
Theoremnomb41 299 Lemma for "Non-Orthomodular Models..." paper.
(a4 b) = (b1 a)
 
Theoremnomb32 300 Lemma for "Non-Orthomodular Models..." paper.
(a3 b) = (b2 a)
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200201-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 >