ZFC: axiomatic set theory

前置知识

6 项必需的前置知识（一直追溯到底）

你将学会

• State the ZFC axioms and explain what each one contributes.
• Encode ordered pairs, relations, functions and the natural numbers as sets, and prove the characteristic property of Kuratowski pairs.
• Explain the difference between proving a theorem in ZFC and proving that ZFC is consistent.

定义

• ZFC is the first-order theory in the language {∈} with the axioms of extensionality, pairing, union, power set, separation (a schema), replacement (a schema), infinity, foundation and choice.
• The Kuratowski ordered pair is (a, b) = {{a}, {a, b}}.
• The von Neumann natural numbers are 0 = ∅ and n + 1 = n ∪ {n}; ω is the least set containing 0 and closed under n ↦ n + 1.

定理

• For Kuratowski pairs, (a, b) = (c, d) if and only if a = c and b = d.
• ZF proves that there is no set of all sets.
• If ZFC is consistent, it cannot prove its own consistency (Gödel's second incompleteness theorem).
• Most of ordinary mathematics, including analysis, algebra and topology, can be formalised in ZFC.

常见误解

• Thinking ZFC says what sets 'really are'; it is a list of assumptions from which theorems are derived.
• Believing natural numbers 'are' von Neumann ordinals; that is one convenient encoding among several.
• Assuming ZFC has been proved consistent; its consistency is assumed, and cannot be proved within ZFC itself if it is consistent.

通向

可选发现

• Elementary topos theory Lawvere's Elementary Theory of the Category of Sets (ETCS) axiomatises sets through functions instead of membership; without an added replacement axiom it is strictly weaker than ZFC.
• Axiomatic set theory: hierarchy, cardinal arithmetic and L Iterating 'sets of sets' transfinitely builds the cumulative hierarchy V_α; with the axiom of foundation, every set appears at some stage.探奇小径 →
• Large cardinals If ZFC is consistent, it cannot prove that an inaccessible cardinal exists; at an inaccessible κ, the stage V_κ of the hierarchy is itself a model of ZFC.探奇小径 →
• Type theory and propositions as types Lean is founded not on ZFC but on a dependent type theory. Each foundation can model the other given suitable assumptions, but they are not interchangeable.
• ← Sets
• ← Russell's paradox and why sets need axioms

延伸阅读

• Herbert B. Enderton, Elements of Set Theory (1977)
• Kenneth Kunen, Set Theory: An Introduction to Independence Proofs (1980)