¿Se puede introducir formalmente la notación de creación de conjuntos en ZFC?

Si uno es completamente formal, entonces puede formular ZFC como un conjunto de fórmulas de primer orden sobre la firma L = { ∈ } que consiste sólo en una relación binaria ∈ . Entonces uno puede enunciar los axiomas usuales de ZFC en este lenguaje formal.

Recientemente aprendí sobre el concepto de Extensión por definición . La idea principal es esta: en la práctica, no estamos trabajando en un lenguaje que solo consiste en ∈ , ¡pero estamos constantemente introduciendo nuevos símbolos! Por ejemplo, observamos primero que hay un conjunto único que no tiene ningún elemento, y esto justifica que podamos darle a este conjunto único un símbolo especial: elegimos ∅ para eso. Del mismo modo, se puede introducir un símbolo norte para los números naturales. Pero el mismo concepto también funciona cuando introducimos nuevos símbolos de funciones y relaciones: por ejemplo, podemos definir la operación ∪ demostrando que para cada A, B , existe un único conjunto A ∪ B con la propiedad ∀ X ( X ∈ A ∪ B ⟺ X ∈ A ∨ X ∈ B ) (después de probar que esto es único cuando se dan dos conjuntos A, B ); también se puede definir una relación ⊆ configurando A ⊆ B :⇔ ∀ X ( X ∈ A ⟹ X ∈ B ) .

Para obtener una definición formal de este concepto de "extensión por definición", consulte el artículo de wikipedia vinculado. Me pregunto:

¿Se puede introducir de manera similar una notación constructora de conjuntos en el lenguaje formal de la teoría de conjuntos? Tengo algo como esto en mente: dado un símbolo fijo A y una fórmula ϕ ( X ) con una variable libre, se puede definir el conjunto { X ∈ A : ϕ ( X ) } ser el conjunto único de todos los elementos de A que satisfacen la propiedad ϕ . ¿Es esta una simple notación humana o puede hacerse precisa de manera similar al concepto de extensión por definición?

Aparentemente no lo suficientemente bien. Lo siento.
@Arthur: Pregunto si es posible agregar una expresión como { X ∈ A ∣ ϕ ( X ) } a la sintaxis formal de ZFC, como se puede agregar ⊆ y ∪ y ∅ a la sintaxis formal. Mi pregunta es un poco estúpida e ingenua, pero en el mejor de los casos, hay algo que aprender :-)
Realmente nunca capté gran parte de la intuición en la lógica matemática más estricta, pero me parece que ϕ es un obstáculo Esa es la razón por la que la comprensión y el reemplazo no son axiomas, sino esquemas de axiomas. Podrías hacer un esquema para la notación de constructor de conjuntos, supongo. O podría estar fuera de mi profundidad.
Para cualquier otra persona que se encuentre con esta publicación, la forma formal de hacerlo es a través de la expansión de definiciones . Esta es la forma rigurosa de apoyar la llamada notación de construcción de conjuntos (que es esencialmente un símbolo constante que atestigua declaraciones existenciales), así como también ∪ (un símbolo de función binaria) y ⊆ (un predicado-símbolo binario). Tenga en cuenta que los dos últimos no están representados por ningún objeto (conjunto) en ZFC.
@ user21820: Le di una respuesta a su pregunta a continuación a lo largo de las líneas de expansión definitoria, pero antes de leer su comentario. Tienes razón. La notación de construcción de conjuntos aplicada a una fórmula dada con una variable libre puede interpretarse como un nuevo símbolo de función unaria que se agregará al lenguaje de la teoría de conjuntos.
@Transcendental: Sí, y la suya es una forma alternativa de pensar al respecto, a saber, que el axioma de especificación proporciona una función definible en conjuntos para cada fórmula, que elimina el subconjunto especificado por la fórmula. La mía era simplemente la noción más general de que todo axioma existencial puede convertirse mecánicamente en una constante definible. =)

Respuestas (3)

Aquí hay un enfoque que no emplea el operador de descripción de Russell yo .

Dada una fórmula de primer orden φ con una variable libre z en el lenguaje de la teoría de conjuntos ( L O S T ), puede agregar (i) un nuevo símbolo de función unaria F φ a L O S T y (ii) el siguiente nuevo axioma para Z F :

( ∀ X ) ( ∀ y ) ( y = F φ ( X ) ⟺ ( ∀ z ) ( z ∈ y ⟺ ( z ∈ X ∧ φ ) ) ) . ( ⋆ )
Por la conocida técnica de Extensión por Definiciones en lógica de primer orden, estas adiciones producen una extensión conservadora de Z F porque por un lado, el Axioma de Esquema de Especificación asegura que
( ∀ X ) ( ∃ y ) ( ∀ z ) ( z ∈ y ⟺ ( z ∈ X ∧ φ ) ) ,
y por otro lado, el Axioma de Extensionalidad asegura que
( ∀ X ) ( ∃ ! y ) ( ∀ z ) ( z ∈ y ⟺ ( z ∈ X ∧ φ ) ) .
Por lo tanto, puede pensar en F φ como una versión formalizada de la notación constructora de conjuntos aplicada a φ .

La notación de construcción de conjuntos es un operador de "formación de términos", es decir, un símbolo que con "entrada" una fórmula produce como "salida" un término , como el de Russell yo para descripciones definidas .

Para "ampliar" el lenguaje con yo , tenemos que :

1) probar: ( ∃ ! z ) q ( z , X 1 , … , X norte )

2) agregue el axioma: y = ( yo z ) q ( z , X 1 , … , X norte ) ↔ q ( y , X 1 , … , X norte ) .

De la misma manera, en teoría de conjuntos, tenemos que probar:

( ∃ ! z ) ( ∀ X ) ( X ∈ z ↔ φ ( X ) )

y luego agregue el axioma:

{ X : φ ( X ) } = ( yo z ) ( ∀ X ) ( X ∈ z ↔ φ ( X ) ) .

Gracias. Parece que las descripciones definitivas son la respuesta perfecta sobre cómo formalizar la notación de creación de conjuntos en ZFC.

Sí, los nombres en el desarrollo del forzamiento pueden verse así, y la definición del universo construible L se puede expresar de esta manera también.

Recuerdo haber visto un símbolo de K al revés utilizado para denotar términos formales que eran esencialmente términos variantes de creación de conjuntos.

¿Se puede introducir formalmente la notación de creación de conjuntos en ZFC?
RespuestasAquíPolítica de privacidad1y, 0v