19/04/20 21:56:35.50 E/H8FvM1.net
メモ
URLﾘﾝｸ(ncatlab.org)
ETCS
Context
Topos Theory
Foundations
Contents
1. Idea
2. Definition
3. A constructive view
4. A contemporary perspective
5. Todd Trimble’s exposition of ETCS
(抜粋)
1. Idea
The Elementary Theory of the Category of Sets , or ETCS for short, is an axiomatic formulation of set theory in a category-theoretic spirit. As such, it is the prototypical structural set theory. Proposed shortly after ETCC in (Lawvere 64) it is also the paradigm for a categorical foundation of mathematics.1
The theory intends to capture in an invariant way the notion of a (constant) ‘abstract set’ whose elements lack internal structure and whose only external property is cardinality with further external relations arising from mappings.
The membership relation is local and relative i.e. membership is meaningful only between an element of a set and a subset of the very same set. (See Lawvere (1976, p.119) for a detailed description of the notion ‘abstract set’.2 3 4 5)
More in detail, ETCS is a first-order theory axiomatizing elementary toposes and specifically those which are well-pointed, have a natural numbers object and satisfy the axiom of choice. The theory omits the axiom of replacement, however.
2. Definition
The axioms of ETCS can be summed up in one sentence as:
Definition 2.1. The category of sets is the topos which
1.is a well-pointed topos
2.has a natural numbers object
3.and satisfies the axiom of choice.
For more details see
・fully formal ETCS.