mmtheorems8 - Quantum Logic Explorer

Jump to page: Contents + 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-1100 12 1101-1118

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

Type	Label	Description
Statement
Theorem	u1lemc4 701	Lemma for Sasaki implication study.
Theorem	u2lemc4 702	Lemma for Dishkant implication study.
Theorem	u3lemc4 703	Lemma for Kalmbach implication study.
Theorem	u4lemc4 704	Lemma for non-tollens implication study.
Theorem	u5lemc4 705	Lemma for relevance implication study.
Theorem	u1lemc6 706	Commutation theorem for Sasaki implication.
(a ->1 b) C (a' ->1 b)
Theorem	comi12 707	Commutation theorem for ->1 and ->2.
(a ->1 b) C (c ->2 a)
Theorem	i1com 708	Commutation expressed with ->1.
b =< (a ->1 b)   =>   a C b
Theorem	comi1 709	Commutation expressed with ->1.
a C b   =>   b =< (a ->1 b)
Theorem	u1lemle1 710	L.e. to Sasaki implication.
a =< b   =>   (a ->1 b) = 1
Theorem	u2lemle1 711	L.e. to Dishkant implication.
a =< b   =>   (a ->2 b) = 1
Theorem	u3lemle1 712	L.e. to Kalmbach implication.
a =< b   =>   (a ->3 b) = 1
Theorem	u4lemle1 713	L.e. to non-tollens implication.
a =< b   =>   (a ->4 b) = 1
Theorem	u5lemle1 714	L.e. to relevance implication.
a =< b   =>   (a ->5 b) = 1
Theorem	u1lemle2 715	Sasaki implication to l.e.
(a ->1 b) = 1   =>   a =< b
Theorem	u2lemle2 716	Dishkant implication to l.e.
(a ->2 b) = 1   =>   a =< b
Theorem	u3lemle2 717	Kalmbach implication to l.e.
(a ->3 b) = 1   =>   a =< b
Theorem	u4lemle2 718	Non-tollens implication to l.e.
(a ->4 b) = 1   =>   a =< b
Theorem	u5lemle2 719	Relevance implication to l.e.
(a ->5 b) = 1   =>   a =< b
Theorem	u1lembi 720	Sasaki implication and biconditional.
((a ->1 b) ^ (b ->1 a)) = (a == b)
Theorem	u2lembi 721	Dishkant implication and biconditional.
((a ->2 b) ^ (b ->2 a)) = (a == b)
Theorem	i2bi 722	Dishkant implication expressed with biconditional.
(a ->2 b) = (b v (a == b))
Theorem	u3lembi 723	Kalmbach implication and biconditional.
((a ->3 b) ^ (b ->3 a)) = (a == b)
Theorem	u4lembi 724	Non-tollens implication and biconditional.
((a ->4 b) ^ (b ->4 a)) = (a == b)
Theorem	u5lembi 725	Relevance implication and biconditional.
((a ->5 b) ^ (b ->5 a)) = (a == b)
Theorem	u12lembi 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.
((a ->1 b) ^ (b ->2 a)) = (a == b)
Theorem	u21lembi 727	Dishkant/Sasaki implication and biconditional.
((a ->2 b) ^ (b ->1 a)) = (a == b)
Theorem	ublemc1 728	Commutation theorem for biimplication.
a C (a == b)
Theorem	ublemc2 729	Commutation theorem for biimplication.
b C (a == b)
Some proofs contributed by Josiah Burroughs
Theorem	u1lemn1b 730	This theorem continues the line of proofs such as u1lemnaa 640, ud1lem0b 256, u1lemnanb 655, etc. (Contributed by Josiah Burroughs 26-May-04.)
(a ->1 b) = ((a ->1 b)' ->1 b)
Theorem	u1lem3var1 731	A 3-variable formula. (Contributed by Josiah Burroughs 26-May-04.)
(((a ->1 c) ^ (b ->1 c))' v (((a ->1 c)' ->1 c) ^ ((b ->1 c)' ->1 c))) = 1
Theorem	oi3oa3lem1 732	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)) v (a ^ b)) = 1
Theorem	oi3oa3 733	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)) v ((((a ->1 c) ^ (((a ->1 c) ^ (b ->1 c)) v (a ^ b))) ->1 c) ^ (((b ->1 c) ^ (((a ->1 c) ^ (b ->1 c)) v (a ^ b))) ->1 c))) = 1
More lemmas for unified implication
Theorem	u1lem1 734	Lemma for unified implication study.
Theorem	u2lem1 735	Lemma for unified implication study.
Theorem	u3lem1 736	Lemma for unified implication study.
Theorem	u4lem1 737	Lemma for unified implication study.
Theorem	u5lem1 738	Lemma for unified implication study.
Theorem	u1lem1n 739	Lemma for unified implication study.
Theorem	u2lem1n 740	Lemma for unified implication study.
Theorem	u3lem1n 741	Lemma for unified implication study.
Theorem	u4lem1n 742	Lemma for unified implication study.
Theorem	u5lem1n 743	Lemma for unified implication study.
Theorem	u1lem2 744	Lemma for unified implication study.
Theorem	u2lem2 745	Lemma for unified implication study.
Theorem	u3lem2 746	Lemma for unified implication study.
Theorem	u4lem2 747	Lemma for unified implication study.
Theorem	u5lem2 748	Lemma for unified implication study.
Theorem	u1lem3 749	Lemma for unified implication study.
Theorem	u2lem3 750	Lemma for unified implication study.
Theorem	u3lem3 751	Lemma for unified implication study.
Theorem	u4lem3 752	Lemma for unified implication study.
Theorem	u5lem3 753	Lemma for unified implication study.
Theorem	u3lem3n 754	Lemma for unified implication study.
Theorem	u4lem3n 755	Lemma for unified implication study.
Theorem	u5lem3n 756	Lemma for unified implication study.
Theorem	u1lem4 757	Lemma for unified implication study.
Theorem	u3lem4 758	Lemma for unified implication study.
Theorem	u4lem4 759	Lemma for unified implication study.
Theorem	u5lem4 760	Lemma for unified implication study.
Theorem	u1lem5 761	Lemma for unified implication study.
Theorem	u2lem5 762	Lemma for unified implication study.
Theorem	u3lem5 763	Lemma for unified implication study.
Theorem	u4lem5 764	Lemma for unified implication study.
Theorem	u5lem5 765	Lemma for unified implication study.
Theorem	u4lem5n 766	Lemma for unified implication study.
Theorem	u3lem6 767	Lemma for unified implication study.
Theorem	u4lem6 768	Lemma for unified implication study.
Theorem	u5lem6 769	Lemma for unified implication study.
Theorem	u24lem 770	Lemma for unified implication study.
Theorem	u12lem 771	Implication lemma.
((a ->1 b) v (a ->2 b)) = (a ->0 b)
Theorem	u1lem7 772	Lemma for unified implication study.
Theorem	u2lem7 773	Lemma for unified implication study.
Theorem	u3lem7 774	Lemma for unified implication study.
Theorem	u2lem7n 775	Lemma for unified implication study.
Theorem	u1lem8 776	Lemma used in study of orthoarguesian law.
((a ->1 b) ^ (a' ->1 b)) = ((a ^ b) v (a' ^ b))
Theorem	u1lem9a 777	Lemma used in study of orthoarguesian law. Equation 4.11 of [MegPav2000] p. 23. This is the first part of the inequality.
(a' ->1 b)' =< a'
Theorem	u1lem9b 778	Lemma used in study of orthoarguesian law. Equation 4.11 of [MegPav2000] p. 23. This is the second part of the inequality.
a' =< (a ->1 b)
Theorem	u1lem9ab 779	Lemma used in study of orthoarguesian law.
(a' ->1 b)' =< (a ->1 b)
Theorem	u1lem11 780	Lemma used in study of orthoarguesian law.
((a' ->1 b) ->1 b) = (a ->1 b)
Theorem	u1lem12 781	Lemma used in study of orthoarguesian law. Equation 4.12 of [MegPav2000] p. 23.
((a ->1 b) ->1 b) = (a' ->1 b)
Theorem	u2lem8 782	Lemma for unified implication study.
Theorem	u3lem8 783	Lemma for unified implication study.
Theorem	u3lem9 784	Lemma for unified implication study.
Theorem	u3lem10 785	Lemma for unified implication study.
Theorem	u3lem11 786	Lemma for unified implication study.
Theorem	u3lem11a 787	Lemma for unified implication study.
Theorem	u3lem12 788	Lemma for unified implication study.
Theorem	u3lem13a 789	Lemma for unified implication study.
Theorem	u3lem13b 790	Lemma for unified implication study.
Theorem	u3lem14a 791	Lemma for unified implication study.
Theorem	u3lem14aa 792	Used to prove ->1 "add antecedent" rule in ->3 system.
(a ->3 (a ->3 ((b ->3 a') ->3 b'))) = 1
Theorem	u3lem14aa2 793	Used to prove ->1 "add antecedent" rule in ->3 system.
(a ->3 (a ->3 (b ->3 (b ->3 a')'))) = 1
Theorem	u3lem14mp 794	Used to prove ->1 modus ponens rule in ->3 system.
((a ->3 b')' ->3 (a ->3 (a ->3 b))) = 1
Theorem	u3lem15 795	Lemma for Kalmbach implication.
Theorem	u3lemax4 796	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 797	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 798	Equivalence to biconditional.
(a == b) = ((a ->1 (a ^ b)) ^ ((a v b) ->1 a))
Theorem	biao 799	Equivalence to biconditional.
(a == b) = ((a ^ b) == (a v b))
Theorem	i2i1i1 800	Equivalence to ->2.
(a ->2 b) = ((a ->1 (a v b)) ^ ((a v b) ->1 b))