Project Page Index Table of Contents
  • Structures, Axiomatisations and Universes
    • Structures
    • Intensional and Extensional Axiomatisations
    • Grothendieck Universes
    • Universe Strength and ZFn
  • Basic Library for ZF
    • Inclusion
    • Well-founded sets
    • Least sets
    • Empty set
    • Singletons
    • Union
    • Separation
    • Power
    • Relational replacement
    • Strength
  • Membership Embeddings
  • Models of ZF with Infinity are uncountable
  • Cumulative Hierarchy
    • Excluded Middle
    • The stages are well-ordered and exhaust all sets
    • Limits
    • Universes
  • Equivalence of ZF>=1 and ZF+Inf
    • Definition of Omega
    • Hereditarily finite sets (HF)
    • The class HF is realized by Omega
    • Inf implies that Omega is a universe
    • Models of ZF>=1 satisfy Infinity
  • Zermelo's Embedding Theorem
  • Categoricity Results
    • ZF is categorical in every cardinality
    • ZFn is categorical for all n
    • Axiom of Choice
  • Truncation Lemma
    • ZF-closed classes induce submodels of ZF
    • Models of strength n admit inner models of ZFn
  • Aczel's Intensional Model Construction
    • Well-Founded Trees
    • Definition of Set Operations
    • Proof of Intensional Axioms
  • Extensional Model of Z via Class Extensionality
  • Extensional Model of ZF' via Canonical Representatives
  • Extensional Model of ZF via Tree Description
  • Large Models
    • Embedding of intensional models yields universes
    • Consistency of ZF>=n
  • Independence of Foundation
    • Models of ZF* admit inner models of ZF
    • Non-Well-Founded Models
Generated by coqdoc and improved with CoqdocJS