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)

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 >