Database of mathematics

There are 113 entries in the database, listed below. Of these, 44 are subject to review, while the remaining 69 are finalized. Dependencies for each entry are listed in brackets. Numberings will update as the database expands.

  1. Terminology: Recursive definition
  2. Terminology: Class, statement [1]
  3. Definition: Membership, element [2]
  4. Definition: Conjunction [1] [2]
  5. Definition: Negation [2]
  6. Definition: Disjunction [1] [2] [4] [5]
  7. Definition: Implication [1] [2] [4] [5]
  8. Definition: Equivalence [1] [2] [4] [7]
  9. Definition: Existential quantification [1] [2]
  10. Definition: Universal quantification [1] [2] [5] [9]
  11. Definition: Occurrence of a variable [1] [2] [3] [4] [5] [9]
  12. Proposition: Variable occurrence in disjunctions [2] [4] [5] [6] [11]
  13. Proposition: Variable occurrence in implications [2] [4] [5] [7] [11]
  14. Proposition: Variable occurrence in equivalences [2] [4] [7] [8] [11] [13]
  15. Proposition: Variable occurrence in universal statements [2] [5] [9] [10] [11]
  16. Definition: Free occurrence of a variable [1] [2] [3] [4] [5] [9] [11]
  17. Definition: Bound occurrence of a variable [1] [2] [4] [5] [9] [11]
  18. Definition: Quantified occurrence of a variable [1] [2] [4] [5] [9]
  19. Definition: Freely substitutable variable [1] [2] [3] [4] [5] [9] [16]
  20. Definition: Substatement [1] [2] [4] [5] [9]
  21. Definition: Proper substatement [2] [4] [5] [9] [20]
  22. Definition: Composite statement [2] [4] [5] [9]
  23. Terminology: Structural induction [1]
  24. Proposition: Variable occurrence in iterated conjunctions [2] [4] [11] [23]
  25. Proposition: Variable occurrence in iterated disjunctions [2] [6] [11] [12] [23]
  26. Proposition: Variable occurrence in implication chains [2] [4] [7] [11] [13] [23]
  27. Proposition: Variable occurrence in equivalence chains [2] [4] [8] [11] [14] [23]
  28. Proposition: Variable occurrence in iterated existence statements [2] [9] [11] [23]
  29. Proposition: Variable occurrence in iterated universal statements [2] [10] [11] [15] [23]
  30. Lemma: A variable occurs in a statement precisely if it occurs free, occurs quantified, or both [1] [2] [3] [4] [5] [9] [11] [16] [18] [23]
  31. Corollary: A variable not occurring in a statement does not occur quantified in the statement [2] [11] [16] [18] [30]
  32. Proposition/definition: Variable substitution [1] [2] [3] [4] [5] [9] [23]
  33. Proposition: Variable substitution in iterated conjunctions [2] [4] [23] [32]
  34. Proposition: Variable substitution in disjunctions [2] [4] [5] [6] [32]
  35. Proposition: Variable substitution in iterated disjunctions [2] [6] [23] [32] [34]
  36. Proposition: Variable substitution in implications [2] [4] [5] [7] [32]
  37. Proposition: Variable substitution in implication chains [2] [4] [7] [23] [32] [36]
  38. Proposition: Variable substitution in equivalences [2] [4] [7] [8] [32] [36]
  39. Lemma: A variable is freely substitutable for a variable not occurring quantified in the statement [1] [2] [3] [4] [5] [9] [18] [19] [23]
  40. Corollary: A variable is freely substitutable for a variable not occurring in the statement [2] [2] [11] [11] [18] [19] [19] [31] [39]
  41. Proposition: Variable substitution in equivalence chains [2] [4] [8] [23] [32] [38]
  42. Proposition: Variable substitution in iterated existence statements [2] [9] [23] [32]
  43. Proposition: Variable substitution in universal statements [2] [5] [9] [10] [32]
  44. Proposition: Variable substitution in iterated universal statements [2] [10] [23] [32] [43]
  45. Lemma: Substituting a variable for itself changes nothing [1] [2] [3] [4] [5] [23] [32]
  46. Lemma: Doing the same variable substitution twice is superfluous [1] [2] [3] [4] [5] [9] [23] [32]
  47. Lemma: A variable occurs quantified in a statement precisely if it remains occurring after substitution [1] [2] [3] [4] [5] [9] [11] [18] [23] [32]
  48. Lemma: Only one new variable can occur after a variable substitution [1] [2] [3] [4] [5] [9] [11] [23] [32]
  49. Proposition/definition: Iterated variable substitution [1] [2] [23] [32]
  50. Terminology: Defined type [2] [32]
  51. Terminology: Context, assumption [2]
  52. Terminology: Inference [2] [51]
  53. Terminology: Entailment [2] [51] [52]
  54. Terminology: Inference rule [2] [51] [52] [53]
  55. Inference rule: Conjunction introduction [2] [4] [52] [54]
  56. Proposition: Iterated conjunction introduction [2] [4] [23] [52] [54] [55]
  57. Inference rule: Conjunction elimination [2] [4] [52] [54]
  58. Theorem: The identity rule [2] [4] [51] [52] [53] [54] [55] [57]
  59. Theorem: The weakening rule [2] [4] [52] [53] [54] [55] [57]
  60. Proposition: Iterated conjunction elimination [2] [4] [23] [52] [54] [57]
  61. Proposition: Idempotence of conjunction [2] [4] [52] [54] [55] [57]
  62. Proposition: Commutativity of conjunction [2] [4] [52] [54] [55] [57]
  63. Proposition: Associativity of conjunction [4] [52] [54] [55] [57]
  64. Inference rule: Negation introduction [2] [5] [52] [53] [54]
  65. Theorem: Law of Noncontradiction [2] [4] [5] [52] [53] [54] [57] [64]
  66. Proposition: Statements entailing their own negation [5] [53] [54] [58] [64]
  67. Proposition: Double negation introduction [2] [5] [52] [54] [58] [59] [64]
  68. Proposition: Triple negation elimination [2] [5] [52] [54] [59] [64] [67]
  69. Proposition: Negation of entailment [2] [5] [52] [53] [54] [59] [64]
  70. Proposition: Double negation of entailment [5] [53] [54] [69]
  71. Theorem: Disjunction introduction [4] [5] [6] [53] [54] [57] [59] [64]
  72. Proposition: Iterated disjunction introduction [2] [6] [23] [52] [54] [71]
  73. Theorem: Conditional introduction [4] [5] [7] [51] [53] [54] [57] [59] [64]
  74. Proposition: Reflexivity of implication [7] [53] [54] [58] [73]
  75. Proposition: Implication chain introduction [2] [4] [7] [23] [52] [53] [54] [55] [73]
  76. Proposition: Weakening rule for implication [7] [54] [59] [73]
  77. Theorem: Biconditional introduction [4] [7] [8] [53] [54] [55] [73]
  78. Proposition: Reflexivity of equivalence [8] [53] [54] [58] [77]
  79. Inference rule: Double negation elimination [5] [52] [54]
  80. Theorem: The cut rule [2] [5] [52] [53] [54] [59] [64] [69] [79]
  81. Theorem: The contraction rule [4] [53] [54] [55] [57] [80]
  82. Theorem: The exchange rule [2] [4] [52] [53] [54] [62] [80]
  83. Proposition: Weakening of assumption [4] [53] [54] [57] [80] [82]
  84. Proposition: Transitivity of entailment [53] [54] [80]
  85. Proposition: Double negation elimination for entailment [5] [53] [54] [67] [79] [80]
  86. Proposition: Negation elimination for entailment [5] [53] [54] [69] [85]
  87. Theorem: Negation elimination [5] [53] [54] [59] [69] [79] [85]
  88. Theorem: Disjunction elimination [4] [5] [6] [51] [53] [54] [55] [59] [64] [79]
  89. Theorem: De Morgan’s laws for disjuncted negations and negated conjunctions [4] [5] [6] [51] [53] [54] [55] [57] [59] [64] [71] [79] [88]
  90. Theorem: De Morgan’s laws for conjuncted negations and negated disjunctions [4] [5] [6] [51] [53] [54] [55] [57] [59] [64] [66] [71] [87] [88]
  91. Theorem: Law of Excluded Middle [4] [5] [6] [54] [59] [64] [65] [79] [90]
  92. Proposition: Iterated disjunction elimination [2] [6] [23] [52] [53] [54] [88]
  93. Proposition: Idempotence of disjunction [2] [6] [52] [53] [54] [58] [71] [88]
  94. Proposition: Commutativity of disjunction [2] [6] [52] [53] [54] [71] [88]
  95. Theorem: Disjunctive syllogism [5] [6] [53] [54] [58] [87] [88] [94]
  96. Proposition: Associativity of disjunction [6] [53] [54] [71] [88]
  97. Theorem: Conditional elimination [4] [5] [7] [53] [54] [55] [59] [64] [79]
  98. Proposition: Implication chain elimination [4] [7] [23] [52] [54] [57] [97]
  99. Proposition: Reverse of conditional introduction [7] [53] [54] [97]
  100. Proposition: Transitivity of implication [7] [53] [54] [73] [84] [99]
  101. Definition: Contrapositive of an implication [5] [7]
  102. Proposition: Contraposition of implication [7] [53] [54] [69] [73] [99] [101]
  103. Theorem: Biconditional elimination [4] [7] [8] [53] [54] [57] [62] [99]
  104. Proposition: Symmetry of equivalence [8] [53] [54] [77] [103]
  105. Proposition: Transitivity of equivalence [8] [53] [54] [77] [84] [103]
  106. Proposition: Implication from equivalence [7] [8] [54] [73] [103] [104]
  107. Proposition: If one side of an equivalence holds, then so does the other [8] [53] [54] [80] [103] [104]
  108. Inference rule: Existential introduction [2] [9] [19] [32] [54]
  109. Theorem: Universal elimination [2] [5] [9] [10] [19] [32] [53] [54] [59] [64] [79] [108]
  110. Inference rule: Existential elimination [2] [9] [11] [32] [51] [53] [54]
  111. Theorem: Universal introduction [2] [5] [9] [10] [11] [32] [51] [53] [54] [66] [67] [87] [110]
  112. Theorem: De Morgan’s laws for universally quantified negations and negated existential quantification [2] [5] [9] [10] [11] [19] [32] [40] [51] [53] [54] [64] [66] [87] [108] [109] [110] [111]
  113. Theorem: De Morgan’s laws for existentially quantified negations and negated universal quantification [2] [5] [11] [19] [32] [40] [53] [54] [59] [64] [67] [79] [87] [109] [110] [111]
    \vdots