P. 1 of Theorem List - Quantum Logic Explorer

Theorem List for Quantum Logic Explorer - 1-100   *Has distinct variable group(s)

Type	Label	Description
Statement
0.1  Ortholattices
0.1.1  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, so is a⊥.
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 ∪ b).
term  (a ∪ 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 ∪3 b).
term  (a ∪3 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. (Contributed by NM, 9-Aug-1997.)
a = a⊥ ⊥
Axiom	ax-a2 31	Axiom for ortholattices. (Contributed by NM, 9-Aug-1997.)
(a ∪ b) = (b ∪ a)
Axiom	ax-a3 32	Axiom for ortholattices. (Contributed by NM, 9-Aug-1997.)
((a ∪ b) ∪ c) = (a ∪ (b ∪ c))
Axiom	ax-a4 33	Axiom for ortholattices. (Contributed by NM, 9-Aug-1997.)
(a ∪ (b ∪ b⊥ )) = (b ∪ b⊥ )
Axiom	ax-a5 34	Axiom for ortholattices. (Contributed by NM, 9-Aug-1997.)
(a ∪ (a⊥ ∪ b)⊥ ) = a
Axiom	ax-r1 35	Inference rule for ortholattices. (Contributed by NM, 9-Aug-1997.)
a = b    ⇒   b = a
Axiom	ax-r2 36	Inference rule for ortholattices. (Contributed by NM, 9-Aug-1997.)
a = b    &   b = c    ⇒   a = c
Axiom	ax-r4 37	Inference rule for ortholattices. (Contributed by NM, 9-Aug-1997.)
a = b    ⇒   a⊥ = b⊥
Axiom	ax-r5 38	Inference rule for ortholattices. (Contributed by NM, 9-Aug-1997.)
a = b    ⇒   (a ∪ c) = (b ∪ c)
Definition	df-b 39	Define biconditional. (Contributed by NM, 9-Aug-1997.)
(a ≡ b) = ((a⊥ ∪ b⊥ )⊥ ∪ (a ∪ b)⊥ )
Definition	df-a 40	Define conjunction. (Contributed by NM, 9-Aug-1997.)
(a ∩ b) = (a⊥ ∪ b⊥ )⊥
Definition	df-t 41	Define true. (Contributed by NM, 9-Aug-1997.)
1 = (a ∪ a⊥ )
Definition	df-f 42	Define false. (Contributed by NM, 9-Aug-1997.)
0 = 1⊥
Definition	df-i0 43	Define classical conditional. (Contributed by NM, 31-Oct-1998.)
(a →0 b) = (a⊥ ∪ b)
Definition	df-i1 44	Define Sasaki (Mittelstaedt) conditional. (Contributed by NM, 23-Nov-1997.)
(a →1 b) = (a⊥ ∪ (a ∩ b))
Definition	df-i2 45	Define Dishkant conditional. (Contributed by NM, 23-Nov-1997.)
(a →2 b) = (b ∪ (a⊥ ∩ b⊥ ))
Definition	df-i3 46	Define Kalmbach conditional. (Contributed by NM, 2-Nov-1997.)
(a →3 b) = (((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ (a⊥ ∪ b)))
Definition	df-i4 47	Define non-tollens conditional. (Contributed by NM, 23-Nov-1997.)
(a →4 b) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ ((a⊥ ∪ b) ∩ b⊥ ))
Definition	df-i5 48	Define relevance conditional. (Contributed by NM, 23-Nov-1997.)
(a →5 b) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ ))
Definition	df-id0 49	Define classical identity. (Contributed by NM, 7-Feb-1999.)
(a ≡0 b) = ((a⊥ ∪ b) ∩ (b⊥ ∪ a))
Definition	df-id1 50	Define asymmetrical identity (for "Non-Orthomodular Models..." paper). (Contributed by NM, 7-Feb-1999.)
(a ≡1 b) = ((a ∪ b⊥ ) ∩ (a⊥ ∪ (a ∩ b)))
Definition	df-id2 51	Define asymmetrical identity (for "Non-Orthomodular Models..." paper). (Contributed by NM, 7-Feb-1999.)
(a ≡2 b) = ((a ∪ b⊥ ) ∩ (b ∪ (a⊥ ∩ b⊥ )))
Definition	df-id3 52	Define asymmetrical identity (for "Non-Orthomodular Models..." paper). (Contributed by NM, 7-Feb-1999.)
(a ≡3 b) = ((a⊥ ∪ b) ∩ (a ∪ (a⊥ ∩ b⊥ )))
Definition	df-id4 53	Define asymmetrical identity (for "Non-Orthomodular Models..." paper). (Contributed by NM, 7-Feb-1999.)
(a ≡4 b) = ((a⊥ ∪ b) ∩ (b⊥ ∪ (a ∩ b)))
Definition	df-o3 54	Defined disjunction. (Contributed by NM, 2-Nov-1997.)
(a ∪3 b) = (a⊥ →3 (a⊥ →3 b))
Definition	df-a3 55	Defined conjunction. (Contributed by NM, 2-Nov-1997.)
(a ∩3 b) = (a⊥ ∪3 b⊥ )⊥
Definition	df-b3 56	Defined biconditional. (Contributed by NM, 2-Nov-1997.)
(a ↔3 b) = ((a →3 b) ∩ (b →3 a))
Definition	df-id3oa 57	The 3-variable orthoarguesian identity term. (Contributed by NM, 22-Sep-1998.)
(a ≡ c ≡OA b) = (((a →1 c) ∩ (b →1 c)) ∪ ((a⊥ →1 c) ∩ (b⊥ →1 c)))
Definition	df-id4oa 58	The 4-variable orthoarguesian identity term. (Contributed by NM, 28-Nov-1998.)
(a ≡ c, d ≡OA b) = ((a ≡ d ≡OA b) ∪ ((a ≡ d ≡OA c) ∩ (b ≡ d ≡OA c)))
0.1.2  Basic lemmas
Theorem	id 59	Identity law. (Contributed by NM, 9-Aug-1997.)
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. (Contributed by NM, 9-Aug-1997.)
(a ∪ a⊥ ) = (b ∪ b⊥ )
Theorem	cm 61	Commutative inference rule for ortholattices. (Contributed by NM, 26-May-2008.)
a = b    ⇒   b = a
Theorem	tr 62	Transitive inference rule for ortholattices. (Contributed by NM, 26-May-2008.)
a = b    &   b = c    ⇒   a = c
Theorem	3tr1 63	Transitive inference useful for introducing definitions. (Contributed by NM, 10-Aug-1997.)
a = b    &   c = a    &   d = b    ⇒   c = d
Theorem	3tr2 64	Transitive inference useful for eliminating definitions. (Contributed by NM, 10-Aug-1997.)
a = b    &   a = c    &   b = d    ⇒   c = d
Theorem	3tr 65	Triple transitive inference. (Contributed by NM, 20-Sep-1998.)
a = b    &   b = c    &   c = d    ⇒   a = d
Theorem	con1 66	Contraposition inference. (Contributed by NM, 10-Aug-1997.)
a⊥ = b⊥    ⇒   a = b
Theorem	con2 67	Contraposition inference. (Contributed by NM, 10-Aug-1997.)
a = b⊥    ⇒   a⊥ = b
Theorem	con3 68	Contraposition inference. (Contributed by NM, 10-Aug-1997.)
a⊥ = b    ⇒   a = b⊥
Theorem	con4 69	Contraposition inference. (Contributed by NM, 26-May-2008.) (Revised by NM, 31-Mar-2011.)
a = b    ⇒   a⊥ = b⊥
Theorem	lor 70	Inference introducing disjunct to left. (Contributed by NM, 10-Aug-1997.)
a = b    ⇒   (c ∪ a) = (c ∪ b)
Theorem	ror 71	Inference introducing disjunct to right. (Contributed by NM, 26-May-2008.) (Revised by NM, 31-Mar-2011.)
a = b    ⇒   (a ∪ c) = (b ∪ c)
Theorem	2or 72	Join both sides with disjunction. (Contributed by NM, 10-Aug-1997.)
a = b    &   c = d    ⇒   (a ∪ c) = (b ∪ d)
Theorem	orcom 73	Commutative law. (Contributed by NM, 27-May-2008.) (Revised by NM, 31-Mar-2011.)
(a ∪ b) = (b ∪ a)
Theorem	ancom 74	Commutative law. (Contributed by NM, 10-Aug-1997.)
(a ∩ b) = (b ∩ a)
Theorem	orass 75	Associative law. (Contributed by NM, 27-May-2008.) (Revised by NM, 31-Mar-2011.)
((a ∪ b) ∪ c) = (a ∪ (b ∪ c))
Theorem	anass 76	Associative law. (Contributed by NM, 12-Aug-1997.)
((a ∩ b) ∩ c) = (a ∩ (b ∩ c))
Theorem	lan 77	Introduce conjunct on left. (Contributed by NM, 10-Aug-1997.)
a = b    ⇒   (c ∩ a) = (c ∩ b)
Theorem	ran 78	Introduce conjunct on right. (Contributed by NM, 10-Aug-1997.)
a = b    ⇒   (a ∩ c) = (b ∩ c)
Theorem	2an 79	Conjoin both sides of hypotheses. (Contributed by NM, 10-Aug-1997.)
a = b    &   c = d    ⇒   (a ∩ c) = (b ∩ d)
Theorem	or12 80	Swap disjuncts. (Contributed by NM, 27-Aug-1997.)
(a ∪ (b ∪ c)) = (b ∪ (a ∪ c))
Theorem	an12 81	Swap conjuncts. (Contributed by NM, 27-Aug-1997.)
(a ∩ (b ∩ c)) = (b ∩ (a ∩ c))
Theorem	or32 82	Swap disjuncts. (Contributed by NM, 27-Aug-1997.)
((a ∪ b) ∪ c) = ((a ∪ c) ∪ b)
Theorem	an32 83	Swap conjuncts. (Contributed by NM, 27-Aug-1997.)
((a ∩ b) ∩ c) = ((a ∩ c) ∩ b)
Theorem	or4 84	Swap disjuncts. (Contributed by NM, 27-Aug-1997.)
((a ∪ b) ∪ (c ∪ d)) = ((a ∪ c) ∪ (b ∪ d))
Theorem	or42 85	Rearrange disjuncts. (Contributed by NM, 4-Mar-2006.)
((a ∪ b) ∪ (c ∪ d)) = ((a ∪ d) ∪ (b ∪ c))
Theorem	an4 86	Swap conjuncts. (Contributed by NM, 27-Aug-1997.)
((a ∩ b) ∩ (c ∩ d)) = ((a ∩ c) ∩ (b ∩ d))
Theorem	oran 87	Disjunction expressed with conjunction. (Contributed by NM, 10-Aug-1997.)
(a ∪ b) = (a⊥ ∩ b⊥ )⊥
Theorem	anor1 88	Conjunction expressed with disjunction. (Contributed by NM, 12-Aug-1997.)
(a ∩ b⊥ ) = (a⊥ ∪ b)⊥
Theorem	anor2 89	Conjunction expressed with disjunction. (Contributed by NM, 12-Aug-1997.)
(a⊥ ∩ b) = (a ∪ b⊥ )⊥
Theorem	anor3 90	Conjunction expressed with disjunction. (Contributed by NM, 15-Dec-1997.)
(a⊥ ∩ b⊥ ) = (a ∪ b)⊥
Theorem	oran1 91	Disjunction expressed with conjunction. (Contributed by NM, 15-Dec-1997.)
(a ∪ b⊥ ) = (a⊥ ∩ b)⊥
Theorem	oran2 92	Disjunction expressed with conjunction. (Contributed by NM, 15-Dec-1997.)
(a⊥ ∪ b) = (a ∩ b⊥ )⊥
Theorem	oran3 93	Disjunction expressed with conjunction. (Contributed by NM, 15-Dec-1997.)
(a⊥ ∪ b⊥ ) = (a ∩ b)⊥
Theorem	dfb 94	Biconditional expressed with others. (Contributed by NM, 10-Aug-1997.)
(a ≡ b) = ((a ∩ b) ∪ (a⊥ ∩ b⊥ ))
Theorem	dfnb 95	Negated biconditional. (Contributed by NM, 30-Aug-1997.)
(a ≡ b)⊥ = ((a ∪ b) ∩ (a⊥ ∪ b⊥ ))
Theorem	bicom 96	Commutative law. (Contributed by NM, 10-Aug-1997.)
(a ≡ b) = (b ≡ a)
Theorem	lbi 97	Introduce biconditional to the left. (Contributed by NM, 10-Aug-1997.)
a = b    ⇒   (c ≡ a) = (c ≡ b)
Theorem	rbi 98	Introduce biconditional to the right. (Contributed by NM, 10-Aug-1997.)
a = b    ⇒   (a ≡ c) = (b ≡ c)
Theorem	2bi 99	Join both sides with biconditional. (Contributed by NM, 10-Aug-1997.)
a = b    &   c = d    ⇒   (a ≡ c) = (b ≡ d)
Theorem	dff2 100	Alternate definition of "false". (Contributed by NM, 10-Aug-1997.)
0 = (a ∪ a⊥ )⊥