Theorem List for Quantum Logic Explorer - 401-500 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | wbile 401 |
Biconditional to l.e.
|
|
|
Theorem | wlebi 402 |
L.e. to biconditional.
|
|
|
Theorem | wle2or 403 |
Disjunction of 2 l.e.'s.
|
|
|
Theorem | wle2an 404 |
Conjunction of 2 l.e.'s.
|
|
|
Theorem | wledi 405 |
Half of distributive law.
|
|
|
Theorem | wledio 406 |
Half of distributive law.
|
|
|
Theorem | wcom0 407 |
Commutation with 0. Kalmbach 83 p. 20.
|
|
|
Theorem | wcom1 408 |
Commutation with 1. Kalmbach 83 p. 20.
|
|
|
Theorem | wlecom 409 |
Comparable elements commute. Beran 84 2.3(iii) p. 40.
|
|
|
Theorem | wbctr 410 |
Transitive inference.
|
|
|
Theorem | wcbtr 411 |
Transitive inference.
|
|
|
Theorem | wcomorr 412 |
Weak commutation law.
|
|
|
Theorem | wcoman1 413 |
Weak commutation law.
|
|
|
Theorem | wcomcom 414 |
Commutation is symmetric. Kalmbach 83 p. 22.
|
|
|
Theorem | wcomcom2 415 |
Commutation equivalence. Kalmbach 83 p. 23.
|
|
|
Theorem | wcomcom3 416 |
Commutation equivalence. Kalmbach 83 p. 23.
|
|
|
Theorem | wcomcom4 417 |
Commutation equivalence. Kalmbach 83 p. 23.
|
|
|
Theorem | wcomd 418 |
Commutation dual. Kalmbach 83 p. 23.
|
|
|
Theorem | wcom3ii 419 |
Lemma 3(ii) of Kalmbach 83 p. 23.
|
|
|
Theorem | wcomcom5 420 |
Commutation equivalence. Kalmbach 83 p. 23.
|
|
|
Theorem | wcomdr 421 |
Commutation dual. Kalmbach 83 p. 23.
|
|
|
Theorem | wcom3i 422 |
Lemma 3(i) of Kalmbach 83 p. 23.
|
|
|
Theorem | wfh1 423 |
Weak structural analog of Foulis-Holland Theorem.
|
|
|
Theorem | wfh2 424 |
Weak structural analog of Foulis-Holland Theorem.
|
|
|
Theorem | wfh3 425 |
Weak structural analog of Foulis-Holland Theorem.
|
|
|
Theorem | wfh4 426 |
Weak structural analog of Foulis-Holland Theorem.
|
|
|
Theorem | wcom2or 427 |
Th. 4.2 Beran p. 49.
|
|
|
Theorem | wcom2an 428 |
Th. 4.2 Beran p. 49.
|
|
|
Theorem | wnbdi 429 |
Negated biconditional (distributive form)
|
|
|
Theorem | wlem14 430 |
Lemma for KA14 soundness.
|
|
|
Theorem | wr5 431 |
Proof of weak orthomodular law from weaker-looking equivalent, wom3 367,
which in turn is derived from ax-wom 361.
|
|
|
0.2.4 Kalmbach axioms (soundness proofs) that
require WOML
|
|
Theorem | ska2 432 |
Soundness theorem for Kalmbach's quantum propositional logic axiom KA2.
|
|
|
Theorem | ska4 433 |
Soundness theorem for Kalmbach's quantum propositional logic axiom KA4.
|
|
|
Theorem | wom2 434 |
Weak orthomodular law for study of weakly orthomodular lattices.
|
|
|
Theorem | ka4ot 435 |
3-variable version of weakly orthomodular law. It is proved from a
weaker-looking equivalent, wom2 434, which in turn is proved from
ax-wom 361.
|
|
|
0.2.5 Weak orthomodular law variants
|
|
Theorem | woml6 436 |
Variant of weakly orthomodular law.
|
|
|
Theorem | woml7 437 |
Variant of weakly orthomodular law.
|
|
|
Theorem | ortha 438 |
Property of orthogonality.
|
|
|
0.3 Orthomodular lattices
|
|
0.3.1 Orthomodular law
|
|
Axiom | ax-r3 439 |
Orthomodular law - when added to an ortholattice, it makes the
ortholattice an orthomodular lattice. See r3a 440 for
a more compact
version.
|
|
|
Theorem | r3a 440 |
Orthomodular law restated.
|
|
|
Theorem | wed 441 |
Weak equivalential detachment (WBMP).
|
|
|
Theorem | r3b 442 |
Orthomodular law from weak equivalential detachment (WBMP).
|
|
|
Theorem | lem3.1 443 |
Lemma used in proof of Th. 3.1 of Pavicic 1993.
|
|
|
Theorem | lem3a.1 444 |
Lemma used in proof of Th. 3.1 of Pavicic 1993.
|
|
|
Theorem | oml 445 |
Orthomodular law. Compare Th. 1 of Pavicic 1987.
|
|
|
Theorem | omln 446 |
Orthomodular law.
|
|
|
Theorem | omla 447 |
Orthomodular law.
|
|
|
Theorem | omlan 448 |
Orthomodular law.
|
|
|
Theorem | oml5 449 |
Orthomodular law.
|
|
|
Theorem | oml5a 450 |
Orthomodular law.
|
|
|
0.3.2 Relationship analogues using OML (ordering;
commutation)
|
|
Theorem | oml2 451 |
Orthomodular law. Kalmbach 83 p. 22.
|
|
|
Theorem | oml3 452 |
Orthomodular law. Kalmbach 83 p. 22.
|
|
|
Theorem | comcom 453 |
Commutation is symmetric. Kalmbach 83 p. 22.
|
|
|
Theorem | comcom3 454 |
Commutation equivalence. Kalmbach 83 p. 23.
|
|
|
Theorem | comcom4 455 |
Commutation equivalence. Kalmbach 83 p. 23.
|
|
|
Theorem | comd 456 |
Commutation dual. Kalmbach 83 p. 23.
|
|
|
Theorem | com3ii 457 |
Lemma 3(ii) of Kalmbach 83 p. 23.
|
|
|
Theorem | comcom5 458 |
Commutation equivalence. Kalmbach 83 p. 23.
|
|
|
Theorem | comcom6 459 |
Commutation equivalence. Kalmbach 83 p. 23.
|
|
|
Theorem | comcom7 460 |
Commutation equivalence. Kalmbach 83 p. 23.
|
|
|
Theorem | comor1 461 |
Commutation law.
|
|
|
Theorem | comor2 462 |
Commutation law.
|
|
|
Theorem | comorr2 463 |
Commutation law.
|
|
|
Theorem | comanr1 464 |
Commutation law.
|
|
|
Theorem | comanr2 465 |
Commutation law.
|
|
|
Theorem | comdr 466 |
Commutation dual. Kalmbach 83 p. 23.
|
|
|
Theorem | com3i 467 |
Lemma 3(i) of Kalmbach 83 p. 23.
|
|
|
Theorem | df2c1 468 |
Dual 'commutes' analogue for analogue of .
|
|
|
Theorem | fh1 469 |
Foulis-Holland Theorem.
|
|
|
Theorem | fh2 470 |
Foulis-Holland Theorem.
|
|
|
Theorem | fh3 471 |
Foulis-Holland Theorem.
|
|
|
Theorem | fh4 472 |
Foulis-Holland Theorem.
|
|
|
Theorem | fh1r 473 |
Foulis-Holland Theorem.
|
|
|
Theorem | fh2r 474 |
Foulis-Holland Theorem.
|
|
|
Theorem | fh3r 475 |
Foulis-Holland Theorem.
|
|
|
Theorem | fh4r 476 |
Foulis-Holland Theorem.
|
|
|
Theorem | fh2c 477 |
Foulis-Holland Theorem.
|
|
|
Theorem | fh4c 478 |
Foulis-Holland Theorem.
|
|
|
Theorem | fh1rc 479 |
Foulis-Holland Theorem.
|
|
|
Theorem | fh2rc 480 |
Foulis-Holland Theorem.
|
|
|
Theorem | fh3rc 481 |
Foulis-Holland Theorem.
|
|
|
Theorem | fh4rc 482 |
Foulis-Holland Theorem.
|
|
|
Theorem | com2or 483 |
Th. 4.2 Beran p. 49.
|
|
|
Theorem | com2an 484 |
Th. 4.2 Beran p. 49.
|
|
|
Theorem | combi 485 |
Commutation theorem for Sasaki implication.
|
|
|
Theorem | nbdi 486 |
Negated biconditional (distributive form)
|
|
|
Theorem | oml4 487 |
Orthomodular law.
|
|
|
Theorem | oml6 488 |
Orthomodular law.
|
|
|
Theorem | gsth 489 |
Gudder-Schelp's Theorem. Beran, p. 262, Th. 4.1.
|
|
|
Theorem | gsth2 490 |
Stronger version of Gudder-Schelp's Theorem. Beran, p. 263, Th. 4.2.
|
|
|
Theorem | gstho 491 |
"OR" version of Gudder-Schelp's Theorem.
|
|
|
Theorem | gt1 492 |
Part of Lemma 1 from Gaisi Takeuti, "Quantum Set Theory".
|
|
|
0.3.3 Commutator (orthomodular lattice
theorems)
|
|
Theorem | cmtr1com 493 |
Commutator equal to 1 commutes. Theorem 2.11 of Beran, p. 86.
|
|
|
Theorem | comcmtr1 494 |
Commutation implies commutator equal to 1. Theorem 2.11 of Beran,
p. 86.
|
|
|
Theorem | i0cmtrcom 495 |
Commutator element commutator implies commutation.
|
|
|
0.3.4 Kalmbach conditional
|
|
Theorem | i3bi 496 |
Kalmbach implication and biconditional.
|
|
|
Theorem | i3or 497 |
Kalmbach implication OR builder.
|
|
|
Theorem | df2i3 498 |
Alternate definition for Kalmbach implication.
|
|
|
Theorem | dfi3b 499 |
Alternate Kalmbach conditional.
|
|
|
Theorem | dfi4b 500 |
Alternate non-tollens conditional.
|
|