Quantum Logic Explorer - mmtheorems

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 - 1-100 - Page 1 of 11

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