mmtheorems - 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

Table of Contents

Ortholattices
    Basic syntax and axioms   wb 1
    Basic lemmas   id 59
    Relationship analogues (ordering; commutation)   df-le 129
    Commutator (ortholattice theorems)   cmtrcom 190
    Weak "orthomodular law" in ortholattices.   wa1 191
    Kalmbach axioms (soundness proofs) that are true in all ortholattices   sklem 230
Weakly orthomodular lattices
    Weak orthomodular law   ax-wom 361
    Weakly orthomodular lattices   wom3 367
    Relationship analogues (ordering; commutation) in WOML   wleoa 376
    Kalmbach axioms (soundness proofs) that require WOML   ska2 432
    Weak orthomodular law variants   woml6 436
Orthomodular lattices
    Orthomodular law   ax-r3 439
    Relationship analogues using OML (ordering; commutation)   oml2 451
    Commutator (orthomodular lattice theorems)   cmtr1com 493
    Kalmbach conditional   i3bi 496
    Unified disjunction   ud1lem1 560
    Lemmas for unified implication study   u1lemaa 600
    Some proofs contributed by Josiah Burroughs   u1lemn1b 730
    More lemmas for unified implication   u1lem1 734
    Some 3-variable theorems   3vth1 804
    OML Lemmas for studying Godowski equations.   govar 896
    OML Lemmas for studying orthoarguesian laws   oas 925
    5OA law   oa8todual 971
    "Godowski/Greechie" form of proper 4-OA   oa4to4u 973
    Some 3-OA inferences (derived under OM)   oa3-2lema 978
Derivation of 4-variable proper OA from OA distributive law
Orthoarguesian laws
    3-variable orthoarguesian law   ax-3oa 998
    4-variable orthoarguesian law   ax-oal4 1026
    6-variable orthoarguesian law   ax-oa6 1029
    The proper 4-variable orthoarguesian law   ax-4oa 1032
Other stronger-than-OML laws
    New state-related equation   ax-newstateeq 1044
Contributions of Roy Longton
    Roy's first section   lem3.3.2 1045
    Roy's second section   lem3.4.1 1074
    Roy's third section   lem4.6.2e1 1079
Weakly distributive ortholattices (WDOL)
    WDOL law   ax-wdol 1101

Statement List for Quantum Logic Explorer - 1-100 - Page 1 of 12

