Theorem List for Quantum Logic Explorer - 301-400   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremnomcon0 301 Lemma for "Non-Orthomodular Models..." paper.
(a0 b) = (b0 a )

Theoremnomcon1 302 Lemma for "Non-Orthomodular Models..." paper.
(a1 b) = (b2 a )

Theoremnomcon2 303 Lemma for "Non-Orthomodular Models..." paper.
(a2 b) = (b1 a )

Theoremnomcon3 304 Lemma for "Non-Orthomodular Models..." paper.
(a3 b) = (b4 a )

Theoremnomcon4 305 Lemma for "Non-Orthomodular Models..." paper.
(a4 b) = (b3 a )

Theoremnomcon5 306 Lemma for "Non-Orthomodular Models..." paper.
(ab) = (ba )

Theoremnom10 307 Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
(a0 (ab)) = (a1 b)

Theoremnom11 308 Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
(a1 (ab)) = (a1 b)

Theoremnom12 309 Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
(a2 (ab)) = (a1 b)

Theoremnom13 310 Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
(a3 (ab)) = (a1 b)

Theoremnom14 311 Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
(a4 (ab)) = (a1 b)

Theoremnom15 312 Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
(a5 (ab)) = (a1 b)

Theoremnom20 313 Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
(a0 (ab)) = (a1 b)

Theoremnom21 314 Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
(a1 (ab)) = (a1 b)

Theoremnom22 315 Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
(a2 (ab)) = (a1 b)

Theoremnom23 316 Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
(a3 (ab)) = (a1 b)

Theoremnom24 317 Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
(a4 (ab)) = (a1 b)

Theoremnom25 318 Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
(a ≡ (ab)) = (a1 b)

Theoremnom30 319 Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
((ab) ≡0 a) = (a1 b)

Theoremnom31 320 Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
((ab) ≡1 a) = (a1 b)

Theoremnom32 321 Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
((ab) ≡2 a) = (a1 b)

Theoremnom33 322 Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
((ab) ≡3 a) = (a1 b)

Theoremnom34 323 Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
((ab) ≡4 a) = (a1 b)

Theoremnom35 324 Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
((ab) ≡ a) = (a1 b)

Theoremnom40 325 Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
((ab) →0 b) = (a2 b)

Theoremnom41 326 Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
((ab) →1 b) = (a2 b)

Theoremnom42 327 Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
((ab) →2 b) = (a2 b)

Theoremnom43 328 Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
((ab) →3 b) = (a2 b)

Theoremnom44 329 Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
((ab) →4 b) = (a2 b)

Theoremnom45 330 Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
((ab) →5 b) = (a2 b)

Theoremnom50 331 Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
((ab) ≡0 b) = (a2 b)

Theoremnom51 332 Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
((ab) ≡1 b) = (a2 b)

Theoremnom52 333 Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
((ab) ≡2 b) = (a2 b)

Theoremnom53 334 Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
((ab) ≡3 b) = (a2 b)

Theoremnom54 335 Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
((ab) ≡4 b) = (a2 b)

Theoremnom55 336 Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
((ab) ≡ b) = (a2 b)

Theoremnom60 337 Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
(b0 (ab)) = (a2 b)

Theoremnom61 338 Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
(b1 (ab)) = (a2 b)

Theoremnom62 339 Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
(b2 (ab)) = (a2 b)

Theoremnom63 340 Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
(b3 (ab)) = (a2 b)

Theoremnom64 341 Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
(b4 (ab)) = (a2 b)

Theoremnom65 342 Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
(b ≡ (ab)) = (a2 b)

Theoremgo1 343 Lemma for proof of Mayet 8-variable "full" equation from 4-variable Godowski equation.
((ab) ∩ (a1 b )) = 0

Theoremi2or 344 Lemma for disjunction of 2 .
((a2 c) ∪ (b2 c)) ≤ ((ab) →2 c)

Theoremi1or 345 Lemma for disjunction of 1 .
((c1 a) ∪ (c1 b)) ≤ (c1 (ab))

Theoremlei2 346 "Less than" analogue is equal to 2 implication.
(a2 b) = (a2 b)

Theoremi5lei1 347 Relevance implication is l.e. Sasaki implication.
(a5 b) ≤ (a1 b)

Theoremi5lei2 348 Relevance implication is l.e. Dishkant implication.
(a5 b) ≤ (a2 b)

