 Home Quantum Logic ExplorerTheorem 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.
a = a

Axiomax-a2 31 Axiom for ortholattices.
(ab) = (ba)

Axiomax-a3 32 Axiom for ortholattices.
((ab) ∪ c) = (a ∪ (bc))

Axiomax-a4 33 Axiom for ortholattices.
(a ∪ (bb )) = (bb )

Axiomax-a5 34 Axiom for ortholattices.
(a ∪ (ab) ) = 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       (ac) = (bc)

Definitiondf-b 39 Define biconditional.
(ab) = ((ab ) ∪ (ab) )

Definitiondf-a 40 Define conjunction.
(ab) = (ab )

Definitiondf-t 41 Define true.
1 = (aa )

Definitiondf-f 42 Define false.
0 = 1

Definitiondf-i0 43 Define classical conditional.
(a0 b) = (ab)

Definitiondf-i1 44 Define Sasaki (Mittelstaedt) conditional.
(a1 b) = (a ∪ (ab))

Definitiondf-i2 45 Define Dishkant conditional.
(a2 b) = (b ∪ (ab ))

Definitiondf-i3 46 Define Kalmbach conditional.
(a3 b) = (((ab) ∪ (ab )) ∪ (a ∩ (ab)))

Definitiondf-i4 47 Define non-tollens conditional.
(a4 b) = (((ab) ∪ (ab)) ∪ ((ab) ∩ b ))

Definitiondf-i5 48 Define relevance conditional.
(a5 b) = (((ab) ∪ (ab)) ∪ (ab ))

Definitiondf-id0 49 Define classical identity.
(a0 b) = ((ab) ∩ (ba))

Definitiondf-id1 50 Define asymmetrical identity (for "Non-Orthomodular Models..." paper).
(a1 b) = ((ab ) ∩ (a ∪ (ab)))

Definitiondf-id2 51 Define asymmetrical identity (for "Non-Orthomodular Models..." paper).
(a2 b) = ((ab ) ∩ (b ∪ (ab )))

Definitiondf-id3 52 Define asymmetrical identity (for "Non-Orthomodular Models..." paper).
(a3 b) = ((ab) ∩ (a ∪ (ab )))

Definitiondf-id4 53 Define asymmetrical identity (for "Non-Orthomodular Models..." paper).
(a4 b) = ((ab) ∩ (b ∪ (ab)))

Definitiondf-o3 54 Defined disjunction.
(a3 b) = (a3 (a3 b))

Definitiondf-a3 55 Defined conjunction.
(a3 b) = (a3 b )

Definitiondf-b3 56 Defined biconditional.
(a3 b) = ((a3 b) ∩ (b3 a))

Definitiondf-id3oa 57 The 3-variable orthoarguesian identity term.
(acOA b) = (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c)))

Definitiondf-id4oa 58 The 4-variable orthoarguesian identity term.
(ac, dOA b) = ((adOA b) ∪ ((adOA c) ∩ (bdOA 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.
(aa ) = (bb )

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       (ca) = (cb)

Theoremror 71 Inference introducing disjunct to right.
a = b       (ac) = (bc)

Theorem2or 72 Join both sides with disjunction.
a = b    &   c = d       (ac) = (bd)

Theoremorcom 73 Commutative law.
(ab) = (ba)

Theoremancom 74 Commutative law.
(ab) = (ba)

Theoremorass 75 Associative law.
((ab) ∪ c) = (a ∪ (bc))

Theoremanass 76 Associative law.
((ab) ∩ c) = (a ∩ (bc))

Theoremlan 77 Introduce conjunct on left.
a = b       (ca) = (cb)

Theoremran 78 Introduce conjunct on right.
a = b       (ac) = (bc)

Theorem2an 79 Conjoin both sides of hypotheses.
a = b    &   c = d       (ac) = (bd)

Theoremor12 80 Swap disjuncts.
(a ∪ (bc)) = (b ∪ (ac))

Theoreman12 81 Swap conjuncts.
(a ∩ (bc)) = (b ∩ (ac))

Theoremor32 82 Swap disjuncts.
((ab) ∪ c) = ((ac) ∪ b)

Theoreman32 83 Swap conjuncts.
((ab) ∩ c) = ((ac) ∩ b)

Theoremor4 84 Swap disjuncts.
((ab) ∪ (cd)) = ((ac) ∪ (bd))

Theoremor42 85 Rearrange disjuncts.
((ab) ∪ (cd)) = ((ad) ∪ (bc))

Theoreman4 86 Swap conjuncts.
((ab) ∩ (cd)) = ((ac) ∩ (bd))

Theoremoran 87 Disjunction expressed with conjunction.
(ab) = (ab )

Theoremanor1 88 Conjunction expressed with disjunction.
(ab ) = (ab)

Theoremanor2 89 Conjunction expressed with disjunction.
(ab) = (ab )

Theoremanor3 90 Conjunction expressed with disjunction.
(ab ) = (ab)

Theoremoran1 91 Disjunction expressed with conjunction.
(ab ) = (ab)

Theoremoran2 92 Disjunction expressed with conjunction.
(ab) = (ab )

Theoremoran3 93 Disjunction expressed with conjunction.
(ab ) = (ab)

Theoremdfb 94 Biconditional expressed with others.
(ab) = ((ab) ∪ (ab ))

Theoremdfnb 95 Negated biconditional.
(ab) = ((ab) ∩ (ab ))

Theorembicom 96 Commutative law.
(ab) = (ba)

Theoremlbi 97 Introduce biconditional to the left.
a = b       (ca) = (cb)

Theoremrbi 98 Introduce biconditional to the right.
a = b       (ac) = (bc)

Theorem2bi 99 Join both sides with biconditional.
a = b    &   c = d       (ac) = (bd)

Theoremdff2 100 Alternate defintion of "false".
0 = (aa )

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 >