[Lattice L46-7]Home PageHome Quantum Logic Explorer
Theorem List (p. 1 of 13)
< Previous  Next >
Bad symbols? Try the
GIF 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, ab is a wff.
wff  ab
 
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 (ab).
term  (ab)
 
Syntaxwo 6 If a and b are terms, so is (ab).
term  (ab)
 
Syntaxwa 7 If a and b are terms, so is (ab).
term  (ab)
 
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 (a2 b).
term  (a2 b)
 
Syntaxwi0 11 If a and b are terms, so is (a0 b).
term  (a0 b)
 
Syntaxwi1 12 If a and b are terms, so is (a1 b).
term  (a1 b)
 
Syntaxwi2 13 If a and b are terms, so is (a2 b).
term  (a2 b)
 
Syntaxwi3 14 If a and b are terms, so is (a3 b).
term  (a3 b)
 
Syntaxwi4 15 If a and b are terms, so is (a4 b).
term  (a4 b)
 
Syntaxwi5 16 If a and b are terms, so is (a5 b).
term  (a5 b)
 
Syntaxwid0 17 If a and b are terms, so is (a0 b).
term  (a0 b)
 
Syntaxwid1 18 If a and b are terms, so is (a1 b).
term  (a1 b)
 
Syntaxwid2 19 If a and b are terms, so is (a2 b).
term  (a2 b)
 
Syntaxwid3 20 If a and b are terms, so is (a3 b).
term  (a3 b)
 
Syntaxwid4 21 If a and b are terms, so is (a4 b).
term  (a4 b)
 
Syntaxwid5 22 If a and b are terms, so is (a5 b).
term  (a5 b)
 
Syntaxwb3 23 If a and b are terms, so is (a3 b).
term  (a3 b)
 
Syntaxwb1 24 If a and b are terms, so is (a3 b).
term  (a1 b)
 
Syntaxwo3 25 If a and b are terms, so is (a3 b).
term  (a3 b)
 
Syntaxwan3 26 If a and b are terms, so is (a3 b).
term  (a3 b)
 
Syntaxwid3oa 27 If a, b, and c are terms, so is (acOA b).
term  (acOA b)
 
Syntaxwid4oa 28 If a, b, c, and d are terms, so is (ac, dOA b).
term  (ac, dOA b)
 
Syntaxwcmtr 29 If a and b are terms, so is C (a, b).
term  C (a, b)
 
Axiomax-a1 30 Axiom for ortholattices. (Contributed by NM, 9-Aug-1997.)
a = a
 
Axiomax-a2 31 Axiom for ortholattices. (Contributed by NM, 9-Aug-1997.)
(ab) = (ba)
 
Axiomax-a3 32 Axiom for ortholattices. (Contributed by NM, 9-Aug-1997.)
((ab) ∪ c) = (a ∪ (bc))
 
Axiomax-a4 33 Axiom for ortholattices. (Contributed by NM, 9-Aug-1997.)
(a ∪ (bb )) = (bb )
 
Axiomax-a5 34 Axiom for ortholattices. (Contributed by NM, 9-Aug-1997.)
(a ∪ (ab) ) = a
 
Axiomax-r1 35 Inference rule for ortholattices. (Contributed by NM, 9-Aug-1997.)
a = b       b = a
 
Axiomax-r2 36 Inference rule for ortholattices. (Contributed by NM, 9-Aug-1997.)
a = b    &   b = c       a = c
 
Axiomax-r4 37 Inference rule for ortholattices. (Contributed by NM, 9-Aug-1997.)
a = b       a = b
 
Axiomax-r5 38 Inference rule for ortholattices. (Contributed by NM, 9-Aug-1997.)
a = b       (ac) = (bc)
 
Definitiondf-b 39 Define biconditional. (Contributed by NM, 9-Aug-1997.)
(ab) = ((ab ) ∪ (ab) )
 
Definitiondf-a 40 Define conjunction. (Contributed by NM, 9-Aug-1997.)
(ab) = (ab )
 
Definitiondf-t 41 Define true. (Contributed by NM, 9-Aug-1997.)
1 = (aa )
 
Definitiondf-f 42 Define false. (Contributed by NM, 9-Aug-1997.)
0 = 1
 
Definitiondf-i0 43 Define classical conditional. (Contributed by NM, 31-Oct-1998.)
(a0 b) = (ab)
 
Definitiondf-i1 44 Define Sasaki (Mittelstaedt) conditional. (Contributed by NM, 23-Nov-1997.)
(a1 b) = (a ∪ (ab))
 
