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

Theoremu1lemc4 701 Lemma for Sasaki implication study.
a C b       (a1 b) = (ab)

Theoremu2lemc4 702 Lemma for Dishkant implication study.
a C b       (a2 b) = (ab)

Theoremu3lemc4 703 Lemma for Kalmbach implication study.
a C b       (a3 b) = (ab)

Theoremu4lemc4 704 Lemma for non-tollens implication study.
a C b       (a4 b) = (ab)

Theoremu5lemc4 705 Lemma for relevance implication study.
a C b       (a5 b) = (ab)

Theoremu1lemc6 706 Commutation theorem for Sasaki implication.
(a1 b) C (a1 b)

Theoremcomi12 707 Commutation theorem for 1 and 2 .
(a1 b) C (c2 a)

Theoremi1com 708 Commutation expressed with 1 .
b ≤ (a1 b)       a C b

Theoremcomi1 709 Commutation expressed with 1 .
a C b       b ≤ (a1 b)

Theoremu1lemle1 710 L.e. to Sasaki implication.
ab       (a1 b) = 1

Theoremu2lemle1 711 L.e. to Dishkant implication.
ab       (a2 b) = 1

Theoremu3lemle1 712 L.e. to Kalmbach implication.
ab       (a3 b) = 1

Theoremu4lemle1 713 L.e. to non-tollens implication.
ab       (a4 b) = 1

Theoremu5lemle1 714 L.e. to relevance implication.
ab       (a5 b) = 1

Theoremu1lemle2 715 Sasaki implication to l.e.
(a1 b) = 1       ab

Theoremu2lemle2 716 Dishkant implication to l.e.
(a2 b) = 1       ab

Theoremu3lemle2 717 Kalmbach implication to l.e.
(a3 b) = 1       ab

Theoremu4lemle2 718 Non-tollens implication to l.e.
(a4 b) = 1       ab

Theoremu5lemle2 719 Relevance implication to l.e.
(a5 b) = 1       ab

Theoremu1lembi 720 Sasaki implication and biconditional.
((a1 b) ∩ (b1 a)) = (ab)

Theoremu2lembi 721 Dishkant implication and biconditional.
((a2 b) ∩ (b2 a)) = (ab)

Theoremi2bi 722 Dishkant implication expressed with biconditional.
(a2 b) = (b ∪ (ab))

Theoremu3lembi 723 Kalmbach implication and biconditional.
((a3 b) ∩ (b3 a)) = (ab)

Theoremu4lembi 724 Non-tollens implication and biconditional.
((a4 b) ∩ (b4 a)) = (ab)

Theoremu5lembi 725 Relevance implication and biconditional.
((a5 b) ∩ (b5 a)) = (ab)

Theoremu12lembi 726 Sasaki/Dishkant implication and biconditional. Equation 4.14 of [MegPav2000] p. 23. The variable i in the paper is set to 1, and j is set to 2.
((a1 b) ∩ (b2 a)) = (ab)

Theoremu21lembi 727 Dishkant/Sasaki implication and biconditional.
((a2 b) ∩ (b1 a)) = (ab)

Theoremublemc1 728 Commutation theorem for biimplication.
a C (ab)

Theoremublemc2 729 Commutation theorem for biimplication.
b C (ab)

0.3.7  Some proofs contributed by Josiah Burroughs

Theoremu1lemn1b 730 This theorem continues the line of proofs such as u1lemnaa 640, ud1lem0b 256, u1lemnanb 655, etc. (Contributed by Josiah Burroughs 26-May-04.)
(a1 b) = ((a1 b)1 b)

Theoremu1lem3var1 731 A 3-variable formula. (Contributed by Josiah Burroughs 26-May-04.)
(((a1 c) ∩ (b1 c)) ∪ (((a1 c)1 c) ∩ ((b1 c)1 c))) = 1

Theoremoi3oa3lem1 732 An attempt at the OA3 conjecture, which is true if (ab) = 1. (Contributed by Josiah Burroughs 27-May-04.)
1 = (ba)       (((a1 c) ∩ (b1 c)) ∪ (ab)) = 1

Theoremoi3oa3 733 An attempt at the OA3 conjecture, which is true if (ab) = 1. (Contributed by Josiah Burroughs 27-May-04.)
1 = (ba)       (((a1 c) ∩ (b1 c)) ∪ ((((a1 c) ∩ (((a1 c) ∩ (b1 c)) ∪ (ab))) →1 c) ∩ (((b1 c) ∩ (((a1 c) ∩ (b1 c)) ∪ (ab))) →1 c))) = 1

0.3.8  More lemmas for unified implication