Theoremi5lei3 349 Relevance implication is l.e. Kalmbach implication.
(a5 b) ≤ (a3 b)

Theoremi5lei4 350 Relevance implication is l.e. non-tollens implication.
(a5 b) ≤ (a4 b)

Theoremid5leid0 351 Quantum identity is less than classical identity.
(ab) ≤ (a0 b)

Theoremid5id0 352 Show that classical identity follows from quantum identity in OL.
(ab) = 1       (a0 b) = 1

Theoremk1-6 353 Statement (6) in proof of Theorem 1 of Kalmbach, Orthomodular Lattices, p. 21.
x = ((xc) ∪ (xc ))       (xc) = ((xc ) ∩ c)

Theoremk1-7 354 Statement (7) in proof of Theorem 1 of Kalmbach, Orthomodular Lattices, p. 21.
x = ((xc) ∪ (xc ))       (xc ) = ((xc) ∩ c )

Theoremk1-8a 355 First part of statement (8) in proof of Theorem 1 of Kalmbach, Orthomodular Lattices, p. 21.
x = ((xc) ∪ (xc ))    &   xc    &   yc       x = ((xy) ∩ c)

Theoremk1-8b 356 Second part of statement (8) in proof of Theorem 1 of Kalmbach, Orthomodular Lattices, p. 21.
y = ((yc) ∪ (yc ))    &   xc    &   yc       y = ((xy) ∩ c )

Theoremk1-2 357 Statement (2) in proof of Theorem 1 of Kalmbach, Orthomodular Lattices, p. 21.
x = ((xc) ∪ (xc ))    &   y = ((yc) ∪ (yc ))    &   ((xc) ∪ (yc)) = ((((xc) ∪ (yc))c) ∪ (((xc) ∪ (yc))c ))       ((xy) ∩ c) = ((xc) ∪ (yc))

Theoremk1-3 358 Statement (3) in proof of Theorem 1 of Kalmbach, Orthomodular Lattices, p. 21.
x = ((xc) ∪ (xc ))    &   y = ((yc) ∪ (yc ))    &   ((xc ) ∪ (yc )) = ((((xc ) ∪ (yc ))c) ∪ (((xc ) ∪ (yc ))c ))       ((xy) ∩ c ) = ((xc ) ∪ (yc ))

Theoremk1-4 359 Statement (4) in proof of Theorem 1 of Kalmbach, Orthomodular Lattices, p. 21.
(x ∩ (xc )) = (((x ∩ (xc )) ∩ c) ∪ ((x ∩ (xc )) ∩ c ))    &   xc       (x ∪ (xc)) = c

Theoremk1-5 360 Statement (5) in proof of Theorem 1 of Kalmbach, Orthomodular Lattices, p. 21.
(x ∩ (xc)) = (((x ∩ (xc)) ∩ c) ∪ ((x ∩ (xc)) ∩ c ))    &   xc       (x ∪ (xc )) = c

0.2  Weakly orthomodular lattices

0.2.1  Weak orthomodular law

Axiomax-wom 361 2-variable WOML rule.
(a ∪ (ab)) = 1       (b ∪ (ab )) = 1

Theorem2vwomr2 362 2-variable WOML rule.
(b ∪ (ab )) = 1       (a ∪ (ab)) = 1

Theorem2vwomr1a 363 2-variable WOML rule.
(a1 b) = 1       (a2 b) = 1

Theorem2vwomr2a 364 2-variable WOML rule.
(a2 b) = 1       (a1 b) = 1

Theorem2vwomlem 365 Lemma from 2-variable WOML rule.
(a2 b) = 1    &   (b2 a) = 1       (ab) = 1

Theoremwr5-2v 366 WOML derived from 2-variable axioms.
(ab) = 1       ((ac) ≡ (bc)) = 1

0.2.2  Weakly orthomodular lattices

Theoremwom3 367 Weak orthomodular law for study of weakly orthomodular lattices.
(ab) = 1       a ≤ ((ac) ≡ (bc))

Theoremwlor 368 Weak orthomodular law.
(ab) = 1       ((ca) ≡ (cb)) = 1

Theoremwran 369 Weak orthomodular law.
(ab) = 1       ((ac) ≡ (bc)) = 1

Theoremwlan 370 Weak orthomodular law.
(ab) = 1       ((ca) ≡ (cb)) = 1

