Quantum Logic Explorer - mmtheorems5

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 - 401-500 - Page 5 of 11

Type	Label	Description
Statement
Theorem	wcom3ii 401	Lemma 3(ii) of Kalmbach 83 p. 23.
C (a, b) = 1    ⇒   ((a ∩ (a⊥ ∪ b)) ≡ (a ∩ b)) = 1
Theorem	wcomcom5 402	Commutation equivalence. Kalmbach 83 p. 23.
C (a⊥ , b⊥ ) = 1    ⇒    C (a, b) = 1
Theorem	wcomdr 403	Commutation dual. Kalmbach 83 p. 23.
(a ≡ ((a ∪ b) ∩ (a ∪ b⊥ ))) = 1    ⇒    C (a, b) = 1
Theorem	wcom3i 404	Lemma 3(i) of Kalmbach 83 p. 23.
((a ∩ (a⊥ ∪ b)) ≡ (a ∩ b)) = 1    ⇒    C (a, b) = 1
Theorem	wfh1 405	Weak structural analog of Foulis-Holland Theorem.
C (a, b) = 1    &    C (a, c) = 1    ⇒   ((a ∩ (b ∪ c)) ≡ ((a ∩ b) ∪ (a ∩ c))) = 1
Theorem	wfh2 406	Weak structural analog of Foulis-Holland Theorem.
C (a, b) = 1    &    C (a, c) = 1    ⇒   ((b ∩ (a ∪ c)) ≡ ((b ∩ a) ∪ (b ∩ c))) = 1
Theorem	wfh3 407	Weak structural analog of Foulis-Holland Theorem.
C (a, b) = 1    &    C (a, c) = 1    ⇒   ((a ∪ (b ∩ c)) ≡ ((a ∪ b) ∩ (a ∪ c))) = 1
Theorem	wfh4 408	Weak structural analog of Foulis-Holland Theorem.
C (a, b) = 1    &    C (a, c) = 1    ⇒   ((b ∪ (a ∩ c)) ≡ ((b ∪ a) ∩ (b ∪ c))) = 1
Theorem	wcom2or 409	Th. 4.2 Beran p. 49.
C (a, b) = 1    &    C (a, c) = 1    ⇒    C (a, (b ∪ c)) = 1
Theorem	wcom2an 410	Th. 4.2 Beran p. 49.
C (a, b) = 1    &    C (a, c) = 1    ⇒    C (a, (b ∩ c)) = 1
Theorem	wnbdi 411	Negated biconditional (distributive form)
((a ≡ b)⊥ ≡ (((a ∪ b) ∩ a⊥ ) ∪ ((a ∪ b) ∩ b⊥ ))) = 1
Theorem	wlem14 412	Lemma for KA14 soundness.
(((a ∩ b⊥ ) ∪ a⊥ )⊥ ∪ ((a ∩ b⊥ ) ∪ ((a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b))) ∪ (a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ )))) = 1
Theorem	wr5 413	Proof of weak orthomodular law from weaker-looking equivalent, wom3 349, which in turn is derived from ax-wom 343.
(a ≡ b) = 1    ⇒   ((a ∪ c) ≡ (b ∪ c)) = 1
Theorem	ska2 414	Soundness theorem for Kalmbach's quantum propositional logic axiom KA2.
((a ≡ b)⊥ ∪ ((b ≡ c)⊥ ∪ (a ≡ c))) = 1
Theorem	ska4 415	Soundness theorem for Kalmbach's quantum propositional logic axiom KA4.
((a ≡ b)⊥ ∪ ((a ∩ c) ≡ (b ∩ c))) = 1
Theorem	wom2 416	Weak orthomodular law for study of weakly orthomodular lattices.
a ≤ ((a ≡ b)⊥ ∪ ((a ∪ c) ≡ (b ∪ c)))
Theorem	ka4ot 417	3-variable version of weakly orthomodular law. It is proved from a weaker-looking equivalent, wom2 416, which in turn is proved from ax-wom 343.
((a ≡ b)⊥ ∪ ((a ∪ c) ≡ (b ∪ c))) = 1
Theorem	woml6 418	Variant of weakly orthomodular law.
((a →1 b)⊥ ∪ (a →2 b)) = 1
Theorem	woml7 419	Variant of weakly orthomodular law.
(((a →2 b) ∩ (b →2 a))⊥ ∪ (a ≡ b)) = 1
Theorem	ortha 420	Property of orthogonality
a ≤ b⊥    ⇒   (a ∩ b) = 0
Axiom	ax-r3 421	Orthomodular law - when added to an ortholattice, it makes the ortholattice an orthomodular lattice. See r3a 422 for a more compact version.
(c ∪ c⊥ ) = ((a⊥ ∪ b⊥ )⊥ ∪ (a ∪ b)⊥ )    ⇒   a = b
Theorem	r3a 422	Orthomodular law restated.
1 = (a ≡ b)    ⇒   a = b
Theorem	wed 423	Weak equivalential detachment (WBMP).
a = b    &   (a ≡ b) = (c ≡ d)    ⇒   c = d
Theorem	r3b 424	Orthomodular law from weak equivalential detachment (WBMP).
(c ∪ c⊥ ) = (a ≡ b)    ⇒   a = b
Theorem	lem3.1 425	Lemma used in proof of Th. 3.1 of Pavicic 1993.
(a ∪ b) = b    &   (b⊥ ∪ a) = 1    ⇒   a = b
Theorem	lem3a.1 426	Lemma used in proof of Th. 3.1 of Pavicic 1993.
(a ∪ b) = b    &   (b⊥ ∪ a) = 1    ⇒   (a ∪ b) = a
Theorem	oml 427	Orthomodular law. Compare Th. 1 of Pavicic 1987.
(a ∪ (a⊥ ∩ (a ∪ b))) = (a ∪ b)
Theorem	omln 428	Orthomodular law.
(a⊥ ∪ (a ∩ (a⊥ ∪ b))) = (a⊥ ∪ b)
Theorem	omla 429	Orthomodular law.
(a ∩ (a⊥ ∪ (a ∩ b))) = (a ∩ b)
Theorem	omlan 430	Orthomodular law.
(a⊥ ∩ (a ∪ (a⊥ ∩ b))) = (a⊥ ∩ b)
Theorem	oml5 431	Orthomodular law.
((a ∩ b) ∪ ((a ∩ b)⊥ ∩ (b ∪ c))) = (b ∪ c)
Theorem	oml5a 432	Orthomodular law.
((a ∪ b) ∩ ((a ∪ b)⊥ ∪ (b ∩ c))) = (b ∩ c)
Theorem	oml2 433	Orthomodular law. Kalmbach 83 p. 22.
a ≤ b    ⇒   (a ∪ (a⊥ ∩ b)) = b
Theorem	oml3 434	Orthomodular law. Kalmbach 83 p. 22.
a ≤ b    &   (b ∩ a⊥ ) = 0    ⇒   a = b
Theorem	comcom 435	Commutation is symmetric. Kalmbach 83 p. 22.
a C b    ⇒   b C a
Theorem	comcom3 436	Commutation equivalence. Kalmbach 83 p. 23.
a C b    ⇒   a⊥ C b
Theorem	comcom4 437	Commutation equivalence. Kalmbach 83 p. 23.
a C b    ⇒   a⊥ C b⊥
Theorem	comd 438	Commutation dual. Kalmbach 83 p. 23.
a C b    ⇒   a = ((a ∪ b) ∩ (a ∪ b⊥ ))
Theorem	com3ii 439	Lemma 3(ii) of Kalmbach 83 p. 23.
a C b    ⇒   (a ∩ (a⊥ ∪ b)) = (a ∩ b)
Theorem	comcom5 440	Commutation equivalence. Kalmbach 83 p. 23.
a⊥ C b⊥    ⇒   a C b
Theorem	comcom6 441	Commutation equivalence. Kalmbach 83 p. 23.
a⊥ C b    ⇒   a C b
Theorem	comcom7 442	Commutation equivalence. Kalmbach 83 p. 23.
a C b⊥    ⇒   a C b
Theorem	comor1 443	Commutation law.
(a ∪ b) C a
Theorem	comor2 444	Commutation law.
(a ∪ b) C b
Theorem	comorr2 445	Commutation law.
b C (a ∪ b)
Theorem	comanr1 446	Commutation law.
a C (a ∩ b)
Theorem	comanr2 447	Commutation law.
b C (a ∩ b)
Theorem	comdr 448	Commutation dual. Kalmbach 83 p. 23.
a = ((a ∪ b) ∩ (a ∪ b⊥ ))    ⇒   a C b
Theorem	com3i 449	Lemma 3(i) of Kalmbach 83 p. 23.
(a ∩ (a⊥ ∪ b)) = (a ∩ b)    ⇒   a C b
Theorem	df2c1 450	Dual 'commutes' analogue for ≡ analogue of =.
a = ((a ∪ b) ∩ (a ∪ b⊥ ))    ⇒   a C b
Theorem	fh1 451	Foulis-Holland Theorem.
a C b    &   a C c    ⇒   (a ∩ (b ∪ c)) = ((a ∩ b) ∪ (a ∩ c))
Theorem	fh2 452	Foulis-Holland Theorem.
a C b    &   a C c    ⇒   (b ∩ (a ∪ c)) = ((b ∩ a) ∪ (b ∩ c))
Theorem	fh3 453	Foulis-Holland Theorem.
a C b    &   a C c    ⇒   (a ∪ (b ∩ c)) = ((a ∪ b) ∩ (a ∪ c))
Theorem	fh4 454	Foulis-Holland Theorem.
a C b    &   a C c    ⇒   (b ∪ (a ∩ c)) = ((b ∪ a) ∩ (b ∪ c))
Theorem	fh1r 455	Foulis-Holland Theorem.
a C b    &   a C c    ⇒   ((b ∪ c) ∩ a) = ((b ∩ a) ∪ (c ∩ a))
Theorem	fh2r 456	Foulis-Holland Theorem.
a C b    &   a C c    ⇒   ((a ∪ c) ∩ b) = ((a ∩ b) ∪ (c ∩ b))
Theorem	fh3r 457	Foulis-Holland Theorem.
a C b    &   a C c    ⇒   ((b ∩ c) ∪ a) = ((b ∪ a) ∩ (c ∪ a))
Theorem	fh4r 458	Foulis-Holland Theorem.
a C b    &   a C c    ⇒   ((a ∩ c) ∪ b) = ((a ∪ b) ∩ (c ∪ b))
Theorem	fh2c 459	Foulis-Holland Theorem.
a C b    &   a C c    ⇒   (b ∩ (c ∪ a)) = ((b ∩ c) ∪ (b ∩ a))
Theorem	fh4c 460	Foulis-Holland Theorem.
a C b    &   a C c    ⇒   (b ∪ (c ∩ a)) = ((b ∪ c) ∩ (b ∪ a))
Theorem	fh1rc 461	Foulis-Holland Theorem.
a C b    &   a C c    ⇒   ((c ∪ b) ∩ a) = ((c ∩ a) ∪ (b ∩ a))
Theorem	fh2rc 462	Foulis-Holland Theorem.
a C b    &   a C c    ⇒   ((c ∪ a) ∩ b) = ((c ∩ b) ∪ (a ∩ b))
Theorem	fh3rc 463	Foulis-Holland Theorem.
a C b    &   a C c    ⇒   ((c ∩ b) ∪ a) = ((c ∪ a) ∩ (b ∪ a))
Theorem	fh4rc 464	Foulis-Holland Theorem.
a C b    &   a C c    ⇒   ((c ∩ a) ∪ b) = ((c ∪ b) ∩ (a ∪ b))
Theorem	com2or 465	Th. 4.2 Beran p. 49.
a C b    &   a C c    ⇒   a C (b ∪ c)
Theorem	com2an 466	Th. 4.2 Beran p. 49.
a C b    &   a C c    ⇒   a C (b ∩ c)
Theorem	combi 467	Commutation theorem for Sasaki implication.
a C (a ≡ b)
Theorem	nbdi 468	Negated biconditional (distributive form)
(a ≡ b)⊥ = (((a ∪ b) ∩ a⊥ ) ∪ ((a ∪ b) ∩ b⊥ ))
Theorem	oml4 469	Orthomodular law.
((a ≡ b) ∩ a) ≤ b
Theorem	oml6 470	Orthomodular law.
(a ∪ (b ∩ (a⊥ ∪ b⊥ ))) = (a ∪ b)
Theorem	gsth 471	Gudder-Schelp's Theorem. Beran, p. 262, Th. 4.1.
a C b    &   b C c    &   a C (b ∩ c)    ⇒   (a ∩ b) C c
Theorem	gsth2 472	Stronger version of Gudder-Schelp's Theorem. Beran, p. 263, Th. 4.2.
b C c    &   a C (b ∩ c)    ⇒   (a ∩ b) C c
Theorem	gstho 473	"OR" version of Gudder-Schelp's Theorem.
b C c    &   a C (b ∪ c)    ⇒   (a ∪ b) C c
Theorem	gt1 474	Part of Lemma 1 from Gaisi Takeuti, "Quantum Set Theory".
a = (b ∪ c)    &   b ≤ d    &   c ≤ d⊥    ⇒   a C d
Theorem	cmtr1com 475	Commutator equal to 1 commutes. Theorem 2.11 of Beran, p. 86.
C (a, b) = 1    ⇒   a C b
Theorem	comcmtr1 476	Commutation implies commutator equal to 1. Theorem 2.11 of Beran, p. 86.
a C b    ⇒    C (a, b) = 1
Theorem	i0cmtrcom 477	Commutator element →0 commutator implies commutation.
(a →0 C (a, b)) = 1    ⇒   a C b
Theorem	i3bi 478	Kalmbach implication and biconditional.
((a →3 b) ∩ (b →3 a)) = (a ≡ b)
Theorem	i3or 479	Kalmbach implication OR builder.
((a ≡ b)⊥ ∪ ((a ∪ c) →3 (b ∪ c))) = 1
Theorem	df2i3 480	Alternate definition for Kalmbach implication.
(a →3 b) = ((a⊥ ∩ b⊥ ) ∪ ((a⊥ ∪ b) ∩ (a ∪ (a⊥ ∩ b))))
Theorem	dfi3b 481	Alternate Kalmbach conditional.
(a →3 b) = ((a⊥ ∪ b) ∩ ((a ∪ (a⊥ ∩ b⊥ )) ∪ (a⊥ ∩ b)))
Theorem	dfi4b 482	Alternate non-tollens conditional.
(a →4 b) = ((a⊥ ∪ b) ∩ ((b⊥ ∪ (b ∩ a⊥ )) ∪ (b ∩ a)))
Theorem	i3n2 483	Equivalence for Kalmbach implication.
(a⊥ →3 b⊥ ) = ((a ∩ b) ∪ ((a ∪ b⊥ ) ∩ (a⊥ ∪ (a ∩ b⊥ ))))
Theorem	ni32 484	Equivalence for Kalmbach implication.
(a →3 b)⊥ = ((a ∪ b) ∩ ((a ∩ b⊥ ) ∪ (a⊥ ∩ (a ∪ b⊥ ))))
Theorem	oi3ai3 485	Theorem for Kalmbach implication.
((a ∩ b) ∪ (a →3 b)⊥ ) = ((a ∪ b) ∩ (a⊥ →3 b⊥ ))
Theorem	i3lem1 486	Lemma for Kalmbach implication.
(a →3 b) = 1    ⇒   ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )) = a⊥
Theorem	i3lem2 487	Lemma for Kalmbach implication.
(a →3 b) = 1    ⇒   a C b
Theorem	i3lem3 488	Lemma for Kalmbach implication.
(a →3 b) = 1    ⇒   ((a⊥ ∪ b) ∩ b⊥ ) = (a⊥ ∩ b⊥ )
Theorem	i3lem4 489	Lemma for Kalmbach implication.
(a →3 b) = 1    ⇒   (a⊥ ∪ b) = 1
Theorem	comi31 490	Commutation theorem.
a C (a →3 b)
Theorem	com2i3 491	Commutation theorem.
a C b    &   a C c    ⇒   a C (b →3 c)
Theorem	comi32 492	Commutation theorem.
a C b    ⇒   a C (b →3 a)
Theorem	lem4 493	Lemma 4 of Kalmbach p. 240.
(a →3 (a →3 b)) = (a⊥ ∪ b)
Theorem	i0i3 494	Translation to Kalmbach implication.
(a⊥ ∪ b) = 1    ⇒   (a →3 (a →3 b)) = 1
Theorem	i3i0 495	Translation from Kalmbach implication.
(a →3 (a →3 b)) = 1    ⇒   (a⊥ ∪ b) = 1
Theorem	ska14 496	Soundness proof for KA14.
((a⊥ ∪ b) →3 (a →3 (a →3 b))) = 1
Theorem	i3le 497	L.e. to Kalmbach implication.
(a →3 b) = 1    ⇒   a ≤ b
Theorem	bii3 498	Biconditional implies Kalmbach implication.
((a ≡ b) →3 (a →3 b)) = 1
Theorem	binr1 499	Pavicic binary logic ax-r1 analog.
(a →3 b) = 1    ⇒   (b⊥ →3 a⊥ ) = 1
Theorem	binr2 500	Pavicic binary logic ax-r2 analog.
(a →3 b) = 1    &   (b →3 c) = 1    ⇒   (a →3 c) = 1