Type	Label	Description
Statement
Ortholattices
Basic syntax and axioms
Syntax	wb 1	If a and b are terms, a = b is a wff.
wff a = b
Syntax	wle 2	If a and b are terms, a =< b is a wff.
wff a =< b
Syntax	wc 3	If a and b are terms, a C b is a wff.
wff a C b
Syntax	wn 4	If a is a term, a' is a wff.
term a'
Syntax	tb 5	If a and b are terms, so is (a == b).
term (a == b)
Syntax	wo 6	If a and b are terms, so is (a v b).
term (a v b)
Syntax	wa 7	If a and b are terms, so is (a ^ b).
term (a ^ b)
Syntax	wt 8	The logical true constant is a term.
term 1
Syntax	wf 9	The logical false constant is a term.
term 0
Syntax	wle2 10	If a and b are terms, so is (a =<2 b).
term (a =<2 b)
Syntax	wi0 11	If a and b are terms, so is (a ->0 b).
term (a ->0 b)
Syntax	wi1 12	If a and b are terms, so is (a ->1 b).
term (a ->1 b)
Syntax	wi2 13	If a and b are terms, so is (a ->2 b).
term (a ->2 b)
Syntax	wi3 14	If a and b are terms, so is (a ->3 b).
term (a ->3 b)
Syntax	wi4 15	If a and b are terms, so is (a ->4 b).
term (a ->4 b)
Syntax	wi5 16	If a and b are terms, so is (a ->5 b).
term (a ->5 b)
Syntax	wid0 17	If a and b are terms, so is (a ==0 b).
term (a ==0 b)
Syntax	wid1 18	If a and b are terms, so is (a ==1 b).
term (a ==1 b)
Syntax	wid2 19	If a and b are terms, so is (a ==2 b).
term (a ==2 b)
Syntax	wid3 20	If a and b are terms, so is (a ==3 b).
term (a ==3 b)
Syntax	wid4 21	If a and b are terms, so is (a ==4 b).
term (a ==4 b)
Syntax	wid5 22	If a and b are terms, so is (a ==5 b).
term (a ==5 b)
Syntax	wb3 23	If a and b are terms, so is (a <->3 b).
term (a <->3 b)
Syntax	wb1 24	If a and b are terms, so is (a <->3 b).
term (a <->1 b)
Syntax	wo3 25	If a and b are terms, so is (a u3 b).
term (a u3 b)
Syntax	wan3 26	If a and b are terms, so is (a ^3 b).
term (a ^3 b)
Syntax	wid3oa 27	If a, b, and c are terms, so is (a == c ==OA b).
term (a == c ==OA b)
Syntax	wid4oa 28	If a, b, c, and d are terms, so is (a == c, d ==OA b).
term (a == c, d ==OA b)
Syntax	wcmtr 29	If a and b are terms, so is C (a, b).
term C (a, b)
Axiom	ax-a1 30	Axiom for ortholattices.
a = a''
Axiom	ax-a2 31	Axiom for ortholattices.
(a v b) = (b v a)
Axiom	ax-a3 32	Axiom for ortholattices.
((a v b) v c) = (a v (b v c))
Axiom	ax-a4 33	Axiom for ortholattices.
(a v (b v b')) = (b v b')
Axiom	ax-a5 34	Axiom for ortholattices.
(a v (a' v b)') = a
Axiom	ax-r1 35	Inference rule for ortholattices.
a = b   =>   b = a
Axiom	ax-r2 36	Inference rule for ortholattices.
a = b   &   b = c   =>   a = c
Axiom	ax-r4 37	Inference rule for ortholattices.
a = b   =>   a' = b'
Axiom	ax-r5 38	Inference rule for ortholattices.
a = b   =>   (a v c) = (b v c)
Definition	df-b 39	Define biconditional.
(a == b) = ((a' v b')' v (a v b)')
Definition	df-a 40	Define conjunction.
(a ^ b) = (a' v b')'
Definition	df-t 41	Define true.
1 = (a v a')
Definition	df-f 42	Define false.
0 = 1'
Definition	df-i0 43	Define classical conditional.
(a ->0 b) = (a' v b)
Definition	df-i1 44	Define Sasaki (Mittelstaedt) conditional.
(a ->1 b) = (a' v (a ^ b))
Definition	df-i2 45	Define Dishkant conditional.
(a ->2 b) = (b v (a' ^ b'))
Definition	df-i3 46	Define Kalmbach conditional.
(a ->3 b) = (((a' ^ b) v (a' ^ b')) v (a ^ (a' v b)))
Definition	df-i4 47	Define non-tollens conditional.
(a ->4 b) = (((a ^ b) v (a' ^ b)) v ((a' v b) ^ b'))
Definition	df-i5 48	Define relevance conditional.
(a ->5 b) = (((a ^ b) v (a' ^ b)) v (a' ^ b'))
Definition	df-id0 49	Define classical identity.
(a ==0 b) = ((a' v b) ^ (b' v a))
Definition	df-id1 50	Define asymmetrical identity (for "Non-Orthomodular Models..." paper).
(a ==1 b) = ((a v b') ^ (a' v (a ^ b)))
Definition	df-id2 51	Define asymmetrical identity (for "Non-Orthomodular Models..." paper).
(a ==2 b) = ((a v b') ^ (b v (a' ^ b')))
Definition	df-id3 52	Define asymmetrical identity (for "Non-Orthomodular Models..." paper).
(a ==3 b) = ((a' v b) ^ (a v (a' ^ b')))
Definition	df-id4 53	Define asymmetrical identity (for "Non-Orthomodular Models..." paper).
(a ==4 b) = ((a' v b) ^ (b' v (a ^ b)))
Definition	df-o3 54	Defined disjunction.
(a u3 b) = (a' ->3 (a' ->3 b))
Definition	df-a3 55	Defined conjunction.
(a ^3 b) = (a' u3 b')'
Definition	df-b3 56	Defined biconditional.
(a <->3 b) = ((a ->3 b) ^ (b ->3 a))
Definition	df-id3oa 57	The 3-variable orthoarguesian identity term.
(a == c ==OA b) = (((a ->1 c) ^ (b ->1 c)) v ((a' ->1 c) ^ (b' ->1 c)))
Definition	df-id4oa 58	The 4-variable orthoarguesian identity term.
(a == c, d ==OA b) = ((a == d ==OA b) v ((a == d ==OA c) ^ (b == d ==OA c)))
Basic lemmas
Theorem	id 59	Identity law.
a = a
Theorem	tt 60	Justification of definition df-t 41 of true (1). This shows that the definition is independent of the variable used to define it.
(a v a') = (b v b')
Theorem	cm 61	Commutative inference rule for ortholattices.
a = b   =>   b = a
Theorem	tr 62	Transitive inference rule for ortholattices.
a = b   &   b = c   =>   a = c
Theorem	3tr1 63	Transitive inference useful for introducing definitions.
a = b   &   c = a   &   d = b   =>   c = d
Theorem	3tr2 64	Transitive inference useful for eliminating definitions.
a = b   &   a = c   &   b = d   =>   c = d
Theorem	3tr 65	Triple transitive inference.
a = b   &   b = c   &   c = d   =>   a = d
Theorem	con1 66	Contraposition inference.
a' = b'   =>   a = b
Theorem	con2 67	Contraposition inference.
a = b'   =>   a' = b
Theorem	con3 68	Contraposition inference.
a' = b   =>   a = b'
Theorem	con4 69	Contraposition inference.
a = b   =>   a' = b'
Theorem	lor 70	Inference introducing disjunct to left.
a = b   =>   (c v a) = (c v b)
Theorem	ror 71	Inference introducing disjunct to right.
a = b   =>   (a v c) = (b v c)
Theorem	2or 72	Join both sides with disjunction.
a = b   &   c = d   =>   (a v c) = (b v d)
Theorem	orcom 73	Commutative law.
(a v b) = (b v a)
Theorem	ancom 74	Commutative law.
(a ^ b) = (b ^ a)
Theorem	orass 75	Associative law.
((a v b) v c) = (a v (b v c))
Theorem	anass 76	Associative law.
((a ^ b) ^ c) = (a ^ (b ^ c))
Theorem	lan 77	Introduce conjunct on left.
a = b   =>   (c ^ a) = (c ^ b)
Theorem	ran 78	Introduce conjunct on right.
a = b   =>   (a ^ c) = (b ^ c)
Theorem	2an 79	Conjoin both sides of hypotheses.
a = b   &   c = d   =>   (a ^ c) = (b ^ d)
Theorem	or12 80	Swap disjuncts.
(a v (b v c)) = (b v (a v c))
Theorem	an12 81	Swap conjuncts.
(a ^ (b ^ c)) = (b ^ (a ^ c))
Theorem	or32 82	Swap disjuncts.
((a v b) v c) = ((a v c) v b)
Theorem	an32 83	Swap conjuncts.
((a ^ b) ^ c) = ((a ^ c) ^ b)
Theorem	or4 84	Swap disjuncts.
((a v b) v (c v d)) = ((a v c) v (b v d))
Theorem	or42 85	Rearrange disjuncts.
((a v b) v (c v d)) = ((a v d) v (b v c))
Theorem	an4 86	Swap conjuncts.
((a ^ b) ^ (c ^ d)) = ((a ^ c) ^ (b ^ d))
Theorem	oran 87	Disjunction expressed with conjunction.
(a v b) = (a' ^ b')'
Theorem	anor1 88	Conjunction expressed with disjunction.
(a ^ b') = (a' v b)'
Theorem	anor2 89	Conjunction expressed with disjunction.
(a' ^ b) = (a v b')'
Theorem	anor3 90	Conjunction expressed with disjunction.
(a' ^ b') = (a v b)'
Theorem	oran1 91	Disjunction expressed with conjunction.
(a v b') = (a' ^ b)'
Theorem	oran2 92	Disjunction expressed with conjunction.
(a' v b) = (a ^ b')'
Theorem	oran3 93	Disjunction expressed with conjunction.
(a' v b') = (a ^ b)'
Theorem	dfb 94	Biconditional expressed with others.
(a == b) = ((a ^ b) v (a' ^ b'))
Theorem	dfnb 95	Negated biconditional.
(a == b)' = ((a v b) ^ (a' v b'))
Theorem	bicom 96	Commutative law.
(a == b) = (b == a)
Theorem	lbi 97	Introduce biconditional to the left.
a = b   =>   (c == a) = (c == b)
Theorem	rbi 98	Introduce biconditional to the right.
a = b   => &n