mmtheorems9 - 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 - 801-900 - Page 9 of 12

Type	Label	Description
Statement
Theorem	i1abs 801	An absorption law for →1 .
((a →1 b)⊥ ∪ (a ∩ b)) = a
Theorem	test 802	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 803	Part of an attempt to crack a potential Kalmbach axiom.
(a ∪ b) ≤ ((a ≡ b)⊥ ∪ ((c ∪ (a ∩ b)) ∩ (c⊥ ∪ (a ∩ b))))
Some 3-variable theorems
Theorem	3vth1 804	A 3-variable theorem. Equivalent to OML.
((a →2 b) ∩ (b ∪ c)⊥ ) ≤ (a →2 c)
Theorem	3vth2 805	A 3-variable theorem. Equivalent to OML.
((a →2 b) ∩ (b ∪ c)⊥ ) = ((a →2 c) ∩ (b ∪ c)⊥ )
Theorem	3vth3 806	A 3-variable theorem. Equivalent to OML.
((a →2 c) ∪ ((a →2 b) ∩ (b ∪ c)⊥ )) = (a →2 c)
Theorem	3vth4 807	A 3-variable theorem.
((a →2 b)⊥ →2 (b ∪ c)) = ((a →2 c)⊥ →2 (b ∪ c))
Theorem	3vth5 808	A 3-variable theorem.
((a →2 b)⊥ →2 (b ∪ c)) = (c ∪ ((a →2 b) ∩ (c →2 b)))
Theorem	3vth6 809	A 3-variable theorem.
((a →2 b)⊥ →2 (b ∪ c)) = (((a →2 b) ∩ (c →2 b)) ∪ ((a →2 c) ∩ (b →2 c)))
Theorem	3vth7 810	A 3-variable theorem.
((a →2 b)⊥ →2 (b ∪ c)) = (a →2 (b ∪ c))
Theorem	3vth8 811	A 3-variable theorem.
(a →2 (b ∪ c)) = (((a →2 b) ∩ (c →2 b)) ∪ ((a →2 c) ∩ (b →2 c)))
Theorem	3vth9 812	A 3-variable theorem.
((a ∪ b) →1 (c →2 b)) = ((b ∪ c) →2 (a →2 b))
Theorem	3vcom 813	3-variable commutation theorem
((a →1 c) ∪ (b →1 c)) C ((a⊥ →1 c) ∩ (b⊥ →1 c))
Theorem	3vded11 814	A 3-variable theorem. Experiment with weak deduction theorem.
b ≤ (c →1 (b →1 a))    ⇒   c ≤ (b →1 a)
Theorem	3vded12 815	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 816	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 817	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 818	A 3-variable theorem. Experiment with weak deduction theorem.
c ≤ ( C (a, b) ∪ C (c, b))    &   c ≤ a    &   c ≤ (a →0 b)    ⇒   c ≤ b
Theorem	3vded3 819	A 3-variable theorem. Experiment with weak deduction theorem.
(c →0 C (a, c)) = 1    &   (c →0 a) = 1    &   (c →0 (a →0 b)) = 1    ⇒   (c →0 b) = 1
Theorem	1oa 820	Orthoarguesian-like law with →1 instead of →0 but true in all OMLs.
((a →2 b) ∩ ((b ∪ c) →1 ((a →2 b) ∩ (a →2 c)))) ≤ (a →2 c)
Theorem	1oai1 821	Orthoarguesian-like OM law.
((a →1 c) ∩ ((a ∩ b)⊥ →1 ((a →1 c) ∩ (b →1 c)))) ≤ (b →1 c)
Theorem	2oai1u 822	Orthoarguesian-like OM law.
((a →1 c) ∩ (((a →1 c) ∩ (b →1 c))⊥ →2 ((a⊥ →1 c) ∩ (b⊥ →1 c)))) ≤ (b →1 c)
Theorem	1oaiii 823	OML analog to orthoarguesian law of Godowski/Greechie, Eq. III with →1 instead of →0 .
((a →2 b) ∩ ((b ∪ c) →1 ((a →2 b) ∩ (a →2 c)))) = ((a →2 c) ∩ ((b ∪ c) →1 ((a →2 b) ∩ (a →2 c))))
Theorem	1oaii 824	OML analog to orthoarguesian law of Godowski/Greechie, Eq. II with →1 instead of →0 .
(b⊥ ∩ ((a →2 b) ∪ ((a →2 c) ∩ ((b ∪ c) →1 ((a →2 b) ∩ (a →2 c)))))) ≤ a⊥
Theorem	2oalem1 825	Lemma for OA-like stuff with →2 instead of →0 .
Theorem	2oath1 826	OA-like theorem with →2 instead of →0 .
((a →2 b) ∩ ((b ∪ c) →2 ((a →2 b) ∩ (a →2 c)))) = ((a →2 b) ∩ (a →2 c))
Theorem	2oath1i1 827	Orthoarguesian-like OM law.
((a →1 c) ∩ ((a ∩ b)⊥ →2 ((a →1 c) ∩ (b →1 c)))) = ((a →1 c) ∩ (b →1 c))
Theorem	1oath1i1u 828	Orthoarguesian-like OM law.
((a →1 c) ∩ (((a →1 c) ∩ (b →1 c))⊥ →1 ((a⊥ →1 c) ∩ (b⊥ →1 c)))) = ((a →1 c) ∩ (b →1 c))
Theorem	oale 829	Relation for studying OA.
((a →2 b) ∩ ((b ∪ c) ∪ ((a →2 b) ∩ (a →2 c)))⊥ ) ≤ (a →2 c)
Theorem	oaeqv 830	Weakened OA implies OA).
((a →2 b) ∩ ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a →2 c)))) ≤ ((b ∪ c) →2 ((a →2 b) ∩ (a →2 c)))    ⇒   ((a →2 b) ∩ ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a →2 c)))) ≤ (a →2 c)
Theorem	3vroa 831	OA-like inference rule (requires OM only).
((a →2 b) ∩ ((b ∪ c) →0 ((a →2 b) ∩ (a →2 c)))) = 1    ⇒   (a →2 c) = 1
Theorem	mlalem 832	Lemma for Mladen's OML.
Theorem	mlaoml 833	Mladen's OML.
((a ≡ b) ∩ (b ≡ c)) ≤ (a ≡ c)
Theorem	eqtr4 834	4-variable transitive law for equivalence.
(((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d)) ≤ (a ≡ d)
Theorem	sac 835	Theorem showing "Sasaki complement" is an operation.
(a →1 c) = (b →1 c)    ⇒   (a⊥ →1 c) = (b⊥ →1 c)
Theorem	sa5 836	Possible axiom for a "Sasaki algebra" for orthoarguesian lattices.
(a →1 c) ≤ (b →1 c)    ⇒   (b⊥ →1 c) ≤ ((a⊥ →1 c) ∪ c)
Theorem	salem1 837	Lemma for attempt at Sasaki algebra.
Theorem	sadm3 838	Weak DeMorgan's law for attempt at Sasaki algebra.
(((a⊥ →1 c) ∩ (b⊥ →1 c)) →1 c) ≤ ((a →1 c) ∪ (b →1 c))
Theorem	bi3 839	Chained biconditional.
((a ≡ b) ∩ (b ≡ c)) = (((a ∩ b) ∩ c) ∪ ((a⊥ ∩ b⊥ ) ∩ c⊥ ))
Theorem	bi4 840	Chained biconditional.
(((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d)) = ((((a ∩ b) ∩ c) ∩ d) ∪ (((a⊥ ∩ b⊥ ) ∩ c⊥ ) ∩ d⊥ ))
Theorem	imp3 841	Implicational product with 3 variables. Theorem 3.20 of "Equations, states, and lattices..." paper.
((a →2 b) ∩ (b →1 c)) = ((a⊥ ∩ b⊥ ) ∪ (b ∩ c))
Theorem	orbi 842	Disjunction of biconditionals.
((a ≡ c) ∪ (b ≡ c)) = (((a →2 c) ∪ (b →2 c)) ∩ ((c →1 a) ∪ (c →1 b)))
Theorem	orbile 843	Disjunction of biconditionals.
((a ≡ c) ∪ (b ≡ c)) ≤ (((a ∩ b) →2 c) ∩ (c →1 (a ∪ b)))
Theorem	mlaconj4 844	For 4GO proof of Mladen's conjecture, that it follows from Eq. (3.30) in OA-GO paper.
((d ≡ e) ∩ ((e⊥ ∩ c⊥ ) ∪ (d ∩ c))) ≤ (d ≡ c)    &   d = (a ∪ b)    &   e = (a ∩ b)    ⇒   ((a ≡ b) ∩ ((a ≡ c) ∪ (b ≡ c))) ≤ (a ≡ c)
Theorem	mlaconj 845	For 5GO proof of Mladen's conjecture.
((a ≡ b) ∩ ((a ≡ c) ∪ (b ≡ c))) ≤ ((((a →1 (a ∩ b)) ∩ ((a ∩ b) →1 ((a ∩ b) ∪ c))) ∩ ((((a ∩ b) ∪ c) →1 c) ∩ (c →1 (a ∪ b)))) ∩ ((a ∪ b) →1 a))
Theorem	mlaconj2 846	For 5GO proof of Mladen's conjecture. Hypothesis is 5GO law consequence.
((((a →1 (a ∩ b)) ∩ ((a ∩ b) →1 ((a ∩ b) ∪ c))) ∩ ((((a ∩ b) ∪ c) →1 c) ∩ (c →1 (a ∪ b)))) ∩ ((a ∪ b) →1 a)) ≤ (a ≡ c)    ⇒   ((a ≡ b) ∩ ((a ≡ c) ∪ (b ≡ c))) ≤ (a ≡ c)
Theorem	i1orni1 847	Complemented antecedent lemma.
((a →1 b) ∪ (a⊥ →1 b)) = 1
Theorem	negantlem1 848	Lemma for negated antecedent identity.
Theorem	negantlem2 849	Lemma for negated antecedent identity.
Theorem	negantlem3 850	Lemma for negated antecedent identity.
Theorem	negantlem4 851	Lemma for negated antecedent identity.
Theorem	negant 852	Negated antecedent identity.
(a →1 c) = (b →1 c)    ⇒   (a⊥ →1 c) = (b⊥ →1 c)
Theorem	negantlem5 853	Negated antecedent identity.
(a →1 c) = (b →1 c)    ⇒   (a⊥ ∩ c⊥ ) = (b⊥ ∩ c⊥ )
Theorem	negantlem6 854	Negated antecedent identity.
(a →1 c) = (b →1 c)    ⇒   (a ∩ c⊥ ) = (b ∩ c⊥ )
Theorem	negantlem7 855	Negated antecedent identity.
(a →1 c) = (b →1 c)    ⇒   (a ∪ c) = (b ∪ c)
Theorem	negantlem8 856	Negated antecedent identity.
(a →1 c) = (b →1 c)    ⇒   (a⊥ ∪ c) = (b⊥ ∪ c)
Theorem	negant0 857	Negated antecedent identity.
(a →1 c) = (b →1 c)    ⇒   (a⊥ →0 c) = (b⊥ →0 c)
Theorem	negant2 858	Negated antecedent identity.
(a →1 c) = (b →1 c)    ⇒   (a⊥ →2 c) = (b⊥ →2 c)
Theorem	negantlem9 859	Negated antecedent identity.
(a →1 c) = (b →1 c)    ⇒   (a →3 c) ≤ (b →3 c)
Theorem	negant3 860	Negated antecedent identity.
(a →1 c) = (b →1 c)    ⇒   (a⊥ →3 c) = (b⊥ →3 c)
Theorem	negantlem10 861	Lemma for negated antecedent identity.
Theorem	negant4 862	Negated antecedent identity.
(a →1 c) = (b →1 c)    ⇒   (a⊥ →4 c) = (b⊥ →4 c)
Theorem	negant5 863	Negated antecedent identity.
(a →1 c) = (b →1 c)    ⇒   (a⊥ →5 c) = (b⊥ →5 c)
Theorem	neg3antlem1 864	Lemma for negated antecedent identity.
Theorem	neg3antlem2 865	Lemma for negated antecedent identity.
Theorem	neg3ant1 866	Lemma for negated antecedent identity.
Theorem	elimconslem 867	Lemma for consequent elimination law.
Theorem	elimcons 868	Consequent elimination law.
(a →1 c) = (b →1 c)    &   (a ∩ c) ≤ (b ∪ c⊥ )    ⇒   a ≤ b
Theorem	elimcons2 869	Consequent elimination law.
(a →1 c) = (b →1 c)    &   (a ∩ (c ∩ (b →1 c))) ≤ (b ∪ (c⊥ ∪ (a →1 c)⊥ ))    ⇒   a ≤ b
Theorem	comanblem1 870	Lemma for biconditional commutation law.
Theorem	comanblem2 871	Lemma for biconditional commutation law.
Theorem	comanb 872	Biconditional commutation law.
(a ∩ b) C ((a ≡ c) ∩ (b ≡ c))
Theorem	comanbn 873	Biconditional commutation law.
(a⊥ ∩ b⊥ ) C ((a ≡ c) ∩ (b ≡ c))
Theorem	mhlemlem1 874	Lemma for Lemma 7.1 of Kalmbach, p. 91.
Theorem	mhlemlem2 875	Lemma for Lemma 7.1 of Kalmbach, p. 91.
Theorem	mhlem 876	Lemma 7.1 of Kalmbach, p. 91.
(a ∪ b) ≤ (c ∪ d)⊥    ⇒   ((a ∪ c) ∩ (b ∪ d)) = ((a ∩ b) ∪ (c ∩ d))
Theorem	mhlem1 877	Lemma for Marsden-Herman distributive law.
Theorem	mhlem2 878	Lemma for Marsden-Herman distributive law.
Theorem	mh 879	Marsden-Herman distributive law. Lemma 7.2 of Kalmbach, p. 91.
a C c    &   a C d    &   b C c    &   b C d    ⇒   ((a ∪ c) ∩ (b ∪ d)) = (((a ∩ b) ∪ (a ∩ d)) ∪ ((c ∩ b) ∪ (c ∩ d)))
Theorem	marsdenlem1 880	Lemma for Marsden-Herman distributive law.
Theorem	marsdenlem2 881	Lemma for Marsden-Herman distributive law.
Theorem	marsdenlem3 882	Lemma for Marsden-Herman distributive law.
Theorem	marsdenlem4 883	Lemma for Marsden-Herman distributive law.
Theorem	mh2 884	Marsden-Herman distributive law. Corollary 3.3 of Beran, p. 259.
a C b    &   b C c    &   c C d    &   d C a    ⇒   ((a ∪ b) ∩ (c ∪ d)) = (((a ∩ c) ∪ (a ∩ d)) ∪ ((b ∩ c) ∪ (b ∩ d)))
Theorem	mlaconjolem 885	Lemma for OML proof of Mladen's conjecture,
Theorem	mlaconjo 886	OML proof of Mladen's conjecture.
((a ≡ b) ∩ ((a ≡ c) ∪ (b ≡ c))) ≤ (a ≡ c)
Theorem	distid 887	Distributive law for identity.
((a ≡ b) ∩ ((a ≡ c) ∪ (b ≡ c))) = (((a ≡ b) ∩ (a ≡ c)) ∪ ((a ≡ b) ∩ (b ≡ c)))
Theorem	mhcor1 888	Corollary of Marsden-Herman Lemma.
((((a →1 b) ∩ (b →2 c)) ∩ (c →1 d)) ∩ (d →2 a)) = (((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d))
Theorem	oago3.29 889	Equation (3.29) of "Equations, states, and lattices..." paper. This shows that it holds in all OMLs, not just 4GO.
((a →1 b) ∩ ((b →2 c) ∩ (c →1 a))) ≤ (a ≡ c)
Theorem	oago3.21x 890	4-variable extension of Equation (3.21) of "Equations, states, and lattices..." paper. This shows that it holds in all OMLs, not just 4GO.
((((a →5 b) ∩ (b →5 c)) ∩ (c →5 d)) ∩ (d →5 a)) = (((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d))
Theorem	cancellem 891	Lemma for cancellation law eliminating →1 consequent.
Theorem	cancel 892	Cancellation law eliminating →1 consequent.
((d ∪ (a →1 c)) →1 c) = ((d ∪ (b →1 c)) →1 c)    ⇒   (d ∪ (a →1 c)) = (d ∪ (b →1 c))
Theorem	kb10iii 893	Exercise 10(iii) of Kalmbach p. 30 (in a rewritten form).
b⊥ ≤ (a →1 c)    ⇒   c⊥ ≤ (a →1 b)
Theorem	e2ast2 894	Show that the E*2 derivative on p. 23 of Mayet, "Equations holding in Hilbert lattices" IJTP 2006, holds in all OMLs.
a ≤ b⊥    &   c ≤ d⊥    &   a ≤ c⊥    ⇒   ((a ∪ b) ∩ (c ∪ d)) ≤ ((b ∪ d) ∪ (a ∪ c)⊥ )
Theorem	e2astlem1 895	Lemma towards a possible proof that E*2 on p. 23 of Mayet, "Equations holding in Hilbert lattices" IJTP 2006, holds in all OMLs.
a ≤ b⊥    &   c ≤ d⊥    &   r ≤ a⊥    &   a ≤ c⊥    &   c ≤ r⊥    ⇒   (((a ∪ b) ∩ (c ∪ d)) ∩ ((a ∪ c) ∪ r)) = ((a ∪ (b ∩ (c ∪ r))) ∩ (c ∪ (d ∩ (a ∪ r))))
OML Lemmas for studying Godowski equations.
Theorem	govar 896	Lemma for converting n-variable Godowski equations to 2n-variable equations
Theorem	govar2 897	Lemma for converting n-variable to 2n-variable Godowski equations.
Theorem	gon2n 898	Lemma for converting n-variable to 2n-variable Godowski equations.
Theorem	go2n4 899	8-variable Godowski equation derived from 4-variable one. The last hypothesis is the 4-variable Godowski equation.
a ≤ b⊥    &   b ≤ c⊥    &   c ≤ d⊥    &   d ≤ e⊥    &   e ≤ f⊥    &   f ≤ g⊥    &   g ≤ h⊥    &   h ≤ a⊥    &   (((c →2 a) ∩ (a →2 g)) ∩ ((g →2 e) ∩ (e →2 c))) ≤ (a →2 c)    ⇒   (((a ∪ b) ∩ (c ∪ d)) ∩ ((e ∪ f) ∩ (g ∪ h))) ≤ (b ∪ c)
Theorem	gomaex4 900	Proof of Mayet Example 4 from 4-variable Godowski equation. R. Mayet, "Equational bases for some varieties of orthomodular lattices related to states," Algebra Universalis 23 (1986), 167-195.
a ≤ b⊥    &   b ≤ c⊥    &   c ≤ d⊥    &   d ≤ e⊥    &   e ≤ f⊥    &   f ≤ g⊥    &   g ≤ h⊥    &   h ≤ a⊥    &   (((a →2 g) ∩ (g →2 e)) ∩ ((e →2 c) ∩ (c →2 a))) ≤ (g →2 a)    &   (((e →2 c) ∩ (c →2 a)) ∩ ((a →2 g) ∩ (g →2 e))) ≤ (c →2 e)    ⇒   ((((a ∪ b) ∩ (c ∪ d)) ∩ ((e ∪ f) ∩ (g ∪ h))) ∩ ((a ∪ h) →1 (d ∪ e)⊥ )) = 0