nLab foundations - contents

foundations

The basis of it all

• mathematical logic

• deduction system, natural deduction, sequent calculus, lambda-calculus, judgment

• type theory, simple type theory, dependent type theory

• collection, object, type, term, set, element

• equality, judgmental equality, typal equality

• universe, size issues

• higher-order logic

 Set theory

set theory

• fundamentals of set theory
  • propositional logic
  • first-order logic
  • typed predicate logic
  • membership relation
  • propositional equality
  • set, element, function, relation
  • universe, small set, large set
• material set theory
  • membership relation, propositional equality, axiom of extensionality
  • pairing structure, axiom of pairing
  • union structure, axiom of union
  • powerset structure, axiom of power sets
  • natural numbers structure, axiom of infinity
• presentations of set theory
  • first-order set theory
  • unsorted set theory
  • simply sorted set theory
    • one-sorted set theory
    • two-sorted set theory
    • three-sorted set theory
  • dependently sorted set theory
  • structurally presented set theory
• structuralism in set theory
  • material set theory
    • ZFC
    • ZFA
    • Mostowski set theory
    • New Foundations
  • structural set theory
    • categorical set theory
      • ETCS
        • fully formal ETCS
        • ETCS with elements
        • Trimble on ETCS I
        • Trimble on ETCS II
        • Trimble on ETCS III
      • structural ZFC
    • allegorical set theory
      • SEAR
• class-set theory
  • class, proper class
  • universal class, universe
  • category of classes
  • category with class structure
• constructive set theory
• algebraic set theory

Foundational axioms

foundational axioms

• basic constructions:

  • axiom of cartesian products
  • axiom of disjoint unions
  • axiom of the empty set
  • axiom of fullness
  • axiom of function sets
  • axiom of power sets
  • axiom of quotient sets

• material axioms:

  • axiom of extensionality
  • axiom of foundation
  • axiom of anti-foundation
  • Mostowski's axiom
  • axiom of pairing
  • axiom of transitive closure
  • axiom of union

• structural axioms:

  • axiom of materialization

• type theoretic axioms:

  • axioms of set truncation
    • uniqueness of identity proofs
    • axiom K
    • boundary separation
    • equality reflection
    • axiom of circle type localization
  • homotopy type theoretic axioms:
    • univalence axiom
    • Whitehead's principle

• axioms of choice:

  • axiom of choice
  • axiom of countable choice
  • axiom of dependent choice
  • axiom of excluded middle
  • axiom of existence
  • axiom of multiple choice
  • Markov's axiom
  • presentation axiom
  • small cardinality selection axiom
  • axiom of small violations of choice
  • axiom of weakly initial sets of covers

• large cardinal axioms:

  • axiom of infinity
  • axiom of universes
  • regular extension axiom
  • inaccessible cardinal
  • measurable cardinal
  • elementary embedding
  • supercompact cardinal
  • Vopěnka's principle

• strong axioms

  • axiom of separation
  • axiom of replacement

• further

  • reflection principle

• axiom of tight apartness

Removing axioms

• constructive mathematics
• predicative mathematics

Edit this sidebar