[Lattice L46-7]Home PageHome Quantum Logic Explorer
Theorem List (p. 1 of 13) 		< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  QLE Home Page  >  Theorem List Contents       This page: Page List

Theorem List for Quantum Logic Explorer - 1-100   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
0.1  Ortholattices
 
0.1.1  Basic syntax and axioms
 
Syntaxwb 1 If a and b are terms, a = b is a wff.
wff a = b
 
Syntaxwle 2 If a and b are terms, a =< b is a wff.
wff a =< b
 
Syntaxwc 3 If a and b are terms, a C b is a wff.
wff a C b
 
Syntaxwn 4 If a is a term, so is a'.
term a'
 
Syntaxtb 5 If a and b are terms, so is (a == b).
term (a == b)
 
Syntaxwo 6 If a and b are terms, so is (a v b).
term (a v b)
 
Syntaxwa 7 If a and b are terms, so is (a ^ b).
term (a ^ b)
 
Syntaxwt 8 The logical true constant is a term.
term 1
 
Syntaxwf 9 The logical false constant is a term.
term 0
 
Syntaxwle2 10 If a and b are terms, so is (a =<2 b).
term (a =<2 b)
 
Syntaxwi0 11 If a and b are terms, so is (a ->0 b).
term (a ->0 b)
 
Syntaxwi1 12 If a and b are terms, so is (a ->1 b).
term (a ->1 b)
 
Syntaxwi2 13 If a and b are terms, so is (a ->2 b).
term (a ->2 b)
 
Syntaxwi3 14 If a and b are terms, so is (a ->3 b).
term (a ->3 b)
 
Syntaxwi4 15 If a and b are terms, so is (a ->4 b).
term (a ->4 b)
 
Syntaxwi5 16 If a and b are terms, so is (a ->5 b).
term (a ->5 b)
 
Syntaxwid0 17 If a and b are terms, so is (a ==0 b).
term (a ==0 b)
 
Syntaxwid1 18 If a and b are terms, so is (a ==1 b).
term (a ==1 b)
 
Syntaxwid2 19 If a and b are terms, so is (a ==2 b).
term (a ==2 b)
 
Syntaxwid3 20 If a and b are terms, so is (a ==3 b).
term (a ==3 b)
 
Syntaxwid4 21 If a and b are terms, so is (a ==4 b).
term (a ==4 b)
 
Syntaxwid5 22 If a and b are terms, so is (a ==5 b).
term (a ==5 b)
 
Syntaxwb3 23 If a and b are terms, so is (a <->3 b).
term (a <->3 b)
 
Syntaxwb1 24 If a and b are terms, so is (a <->3 b).
term (a <->1 b)
 
Syntaxwo3 25 If a and b are terms, so is (a u3 b).
term (a u3 b)
 
Syntaxwan3 26 If a and b are terms, so is (a ^3 b).
term (a ^3 b)
 
Syntaxwid3oa 27 If a, b, and c are terms, so is (a == c ==OA b).
term (a == c ==OA b)
 
Syntaxwid4oa 28 If a, b, c, and d are terms, so is (a == c, d ==OA b).
term (a == c, d ==OA b)
 
Syntaxwcmtr 29 If a and b are terms, so is C (a, b).
term C (a, b)
 
Axiomax-a1 30 Axiom for ortholattices.
a = a''
 
Axiomax-a2 31 Axiom for ortholattices.
(a v b) = (b v a)
 
Axiomax-a3 32 Axiom for ortholattices.
((a v b) v c) = (a v (b v c))
 
