structure for 'Formal Logic'    |     alphabetical list of themes    |     unexpand these ideas

4. Formal Logic / F. Set Theory ST / 4. Axioms for Sets / n. Axiom of Comprehension

[axiom saying a set exists which satisfies a predicate]

3 ideas
Comprehension: ∃y ∀x (x ∈ y ↔ x ∈ z ∧ φ) [Kunen]
     Full Idea: Comprehension Scheme: for each formula φ without y free, the universal closure of this is an axiom: ∃y ∀x (x ∈ y ↔ x ∈ z ∧ φ). That is, there must be a set y if it can be defined by the formula φ.
     From: Kenneth Kunen (Set Theory [1980], §1.5)
     A reaction: Unrestricted comprehension leads to Russell's paradox, so restricting it in some way (e.g. by the Axiom of Specification) is essential.
Comprehension Axiom: if a collection is clearly specified, it is a set [Wolf,RS]
     Full Idea: The comprehension axiom says that any collection of objects that can be clearly specified can be considered to be a set.
     From: Robert S. Wolf (A Tour through Mathematical Logic [2005], 2.2)
     A reaction: This is virtually tautological, since I presume that 'clearly specified' means pinning down exact which items are the members, which is what a set is (by extensionality). The naïve version is, of course, not so hot.
A comprehension axiom is 'predicative' if the formula has no bound second-order variables [Linnebo]
     Full Idea: If φ contains no bound second-order variables, the corresponding comprehension axiom is said to be 'predicative'; otherwise it is 'impredicative'.
     From: Øystein Linnebo (Plural Quantification Exposed [2003], §1)
     A reaction: ['Predicative' roughly means that a new predicate is created, and 'impredicative' means that it just uses existing predicates]