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.

  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] [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] [39]
  41. Proposition: Generalized conjunction introduction [2] [3] [4] [39] [40]
  42. Inference rule: Conjunction elimination [4] [39]
  43. Proposition: Generalized conjunction elimination [2] [3] [4] [39] [42]
  44. Proposition: Idempotence of conjunction [4] [39] [40] [42]
  45. Proposition: Commutativity of conjunction [4] [39] [40] [42]
  46. Proposition: Associativity of conjunction [4] [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] [39] [47] [48] [49]
  54. Proposition: Double negation of entailment [5] [38] [39] [51]
  55. Proposition: Triple negation elimination [5] [39] [47] [49] [53]
  56. Inference rule: Double negation elimination [5] [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