Prueba trivial en ZFC

Question

Tomemos algún teorema de ZFC, por ejemplo: $$(1)\: \exists x \forall y ( y \notin x) $$ Podemos entonces elegir una constante, denotarla por ' $\varnothing$ ' para obtener lo siguiente: $$(2)\:\forall x (x\notin \varnothing) $$ Mi pregunta es: ¿cuál es la prueba precisa de (2) dada (1)? Además, dejemos que los axiomas de FOL sean los de Metalogic de Geoffrey Hunter (esquemas axiomáticos QS1-7), más los axiomas de ZFC (aunque creo que son irrelevantes). La única regla de inferencia permitida es el modus ponens.

P.D. Sé que la pregunta es ridícula, y obviamente el "salto" entre (1) y (2) tiene sentido. Lo único que me molesta es que no puedo justificar este "salto" formalmente :)

Answer 1

Es un teorema estándar sobre FOL que dada una teoría que conlleva una wff $\exists_1x\varphi(x)$ entonces podemos añadir de forma conservadora una nueva constante $c$ al lenguaje de la teoría, junto con el nuevo axioma $\varphi(c)$ . Esto es conservador en el sentido de que todavía no podremos demostrar nada en el lenguaje de la teoría original que no pudiéramos demostrar antes (incluso cuando usamos la nueva constante para instanciar viejos axiomas universales - véase el importante comentario de Henning Makholm más abajo). Así que hay un buen sentido en el que la nueva constante sólo espolvorea sobre la teoría original algo de "azúcar sintáctico" (alguna notación bonita que permite que la medicina baje más fácilmente, ayudándonos a poner las cosas de forma más ágil o más fácil de recordar) sin cambiar en absoluto el poder básico de la teoría.

Eso es todo lo que ocurre en el presente caso. Añadir notación para el conjunto vacío es típicamente añadir azúcar sintáctico, lo que se nos permite hacer porque, una vez que sabemos que hay un conjunto sin miembros, es inmediato que éste es único, así que tenemos $\exists_1x\forall y(y \notin x)$ y podemos aplicar el mencionado teorema estándar.

Answer 2

Vea lo siguiente Correo electrónico: .

Forma George Tourlakis, Lecturas de Lógica y Teoría de Conjuntos. Volumen 2 : Teoría de conjuntos , página 122 :

"Recordemos los fundamentos de la introducción de nuevos símbolos de función [en la lógica de primer orden]. Supongamos que tenemos lo siguiente:

$\vdash_T (\exists y) A(y, x)$ --- [llámalo : " existencia condición"]

y

$\vdash_T A(y, x) \land A(z, x) \rightarrow y = z$ --- [llámalo : " singularidad condición"]

entonces podemos introducir un nuevo símbolo de función, por ejemplo $f_A$ en la lengua de $T$ por el axioma

$f_ A(x) = y \leftrightarrow A(y, x)$ ".

Ahora, en $\mathsf {ZFC}$ tenemos el Conjunto nulo axioma :

$\exists y \lnot \exists x (x \in y)$

es decir

$\exists y \forall x (x \notin y)$ .

Como es demostrable a partir de este axioma y del Extensionalidad axioma de que existe un único conjunto de este tipo, podemos utilizar la "técnica" descrita anteriormente para introducir la notación ' $\emptyset$ para indicarlo.

En conclusión, es no basta con demostrar la condición de "existencia"; se necesita también la condición de "unicidad".

Answer 3

Añadamos mi punto de vista más bien informal:

Creo que las definiciones sólo se consideran una especie de meta cosa y no forman realmente parte de la lengua.

Así que hay que elegir una forma de dar un significado a las definiciones.

Se me ocurren dos tipos de definiciones:

• Una propiedad. Digamos que $x$ no está vacío significa que $\exists y(y\in x)$
• Un objeto. Se quiere denotar el $\varnothing$ el $x$ tal que $x$ no está vacío.

Ahora vamos a intentar resolver la siguiente fórmula $$\forall x(x\text{ is not empty}\Longrightarrow x\ne\varnothing)$$

Está bastante claro cómo resolver una propiedad, equivale a $$\forall x(\exists y(y\in x)\Longrightarrow x\ne\varnothing)$$ pero ¿qué pasa con $\varnothing$ ? Una forma de verlo es decir que la fórmula es válida para todos $x$ ( $z$ en este caso) de la definición de $\varnothing$ $$\forall z(\exists y(y\in z)\Longrightarrow\forall x(\exists y(y\in x)\Longrightarrow x\ne z))$$ Para que esto sea realmente útil, es necesario conocer tales $z$ existe y que es único. Ambas cosas están garantizadas si $\varnothing$ está bien definida.