Definitiondf-i2 45 Define Dishkant conditional. (Contributed by NM, 23-Nov-1997.)
(a2 b) = (b ∪ (ab ))
 
Definitiondf-i3 46 Define Kalmbach conditional. (Contributed by NM, 2-Nov-1997.)
(a3 b) = (((ab) ∪ (ab )) ∪ (a ∩ (ab)))
 
Definitiondf-i4 47 Define non-tollens conditional. (Contributed by NM, 23-Nov-1997.)
(a4 b) = (((ab) ∪ (ab)) ∪ ((ab) ∩ b ))
 
Definitiondf-i5 48 Define relevance conditional. (Contributed by NM, 23-Nov-1997.)
(a5 b) = (((ab) ∪ (ab)) ∪ (ab ))
 
Definitiondf-id0 49 Define classical identity. (Contributed by NM, 7-Feb-1999.)
(a0 b) = ((ab) ∩ (ba))
 
Definitiondf-id1 50 Define asymmetrical identity (for "Non-Orthomodular Models..." paper). (Contributed by NM, 7-Feb-1999.)
(a1 b) = ((ab ) ∩ (a ∪ (ab)))
 
Definitiondf-id2 51 Define asymmetrical identity (for "Non-Orthomodular Models..." paper). (Contributed by NM, 7-Feb-1999.)
(a2 b) = ((ab ) ∩ (b ∪ (ab )))
 
Definitiondf-id3 52 Define asymmetrical identity (for "Non-Orthomodular Models..." paper). (Contributed by NM, 7-Feb-1999.)
(a3 b) = ((ab) ∩ (a ∪ (ab )))
 
Definitiondf-id4 53 Define asymmetrical identity (for "Non-Orthomodular Models..." paper). (Contributed by NM, 7-Feb-1999.)
(a4 b) = ((ab) ∩ (b ∪ (ab)))
 
Definitiondf-o3 54 Defined disjunction. (Contributed by NM, 2-Nov-1997.)
(a3 b) = (a3 (a3 b))
 
Definitiondf-a3 55 Defined conjunction. (Contributed by NM, 2-Nov-1997.)
(a3 b) = (a3 b )
 
Definitiondf-b3 56 Defined biconditional. (Contributed by NM, 2-Nov-1997.)
(a3 b) = ((a3 b) ∩ (b3 a))
 
Definitiondf-id3oa 57 The 3-variable orthoarguesian identity term. (Contributed by NM, 22-Sep-1998.)
(acOA b) = (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c)))
 
Definitiondf-id4oa 58 The 4-variable orthoarguesian identity term. (Contributed by NM, 28-Nov-1998.)
(ac, dOA b) = ((adOA b) ∪ ((adOA c) ∩ (bdOA c)))
 
0.1.2  Basic lemmas
 
Theoremid 59 Identity law. (Contributed by NM, 9-Aug-1997.)
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. (Contributed by NM, 9-Aug-1997.)
(aa ) = (bb )
 
Theoremcm 61 Commutative inference rule for ortholattices. (Contributed by NM, 26-May-2008.)
a = b       b = a
 
Theoremtr 62 Transitive inference rule for ortholattices. (Contributed by NM, 26-May-2008.)
a = b    &   b = c       a = c
 
Theorem3tr1 63 Transitive inference useful for introducing definitions. (Contributed by NM, 10-Aug-1997.)
a = b    &   c = a    &   d = b       c = d
 
Theorem3tr2 64 Transitive inference useful for eliminating definitions. (Contributed by NM, 10-Aug-1997.)
a = b    &   a = c    &   b = d       c = d
 
Theorem3tr 65 Triple transitive inference. (Contributed by NM, 20-Sep-1998.)
a = b    &   b = c    &   c = d       a = d
 
Theoremcon1 66 Contraposition inference. (Contributed by NM, 10-Aug-1997.)
a = b       a = b
 
Theoremcon2 67 Contraposition inference. (Contributed by NM, 10-Aug-1997.)
a = b       a = b
 
Theoremcon3 68 Contraposition inference. (Contributed by NM, 10-Aug-1997.)
a = b       a = b
 
Theoremcon4 69 Contraposition inference. (Contributed by NM, 26-May-2008.) (Revised by NM, 31-Mar-2011.)
a = b       a = b
 
Theoremlor 70 Inference introducing disjunct to left. (Contributed by NM, 10-Aug-1997.)
a = b       (ca) = (cb)
 
Theoremror 71 Inference introducing disjunct to right. (Contributed by NM, 26-May-2008.) (Revised by NM, 31-Mar-2011.)
a = b       (ac) = (bc)
 
