Demostrar ∀w(∀v((v=w∧φ(v))⇔φ(w)))

En esta pregunta matemática mía , una respuesta me indicó este teorema:

∀w(∀v((v=w∧φ(v))⇔φ(w)))

lo que a su vez, afirmó el que responde, implica otro teorema:

∃v(v=t∧φ(v))⇔φ(t)

que era el hecho que necesitaba para mi prueba.

Sin embargo, ¿cómo se probaría este primer teorema? El libro Axiomatic Set Theory de Patrick Suppes, que ha sido un gran recurso para mí, demuestra un resultado similar y∈{x:ψ(x)}⇔ψ(y)en la página 34; sin embargo, que yo sepa, el resultado particular que busco no se responde en este libro. ¿Alguien puede señalarme un buen libro donde se demuestre esto? ¡Gracias!

Se me acaba de ocurrir que podría haber leído mal tu pregunta. ¿Quieres saber cómo probar ∀w(∀v((v=w∧φ(v))⇔φ(w)))?
@Dennis Sí, mis disculpas, mi pregunta no fue clara. Me refiero a preguntar sobre el resultado ∀w(∀v((v=w∧φ(v))⇔φ(w))): ¿dónde puedo encontrar esto probado?
Creo que descubrí el problema, pero antes de editar la respuesta, ¿quisiste decir que el operador final en ∀w(∀v((v=w∧φ(v))⇔φ(w))) sea bicondicional? ? En la pregunta que cita, la respuesta contiene esto: ∀w∀v((v=w∧φ(v))⟹φ(w)), pero no su fórmula con un bicondicional. (Dicho sea de paso, la versión condicional es válida; sin embargo, una vez que cambia la condicional a bicondicional, deja de ser válida.
Sí, la respuesta dice ∀w(∀v((v=w∧φ(v))⇒φ(w))), pero creo que ∀w(∀v((v=w∧φ(v))⇔φ(w)))(más fuerte) también debería ser cierto, ¿no es así?
Traté de aclarar mis pensamientos, pero una vez más lo estoy haciendo a las 3 a.m. Entonces, si algo no tiene sentido, retrocede, porque podría haber estropeado algo.
Creo que Dennis tiene razón. El condicional directo es correcto: de hecho, si tomamos la fórmula como un esquema que se cumple para cualquier φ, entonces es en efecto una afirmación de la indiscernibilidad de los idénticos. Pero lo contrario no se sostiene. Si desea intentar establecer la identidad de los indiscernibles, deberá reformular la fórmula.

Respuestas (1)

Bueno, es tarde en la noche, así que estoy seguro de que repetiré los errores del pasado y arruinaré algo aquí. Pero vamos a darle una oportunidad.

Empiezas con la frase original:

∀w(∀v((v=w∧φ(v))⇔φ(w)))

A partir de ahí, solo necesitamos descargar el cuantificador más externo, instanciando el término "t" (suponiendo que tengamos dicho término por ahí):

∀v((v=t∧φ(v))⇔φ(t)))

Luego instanciamos una vez más:

(r=t∧φ(r))⇔φ(t)

Finalmente, generalizamos existencialmente:

∃v(v=t∧φ(v))⇔φ(t)

Para una versión mía privada de sueño, eso parece ser lo que buscas. Si me equivoqué en algo, házmelo saber y revisaré la pregunta con la cabeza más clara.

Actualizar

Bien, he compuesto pruebas de cada uno de los principios (las versiones condicional y bicondicional) como pruebas de árbol al estilo de la Introducción a la lógica no clásica de Graham Priest . Avísame si tienes problemas para entenderlos.

Primero el condicional, que demuestro vía reductio ad absurdum asumiendo su negación:ingrese la descripción de la imagen aquí

Dado que la prueba termina en una contradicción ( a es tanto φ como no-φ), el condicional negado conduce a la contradicción y, por lo tanto, nuestro condicional original es válido.

Ok, entonces el condicional es válido, ¿qué pasa con el bicondicional? De nuevo, no creo que sea válido. Considere el siguiente intento de prueba:ingrese la descripción de la imagen aquí

Ahora bien, la rama de la izquierda conduce a la contradicción y así se cierra. La rama de la derecha, por otro lado, no implica contradicciones, por lo que la negación del bicondicional no es inválida. Pero si la negación del bicondicional no es inválida, entonces el bicondicional no es válido.

El problema es el lado derecho a izquierdo del bicondicional, ya que si comenzamos asumiendo que b es φ eso no garantiza que b sea el único objeto en el dominio. Si hay otro objeto a que no es idéntico a be, entonces aunque b es φ, el consecuente del lado derecho a izquierdo resulta falso ya que a no es idéntico a b .