Axiom schema of predicative separation

Short description: Schema of axioms in set theory

In axiomatic set theory, the axiom schema of predicative separation, or of restricted, or Δ0 separation, is a schema of axioms which is a restriction of the usual axiom schema of separation in Zermelo–Fraenkel set theory. This name Δ0 stems from the Lévy hierarchy, in analogy with the arithmetic hierarchy.

## Contents

* 1 Statement
* 1.1 Motivation
* 2 Theories
* 2.1 Finite axiomatizability
* 3 See also

## Statement

The axiom asserts only the existence of a subset of a set if that subset can be defined without reference to the entire universe of sets. The formal statement of this is the same as full separation schema, but with a restriction on the formulas that may be used: For any formula φ,

[math]\displaystyle{ \forall x \; \exists y \; \forall z \; (z \in y \leftrightarrow z \in x \wedge \phi(z)) }[/math]

provided that φ contains only bounded quantifiers and, as usual, that the variable y is not free in it. So all quantifiers in φ, if any, must appear in the forms

[math]\displaystyle{ \exists u \in v \; \psi(u) }[/math]
[math]\displaystyle{ \forall u \in v \; \psi(u) }[/math]

for some sub-formula ψ and, of course, the definition of [math]\displaystyle{ v }[/math] is bound to those rules as well.

### Motivation

This restriction is necessary from a predicative point of view, since the universe of all sets contains the set being defined. If it were referenced in the definition of the set, the definition would be circular.

## Theories

The axiom appears in the systems of constructive set theory CST and CZF, as well as in the system of Kripke–Platek set theory.

### Finite axiomatizability

Although the schema contains one axiom for each restricted formula φ, it is possible in CZF to replace this schema with a finite number of axioms.

## See also

* Constructive set theory
* Axiom schema of separation

0.00

(0 votes)

Original source: https://en.wikipedia.org/wiki/ Axiom schema of predicative separation. Read more

|

Retrieved from "https://handwiki.org/wiki/index.php?title=Axiom_schema_of_predicative_separation&oldid=2421312"