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

Table of Contents

Ortholattices
    Basic lemmas   id 59
    Relationship analogues (ordering; commutation)   df-le 123
    Commutator (ortholattice theorems)   cmtrcom 184
    Weak "orthomodular law" in ortholattices.   wa1 185
    Kalmbach axioms (soundness proofs) that are true in all ortholattices   sklem 224
Weakly orthomodular lattices
    Weak orthomodular law   ax-wom 347
    Weakly orthomodular lattices   wom3 353
    Relationship analogues (ordering; commutation) in WOML   wleoa 362
    Kalmbach axioms (soundness proofs) that require WOML   ska2 418
    Weak orthomodular law variants   woml6 422
Orthomodular lattices
    Orthomodular law   ax-r3 425
    Relationship analogues using OML (ordering; commutation)   oml2 437
    Commutator (orthomodular lattice theorems)   cmtr1com 479
    Kalmbach conditional   i3bi 482
    Unified disjunction   ud1lem1 546
    Lemmas for unified implication study   u1lemaa 586
    Some proofs contributed by Josiah Burroughs   u1lemn1b 716
    More lemmas for unified implication   u1lem1 720
    Some 3-variable theorems   3vth1 790
    OML Lemmas for studying Godowski equations.   govar 882
    OML Lemmas for studying orthoarguesian laws   oas 911
    5OA law   oa8todual 957
    "Godowski/Greechie" form of proper 4-OA   oa4to4u 959
    Some 3-OA inferences (derived under OM)   oa3-2lema 964
Derivation of 4-variable proper OA from OA distributive law
Orthoarguesian laws
    3-variable orthoarguesian law   ax-3oa 984
    4-variable orthoarguesian law   ax-oal4 1012
    6-variable orthoarguesian law   ax-oa6 1015
    The proper 4-variable orthoarguesian law   ax-4oa 1018
Other stronger-than-OML laws
    New state-related equation   ax-newstateeq 1030
Contributions of Roy Longton
    Roy's first section   lem3.3.2 1031
    Roy's second section   lem3.4.1 1060
    Roy's third section   lem4.6.2e1 1065
Weakly distributive ortholattices (WDOL)
    WDOL law   ax-wdol 1087

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

Type	Label	Description
Statement
Ortholattices
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	3tr1 61	Transitive inference useful for introducing definitions.
a = b   &   c = a   &   d = b   =>   c = d
Theorem	3tr2 62	Transitive inference useful for eliminating definitions.
a = b   &   a = c   &   b = d   =>   c = d
Theorem	3tr 63	Triple transitive inference.
a = b   &   b = c   &   c = d   =>   a = d
Theorem	con1 64	Contraposition inference.
a' = b'   =>   a = b
Theorem	con2 65	Contraposition inference.
a = b'   =>   a' = b
Theorem	con3 66	Contraposition inference.
a' = b   =>   a = b'
Theorem	lor 67	Inference introducing disjunct to left.
a = b   =>   (c v a) = (c v b)
Theorem	2or 68	Join both sides with disjunction.
a = b   &   c = d   =>   (a v c) = (b v d)
Theorem	ancom 69	Commutative law.
(a ^ b) = (b ^ a)
Theorem	anass 70	Associative law.
((a ^ b) ^ c) = (a ^ (b ^ c))
Theorem	lan 71	Introduce conjunct on left.
a = b   =>   (c ^ a) = (c ^ b)
Theorem	ran 72	Introduce conjunct on right.
a = b   =>   (a ^ c) = (b ^ c)
Theorem	2an 73	Conjoin both sides of hypotheses.
a = b   &   c = d   =>   (a ^ c) = (b ^ d)
Theorem	or12 74	Swap disjuncts.
(a v (b v c)) = (b v (a v c))
Theorem	an12 75	Swap conjuncts.
(a ^ (b ^ c)) = (b ^ (a ^ c))
Theorem	or32 76	Swap disjuncts.
((a v b) v c) = ((a v c) v b)
Theorem	an32 77	Swap conjuncts.
((a ^ b) ^ c) = ((a ^ c) ^ b)
Theorem	or4 78	Swap disjuncts.
((a v b) v (c v d)) = ((a v c) v (b v d))
Theorem	or42 79	Rearrange disjuncts.
((a v b) v (c v d)) = ((a v d) v (b v c))
Theorem	an4 80	Swap conjuncts.
((a ^ b) ^ (c ^ d)) = ((a ^ c) ^ (b ^ d))
Theorem	oran 81	Disjunction expressed with conjunction.
(a v b) = (a' ^ b')'
Theorem	anor1 82	Conjunction expressed with disjunction.
(a ^ b') = (a' v b)'
Theorem	anor2 83	Conjunction expressed with disjunction.
(a' ^ b) = (a v b')'
Theorem	anor3 84	Conjunction expressed with disjunction.
(a' ^ b') = (a v b)'
Theorem	oran1 85	Disjunction expressed with conjunction.
(a v b') = (a' ^ b)'
Theorem	oran2 86	Disjunction expressed with conjunction.
(a' v b) = (a ^ b')'
Theorem	oran3 87	Disjunction expressed with conjunction.
(a' v b') = (a ^ b)'
Theorem	dfb 88	Biconditional expressed with others.
(a == b) = ((a ^ b) v (a' ^ b'))
Theorem	dfnb 89	Negated biconditional.
(a == b)' = ((a v b) ^ (a' v b'))
Theorem	bicom 90	Commutative law.
(a == b) = (b == a)
Theorem	lbi 91	Introduce biconditional to the left.
a = b   =>   (c == a) = (c == b)
Theorem	rbi 92	Introduce biconditional to the right.
a = b   =>   (a == c) = (b == c)
Theorem	2bi 93	Join both sides with biconditional.
a = b   &   c = d   =>   (a == c) = (b == d)
Theorem	dff2 94	Alternate defintion of "false".
0 = (a v a')'
Theorem	dff 95	Alternate defintion of "false".
0 = (a ^ a')
Theorem	or0 96	Disjunction with 0.
(a v 0) = a
Theorem	or0r 97	Disjunction with 0.
(0 v a) = a
Theorem	or1 98	Disjunction with 1.
(a v 1) = 1
Theorem	or1r 99	Disjunction with 1.
(1 v a) = 1