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

Type	Label	Description
Statement
Theorem	wbile 401	Biconditional to l.e.
(a == b) = 1   =>   (a =<2 b) = 1
Theorem	wlebi 402	L.e. to biconditional.
(a =<2 b) = 1   &   (b =<2 a) = 1   =>   (a == b) = 1
Theorem	wle2or 403	Disjunction of 2 l.e.'s
(a =<2 b) = 1   &   (c =<2 d) = 1   =>   ((a v c) =<2 (b v d)) = 1
Theorem	wle2an 404	Conjunction of 2 l.e.'s
(a =<2 b) = 1   &   (c =<2 d) = 1   =>   ((a ^ c) =<2 (b ^ d)) = 1
Theorem	wledi 405	Half of distributive law.
(((a ^ b) v (a ^ c)) =<2 (a ^ (b v c))) = 1
Theorem	wledio 406	Half of distributive law.
((a v (b ^ c)) =<2 ((a v b) ^ (a v c))) = 1
Theorem	wcom0 407	Commutation with 0. Kalmbach 83 p. 20.
C (a, 0) = 1
Theorem	wcom1 408	Commutation with 1. Kalmbach 83 p. 20.
C (1, a) = 1
Theorem	wlecom 409	Comparable elements commute. Beran 84 2.3(iii) p. 40.
(a =<2 b) = 1   =>   C (a, b) = 1
Theorem	wbctr 410	Transitive inference.
(a == b) = 1   &   C (b, c) = 1   =>   C (a, c) = 1
Theorem	wcbtr 411	Transitive inference.
C (a, b) = 1   &   (b == c) = 1   =>   C (a, c) = 1
Theorem	wcomorr 412	Weak commutation law.
C (a, (a v b)) = 1
Theorem	wcoman1 413	Weak commutation law.
C ((a ^ b), a) = 1
Theorem	wcomcom 414	Commutation is symmetric. Kalmbach 83 p. 22.
C (a, b) = 1   =>   C (b, a) = 1
Theorem	wcomcom2 415	Commutation equivalence. Kalmbach 83 p. 23.
C (a, b) = 1   =>   C (a, b') = 1
Theorem	wcomcom3 416	Commutation equivalence. Kalmbach 83 p. 23.
C (a, b) = 1   =>   C (a', b) = 1
Theorem	wcomcom4 417	Commutation equivalence. Kalmbach 83 p. 23.
C (a, b) = 1   =>   C (a', b') = 1
Theorem	wcomd 418	Commutation dual. Kalmbach 83 p. 23.
C (a, b) = 1   =>   (a == ((a v b) ^ (a v b'))) = 1
Theorem	wcom3ii 419	Lemma 3(ii) of Kalmbach 83 p. 23.
C (a, b) = 1   =>   ((a ^ (a' v b)) == (a ^ b)) = 1
Theorem	wcomcom5 420	Commutation equivalence. Kalmbach 83 p. 23.
C (a', b') = 1   =>   C (a, b) = 1
Theorem	wcomdr 421	Commutation dual. Kalmbach 83 p. 23.
(a == ((a v b) ^ (a v b'))) = 1   =>   C (a, b) = 1
Theorem	wcom3i 422	Lemma 3(i) of Kalmbach 83 p. 23.
((a ^ (a' v b)) == (a ^ b)) = 1   =>   C (a, b) = 1
Theorem	wfh1 423	Weak structural analog of Foulis-Holland Theorem.
C (a, b) = 1   &   C (a, c) = 1   =>   ((a ^ (b v c)) == ((a ^ b) v (a ^ c))) = 1
Theorem	wfh2 424	Weak structural analog of Foulis-Holland Theorem.
C (a, b) = 1   &   C (a, c) = 1   =>   ((b ^ (a v c)) == ((b ^ a) v (b ^ c))) = 1
Theorem	wfh3 425	Weak structural analog of Foulis-Holland Theorem.
C (a, b) = 1   &   C (a, c) = 1   =>   ((a v (b ^ c)) == ((a v b) ^ (a v c))) = 1
Theorem	wfh4 426	Weak structural analog of Foulis-Holland Theorem.
C (a, b) = 1   &   C (a, c) = 1   =>   ((b v (a ^ c)) == ((b v a) ^ (b v c))) = 1
Theorem	wcom2or 427	Th. 4.2 Beran p. 49.
C (a, b) = 1   &   C (a, c) = 1   =>   C (a, (b v c)) = 1
Theorem	wcom2an 428	Th. 4.2 Beran p. 49.
C (a, b) = 1   &   C (a, c) = 1   =>   C (a, (b ^ c)) = 1
Theorem	wnbdi 429	Negated biconditional (distributive form)
((a == b)' == (((a v b) ^ a') v ((a v b) ^ b'))) = 1
Theorem	wlem14 430	Lemma for KA14 soundness.
Theorem	wr5 431	Proof of weak orthomodular law from weaker-looking equivalent, wom3 367, which in turn is derived from ax-wom 361.
(a == b) = 1   =>   ((a v c) == (b v c)) = 1
Kalmbach axioms (soundness proofs) that require WOML
Theorem	ska2 432	Soundness theorem for Kalmbach's quantum propositional logic axiom KA2.
((a == b)' v ((b == c)' v (a == c))) = 1
Theorem	ska4 433	Soundness theorem for Kalmbach's quantum propositional logic axiom KA4.
((a == b)' v ((a ^ c) == (b ^ c))) = 1
Theorem	wom2 434	Weak orthomodular law for study of weakly orthomodular lattices.
a =< ((a == b)' v ((a v c) == (b v c)))
Theorem	ka4ot 435	3-variable version of weakly orthomodular law. It is proved from a weaker-looking equivalent, wom2 434, which in turn is proved from ax-wom 361.
((a == b)' v ((a v c) == (b v c))) = 1
Weak orthomodular law variants
Theorem	woml6 436	Variant of weakly orthomodular law.
((a ->1 b)' v (a ->2 b)) = 1
Theorem	woml7 437	Variant of weakly orthomodular law.
(((a ->2 b) ^ (b ->2 a))' v (a == b)) = 1
Theorem	ortha 438	Property of orthogonality
a =< b'   =>   (a ^ b) = 0
Orthomodular lattices
Orthomodular law
Axiom	ax-r3 439	Orthomodular law - when added to an ortholattice, it makes the ortholattice an orthomodular lattice. See r3a 440 for a more compact version.
(c v c') = ((a' v b')' v (a v b)')   =>   a = b
Theorem	r3a 440	Orthomodular law restated.
1 = (a == b)   =>   a = b
Theorem	wed 441	Weak equivalential detachment (WBMP).
a = b   &   (a == b) = (c == d)   =>   c = d
Theorem	r3b 442	Orthomodular law from weak equivalential detachment (WBMP).
(c v c') = (a == b)   =>   a = b
Theorem	lem3.1 443	Lemma used in proof of Th. 3.1 of Pavicic 1993.
(a v b) = b   &   (b' v a) = 1   =>   a = b
Theorem	lem3a.1 444	Lemma used in proof of Th. 3.1 of Pavicic 1993.
(a v b) = b   &   (b' v a) = 1   =>   (a v b) = a
Theorem	oml 445	Orthomodular law. Compare Th. 1 of Pavicic 1987.
(a v (a' ^ (a v b))) = (a v b)
Theorem	omln 446	Orthomodular law.
(a' v (a ^ (a' v b))) = (a' v b)
Theorem	omla 447	Orthomodular law.
(a ^ (a' v (a ^ b))) = (a ^ b)
Theorem	omlan 448	Orthomodular law.
(a' ^ (a v (a' ^ b))) = (a' ^ b)
Theorem	oml5 449	Orthomodular law.
((a ^ b) v ((a ^ b)' ^ (b v c))) = (b v c)
Theorem	oml5a 450	Orthomodular law.
((a v b) ^ ((a v b)' v (b ^ c))) = (b ^ c)
Relationship analogues using OML (ordering; commutation)
Theorem	oml2 451	Orthomodular law. Kalmbach 83 p. 22.
a =< b   =>   (a v (a' ^ b)) = b
Theorem	oml3 452	Orthomodular law. Kalmbach 83 p. 22.
a =< b   &   (b ^ a') = 0   =>   a = b
Theorem	comcom 453	Commutation is symmetric. Kalmbach 83 p. 22.
a C b   =>   b C a
Theorem	comcom3 454	Commutation equivalence. Kalmbach 83 p. 23.
a C b   =>   a' C b
Theorem	comcom4 455	Commutation equivalence. Kalmbach 83 p. 23.
a C b   =>   a' C b'
Theorem	comd 456	Commutation dual. Kalmbach 83 p. 23.
a C b   =>   a = ((a v b) ^ (a v b'))
Theorem	com3ii 457	Lemma 3(ii) of Kalmbach 83 p. 23.
a C b   =>   (a ^ (a' v b)) = (a ^ b)
Theorem	comcom5 458	Commutation equivalence. Kalmbach 83 p. 23.
a' C b'   =>   a C b
Theorem	comcom6 459	Commutation equivalence. Kalmbach 83 p. 23.
a' C b   =>   a C b
Theorem	comcom7 460	Commutation equivalence. Kalmbach 83 p. 23.
a C b'   =>   a C b
Theorem	comor1 461	Commutation law.
(a v b) C a
Theorem	comor2 462	Commutation law.
(a v b) C b
Theorem	comorr2 463	Commutation law.
b C (a v b)
Theorem	comanr1 464	Commutation law.
a C (a ^ b)
Theorem	comanr2 465	Commutation law.
b C (a ^ b)
Theorem	comdr 466	Commutation dual. Kalmbach 83 p. 23.
a = ((a v b) ^ (a v b'))   =>   a C b
Theorem	com3i 467	Lemma 3(i) of Kalmbach 83 p. 23.
(a ^ (a' v b)) = (a ^ b)   =>   a C b
Theorem	df2c1 468	Dual 'commutes' analogue for == analogue of =.
a = ((a v b) ^ (a v b'))   =>   a C b
Theorem	fh1 469	Foulis-Holland Theorem.
a C b   &   a C c   =>   (a ^ (b v c)) = ((a ^ b) v (a ^ c))
Theorem	fh2 470	Foulis-Holland Theorem.
a C b   &   a C c   =>   (b ^ (a v c)) = ((b ^ a) v (b ^ c))
Theorem	fh3 471	Foulis-Holland Theorem.
a C b   &   a C c   =>   (a v (b ^ c)) = ((a v b) ^ (a v c))
Theorem	fh4 472	Foulis-Holland Theorem.
a C b   &   a C c   =>   (b v (a ^ c)) = ((b v a) ^ (b v c))
Theorem	fh1r 473	Foulis-Holland Theorem.
a C b   &   a C c   =>   ((b v c) ^ a) = ((b ^ a) v (c ^ a))
Theorem	fh2r 474	Foulis-Holland Theorem.
a C b   &   a C c   =>   ((a v c) ^ b) = ((a ^ b) v (c ^ b))
Theorem	fh3r 475	Foulis-Holland Theorem.
a C b   &   a C c   =>   ((b ^ c) v a) = ((b v a) ^ (c v a))
Theorem	fh4r 476	Foulis-Holland Theorem.
a C b   &   a C c   =>   ((a ^ c) v b) = ((a v b) ^ (c v b))
Theorem	fh2c 477	Foulis-Holland Theorem.
a C b   &   a C c   =>   (b ^ (c v a)) = ((b ^ c) v (b ^ a))
Theorem	fh4c 478	Foulis-Holland Theorem.
a C b   &   a C c   =>   (b v (c ^ a)) = ((b v c) ^ (b v a))
Theorem	fh1rc 479	Foulis-Holland Theorem.
a C b   &   a C c   =>   ((c v b) ^ a)