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

Type	Label	Description
Statement
Theorem	i3n2 501	Equivalence for Kalmbach implication.
(a' ->3 b') = ((a ^ b) v ((a v b') ^ (a' v (a ^ b'))))
Theorem	ni32 502	Equivalence for Kalmbach implication.
(a ->3 b)' = ((a v b) ^ ((a ^ b') v (a' ^ (a v b'))))
Theorem	oi3ai3 503	Theorem for Kalmbach implication.
((a ^ b) v (a ->3 b)') = ((a v b) ^ (a' ->3 b'))
Theorem	i3lem1 504	Lemma for Kalmbach implication.
Theorem	i3lem2 505	Lemma for Kalmbach implication.
Theorem	i3lem3 506	Lemma for Kalmbach implication.
Theorem	i3lem4 507	Lemma for Kalmbach implication.
Theorem	comi31 508	Commutation theorem.
a C (a ->3 b)
Theorem	com2i3 509	Commutation theorem.
a C b   &   a C c   =>   a C (b ->3 c)
Theorem	comi32 510	Commutation theorem.
a C b   =>   a C (b ->3 a)
Theorem	lem4 511	Lemma 4 of Kalmbach p. 240.
(a ->3 (a ->3 b)) = (a' v b)
Theorem	i0i3 512	Translation to Kalmbach implication.
(a' v b) = 1   =>   (a ->3 (a ->3 b)) = 1
Theorem	i3i0 513	Translation from Kalmbach implication.
(a ->3 (a ->3 b)) = 1   =>   (a' v b) = 1
Theorem	ska14 514	Soundness proof for KA14.
((a' v b) ->3 (a ->3 (a ->3 b))) = 1
Theorem	i3le 515	L.e. to Kalmbach implication.
(a ->3 b) = 1   =>   a =< b
Theorem	bii3 516	Biconditional implies Kalmbach implication.
((a == b) ->3 (a ->3 b)) = 1
Theorem	binr1 517	Pavicic binary logic ax-r1 analog.
(a ->3 b) = 1   =>   (b' ->3 a') = 1
Theorem	binr2 518	Pavicic binary logic ax-r2 analog.
(a ->3 b) = 1   &   (b ->3 c) = 1   =>   (a ->3 c) = 1
Theorem	binr3 519	Pavicic binary logic axr3 analog.
(a ->3 c) = 1   &   (b ->3 c) = 1   =>   ((a v b) ->3 c) = 1
Theorem	i31 520	Theorem for Kalmbach implication.
(a ->3 1) = 1
Theorem	i3aa 521	Add antecedent.
a = 1   =>   (b ->3 a) = 1
Theorem	i3abs1 522	Antecedent absorption.
(a ->3 (a ->3 (a ->3 b))) = (a ->3 (a ->3 b))
Theorem	i3abs2 523	Antecedent absorption.
(a ->3 (a ->3 (a ->3 b))) = 1   =>   (a ->3 (a ->3 b)) = 1
Theorem	i3abs3 524	Antecedent absorption.
((a ->3 b) ->3 ((a ->3 b) ->3 a)) = ((a ->3 b) ->3 a)
Theorem	i3orcom 525	Commutative law for conjunction with Kalmbach implication.
((a v b) ->3 (b v a)) = 1
Theorem	i3ancom 526	Commutative law for disjunction with Kalmbach implication.
((a ^ b) ->3 (b ^ a)) = 1
Theorem	bi3tr 527	Transitive inference.
a = b   &   (b ->3 c) = 1   =>   (a ->3 c) = 1
Theorem	i3btr 528	Transitive inference.
(a ->3 b) = 1   &   b = c   =>   (a ->3 c) = 1
Theorem	i33tr1 529	Transitive inference useful for introducing definitions.
(a ->3 b) = 1   &   c = a   &   d = b   =>   (c ->3 d) = 1
Theorem	i33tr2 530	Transitive inference useful for eliminating definitions.
(a ->3 b) = 1   &   a = c   &   b = d   =>   (c ->3 d) = 1
Theorem	i3con1 531	Contrapositive.
(a' ->3 b') = 1   =>   (b ->3 a) = 1
Theorem	i3ror 532	WQL (Weak Quantum Logic) rule.
(a ->3 b) = 1   =>   ((a v c) ->3 (b v c)) = 1
Theorem	i3lor 533	WQL (Weak Quantum Logic) rule.
(a ->3 b) = 1   =>   ((c v a) ->3 (c v b)) = 1
Theorem	i32or 534	WQL (Weak Quantum Logic) rule.
(a ->3 b) = 1   &   (c ->3 d) = 1   =>   ((a v c) ->3 (b v d)) = 1
Theorem	i3ran 535	WQL (Weak Quantum Logic) rule.
(a ->3 b) = 1   =>   ((a ^ c) ->3 (b ^ c)) = 1
Theorem	i3lan 536	WQL (Weak Quantum Logic) rule.
(a ->3 b) = 1   =>   ((c ^ a) ->3 (c ^ b)) = 1
Theorem	i32an 537	WQL (Weak Quantum Logic) rule.
(a ->3 b) = 1   &   (c ->3 d) = 1   =>   ((a ^ c) ->3 (b ^ d)) = 1
Theorem	i3ri3 538	WQL (Weak Quantum Logic) rule.
(a ->3 b) = 1   &   (b ->3 a) = 1   =>   ((a ->3 c) ->3 (b ->3 c)) = 1
Theorem	i3li3 539	WQL (Weak Quantum Logic) rule.
(a ->3 b) = 1   &   (b ->3 a) = 1   =>   ((c ->3 a) ->3 (c ->3 b)) = 1
Theorem	i32i3 540	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 541	Transitive inference.
(a ->3 (a ->3 b)) = 1   &   (b ->3 c) = 1   =>   (a ->3 (a ->3 c)) = 1
Theorem	i3i0tr 542	Transitive inference.
(a ->3 b) = 1   &   (b ->3 (b ->3 c)) = 1   =>   (a ->3 (a ->3 c)) = 1
Theorem	i3th1 543	Theorem for Kalmbach implication.
(a ->3 (a ->3 (b ->3 a))) = 1
Theorem	i3th2 544	Theorem for Kalmbach implication.
(a ->3 (b ->3 (b ->3 a))) = 1
Theorem	i3th3 545	Theorem for Kalmbach implication.
(a' ->3 (a ->3 (a ->3 b))) = 1
Theorem	i3th4 546	Theorem for Kalmbach implication.
(a ->3 (b ->3 b)) = 1
Theorem	i3th5 547	Theorem for Kalmbach implication.
((a ->3 b) ->3 (a ->3 (a ->3 b))) = 1
Theorem	i3th6 548	Theorem for Kalmbach implication.
((a ->3 (a ->3 (a ->3 b))) ->3 (a ->3 (a ->3 b))) = 1
Theorem	i3th7 549	Theorem for Kalmbach implication.
(a ->3 ((a ->3 b) ->3 a)) = 1
Theorem	i3th8 550	Theorem for Kalmbach implication.
((a ->3 b)' ->3 ((a ->3 b) ->3 a)) = 1
Theorem	i3con 551	Theorem for Kalmbach implication.
((a ->3 b) ->3 ((a ->3 b) ->3 (b' ->3 a'))) = 1
Theorem	i3orlem1 552	Lemma for Kalmbach implication OR builder.
Theorem	i3orlem2 553	Lemma for Kalmbach implication OR builder.
Theorem	i3orlem3 554	Lemma for Kalmbach implication OR builder.
Theorem	i3orlem4 555	Lemma for Kalmbach implication OR builder.
Theorem	i3orlem5 556	Lemma for Kalmbach implication OR builder.
Theorem	i3orlem6 557	Lemma for Kalmbach implication OR builder.
Theorem	i3orlem7 558	Lemma for Kalmbach implication OR builder.
Theorem	i3orlem8 559	Lemma for Kalmbach implication OR builder.
Unified disjunction
Theorem	ud1lem1 560	Lemma for unified disjunction.
Theorem	ud1lem2 561	Lemma for unified disjunction.
Theorem	ud1lem3 562	Lemma for unified disjunction.
Theorem	ud2lem1 563	Lemma for unified disjunction.
Theorem	ud2lem2 564	Lemma for unified disjunction.
Theorem	ud2lem3 565	Lemma for unified disjunction.
Theorem	ud3lem1a 566	Lemma for unified disjunction.
Theorem	ud3lem1b 567	Lemma for unified disjunction.
Theorem	ud3lem1c 568	Lemma for unified disjunction.
Theorem	ud3lem1d 569	Lemma for unified disjunction.
Theorem	ud3lem1 570	Lemma for unified disjunction.
Theorem	ud3lem2 571	Lemma for unified disjunction.
Theorem	ud3lem3a 572	Lemma for unified disjunction.
Theorem	ud3lem3b 573	Lemma for unified disjunction.
Theorem	ud3lem3c 574	Lemma for unified disjunction.
Theorem	ud3lem3d 575	Lemma for unified disjunction.
Theorem	ud3lem3 576	Lemma for unified disjunction.
Theorem	ud4lem1a 577	Lemma for unified disjunction.
Theorem	ud4lem1b 578	Lemma for unified disjunction.
Theorem	ud4lem1c 579	Lemma for unified disjunction.
Theorem	ud4lem1d 580	Lemma for unified disjunction.
Theorem	ud4lem1 581	Lemma for unified disjunction.
Theorem	ud4lem2 582	Lemma for unified disjunction.
Theorem	ud4lem3a 583	Lemma for unified disjunction.
Theorem	ud4lem3b 584	Lemma for unified disjunction.
Theorem	ud4lem3 585	Lemma for unified disjunction.
Theorem	ud5lem1a 586	Lemma for unified disjunction.
Theorem	ud5lem1b 587	Lemma for unified disjunction.
Theorem	ud5lem1c 588	Lemma for unified disjunction.
Theorem	ud5lem1 589	Lemma for unified disjunction.
Theorem	ud5lem2 590	Lemma for unified disjunction.
Theorem	ud5lem3a 591	Lemma for unified disjunction.
Theorem	ud5lem3b 592	Lemma for unified disjunction.
Theorem	ud5lem3c 593	Lemma for unified disjunction.
Theorem	ud5lem3 594	Lemma for unified disjunction.
Theorem	ud1 595	Unified disjunction for Sasaki implication.
(a v b) = ((a ->1 b) ->1 (((a ->1 b) ->1 (b ->1 a)) ->1 a))
Theorem	ud2 596	Unified disjunction for Dishkant implication.
(a v b) = ((a ->2 b) ->2 (((a ->2 b) ->2 (b ->2 a)) ->2 a))
Theorem	ud3 597	Unified disjunction for Kalmbach implication.
(a v b) = ((a ->3 b) ->3 (((a ->3 b) ->3 (b ->3 a)) ->3 a))
Theorem	ud4 598	Unified disjunction for non-tollens implication.
(a v b) = ((a ->4 b) ->4 (((a ->4 b) ->4 (b ->4 a)) ->4 a))
Theorem	ud5 599	Unified disjunction for relevance implication.
(a v b) = ((a ->5 b) ->5 (((a ->5 b) ->5 (b ->5 a)) ->5 a))
Lemmas for unified implication study
Theorem	u1lemaa 600	Lemma for Sasaki implication study. Equation 4.10 of [MegPav2000] p. 23. This is the second part of the equation.