¿Cómo puedo probar que las dos definiciones siguientes del cuantificador de unicidad en lógica de primer orden son equivalentes?

Ya sé que la segunda definición de unicidad implica la primera, porque si el predicado se cumple para todos los valores de z, entonces también se cumple solo para los valores de z para los que z=x, lo que nos dejaría con un predicado que es equivalente a la primera definición. Pero, ¿cómo pruebo que la primera definición de unicidad también implica la segunda?

Es básicamente el mismo razonamiento. Debido a que una declaración universal (forma de$\forall y~Q(y)$) puede eliminarse a variables arbitrarias de cualquier letra (es decir: no solo$y$, pero también$z$).

Así que toma arbitrariamente$y$y arbitrario$z$y derivar$~P(y)\land P(z) \to y=z~$por medio de$~P(y)\to y=x~$y$~P(z)\to z=x~$y eliminación de la igualdad .

Para empezar, creo que puede ser más fácil pensar en su problema en términos de dos fórmulas equivalentes sobre el predicado$P$en lugar de dos definiciones equivalentes, es decir considerar esta equivalencia:

$$\exists u (P(u) \land \forall v (P(v) \Rightarrow v = u)) \Leftrightarrow \exists x P(x) \land \forall y \forall z (P(y) \land P(z) \Rightarrow y = z)$$ Tenga en cuenta que también cambié los nombres de las variables para que sean todos distintos. Puede ayudar a evitar confusiones durante la prueba.

$\Rightarrow$dirección

Sabemos que existe$u$tal que$P(u)$(1) y$\forall v(P(v) \Rightarrow v = u)$(2). ahora toma$x = u$y podemos inferir$\exists x P(x)$. Ahora considere arbitrario$y$y$z$tal que$P(y)$y$P(z)$sostener. Podemos aplicar (2) para deducir$y = u$y$z = u$. Usando las propiedades de la igualdad obtenemos$y = z$, que completa la prueba del lado derecho.

$\Leftarrow$dirección

Sabemos$\exists x P(x)$(3) y$\forall y \forall z (P(y) \land P(z) \Rightarrow y = z)$. Podemos tomar$x = u$e inferir$P(u)$de (3). Ahora considere un arbitrario$v$tal que$P(v)$. Podemos aplicar (4) en$y = v$y$z = u$para obtener$v = u$y completa la demostración.

Discusión

Observe que si reemplazamos la igualdad con un predicado binario arbitrario$Q$, el$\Leftarrow$seguirá funcionando, pero el$\Rightarrow$necesidades de dirección$Q(y, u) \land Q(z, u) \Rightarrow Q(y, z)$para el último paso. Entonces, en cierto sentido, la segunda definición es más fuerte porque implica la primera sin depender de qué es la igualdad como una relación binaria.

Esencialmente quieres la derivación de

$$\exists x\;\Big(Px\wedge\forall y\forall z\;\big( Py\wedge Pz \to y=z\big)\Big)$$ de $$\exists x\;\Big(Px\wedge\forall y\;\big(Py\to y=x\big)\Big).$$

Aquí hay una prueba, utilizando el sistema de prueba en https://proofs.openlogicproject.org/ con reglas de inferencia adicionales Introducción de igualdad y sustitución:

Usando una forma de deducción natural (captura de pantalla de mi comprobador de pruebas):