Schemat aksjomatu separacji predykatywnej

₀ W aksjomatycznej teorii mnogości schemat aksjomatu separacji predykatywnej lub separacji ograniczonej lub separacji Δ ₀ jest schematem aksjomatów , który jest ograniczeniem zwykłego schematu aksjomatu separacji w teorii mnogości Zermelo – Fraenkla . Nazwa ta Δ wywodzi się z hierarchii Lévy'ego , analogicznie do hierarchii arytmetycznej .

Oświadczenie

Aksjomat stwierdza istnienie podzbioru zbioru tylko wtedy, gdy ten podzbiór można zdefiniować bez odniesienia do całego wszechświata zbiorów. Formalne stwierdzenie tego jest takie samo, jak w przypadku pełnego schematu separacji, ale z ograniczeniem wzorów, których można użyć: Dla dowolnego wzoru φ,

${\ Displaystyle \ forall x \; \ istnieje y \; \ forall z \; (z \ w y \ strzałka w lewo z \ w x \ klin \phi (z))}$

pod warunkiem, że φ zawiera tylko kwantyfikatory ograniczone i jak zwykle zmienna y nie jest w nim dowolna. Tak więc wszystkie kwantyfikatory w φ, jeśli występują, muszą pojawić się w formularzach

${\ Displaystyle \ istnieje u \ w v \; \ psi (u)}$

${\ Displaystyle \ forall u \ w v \; \ psi (u)}$

dla niektórych podformuł ψ i oczywiście definicja $.$ również związana z tymi regułami

Motywacja

To ograniczenie jest konieczne z predykatywnego punktu widzenia, ponieważ wszechświat wszystkich zbiorów zawiera zbiór, który jest definiowany. Gdyby do niego odwoływano się w definicji zbioru, definicja byłaby kolista.

teorie

Aksjomat ten pojawia się w systemach konstruktywnej teorii mnogości CST i CZF, a także w systemie teorii mnogości Kripkego – Plateka .

Skończona aksjomatyzowalność

Chociaż schemat zawiera jeden aksjomat dla każdej ograniczonej formuły φ, w CZF możliwe jest zastąpienie tego schematu skończoną liczbą aksjomatów.

Zobacz też

• Konstruktywna teoria mnogości
• Schemat aksjomatu separacji