Database

There are 68 entries in the database, listed below. Dependencies for each entry are listed in brackets. Numberings update automatically as the database is expanded. If an entry is colored orange, this means its contents is tentative and under review.

  1. Terminology: Class, membership
  2. Terminology: Recursion, structural induction
  3. Terminology: Statement [1] [2]
  4. Definition: Conjunction [2] [3]
  5. Definition: Negation [3]
  6. Definition: Disjunction [2] [3] [4] [5]
  7. Definition: Implication [2] [3] [4] [5]
  8. Definition: Equivalence [2] [3] [4] [7]
  9. Definition: Existential quantification [1] [2] [3]
  10. Definition: Bounded existence statement [1] [3] [4] [9]
  11. Definition: Universal quantification [1] [2] [3] [5] [9]
  12. Definition: Bounded universal statement [1] [3] [4] [7] [11]

  13. Definition: Occurrence of a variable [1] [2] [3] [4] [5] [9]
  14. Proposition: Variable occurrence in generalized conjunctions [1] [2] [3] [4] [13]
  15. Proposition: Variable occurrence in disjunctions [1] [3] [4] [5] [6] [13]
  16. Proposition: Variable occurrence in implications [1] [3] [4] [5] [7] [13]
  17. Proposition: Variable occurrence in equivalences [1] [3] [4] [7] [8] [13] [16]
  18. Proposition: Variable occurrence in generalized existence statements [1] [2] [3] [9] [13]
  19. Proposition: Variable occurrence in universal statements [1] [3] [5] [9] [11] [13]
  20. Proposition: Variable occurrence in generalized universal statements [1] [2] [3] [11] [13] [19]

  21. Definition: Free occurrence of a variable [1] [2] [3] [4] [5] [9] [13]

  22. Proposition/definition: Variable substitution [1] [2] [3] [4] [5] [9]
  23. Proposition: Variable substitution in disjunctions [1] [3] [4] [5] [6] [22]
  24. Proposition: Variable substitution in implications [1] [3] [4] [5] [7] [22]
  25. Proposition: Variable substitution in equivalences [1] [3] [4] [7] [8] [22] [24]
  26. Proposition: Variable substitution in universal statements [1] [3] [5] [9] [11] [22]

  27. Definition: Simple multiple variable substitution [2] [22]
  28. Definition: Multiple variable substitution [1] [3] [27]
  29. Terminology: Predicate [1] [3] [21] [28]
  30. Definition: Unary predicate [29]
  31. Definition: Set, proper class [1] [9] [30]
  32. Definition: Binary predicate [1] [29]
  33. Definition: Membership predicate [1] [29] [32]
  34. Definition: Conjunction of binary predicates [2] [4] [32]
  35. Definition: Negation of binary predicates [29] [32]
  36. Proposition/definition: Reverse binary predicate [29] [32]
  37. Definition: Equality, distinctness [1] [3] [5] [8] [12] [31] [32] [35]

  38. Terminology: Inference, entailment [3]
  39. Terminology: Inference rule [3] [38]
  40. Inference rule: Conjunction introduction [4] [38] [39]
  41. Proposition: Generalized conjunction introduction [2] [3] [4] [38] [39] [40]
  42. Inference rule: Conjunction elimination [4] [38] [39]
  43. Proposition: Generalized conjunction elimination [2] [3] [4] [38] [39] [42]
  44. Proposition: Idempotence of conjunction [4] [38] [39] [40] [42]
  45. Proposition: Commutativity of conjunction [4] [38] [39] [40] [42]
  46. Proposition: Associativity of conjunction [4] [38] [39] [40] [42]
  47. Theorem: The weakening rule [4] [38] [39] [40] [42]
  48. Theorem: The identity rule [3] [4] [38] [39] [40] [42]

  49. Inference rule: Negation introduction [5] [38] [39]
  50. Theorem: Law of Noncontradiction [4] [5] [38] [39] [42] [49]
  51. Proposition: Negation of entailment [5] [38] [39] [47] [49]
  52. Proposition: Statements entailing their own negation [5] [38] [39] [48] [49]
  53. Proposition: Double negation introduction [5] [38] [39] [47] [48] [49]
  54. Proposition: Double negation of entailment [5] [38] [39] [51]
  55. Proposition: Triple negation elimination [5] [38] [39] [47] [49] [53]

  56. Inference rule: Double negation elimination [5] [38] [39]
  57. Theorem: The cut rule [5] [38] [39] [47] [49] [51] [56]
  58. Theorem: The exchange rule [4] [38] [39] [45] [57]
  59. Theorem: The contraction rule [4] [38] [39] [40] [42] [57]
  60. Proposition: Weakening of assumption [4] [38] [39] [42] [57] [58]
  61. Proposition: Transitivity of entailment [38] [39] [57]
  62. Proposition: Double negation elimination for entailment [5] [38] [39] [53] [56] [57]
  63. Theorem: Negation elimination [5] [38] [39] [47] [51] [56] [62]
  64. Proposition: Negation elimination for entailment [5] [38] [39] [51] [62]

  65. Terminology: Axiom [3] [38]
  66. Axiom of Extensionality [1] [7] [11] [12] [31] [37] [65]
  67. Axiom of Pairing [6] [8] [10] [12] [31] [37] [65]
  68. Axiom of Difference [1] [4] [8] [9] [11] [12] [31] [35] [65]
    \vdots