Theoremu1lem1 734 Lemma for unified implication study.
((a1 b) →1 a) = a

Theoremu2lem1 735 Lemma for unified implication study.
((a2 b) →2 a) = a

Theoremu3lem1 736 Lemma for unified implication study.
((a3 b) →3 a) = ((ab) ∩ (ab ))

Theoremu4lem1 737 Lemma for unified implication study.
((a4 b) →4 a) = ((((ab) ∪ (ab )) ∪ a ) ∩ ((ab) ∩ (ab )))

Theoremu5lem1 738 Lemma for unified implication study.
((a5 b) →5 a) = ((ab) ∩ (ab ))

Theoremu1lem1n 739 Lemma for unified implication study.
((a1 b) →1 a) = a

Theoremu2lem1n 740 Lemma for unified implication study.
((a2 b) →2 a) = a

Theoremu3lem1n 741 Lemma for unified implication study.
((a3 b) →3 a) = ((ab) ∪ (ab ))

Theoremu4lem1n 742 Lemma for unified implication study.
((a4 b) →4 a) = ((((ab) ∩ (ab )) ∩ a) ∪ ((ab) ∪ (ab )))

Theoremu5lem1n 743 Lemma for unified implication study.
((a5 b) →5 a) = ((ab) ∪ (ab ))

Theoremu1lem2 744 Lemma for unified implication study.
(((a1 b) →1 a) →1 a) = 1

Theoremu2lem2 745 Lemma for unified implication study.
(((a2 b) →2 a) →2 a) = 1

Theoremu3lem2 746 Lemma for unified implication study.
(((a3 b) →3 a) →3 a) = (a ∪ ((ab) ∪ (ab )))

Theoremu4lem2 747 Lemma for unified implication study.
(((a4 b) →4 a) →4 a) = (a ∪ ((ab) ∪ (ab )))

Theoremu5lem2 748 Lemma for unified implication study.
(((a5 b) →5 a) →5 a) = (a ∪ ((ab) ∪ (ab )))

Theoremu1lem3 749 Lemma for unified implication study.
(a1 (b1 a)) = (a ∪ ((ab) ∪ (ab )))

Theoremu2lem3 750 Lemma for unified implication study.
(a2 (b2 a)) = 1

Theoremu3lem3 751 Lemma for unified implication study.
(a3 (b3 a)) = (a ∪ ((ab) ∪ (ab )))

Theoremu4lem3 752 Lemma for unified implication study.
(a4 (b4 a)) = (a ∪ ((ab) ∪ (ab )))

Theoremu5lem3 753 Lemma for unified implication study.
(a5 (b5 a)) = (a ∪ ((ab) ∪ (ab )))

Theoremu3lem3n 754 Lemma for unified implication study.
(a3 (b3 a)) = (a ∩ ((ab) ∩ (ab )))

Theoremu4lem3n 755 Lemma for unified implication study.
(a4 (b4 a)) = (a ∩ ((ab) ∩ (ab )))

Theoremu5lem3n 756 Lemma for unified implication study.
(a5 (b5 a)) = (a ∩ ((ab) ∩ (ab )))

Theoremu1lem4 757 Lemma for unified implication study.
(a1 (a1 (b1 a))) = (a1 (b1 a))

Theoremu3lem4 758 Lemma for unified implication study.
(a3 (a3 (b3 a))) = 1

Theoremu4lem4 759 Lemma for unified implication study.
(a4 (a4 (b4 a))) = (a4 (b4 a))

Theoremu5lem4 760 Lemma for unified implication study.
(a5 (a5 (b5 a))) = (a5 (b5 a))

Theoremu1lem5 761 Lemma for unified implication study.
(a1 (a1 b)) = (a1 b)

Theoremu2lem5 762 Lemma for unified implication study.
(a2 (a2 b)) = (a2 b)

Theoremu3lem5 763 Lemma for unified implication study.
(a3 (a3 b)) = (ab)

Theoremu4lem5 764 Lemma for unified implication study.
(a4 (a4 b)) = ((ab ) ∪ b)

Theoremu5lem5 765 Lemma for unified implication study.
(a5 (a5 b)) = (a ∪ (ab))

Theoremu4lem5n 766 Lemma for unified implication study.
(a4 (a4 b)) = ((ab) ∩ b )

Theoremu3lem6 767 Lemma for unified implication study.
(a3 (a3 (a3 b))) = (a3 (a3 b))

Theoremu4lem6 768 Lemma for unified implication study.
(a4 (a4 (a4 b))) = (a4 b)

Theoremu5lem6 769 Lemma for unified implication study.
(a5 (a5 (a5 b))) = (a5 (a5 b))

