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 v b).
term (a v 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 u3 b).
term (a u3 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 v b) = (b v a)
Axiom	ax-a3 31	Axiom for ortholattices.
((a v b) v c) = (a v (b v c))
Axiom	ax-a4 32	Axiom for ortholattices.
(a v (b v b_|_)) = (b v b_|_)
Axiom	ax-a5 33	Axiom for ortholattices.
(a v (a_|_ v 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 v c) = (b v c)
Definition	df-b 38	Define biconditional.
(a == b) = ((a_|_ v b_|_)_|_ v (a v b)_|_)
Definition	df-a 39	Define conjunction.
(a ^ b) = (a_|_ v b_|_)_|_
Definition	df-t 40	Define true.
1 = (a v a_|_)
Definition	df-f 41	Define false.
0 = 1_|_
Definition	df-i0 42	Define classical conditional.
(a ->0 b) = (a_|_ v b)
Definition	df-i1 43	Define Sasaki (Mittelstaedt) conditional.
(a ->1 b) = (a_|_ v (a ^ b))
Definition	df-i2 44	Define Dishkant conditional.
(a ->2 b) = (b v (a_|_ ^ b_|_))
Definition	df-i3 45	Define Kalmbach conditional.
(a ->3 b) = (((a_|_ ^ b) v (a_|_ ^ b_|_)) v (a ^ (a_|_ v b)))
Definition	df-i4 46	Define non-tollens conditional.
(a ->4 b) = (((a ^ b) v (a_|_ ^ b)) v ((a_|_ v b) ^ b_|_))
Definition	df-i5 47	Define relevance conditional.
(a ->5 b) = (((a ^ b) v (a_|_ ^ b)) v (a_|_ ^ b_|_))
Definition	df-id0 48	Define classical identity.
(a ==0 b) = ((a_|_ v b) ^ (b_|_ v a))
Definition	df-id1 49	Define asymmetrical identity (for "Non-Orthomodular Models..." paper).
(a ==1 b) = ((a v b_|_) ^ (a_|_ v (a ^ b)))
Definition	df-id2 50	Define asymmetrical identity (for "Non-Orthomodular Models..." paper).
(a ==2 b) = ((a v b_|_) ^ (b v (a_|_ ^ b_|_)))
Definition	df-id3 51	Define asymmetrical identity (for "Non-Orthomodular Models..." paper).
(a ==3 b) = ((a_|_ v b) ^ (a v (a_|_ ^ b_|_)))
Definition	df-id4 52	Define asymmetrical identity (for "Non-Orthomodular Models..." paper).
(a ==4 b) = ((a_|_ v b) ^ (b_|_ v (a ^ b)))
Definition	df-o3 53	Defined disjunction.
(a u3 b) = (a_|_ ->3 (a_|_ ->3 b))
Definition	df-a3 54	Defined conjunction.
(a ^3 b) = (a_|_ u3 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)) v ((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) v ((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 v a_|_) = (b v 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 v a) = (c v b)
Theorem	2or 67	Join both sides with disjunction.
a = b   &   c = d   =>   (a v c) = (b v 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 v (b v c)) = (b v (a v c))
Theorem	an12 74	Swap conjuncts.
(a ^ (b ^ c)) = (b ^ (a ^ c))
Theorem	or32 75	Swap disjuncts.
((a v b) v c) = ((a v c) v b)
Theorem	an32 76	Swap conjuncts.
((a ^ b) ^ c) = ((a ^ c) ^ b)
Theorem	or4 77	Swap disjuncts.
((a v b) v (c v d)) = ((a v c) v (b v d))
Theorem	an4 78	Swap conjuncts.
((a ^ b) ^ (c ^ d)) = ((a ^ c) ^ (b ^ d))
Theorem	oran 79	Disjunction expressed with conjunction.
(a v b) = (a_|_ ^ b_|_)_|_
Theorem	anor1 80	Conjunction expressed with disjunction.
(a ^ b_|_) = (a_|_ v b)_|_
Theorem	anor2 81	Conjunction expressed with disjunction.
(a_|_ ^ b) = (a v b_|_)_|_
Theorem	anor3 82	Conjunction expressed with disjunction.
(a_|_ ^ b_|_) = (a v b)_|_
Theorem	oran1 83	Disjunction expressed with conjunction.
(a v b_|_) = (a_|_ ^ b)_|_
Theorem	oran2 84	Disjunction expressed with conjunction.
(a_|_ v b) = (a ^ b_|_)_|_
Theorem	oran3 85	Disjunction expressed with conjunction.
(a_|_ v b_|_) = (a ^ b)_|_
Theorem	dfb 86	Biconditional expressed with others.
(a == b) = ((a ^ b) v (a_|_ ^ b_|_))
Theorem	dfnb 87	Negated biconditional.
(a == b)_|_ = ((a v b) ^ (a_|_ v 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 v a_|_)_|_
Theorem	dff 93	Alternate defintion of "false".
0 = (a ^ a_|_)
Theorem	or0 94	Disjunction with 0.
(a v 0) = a
Theorem	or0r 95	Disjunction with 0.
(0 v a) = a
Theorem	or1 96	Disjunction with 1.
(a v 1) = 1
Theorem	or1r 97	Disjunction with 1.
(1 v 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