Quantum Logic Explorer - mmtheorems6

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 - 501-600 - Page 6 of 11

Type	Label	Description
Statement
Theorem	binr3 501	Pavicic binary logic axr3 analog.
(a →3 c) = 1    &   (b →3 c) = 1    ⇒   ((a ∪ b) →3 c) = 1
Theorem	i31 502	Theorem for Kalmbach implication.
(a →3 1) = 1
Theorem	i3aa 503	Add antecedent.
a = 1    ⇒   (b →3 a) = 1
Theorem	i3abs1 504	Antecedent absorption.
(a →3 (a →3 (a →3 b))) = (a →3 (a →3 b))
Theorem	i3abs2 505	Antecedent absorption.
(a →3 (a →3 (a →3 b))) = 1    ⇒   (a →3 (a →3 b)) = 1
Theorem	i3abs3 506	Antecedent absorption.
((a →3 b) →3 ((a →3 b) →3 a)) = ((a →3 b) →3 a)
Theorem	i3orcom 507	Commutative law for conjunction with Kalmbach implication.
((a ∪ b) →3 (b ∪ a)) = 1
Theorem	i3ancom 508	Commutative law for disjunction with Kalmbach implication.
((a ∩ b) →3 (b ∩ a)) = 1
Theorem	bi3tr 509	Transitive inference.
a = b    &   (b →3 c) = 1    ⇒   (a →3 c) = 1
Theorem	i3btr 510	Transitive inference.
(a →3 b) = 1    &   b = c    ⇒   (a →3 c) = 1
Theorem	i33tr1 511	Transitive inference useful for introducing definitions.
(a →3 b) = 1    &   c = a    &   d = b    ⇒   (c →3 d) = 1
Theorem	i33tr2 512	Transitive inference useful for eliminating definitions.
(a →3 b) = 1    &   a = c    &   b = d    ⇒   (c →3 d) = 1
Theorem	i3con1 513	Contrapositive.
(a⊥ →3 b⊥ ) = 1    ⇒   (b →3 a) = 1
Theorem	i3ror 514	WQL (Weak Quantum Logic) rule.
(a →3 b) = 1    ⇒   ((a ∪ c) →3 (b ∪ c)) = 1
Theorem	i3lor 515	WQL (Weak Quantum Logic) rule.
(a →3 b) = 1    ⇒   ((c ∪ a) →3 (c ∪ b)) = 1
Theorem	i32or 516	WQL (Weak Quantum Logic) rule.
(a →3 b) = 1    &   (c →3 d) = 1    ⇒   ((a ∪ c) →3 (b ∪ d)) = 1
Theorem	i3ran 517	WQL (Weak Quantum Logic) rule.
(a →3 b) = 1    ⇒   ((a ∩ c) →3 (b ∩ c)) = 1
Theorem	i3lan 518	WQL (Weak Quantum Logic) rule.
(a →3 b) = 1    ⇒   ((c ∩ a) →3 (c ∩ b)) = 1
Theorem	i32an 519	WQL (Weak Quantum Logic) rule.
(a →3 b) = 1    &   (c →3 d) = 1    ⇒   ((a ∩ c) →3 (b ∩ d)) = 1
Theorem	i3ri3 520	WQL (Weak Quantum Logic) rule.
(a →3 b) = 1    &   (b →3 a) = 1    ⇒   ((a →3 c) →3 (b →3 c)) = 1
Theorem	i3li3 521	WQL (Weak Quantum Logic) rule.
(a →3 b) = 1    &   (b →3 a) = 1    ⇒   ((c →3 a) →3 (c →3 b)) = 1
Theorem	i32i3 522	WQL (Weak Quantum Logic) rule.
(a →3 b) = 1    &   (b →3 a) = 1    &   (c →3 d) = 1    &   (d →3 c) = 1    ⇒   ((a →3 c) →3 (b →3 d)) = 1
Theorem	i0i3tr 523	Transitive inference.
(a →3 (a →3 b)) = 1    &   (b →3 c) = 1    ⇒   (a →3 (a →3 c)) = 1
Theorem	i3i0tr 524	Transitive inference.
(a →3 b) = 1    &   (b →3 (b →3 c)) = 1    ⇒   (a →3 (a →3 c)) = 1
Theorem	i3th1 525	Theorem for Kalmbach implication.
(a →3 (a →3 (b →3 a))) = 1
Theorem	i3th2 526	Theorem for Kalmbach implication.
(a →3 (b →3 (b →3 a))) = 1
Theorem	i3th3 527	Theorem for Kalmbach implication.
(a⊥ →3 (a →3 (a →3 b))) = 1
Theorem	i3th4 528	Theorem for Kalmbach implication.
(a →3 (b →3 b)) = 1
Theorem	i3th5 529	Theorem for Kalmbach implication.
((a →3 b) →3 (a →3 (a →3 b))) = 1
Theorem	i3th6 530	Theorem for Kalmbach implication.
((a →3 (a →3 (a →3 b))) →3 (a →3 (a →3 b))) = 1
Theorem	i3th7 531	Theorem for Kalmbach implication.
(a →3 ((a →3 b) →3 a)) = 1
Theorem	i3th8 532	Theorem for Kalmbach implication.
((a →3 b)⊥ →3 ((a →3 b) →3 a)) = 1
Theorem	i3con 533	Theorem for Kalmbach implication.
((a →3 b) →3 ((a →3 b) →3 (b⊥ →3 a⊥ ))) = 1
Theorem	i3orlem1 534	Lemma for Kalmbach implication OR builder.
((a ∪ c) ∩ ((a ∪ c)⊥ ∪ (b ∪ c))) ≤ ((a ∪ c) →3 (b ∪ c))
Theorem	i3orlem2 535	Lemma for Kalmbach implication OR builder.
(a ∩ b) ≤ ((a ∪ c) →3 (b ∪ c))
Theorem	i3orlem3 536	Lemma for Kalmbach implication OR builder.
c ≤ ((a ∪ c) →3 (b ∪ c))
Theorem	i3orlem4 537	Lemma for Kalmbach implication OR builder.
((a ∪ c)⊥ ∩ (b ∪ c)) ≤ ((a ∪ c) →3 (b ∪ c))
Theorem	i3orlem5 538	Lemma for Kalmbach implication OR builder.
((a⊥ ∩ b⊥ ) ∩ c⊥ ) ≤ ((a ∪ c) →3 (b ∪ c))
Theorem	i3orlem6 539	Lemma for Kalmbach implication OR builder.
((a →3 b)⊥ ∪ ((a ∪ c) →3 (b ∪ c))) = (((a ∪ b) ∩ (a⊥ →3 b⊥ )) ∪ ((a ∪ c) →3 (b ∪ c)))
Theorem	i3orlem7 540	Lemma for Kalmbach implication OR builder.
(a ∩ b⊥ ) ≤ ((a →3 b)⊥ ∪ ((a ∪ c) →3 (b ∪ c)))
Theorem	i3orlem8 541	Lemma for Kalmbach implication OR builder.
(((a ∪ b) ∩ (a ∪ b⊥ )) ∩ a⊥ ) ≤ ((a →3 b)⊥ ∪ ((a ∪ c) →3 (b ∪ c)))
Theorem	ud1lem1 542	Lemma for unified disjunction.
((a →1 b) →1 (b →1 a)) = (a ∪ (a⊥ ∩ b⊥ ))
Theorem	ud1lem2 543	Lemma for unified disjunction.
((a ∪ (a⊥ ∩ b⊥ )) →1 a) = (a ∪ b)
Theorem	ud1lem3 544	Lemma for unified disjunction.
((a →1 b) →1 (a ∪ b)) = (a ∪ b)
Theorem	ud2lem1 545	Lemma for unified disjunction.
((a →2 b) →2 (b →2 a)) = (a ∪ (a⊥ ∩ b⊥ ))
Theorem	ud2lem2 546	Lemma for unified disjunction.
((a ∪ (a⊥ ∩ b⊥ )) →2 a) = (a ∪ b)
Theorem	ud2lem3 547	Lemma for unified disjunction.
((a →2 b) →2 (a ∪ b)) = (a ∪ b)
Theorem	ud3lem1a 548	Lemma for unified disjunction.
((a →3 b)⊥ ∩ (b →3 a)) = (a ∩ b⊥ )
Theorem	ud3lem1b 549	Lemma for unified disjunction.
((a →3 b)⊥ ∩ (b →3 a)⊥ ) = 0
Theorem	ud3lem1c 550	Lemma for unified disjunction.
((a →3 b)⊥ ∪ (b →3 a)) = (a ∪ b⊥ )
Theorem	ud3lem1d 551	Lemma for unified disjunction.
((a →3 b) ∩ ((a →3 b)⊥ ∪ (b →3 a))) = ((a⊥ ∩ b⊥ ) ∪ (a ∩ (a⊥ ∪ b)))
Theorem	ud3lem1 552	Lemma for unified disjunction.
((a →3 b) →3 (b →3 a)) = (a ∪ (a⊥ ∩ b⊥ ))
Theorem	ud3lem2 553	Lemma for unified disjunction.
((a ∪ (a⊥ ∩ b⊥ )) →3 a) = (a ∪ b)
Theorem	ud3lem3a 554	Lemma for unified disjunction.
((a →3 b)⊥ ∩ (a ∪ b)) = (a →3 b)⊥
Theorem	ud3lem3b 555	Lemma for unified disjunction.
((a →3 b)⊥ ∩ (a ∪ b)⊥ ) = 0
Theorem	ud3lem3c 556	Lemma for unified disjunction.
((a →3 b)⊥ ∪ (a ∪ b)) = (a ∪ b)
Theorem	ud3lem3d 557	Lemma for unified disjunction.
((a →3 b) ∩ ((a →3 b)⊥ ∪ (a ∪ b))) = ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b)))
Theorem	ud3lem3 558	Lemma for unified disjunction.
((a →3 b) →3 (a ∪ b)) = (a ∪ b)
Theorem	ud4lem1a 559	Lemma for unified disjunction.
((a →4 b) ∩ (b →4 a)) = ((a ∩ b) ∪ (a⊥ ∩ b⊥ ))
Theorem	ud4lem1b 560	Lemma for unified disjunction.
((a →4 b)⊥ ∩ (b →4 a)) = (a ∩ b⊥ )
Theorem	ud4lem1c 561	Lemma for unified disjunction.
((a →4 b)⊥ ∪ (b →4 a)) = (a ∪ b⊥ )
Theorem	ud4lem1d 562	Lemma for unified disjunction.
(((a →4 b)⊥ ∪ (b →4 a)) ∩ (b →4 a)⊥ ) = (((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ b)) ∩ a)
Theorem	ud4lem1 563	Lemma for unified disjunction.
((a →4 b) →4 (b →4 a)) = (a ∪ (a⊥ ∩ b⊥ ))
Theorem	ud4lem2 564	Lemma for unified disjunction.
((a ∪ (a⊥ ∩ b⊥ )) →4 a) = (a ∪ b)
Theorem	ud4lem3a 565	Lemma for unified disjunction.
((a →4 b)⊥ ∩ (a ∪ b)) = (a →4 b)⊥
Theorem	ud4lem3b 566	Lemma for unified disjunction.
((a →4 b)⊥ ∪ (a ∪ b)) = (a ∪ b)
Theorem	ud4lem3 567	Lemma for unified disjunction.
((a →4 b) →4 (a ∪ b)) = (a ∪ b)
Theorem	ud5lem1a 568	Lemma for unified disjunction.
((a →5 b) ∩ (b →5 a)) = ((a ∩ b) ∪ (a⊥ ∩ b⊥ ))
Theorem	ud5lem1b 569	Lemma for unified disjunction.
((a →5 b)⊥ ∩ (b →5 a)) = (a ∩ b⊥ )
Theorem	ud5lem1c 570	Lemma for unified disjunction.
((a →5 b)⊥ ∩ (b →5 a)⊥ ) = (((a ∪ b) ∩ (a ∪ b⊥ )) ∩ ((a⊥ ∪ b) ∩ (a⊥ ∪ b⊥ )))
Theorem	ud5lem1 571	Lemma for unified disjunction.
((a →5 b) →5 (b →5 a)) = (a ∪ b⊥ )
Theorem	ud5lem2 572	Lemma for unified disjunction.
((a ∪ b⊥ ) →5 a) = (a ∪ (a⊥ ∩ b))
Theorem	ud5lem3a 573	Lemma for unified disjunction.
((a →5 b) ∩ (a ∪ (a⊥ ∩ b))) = ((a ∩ b) ∪ (a⊥ ∩ b))
Theorem	ud5lem3b 574	Lemma for unified disjunction.
((a →5 b)⊥ ∩ (a ∪ (a⊥ ∩ b))) = (a ∩ (a⊥ ∪ b⊥ ))
Theorem	ud5lem3c 575	Lemma for unified disjunction.
((a →5 b)⊥ ∩ (a ∪ (a⊥ ∩ b))⊥ ) = (((a ∪ b) ∩ (a ∪ b⊥ )) ∩ a⊥ )
Theorem	ud5lem3 576	Lemma for unified disjunction.
((a →5 b) →5 (a ∪ (a⊥ ∩ b))) = (a ∪ b)
Theorem	ud1 577	Unified disjunction for Sasaki implication.
(a ∪ b) = ((a →1 b) →1 (((a →1 b) →1 (b →1 a)) →1 a))
Theorem	ud2 578	Unified disjunction for Dishkant implication.
(a ∪ b) = ((a →2 b) →2 (((a →2 b) →2 (b →2 a)) →2 a))
Theorem	ud3 579	Unified disjunction for Kalmbach implication.
(a ∪ b) = ((a →3 b) →3 (((a →3 b) →3 (b →3 a)) →3 a))
Theorem	ud4 580	Unified disjunction for non-tollens implication.
(a ∪ b) = ((a →4 b) →4 (((a →4 b) →4 (b →4 a)) →4 a))
Theorem	ud5 581	Unified disjunction for relevance implication.
(a ∪ b) = ((a →5 b) →5 (((a →5 b) →5 (b →5 a)) →5 a))
Theorem	u1lemaa 582	Lemma for Sasaki implication study.
((a →1 b) ∩ a) = (a ∩ b)
Theorem	u2lemaa 583	Lemma for Dishkant implication study.
((a →2 b) ∩ a) = (a ∩ b)
Theorem	u3lemaa 584	Lemma for Kalmbach implication study.
((a →3 b) ∩ a) = (a ∩ (a⊥ ∪ b))
Theorem	u4lemaa 585	Lemma for non-tollens implication study.
((a →4 b) ∩ a) = (a ∩ b)
Theorem	u5lemaa 586	Lemma for relevance implication study.
((a →5 b) ∩ a) = (a ∩ b)
Theorem	u1lemana 587	Lemma for Sasaki implication study.
((a →1 b) ∩ a⊥ ) = a⊥
Theorem	u2lemana 588	Lemma for Dishkant implication study.
((a →2 b) ∩ a⊥ ) = ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))
Theorem	u3lemana 589	Lemma for Kalmbach implication study.
((a →3 b) ∩ a⊥ ) = ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))
Theorem	u4lemana 590	Lemma for non-tollens implication study.
((a →4 b) ∩ a⊥ ) = ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))
Theorem	u5lemana 591	Lemma for relevance implication study.
((a →5 b) ∩ a⊥ ) = ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))
Theorem	u1lemab 592	Lemma for Sasaki implication study.
((a →1 b) ∩ b) = ((a ∩ b) ∪ (a⊥ ∩ b))
Theorem	u2lemab 593	Lemma for Dishkant implication study.
((a →2 b) ∩ b) = b
Theorem	u3lemab 594	Lemma for Kalmbach implication study.
((a →3 b) ∩ b) = ((a ∩ b) ∪ (a⊥ ∩ b))
Theorem	u4lemab 595	Lemma for non-tollens implication study.
((a →4 b) ∩ b) = ((a ∩ b) ∪ (a⊥ ∩ b))
Theorem	u5lemab 596	Lemma for relevance implication study.
((a →5 b) ∩ b) = ((a ∩ b) ∪ (a⊥ ∩ b))
Theorem	u1lemanb 597	Lemma for Sasaki implication study.
((a →1 b) ∩ b⊥ ) = (a⊥ ∩ b⊥ )
Theorem	u2lemanb 598	Lemma for Dishkant implication study.
((a →2 b) ∩ b⊥ ) = (a⊥ ∩ b⊥ )
Theorem	u3lemanb 599	Lemma for Kalmbach implication study.
((a →3 b) ∩ b⊥ ) = (a⊥ ∩ b⊥ )
Theorem	u4lemanb 600	Lemma for non-tollens implication study.
((a →4 b) ∩ b⊥ ) = ((a⊥ ∪ b) ∩ b⊥ )