Axiomax-a4 33 Axiom for ortholattices.
(a v (b v b')) = (b v b')
 
Axiomax-a5 34 Axiom for ortholattices.
(a v (a' v b)') = a
 
Axiomax-r1 35 Inference rule for ortholattices.
a = b   =>   b = a
 
Axiomax-r2 36 Inference rule for ortholattices.
a = b   &   b = c   =>   a = c
 
Axiomax-r4 37 Inference rule for ortholattices.
a = b   =>   a' = b'
 
Axiomax-r5 38 Inference rule for ortholattices.
a = b   =>   (a v c) = (b v c)
 
Definitiondf-b 39 Define biconditional.
(a == b) = ((a' v b')' v (a v b)')
 
Definitiondf-a 40 Define conjunction.
(a ^ b) = (a' v b')'
 
Definitiondf-t 41 Define true.
1 = (a v a')
 
Definitiondf-f 42 Define false.
0 = 1'
 
Definitiondf-i0 43 Define classical conditional.
(a ->0 b) = (a' v b)
 
Definitiondf-i1 44 Define Sasaki (Mittelstaedt) conditional.
(a ->1 b) = (a' v (a ^ b))
 
Definitiondf-i2 45 Define Dishkant conditional.
(a ->2 b) = (b v (a' ^ b'))
 
Definitiondf-i3 46 Define Kalmbach conditional.
(a ->3 b) = (((a' ^ b) v (a' ^ b')) v (a ^ (a' v b)))
 
Definitiondf-i4 47 Define non-tollens conditional.
(a ->4 b) = (((a ^ b) v (a' ^ b)) v ((a' v b) ^ b'))
 
Definitiondf-i5 48 Define relevance conditional.
(a ->5 b) = (((a ^ b) v (a' ^ b)) v (a' ^ b'))
 
Definitiondf-id0 49 Define classical identity.
(a ==0 b) = ((a' v b) ^ (b' v a))
 
Definitiondf-id1 50 Define asymmetrical identity (for "Non-Orthomodular Models..." paper).
(a ==1 b) = ((a v b') ^ (a' v (a ^ b)))
 
Definitiondf-id2 51 Define asymmetrical identity (for "Non-Orthomodular Models..." paper).
(a ==2 b) = ((a v b') ^ (b v (a' ^ b')))
 
Definitiondf-id3 52 Define asymmetrical identity (for "Non-Orthomodular Models..." paper).
(a ==3 b) = ((a' v b) ^ (a v (a' ^ b')))
 
Definitiondf-id4 53 Define asymmetrical identity (for "Non-Orthomodular Models..." paper).
(a ==4 b) = ((a' v b) ^ (b' v (a ^ b)))
 
Definitiondf-o3 54 Defined disjunction.
(a u3 b) = (a' ->3 (a' ->3 b))
 
Definitiondf-a3 55 Defined conjunction.
(a ^3 b) = (a' u3 b')'
 
Definitiondf-b3 56 Defined biconditional.
(a <->3 b) = ((a ->3 b) ^ (b ->3 a))
 
Definitiondf-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)))
 
Definitiondf-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)))
 
0.1.2  Basic lemmas
 
Theoremid 59 Identity law.
a = a
 
Theoremtt 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')
 
Theoremcm 61 Commutative inference rule for ortholattices.
a = b   =>   b = a
 
Theoremtr 62 Transitive inference rule for ortholattices.
a = b   &   b = c   =>   a = c
 
Theorem3tr1 63 Transitive inference useful for introducing definitions.
a = b   &   c = a   &   d = b   =>   c = d
 
Theorem3tr2 64 Transitive inference useful for eliminating definitions.
a = b   &   a = c   &   b = d   =>   c = d
 
Theorem3tr 65 Triple transitive inference.
a = b   &   b = c   &   c = d   =>   a = d
 
Theoremcon1 66 Contraposition inference.
a' = b'   =>   a = b
 
Theoremcon2 67 Contraposition inference.
a = b'   =>   a' = b
 
Theoremcon3 68 Contraposition inference.
a' = b   =>   a = b'
 
Theoremcon4 69 Contraposition inference.
a = b   =>   a' = b'
 
Theoremlor 70 Inference introducing disjunct to left.
a = b   =>   (c v a) = (c v b)
 
Theoremror 71 Inference introducing disjunct to right.
a = b   =>   (a v c) = (b v c)
 
Theorem2or 72 Join both sides with disjunction.
a = b   &   c = d   =>   (a v c) = (b v d)
 
Theoremorcom 73 Commutative law.
(a v b) = (b v a)
 
Theoremancom 74 Commutative law.
(a ^ b) = (b ^ a)
 
Theoremorass 75 Associative law.
((a v b) v c) = (a v (b v c))
 
Theoremanass 76 Associative law.
((a ^ b) ^ c) = (a ^ (b ^ c))
 
Theoremlan 77 Introduce conjunct on left.
a = b   =>   (c ^ a) = (c ^ b)
 
Theoremran 78 Introduce conjunct on right.
a = b   =>   (a ^ c) = (b ^ c)
 
Theorem2an 79 Conjoin both sides of hypotheses.
a = b   &   c = d   =>   (a ^ c) = (b ^ d)
 
Theoremor12 80 Swap disjuncts.
(a v (b v c)) = (b v (a v c))
 
Theoreman12 81 Swap conjuncts.
(a ^ (b ^ c)) = (b ^ (a ^ c))
 
Theoremor32 82 Swap disjuncts.
((a v b) v c) = ((a v c) v b)
 
Theoreman32 83 Swap conjuncts.
((a ^ b) ^ c) = ((a ^ c) ^ b)
 
Theoremor4 84 Swap disjuncts.
((a v b) v (c v d)) = ((a v c) v (b v d))
 
Theoremor42 85 Rearrange disjuncts.
((a v b) v (c v d)) = ((a v d) v (b v c))
 
Theoreman4 86 Swap conjuncts.
((a ^ b) ^ (c ^ d)) = ((a ^ c) ^ (b ^ d))
 
Theoremoran 87 Disjunction expressed with conjunction.
(a v b) = (a' ^ b')'
 
Theoremanor1 88 Conjunction expressed with disjunction.
(a ^ b') = (a' v b)'
 
Theoremanor2 89 Conjunction expressed with disjunction.
(a' ^ b) = (a v b')'
 
Theoremanor3 90 Conjunction expressed with disjunction.
(a' ^ b') = (a v b)'
 
Theoremoran1 91 Disjunction expressed with conjunction.
(a v b') = (a' ^ b)'
 
Theoremoran2 92 Disjunction expressed with conjunction.
(a' v b) = (a ^ b')'
 
Theoremoran3 93 Disjunction expressed with conjunction.
(a' v b') = (a ^ b)'
 
Theoremdfb 94 Biconditional expressed with others.
(a == b) = ((a ^ b) v (a' ^ b'))
 
Theoremdfnb 95 Negated biconditional.
(a == b)' = ((a v b) ^ (a' v b'))
 
Theorembicom 96 Commutative law.
(a == b) = (b == a)
 
Theoremlbi 97 Introduce biconditional to the left.
a = b   =>   (c == a) = (c == b)
 
Theoremrbi 98 Introduce biconditional to the right.
a = b   =>   (a == c) = (b == c)
 
Theorem2bi 99 Join both sides with biconditional.
a = b   &   c = d   =>   (a == c) = (b == d)
 
Theoremdff2 100 Alternate defintion of "false".
0 = (a v a')'
    < Previous  Next >
Page List
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-1200 13 1201-1215
  Copyright terms: Public domain < Previous  Next >