Quantum Logic Explorer - mmtheorems8

Jump to page: 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1024

Statement List for Quantum Logic Explorer - 701-800 - Page 8 of 11

Type	Label	Description
Statement
Theorem	u5lemle2 701	Relevance implication to l.e.
(a →5 b) = 1    ⇒   a ≤ b
Theorem	u1lembi 702	Sasaki implication and biconditional.
((a →1 b) ∩ (b →1 a)) = (a ≡ b)
Theorem	u2lembi 703	Dishkant implication and biconditional.
((a →2 b) ∩ (b →2 a)) = (a ≡ b)
Theorem	i2bi 704	Dishkant implication expressed with biconditional.
(a →2 b) = (b ∪ (a ≡ b))
Theorem	u3lembi 705	Kalmbach implication and biconditional.
((a →3 b) ∩ (b →3 a)) = (a ≡ b)
Theorem	u4lembi 706	Non-tollens implication and biconditional.
((a →4 b) ∩ (b →4 a)) = (a ≡ b)
Theorem	u5lembi 707	Relevance implication and biconditional.
((a →5 b) ∩ (b →5 a)) = (a ≡ b)
Theorem	u12lembi 708	Sasaki/Dishkant implication and biconditional.
((a →1 b) ∩ (b →2 a)) = (a ≡ b)
Theorem	u21lembi 709	Dishkant/Sasaki implication and biconditional.
((a →2 b) ∩ (b →1 a)) = (a ≡ b)
Theorem	ublemc1 710	Commutation theorem for biimplication.
a C (a ≡ b)
Theorem	ublemc2 711	Commutation theorem for biimplication.
b C (a ≡ b)
Theorem	u1lemn1b 712	This theorem continues the line of proofs such as u1lemnaa 622, ud1lem0b 248, u1lemnanb 637, etc. (Contributed by Josiah Burroughs 26-May-04.)
(a →1 b) = ((a →1 b)⊥ →1 b)
Theorem	u1lem3var1 713	A 3-variable formula. (Contributed by Josiah Burroughs 26-May-04.)
(((a →1 c) ∩ (b →1 c))⊥ ∪ (((a →1 c)⊥ →1 c) ∩ ((b →1 c)⊥ →1 c))) = 1
Theorem	oi3oa3lem1 714	An attempt at the OA3 conjecture, which is true if (a ≡ b) = 1. (Contributed by Josiah Burroughs 27-May-04.)
1 = (b ≡ a)    ⇒   (((a →1 c) ∩ (b →1 c)) ∪ (a ∩ b)) = 1
Theorem	oi3oa3 715	An attempt at the OA3 conjecture, which is true if (a ≡ b) = 1. (Contributed by Josiah Burroughs 27-May-04.)
1 = (b ≡ a)    ⇒   (((a →1 c) ∩ (b →1 c)) ∪ ((((a →1 c) ∩ (((a →1 c) ∩ (b →1 c)) ∪ (a ∩ b))) →1 c) ∩ (((b →1 c) ∩ (((a →1 c) ∩ (b →1 c)) ∪ (a ∩ b))) →1 c))) = 1
Theorem	u1lem1 716	Lemma for unified implication study.
((a →1 b) →1 a) = a
Theorem	u2lem1 717	Lemma for unified implication study.
((a →2 b) →2 a) = a
Theorem	u3lem1 718	Lemma for unified implication study.
((a →3 b) →3 a) = ((a ∪ b) ∩ (a ∪ b⊥ ))
Theorem	u4lem1 719	Lemma for unified implication study.
((a →4 b) →4 a) = ((((a ∩ b) ∪ (a ∩ b⊥ )) ∪ a⊥ ) ∩ ((a ∪ b) ∩ (a ∪ b⊥ )))
Theorem	u5lem1 720	Lemma for unified implication study.
((a →5 b) →5 a) = ((a ∪ b) ∩ (a ∪ b⊥ ))
Theorem	u1lem1n 721	Lemma for unified implication study.
((a →1 b) →1 a)⊥ = a⊥
Theorem	u2lem1n 722	Lemma for unified implication study.
((a →2 b) →2 a)⊥ = a⊥
Theorem	u3lem1n 723	Lemma for unified implication study.
((a →3 b) →3 a)⊥ = ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))
Theorem	u4lem1n 724	Lemma for unified implication study.
((a →4 b) →4 a)⊥ = ((((a⊥ ∪ b) ∩ (a⊥ ∪ b⊥ )) ∩ a) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )))
Theorem	u5lem1n 725	Lemma for unified implication study.
((a →5 b) →5 a)⊥ = ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))
Theorem	u1lem2 726	Lemma for unified implication study.
(((a →1 b) →1 a) →1 a) = 1
Theorem	u2lem2 727	Lemma for unified implication study.
(((a →2 b) →2 a) →2 a) = 1
Theorem	u3lem2 728	Lemma for unified implication study.
(((a →3 b) →3 a) →3 a) = (a ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )))
Theorem	u4lem2 729	Lemma for unified implication study.
(((a →4 b) →4 a) →4 a) = (a ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )))
Theorem	u5lem2 730	Lemma for unified implication study.
(((a →5 b) →5 a) →5 a) = (a ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )))
Theorem	u1lem3 731	Lemma for unified implication study.
(a →1 (b →1 a)) = (a⊥ ∪ ((a ∩ b) ∪ (a ∩ b⊥ )))
Theorem	u2lem3 732	Lemma for unified implication study.
(a →2 (b →2 a)) = 1
Theorem	u3lem3 733	Lemma for unified implication study.
(a →3 (b →3 a)) = (a ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )))
Theorem	u4lem3 734	Lemma for unified implication study.
(a →4 (b →4 a)) = (a⊥ ∪ ((a ∩ b) ∪ (a ∩ b⊥ )))
Theorem	u5lem3 735	Lemma for unified implication study.
(a →5 (b →5 a)) = (a⊥ ∪ ((a ∩ b) ∪ (a ∩ b⊥ )))
Theorem	u3lem3n 736	Lemma for unified implication study.
(a →3 (b →3 a))⊥ = (a⊥ ∩ ((a ∪ b) ∩ (a ∪ b⊥ )))
Theorem	u4lem3n 737	Lemma for unified implication study.
(a →4 (b →4 a))⊥ = (a ∩ ((a⊥ ∪ b) ∩ (a⊥ ∪ b⊥ )))
Theorem	u5lem3n 738	Lemma for unified implication study.
(a →5 (b →5 a))⊥ = (a ∩ ((a⊥ ∪ b) ∩ (a⊥ ∪ b⊥ )))
Theorem	u1lem4 739	Lemma for unified implication study.
(a →1 (a →1 (b →1 a))) = (a →1 (b →1 a))
Theorem	u3lem4 740	Lemma for unified implication study.
(a →3 (a →3 (b →3 a))) = 1
Theorem	u4lem4 741	Lemma for unified implication study.
(a →4 (a →4 (b →4 a))) = (a →4 (b →4 a))
Theorem	u5lem4 742	Lemma for unified implication study.
(a →5 (a →5 (b →5 a))) = (a →5 (b →5 a))
Theorem	u1lem5 743	Lemma for unified implication study.
(a →1 (a →1 b)) = (a →1 b)
Theorem	u2lem5 744	Lemma for unified implication study.
(a →2 (a →2 b)) = (a →2 b)
Theorem	u3lem5 745	Lemma for unified implication study.
(a →3 (a →3 b)) = (a⊥ ∪ b)
Theorem	u4lem5 746	Lemma for unified implication study.
(a →4 (a →4 b)) = ((a⊥ ∩ b⊥ ) ∪ b)
Theorem	u5lem5 747	Lemma for unified implication study.
(a →5 (a →5 b)) = (a⊥ ∪ (a ∩ b))
Theorem	u4lem5n 748	Lemma for unified implication study.
(a →4 (a →4 b))⊥ = ((a ∪ b) ∩ b⊥ )
Theorem	u3lem6 749	Lemma for unified implication study.
(a →3 (a →3 (a →3 b))) = (a →3 (a →3 b))
Theorem	u4lem6 750	Lemma for unified implication study.
(a →4 (a →4 (a →4 b))) = (a →4 b)
Theorem	u5lem6 751	Lemma for unified implication study.
(a →5 (a →5 (a →5 b))) = (a →5 (a →5 b))
Theorem	u24lem 752	Lemma for unified implication study.
((a →2 b) ∩ (a →4 b)) = (a →5 b)
Theorem	u12lem 753	Implication lemma.
((a →1 b) ∪ (a →2 b)) = (a →0 b)
Theorem	u1lem7 754	Lemma for unified implication study.
(a →1 (a⊥ →1 b)) = 1
Theorem	u2lem7 755	Lemma for unified implication study.
(a →2 (a⊥ →2 b)) = (((a ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ )) ∪ b)
Theorem	u3lem7 756	Lemma for unified implication study.
(a →3 (a⊥ →3 b)) = (a⊥ ∪ ((a ∩ b) ∪ (a ∩ b⊥ )))
Theorem	u2lem7n 757	Lemma for unified implication study.
(a →2 (a⊥ →2 b))⊥ = (((a ∪ b) ∩ (a⊥ ∪ b)) ∩ b⊥ )
Theorem	u1lem8 758	Lemma used in study of orthoarguesian law.
((a →1 b) ∩ (a⊥ →1 b)) = ((a ∩ b) ∪ (a⊥ ∩ b))
Theorem	u1lem9a 759	Lemma used in study of orthoarguesian law.
(a⊥ →1 b)⊥ ≤ a⊥
Theorem	u1lem9b 760	Lemma used in study of orthoarguesian law.
a⊥ ≤ (a →1 b)
Theorem	u1lem9ab 761	Lemma used in study of orthoarguesian law.
(a⊥ →1 b)⊥ ≤ (a →1 b)
Theorem	u1lem11 762	Lemma used in study of orthoarguesian law.
((a⊥ →1 b) →1 b) = (a →1 b)
Theorem	u1lem12 763	Lemma used in study of orthoarguesian law.
((a →1 b) →1 b) = (a⊥ →1 b)
Theorem	u2lem8 764	Lemma for unified implication study.
(a⊥ →2 (a →2 (a⊥ →2 b))) = (a →2 (a⊥ →2 b))
Theorem	u3lem8 765	Lemma for unified implication study.
(a⊥ →3 (a →3 (a⊥ →3 b))) = 1
Theorem	u3lem9 766	Lemma for unified implication study.
(a →3 (a →3 (a⊥ →3 b))) = (a →3 (a⊥ →3 b))
Theorem	u3lem10 767	Lemma for unified implication study.
(a →3 (a⊥ ∩ (a ∪ b))) = a⊥
Theorem	u3lem11 768	Lemma for unified implication study.
(a →3 (b⊥ ∩ (a ∪ b))) = (a →3 b⊥ )
Theorem	u3lem11a 769	Lemma for unified implication study.
(a →3 ((b →3 a) →3 (a →3 b))⊥ ) = (a →3 b⊥ )
Theorem	u3lem12 770	Lemma for unified implication study.
(a →3 (a →3 b⊥ ))⊥ = (a ∩ b)
Theorem	u3lem13a 771	Lemma for unified implication study.
(a →3 (a →3 b⊥ )⊥ ) = (a →1 b)
Theorem	u3lem13b 772	Lemma for unified implication study.
((a →3 b⊥ ) →3 a⊥ ) = (a →1 b)
Theorem	u3lem14a 773	Lemma for unified implication study.
(a →3 ((b →3 a⊥ ) →3 b⊥ )) = (a →3 (b →3 a))
Theorem	u3lem14aa 774	Used to prove →1 "add antecedent" rule in →3 system.
(a →3 (a →3 ((b →3 a⊥ ) →3 b⊥ ))) = 1
Theorem	u3lem14aa2 775	Used to prove →1 "add antecedent" rule in →3 system.
(a →3 (a →3 (b →3 (b →3 a⊥ )⊥ ))) = 1
Theorem	u3lem14mp 776	Used to prove →1 modus ponens rule in →3 system.
((a →3 b⊥ )⊥ →3 (a →3 (a →3 b))) = 1
Theorem	u3lem15 777	Lemma for Kalmbach implication.
((a →3 b) ∩ (a ∪ b)) = ((a⊥ ∪ b) ∩ (a ∪ (a⊥ ∩ b)))
Theorem	u3lemax4 778	Possible axiom for Kalmbach implication system.
((a →3 b) →3 ((a →3 b) →3 ((b →3 a) →3 ((b →3 a) →3 ((c →3 (c →3 a)) →3 (c →3 (c →3 b))))))) = 1
Theorem	u3lemax5 779	Possible axiom for Kalmbach implication system.
((a →3 b) →3 ((a →3 b) →3 ((b →3 a) →3 ((b →3 a) →3 ((b →3 c) →3 ((b →3 c) →3 ((c →3 b) →3 ((c →3 b) →3 (a →3 c))))))))) = 1
Theorem	bi1o1a 780	Equivalence to biconditional.
(a ≡ b) = ((a →1 (a ∩ b)) ∩ ((a ∪ b) →1 a))
Theorem	biao 781	Equivalence to biconditional.
(a ≡ b) = ((a ∩ b) ≡ (a ∪ b))
Theorem	i2i1i1 782	Equivalence to →2 .
(a →2 b) = ((a →1 (a ∪ b)) ∩ ((a ∪ b) →1 b))
Theorem	i1abs 783	An absorption law for →1 .
((a →1 b)⊥ ∪ (a ∩ b)) = a
Theorem	test 784	Part of an attempt to crack a potential Kalmbach axiom.
(((c ∪ (a⊥ ∪ b⊥ )) ∩ (c⊥ ∩ (c ∪ (a ∩ b)))) ∪ ((c⊥ ∩ (a ∩ b)) ∪ (c ∩ (c⊥ ∪ (a ∩ b))))) = ((c ∪ (a ∩ b)) ∩ (c⊥ ∪ (a ∩ b)))
Theorem	test2 785	Part of an attempt to crack a potential Kalmbach axiom.
(a ∪ b) ≤ ((a ≡ b)⊥ ∪ ((c ∪ (a ∩ b)) ∩ (c⊥ ∪ (a ∩ b))))
Theorem	3vth1 786	A 3-variable theorem. Equivalent to OML.
((a →2 b) ∩ (b ∪ c)⊥ ) ≤ (a →2 c)
Theorem	3vth2 787	A 3-variable theorem. Equivalent to OML.
((a →2 b) ∩ (b ∪ c)⊥ ) = ((a →2 c) ∩ (b ∪ c)⊥ )
Theorem	3vth3 788	A 3-variable theorem. Equivalent to OML.
((a →2 c) ∪ ((a →2 b) ∩ (b ∪ c)⊥ )) = (a →2 c)
Theorem	3vth4 789	A 3-variable theorem.
((a →2 b)⊥ →2 (b ∪ c)) = ((a →2 c)⊥ →2 (b ∪ c))
Theorem	3vth5 790	A 3-variable theorem.
((a →2 b)⊥ →2 (b ∪ c)) = (c ∪ ((a →2 b) ∩ (c →2 b)))
Theorem	3vth6 791	A 3-variable theorem.
((a →2 b)⊥ →2 (b ∪ c)) = (((a →2 b) ∩ (c →2 b)) ∪ ((a →2 c) ∩ (b →2 c)))
Theorem	3vth7 792	A 3-variable theorem.
((a →2 b)⊥ →2 (b ∪ c)) = (a →2 (b ∪ c))
Theorem	3vth8 793	A 3-variable theorem.
(a →2 (b ∪ c)) = (((a →2 b) ∩ (c →2 b)) ∪ ((a →2 c) ∩ (b →2 c)))
Theorem	3vth9 794	A 3-variable theorem.
((a ∪ b) →1 (c →2 b)) = ((b ∪ c) →2 (a →2 b))
Theorem	3vcom 795	3-variable commutation theorem
((a →1 c) ∪ (b →1 c)) C ((a⊥ →1 c) ∩ (b⊥ →1 c))
Theorem	3vded11 796	A 3-variable theorem. Experiment with weak deduction theorem.
b ≤ (c →1 (b →1 a))    ⇒   c ≤ (b →1 a)
Theorem	3vded12 797	A 3-variable theorem. Experiment with weak deduction theorem.
(a ∩ (c →1 a)) ≤ (c →1 (b →1 a))    &   c ≤ a    ⇒   c ≤ (b →1 a)
Theorem	3vded13 798	A 3-variable theorem. Experiment with weak deduction theorem.
(b ∩ (c →1 a)) ≤ (c →1 (b →1 a))    &   c ≤ a    ⇒   c ≤ (b →1 a)
Theorem	3vded21 799	A 3-variable theorem. Experiment with weak deduction theorem.
c ≤ ((a →0 b) →0 (c →2 b))    &   c ≤ (a →0 b)    ⇒   c ≤ b
Theorem	3vded22 800	A 3-variable theorem. Experiment with weak deduction theorem.
c ≤ ( C (a, b) ∪ C (c, b))    &   c ≤ a    &   c ≤ (a →0 b)    ⇒   c ≤ b