La teoría de conjuntos de Kripke-Platek con urelementos ( KPU ) es un sistema de axiomas para la teoría de conjuntos con urelementos , basado en la teoría de conjuntos tradicional de Kripke-Platek (libre de urelementos) . Es considerablemente más débil que el (relativamente) familiar sistema ZFU . El propósito de permitir elementos es permitir que objetos grandes o de alta complejidad (como el conjunto de todos los reales ) se incluyan en los modelos transitivos de la teoría sin alterar las propiedades habituales de ordenamiento correcto y de la teoría de la recursividad del universo construible ; KP es tan débil que es difícil hacerlo por medios tradicionales .
Preliminares
La forma habitual de expresar los axiomas supone un lenguaje de primer orden clasificado en dos con un solo símbolo de relación binaria . Letras del tipo designar elementos, de los cuales puede que no haya ninguno, mientras que las letras del tipo designar conjuntos. Las cartas puede denotar tanto conjuntos como urelementos.
Las letras de los conjuntos pueden aparecer en ambos lados de , mientras que los de urelements solo pueden aparecer a la izquierda, es decir, los siguientes son ejemplos de expresiones válidas: , .
El enunciado de los axiomas también requiere referencia a una cierta colección de fórmulas llamadas -fórmulas. La colección Consiste en aquellas fórmulas que se pueden construir usando las constantes, , , , y cuantificación acotada. Esa es la cuantificación de la forma o dónde se le da conjunto.
Axiomas
Los axiomas de KPU son los cierres universales de las siguientes fórmulas:
- Extensionalidad :
- Fundación : este es un esquema de axioma donde para cada fórmula tenemos .
- Maridaje :
- Unión :
- Δ 0 -Separación : Este es nuevamente un esquema de axioma , donde para cada-fórmula tenemos lo siguiente .
- - Colección : Este es también un esquema de axioma , para cada-fórmula tenemos .
- Establecer existencia:
Supuestos adicionales
Técnicamente, estos son axiomas que describen la partición de objetos en conjuntos y elementos.
Aplicaciones
KPU se puede aplicar a la teoría de modelos de lenguajes infinitarios . Los modelos de KPU considerados como conjuntos dentro de un universo máximo que son transitivos como tales se denominan conjuntos admisibles .
Ver también
Referencias
- Barwise, Jon (1975), Conjuntos y estructuras admisibles , Springer-Verlag, ISBN 3-540-07451-1.
- Gostanian, Richard (1980), "Modelos construibles de subsistemas de ZF", Journal of Symbolic Logic , 45 : 237-250, doi : 10.2307 / 2273185 , JSTOR 2273185.