Ayuda con las reglas de identidad de la lógica de primer orden con igualdad

Question

Soy principiante en lógica y estoy estudiando con libros de texto. Ahora mismo sólo me queda la lógica de predicados con identidad y necesito hacer algunas preguntas, para poder liberar mi mente de dudas y dormir bien por la noche.

Hacer las reglas de identidad (Id)

p//x=x (reflexividad);

x=y y=x (simetría);

x=y/y=z//x=z (transitividad);

Fx/x=y//Fy, Fx/¬Fy//¬(x=y) (sustitución);

¿se aplica tanto a las variables como a las constantes?

Estoy casi seguro de que sí, pero hay un libro de texto que dice que sólo se aplica a las constantes, y luego una edición más reciente del mismo libro dice que se aplica tanto a las variables como a las constantes. Así que necesito estar seguro.

Otra pregunta:

Si tengo

1. Raa
2. ¬Rab

¿Puedo inferir de ambas premisas la línea ¬(a=b) con las reglas de Id, o necesito algún paso intermedio? ¿O es simplemente un error?

Una última pregunta: al hacer la Instanciación Existencial (EI), sé que puedo sustituir la variable por una nueva constante, una que no haya aparecido en la prueba en ninguna línea anterior y en la línea de la conclusión, y luego dejar de lado el cuantificador; pero hay un libro de texto que dice que podría instanciar con una variable, siempre que sea una nueva que no haya sido utilizada, ¿eso significa que puedo hacer EI tanto con variables como con constantes? Estaba seguro de que sólo podía instanciar con una constante, y que la constante debía ser un "nombre temporal". ¿Puede alguien aclararme esto?

Answer 1

Trataré tu primera y última pregunta al mismo tiempo: hay diferentes sistemas formales de lógica, y sí, algunos usarán variables al eliminar cuantificadores, mientras que otros usan constantes. Para los primeros tipos de sistemas, las reglas de identidad se aplican tanto a las variables como a las constantes, pero para los últimos tipos de sistemas, las reglas de identidad sólo se aplican a las constantes.

Entonces, para inferir $\neg a = b$ probablemente tengas que hacer una prueba por contradicción: suponer $a=b$ , infiere $Rab$ sustituyendo $b$ para el segundo $a$ en $Raa$ y que se contradice con $\neg Rab$

Answer 2

Esta respuesta es sólo a una parte de la pregunta. Es similar a la sugerida por Bram28 aunque coloca los pasos en un comprobador de pruebas:

Si tengo

1. Raa
2. ¬Rab

¿Puedo inferir de ambas premisas la línea ¬(a=b) con las reglas de Id, o necesito algún paso intermedio? ¿O es simplemente un error?

He aquí una prueba:

Puedo utilizar la igualdad asumida en la línea 3 para hacer la sustitución en la línea 2 que me permite derivar la línea 4. Esto me lleva a una contradicción (línea 5) que me permite negar la igualdad asumida.

---

Editor y comprobador de pruebas de deducción natural al estilo de JavaScript/PHP de Kevin Klement http://proofs.openlogicproject.org/