Theoremu24lem 770 Lemma for unified implication study.
((a2 b) ∩ (a4 b)) = (a5 b)

Theoremu12lem 771 Implication lemma.
((a1 b) ∪ (a2 b)) = (a0 b)

Theoremu1lem7 772 Lemma for unified implication study.
(a1 (a1 b)) = 1

Theoremu2lem7 773 Lemma for unified implication study.
(a2 (a2 b)) = (((ab ) ∪ (ab )) ∪ b)

Theoremu3lem7 774 Lemma for unified implication study.
(a3 (a3 b)) = (a ∪ ((ab) ∪ (ab )))

Theoremu2lem7n 775 Lemma for unified implication study.
(a2 (a2 b)) = (((ab) ∩ (ab)) ∩ b )

Theoremu1lem8 776 Lemma used in study of orthoarguesian law.
((a1 b) ∩ (a1 b)) = ((ab) ∪ (ab))

Theoremu1lem9a 777 Lemma used in study of orthoarguesian law. Equation 4.11 of [MegPav2000] p. 23. This is the first part of the inequality.
(a1 b)a

Theoremu1lem9b 778 Lemma used in study of orthoarguesian law. Equation 4.11 of [MegPav2000] p. 23. This is the second part of the inequality.
a ≤ (a1 b)

Theoremu1lem9ab 779 Lemma used in study of orthoarguesian law.
(a1 b) ≤ (a1 b)

Theoremu1lem11 780 Lemma used in study of orthoarguesian law.
((a1 b) →1 b) = (a1 b)

Theoremu1lem12 781 Lemma used in study of orthoarguesian law. Equation 4.12 of [MegPav2000] p. 23.
((a1 b) →1 b) = (a1 b)

Theoremu2lem8 782 Lemma for unified implication study.
(a2 (a2 (a2 b))) = (a2 (a2 b))

Theoremu3lem8 783 Lemma for unified implication study.
(a3 (a3 (a3 b))) = 1

Theoremu3lem9 784 Lemma for unified implication study.
(a3 (a3 (a3 b))) = (a3 (a3 b))

Theoremu3lem10 785 Lemma for unified implication study.
(a3 (a ∩ (ab))) = a

Theoremu3lem11 786 Lemma for unified implication study.
(a3 (b ∩ (ab))) = (a3 b )

Theoremu3lem11a 787 Lemma for unified implication study.
(a3 ((b3 a) →3 (a3 b)) ) = (a3 b )

Theoremu3lem12 788 Lemma for unified implication study.
(a3 (a3 b )) = (ab)

Theoremu3lem13a 789 Lemma for unified implication study.
(a3 (a3 b ) ) = (a1 b)

Theoremu3lem13b 790 Lemma for unified implication study.
((a3 b ) →3 a ) = (a1 b)

Theoremu3lem14a 791 Lemma for unified implication study.
(a3 ((b3 a ) →3 b )) = (a3 (b3 a))

Theoremu3lem14aa 792 Used to prove 1 "add antecedent" rule in 3 system.
(a3 (a3 ((b3 a ) →3 b ))) = 1

Theoremu3lem14aa2 793 Used to prove 1 "add antecedent" rule in 3 system.
(a3 (a3 (b3 (b3 a ) ))) = 1

Theoremu3lem14mp 794 Used to prove 1 modus ponens rule in 3 system.
((a3 b )3 (a3 (a3 b))) = 1

Theoremu3lem15 795 Lemma for Kalmbach implication.
((a3 b) ∩ (ab)) = ((ab) ∩ (a ∪ (ab)))

Theoremu3lemax4 796 Possible axiom for Kalmbach implication system.
((a3 b) →3 ((a3 b) →3 ((b3 a) →3 ((b3 a) →3 ((c3 (c3 a)) →3 (c3 (c3 b))))))) = 1

Theoremu3lemax5 797 Possible axiom for Kalmbach implication system.
((a3 b) →3 ((a3 b) →3 ((b3 a) →3 ((b3 a) →3 ((b3 c) →3 ((b3 c) →3 ((c3 b) →3 ((c3 b) →3 (a3 c))))))))) = 1

Theorembi1o1a 798 Equivalence to biconditional.
(ab) = ((a1 (ab)) ∩ ((ab) →1 a))

Theorembiao 799 Equivalence to biconditional.
(ab) = ((ab) ≡ (ab))

Theoremi2i1i1 800 Equivalence to 2 .
(a2 b) = ((a1 (ab)) ∩ ((ab) →1 b))

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1215
 Copyright terms: Public domain < Previous  Next >