Theorem2or 72 Join both sides with disjunction. (Contributed by NM, 10-Aug-1997.)
a = b    &   c = d       (ac) = (bd)
 
Theoremorcom 73 Commutative law. (Contributed by NM, 27-May-2008.) (Revised by NM, 31-Mar-2011.)
(ab) = (ba)
 
Theoremancom 74 Commutative law. (Contributed by NM, 10-Aug-1997.)
(ab) = (ba)
 
Theoremorass 75 Associative law. (Contributed by NM, 27-May-2008.) (Revised by NM, 31-Mar-2011.)
((ab) ∪ c) = (a ∪ (bc))
 
Theoremanass 76 Associative law. (Contributed by NM, 12-Aug-1997.)
((ab) ∩ c) = (a ∩ (bc))
 
Theoremlan 77 Introduce conjunct on left. (Contributed by NM, 10-Aug-1997.)
a = b       (ca) = (cb)
 
Theoremran 78 Introduce conjunct on right. (Contributed by NM, 10-Aug-1997.)
a = b       (ac) = (bc)
 
Theorem2an 79 Conjoin both sides of hypotheses. (Contributed by NM, 10-Aug-1997.)
a = b    &   c = d       (ac) = (bd)
 
Theoremor12 80 Swap disjuncts. (Contributed by NM, 27-Aug-1997.)
(a ∪ (bc)) = (b ∪ (ac))
 
Theoreman12 81 Swap conjuncts. (Contributed by NM, 27-Aug-1997.)
(a ∩ (bc)) = (b ∩ (ac))
 
Theoremor32 82 Swap disjuncts. (Contributed by NM, 27-Aug-1997.)
((ab) ∪ c) = ((ac) ∪ b)
 
Theoreman32 83 Swap conjuncts. (Contributed by NM, 27-Aug-1997.)
((ab) ∩ c) = ((ac) ∩ b)
 
Theoremor4 84 Swap disjuncts. (Contributed by NM, 27-Aug-1997.)
((ab) ∪ (cd)) = ((ac) ∪ (bd))
 
Theoremor42 85 Rearrange disjuncts. (Contributed by NM, 4-Mar-2006.)
((ab) ∪ (cd)) = ((ad) ∪ (bc))
 
Theoreman4 86 Swap conjuncts. (Contributed by NM, 27-Aug-1997.)
((ab) ∩ (cd)) = ((ac) ∩ (bd))
 
Theoremoran 87 Disjunction expressed with conjunction. (Contributed by NM, 10-Aug-1997.)
(ab) = (ab )
 
Theoremanor1 88 Conjunction expressed with disjunction. (Contributed by NM, 12-Aug-1997.)
(ab ) = (ab)
 
Theoremanor2 89 Conjunction expressed with disjunction. (Contributed by NM, 12-Aug-1997.)
(ab) = (ab )
 
Theoremanor3 90 Conjunction expressed with disjunction. (Contributed by NM, 15-Dec-1997.)
(ab ) = (ab)
 
Theoremoran1 91 Disjunction expressed with conjunction. (Contributed by NM, 15-Dec-1997.)
(ab ) = (ab)
 
Theoremoran2 92 Disjunction expressed with conjunction. (Contributed by NM, 15-Dec-1997.)
(ab) = (ab )
 
Theoremoran3 93 Disjunction expressed with conjunction. (Contributed by NM, 15-Dec-1997.)
(ab ) = (ab)
 
Theoremdfb 94 Biconditional expressed with others. (Contributed by NM, 10-Aug-1997.)
(ab) = ((ab) ∪ (ab ))
 
Theoremdfnb 95 Negated biconditional. (Contributed by NM, 30-Aug-1997.)
(ab) = ((ab) ∩ (ab ))
 
Theorembicom 96 Commutative law. (Contributed by NM, 10-Aug-1997.)
(ab) = (ba)
 
Theoremlbi 97 Introduce biconditional to the left. (Contributed by NM, 10-Aug-1997.)
a = b       (ca) = (cb)
 
Theoremrbi 98 Introduce biconditional to the right. (Contributed by NM, 10-Aug-1997.)
a = b       (ac) = (bc)
 
Theorem2bi 99 Join both sides with biconditional. (Contributed by NM, 10-Aug-1997.)
a = b    &   c = d       (ac) = (bd)
 
Theoremdff2 100 Alternate definition of "false". (Contributed by NM, 10-Aug-1997.)
0 = (aa )
    < 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-1217
  Copyright terms: Public domain < Previous  Next >