¿Existen razones realmente convincentes para permitir deducciones naturales en fórmulas con variables libres?

Question

Veo que algunos libros de texto permiten hacer deducciones no sólo de primer orden frases (es decir, sin variables libres), sino también fórmulas con variables libres. Por ejemplo, es legal escribir $\vdash Px\to\exists x Px$ en su libro.

Bueno, yo había aprendido lógica matemática básica en el libro de Causey, que confinaba cada línea en una prueba de deducción (incluyendo premisas, conclusión y pasos intermedios) a ser frase solamente, y me siento bastante cómodo al respecto. Ahora estoy turing para estudiar lógica matemática clásica, entonces de repente se me ocurrió esta pregunta. ¿Por qué (algunas?) personas aceptan hacer algo así? ¿Hay algún beneficio convincente?

Answer 1

Entiendo perfectamente su punto de vista. Al estar acostumbrado a un sistema de pruebas en el que cada línea tiene que ser una sentencia (es decir, ¡no se permiten variables libres!), yo también encuentro "molestos" y algo "feos" los sistemas de pruebas en los que intervienen variables libres... ¡aunque sin duda gran parte de eso es a lo que estás acostumbrado!

En los comentarios se sugiere que es agradable trabajar con 'x' como referencia lingüística a algún objeto 'arbitrario', y eso ciertamente tiene sentido, pero tú y yo simplemente usamos alguna constante 'arbitraria' en su lugar... de nuevo, mucho de lo que tiene 'sentido' aquí es simplemente a lo que estamos acostumbrados.

Aún así, creo que en realidad es una buena razón para poder hacer inferencias lógicas sobre fórmulas generales. Para ver esto, observe que podemos extender las nociones de equivalencia lógica, implicación, etc. a las fórmulas en general. Por ejemplo $P(x) \lor \neg P(x)$ es una tautología lógica en el sentido de que dada cualquier asignación variable e interpretación de $P$ la afirmación resulta cierta.

Y algo como la equivalencia lógica entre fórmulas es en realidad una noción realmente importante, ya que nos permite afirmar que, por ejemplo, que las sentencias $\forall x (P(x) \rightarrow Q(x))$ et $\forall x (\neg Q(x) \rightarrow \neg P(x))$ son lógicamente equivalentes señalando que sus cuerpos son lógicamente equivalentes fórmulas y utilizando el "Principio de sustitución de fórmulas lógicamente equivalentes" que afirma que la sustitución de fórmulas lógicamente equivalentes en fórmulas mayores da como resultado fórmulas lógicamente equivalentes (este Principio es a su vez una generalización del Principio de sustitución de oraciones lógicamente equivalentes, por supuesto).

Por lo tanto, es realmente útil poder generalizar conceptos lógicos importantes a fórmulas, en lugar de sólo a frases. Así que tendría sentido disponer de un sistema de demostración capaz de demostrar esas propiedades y relaciones lógicas para las fórmulas en general.