Theoremwr2 371 Inference rule of AUQL.
(ab) = 1    &   (bc) = 1       (ac) = 1

Theoremw2or 372 Join both sides with disjunction.
(ab) = 1    &   (cd) = 1       ((ac) ≡ (bd)) = 1

Theoremw2an 373 Join both sides with conjunction.
(ab) = 1    &   (cd) = 1       ((ac) ≡ (bd)) = 1

Theoremw3tr1 374 Transitive inference useful for introducing definitions.
(ab) = 1    &   (ca) = 1    &   (db) = 1       (cd) = 1

Theoremw3tr2 375 Transitive inference useful for eliminating definitions.
(ab) = 1    &   (ac) = 1    &   (bd) = 1       (cd) = 1

0.2.3  Relationship analogues (ordering; commutation) in WOML

Theoremwleoa 376 Relation between two methods of expressing "less than or equal to".
((ac) ≡ b) = 1       ((ab) ≡ a) = 1

Theoremwleao 377 Relation between two methods of expressing "less than or equal to".
((cb) ≡ a) = 1       ((ab) ≡ b) = 1

Theoremwdf-le1 378 Define 'less than or equal to' analogue for analogue of =.
((ab) ≡ b) = 1       (a2 b) = 1

Theoremwdf-le2 379 Define 'less than or equal to' analogue for analogue of =.
(a2 b) = 1       ((ab) ≡ b) = 1

Theoremwom4 380 Orthomodular law. Kalmbach 83 p. 22.
(a2 b) = 1       ((a ∪ (ab)) ≡ b) = 1

Theoremwom5 381 Orthomodular law. Kalmbach 83 p. 22.
(a2 b) = 1    &   ((ba ) ≡ 0) = 1       (ab) = 1

Theoremwcomlem 382 Analogue of commutation is symmetric. Similar to Kalmbach 83 p. 22.
(a ≡ ((ab) ∪ (ab ))) = 1       (b ≡ ((ba) ∪ (ba ))) = 1

Theoremwdf-c1 383 Show that commutator is a 'commutes' analogue for analogue of =.
(a ≡ ((ab) ∪ (ab ))) = 1        C (a, b) = 1

Theoremwdf-c2 384 Show that commutator is a 'commutes' analogue for analogue of =.
C (a, b) = 1       (a ≡ ((ab) ∪ (ab ))) = 1

Theoremwdf2le1 385 Alternate definition of 'less than or equal to'.
((ab) ≡ a) = 1       (a2 b) = 1

Theoremwdf2le2 386 Alternate definition of 'less than or equal to'.
(a2 b) = 1       ((ab) ≡ a) = 1

Theoremwleo 387 L.e. absorption.
(a2 (ab)) = 1

Theoremwlea 388 L.e. absorption.
((ab) ≤2 a) = 1

Theoremwle1 389 Anything is l.e. 1.
(a2 1) = 1

Theoremwle0 390 0 is l.e. anything.
(0 ≤2 a) = 1

Theoremwler 391 Add disjunct to right of l.e.
(a2 b) = 1       (a2 (bc)) = 1

Theoremwlel 392 Add conjunct to left of l.e.
(a2 b) = 1       ((ac) ≤2 b) = 1

Theoremwleror 393 Add disjunct to right of both sides.
(a2 b) = 1       ((ac) ≤2 (bc)) = 1

Theoremwleran 394 Add conjunct to right of both sides.
(a2 b) = 1       ((ac) ≤2 (bc)) = 1

Theoremwlecon 395 Contrapositive for l.e.
(a2 b) = 1       (b2 a ) = 1

Theoremwletr 396 Transitive law for l.e.
(a2 b) = 1    &   (b2 c) = 1       (a2 c) = 1

Theoremwbltr 397 Transitive inference.
(ab) = 1    &   (b2 c) = 1       (a2 c) = 1

Theoremwlbtr 398 Transitive inference.
(a2 b) = 1    &   (bc) = 1       (a2 c) = 1

Theoremwle3tr1 399 Transitive inference useful for introducing definitions.
(a2 b) = 1    &   (ca) = 1    &   (db) = 1       (c2 d) = 1

Theoremwle3tr2 400 Transitive inference useful for eliminating definitions.
(a2 b) = 1    &   (ac) = 1    &   (bd) = 1       (c2 d) = 1

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300301-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 >