¿Por qué es necesario un sistema axiomático en lógica proposicional?

Question

Estoy intentando aprender lógica proposicional. He leído que el sistema axiomático se define porque hay algunos problemas que no se pueden resolver utilizando tablas de verdad. He encontrado un problema de este tipo en la lógica de predicados cuando usamos cuantificadores. Allí debemos usar axiomas para derivar una fórmula que contenga cuantificador, ya que no podemos construir la tabla de verdad de esa fórmula. Pero me interesa saber por qué necesitamos un sistema axiomático en lógica proposicional. Podemos comprobar si una fórmula es una tautología usando su tabla de verdad.

Answer 1

Como has dicho podemos comprobar si una fórmula es una tautología simplemente mirando su tabla de verdad, de todos modos estudiar un sistema lógico (es decir, un sistema con axiomas y reglas de inferencia) también para la lógica proposicional puede ser interesante por diferentes razones:

• en primer lugar está la razón didáctica: es un sistema deductivo simple, de hecho se puede ver como sólo un fragmento del sistema para la lógica de primer orden, por lo que ayuda a familiarizarse con los sistemas deductivos;

• una segunda razón es la complejidad: a veces probar la validez lógica de una fórmula a través de un sistema deductivo puede ser más fácil que probarla a través de tablas de verdad, que implican calcular los valores de verdad de una fórmula para todas las posibles valoraciones de las variables, lo que puede ser fácil y problemático para fórmulas con un gran número de variables, mientras que en muchos casos escribir una prueba puede ser mucho más fácil con sólo aplicar unas pocas reglas de inferencia.

Probablemente también haya otras razones que ahora no recuerdo, pero me reservo el derecho de añadirlas más adelante :)

Answer 2

(a) Giorgio Mossa tiene razón. Dos razones para considerar sistemas deductivos para la lógica proposicional funcional de verdad estándar son

1. se pueden utilizar como ejemplos de juguete, como ejercicios de calentamiento para la tarea más seria de considerar el sistema de pruebas modal y otras lógicas,
2. pueden (en algunos casos) proporcionar pruebas de validez clásica de forma más eficiente que hackear una tabla de verdad.

(b) Pero, por supuesto, todo depende del sistema deductivo que se mire. El OP menciona sistemas axiomáticos. Bueno, aquí hay un sistema axiomático perfectamente bueno para la lógica proposicional (no es sólo un truco, sino que se usa en algunos libros para el fragmento proposicional de la teoría de la cuantificación):

Para cualquier tautología verdadero-funcional $\varphi$ , $\varphi$ es un axioma.

Y para la lógica proposicional pura no se necesita ninguna regla de inferencia adicional, ¡así que todas las pruebas del sistema axiomático son de una sola línea! Eso está muy bien, ya que es recursivamente decidible lo que es un axioma, lo que la convierte en una lógica axiomática kosher -- ¡y una que es trivialmente sólida y completa para los teoremas de la lógica proposicional clásica!

(c) Pero dejemos a un lado estos ejemplos trivializadores, ¡aunque nos recuerden que diferentes sistemas deductivos tendrán diferentes virtudes! Y, de hecho, dejemos a un lado los sistemas axiomáticos en el sentido más general de los sistemas de Frege-Hilbert (de todos modos, no suelen tener la virtud (2)). Concentrémonos en los sistemas de prueba de deducción natural de uno u otro estilo. Ahora hay una razón adicional para interesarse por ellos:

3 Podría decirse que las reglas ND de introducción y eliminación de conectivas fijan su sentido.

Podría decirse que lo que captamos al comprender preformalmente los operadores lógicos es su papel inferencial, es cómo podemos usarlos en la argumentación (en un lema wittgensteiniano, preguntar por el significado [de los operadores lógicos] es usar por su uso [inferencial]). Entonces, en el caso de la lógica proposicional, se puede pensar que un sistema de Deducción Natural pretende encapsular directamente el significado de las conectivas estableciendo las reglas inferenciales que rigen su uso, que determinan su significado.

Desde este punto de vista, que debemos a Gentzen, hay una especie de prioridad a las reglas de deducción en un sistema ND - y será un no trivial descubrimiento que el sistema resultante es sólido y completo con respecto a una interpretación booleana funcional de la verdad.

(d) O eso será un descubrimiento si, efectivamente, aceptamos las reglas "clásicas" de la ND. Pero, por supuesto, hay problemas al respecto. Desde la perspectiva de Gentzen, podría decirse que hay algo anómalo en las reglas de negación clásicas (los llamados fallos en la "armonía"). Y también podemos preocuparnos por las reglas estructurales clásicas que permiten el encadenamiento ilimitado de pruebas de un modo que nos da falacias (¿?) de irrelevancia. Pero los detalles no importan por ahora, sólo el siguiente punto general:

4 Al considerar los sistemas ND para la lógica proposicional clásica, también podemos -de una manera suave y natural- investigar lógicas no clásicas vecinas que posiblemente eviten algunas deficiencias del paradigma clásico.

Answer 3

Otro uso importante de los sistemas deductivos es la demostración de resultados de compacidad. En cuanto se dispone de un sistema deductivo completo y sólido en el que las pruebas son finitas, se tiene un teorema de compacidad: si una fórmula $\phi$ se deduce de algún conjunto infinito de premisas, entonces de hecho se deduce de algún subconjunto finito.

La compacidad de la lógica proposicional es una herramienta mucho más débil que la compacidad de la lógica de predicados, pero sirve como ejemplo de juguete y no es del todo inútil por derecho propio: sigue siendo lo bastante fuerte, por ejemplo, para expresar muchos de los argumentos de compacidad utilizados en combinatoria, en los que se deduce un resultado infinito a partir de sus equivalentes finitos. Por ejemplo, el teorema de los cuatro colores para grafos planos infinitos puede demostrarse a partir del caso finito de esta manera.

Por supuesto, con esta perspectiva, realmente no te importa qué sistema de pruebas que utilices, siempre que esté completo. Esta es una de las razones por las que se utilizan los engorrosos sistemas de Hilbert: demostrar cualquier resultado que merezca la pena en ellos supone una cantidad de trabajo frustrante, pero demostrar resultados metalógicos como la completitud es comparativamente fácil.

Answer 4

Las tablas verdadero-falso dependen de la semántica lógica utilizada. Por ejemplo, si se utiliza una tabla de verdad para una semántica lógica de dos valores, ésta muestra que la fórmula bien formada es siempre verdadera con esa semántica de dos valores.

Por otra parte, los sistemas axiomáticos no son locales a la semántica lógica utilizada. Si demuestras algo, habrás demostrado que no es válido sólo para esa semántica, sino para cualquier semántica en la que se cumplan los axiomas. Has demostrado que la fórmula es válida para varios modelos. Esto es comparable a cómo si usas los axiomas del álgebra de Boole para demostrar una ecuación, has demostrado más que si sólo hubieras usado el álgebra de Boole 0-1, y no tuvieras el resultado de que el álgebra de Boole 0-1 puede usarse para demostrar ecuaciones verdaderas para álgebras más grandes.

Así pues, si la motivación de una lógica consiste en parte en abordar más de una semántica posible, puede ser preferible un sistema axiomático.

Además, si estudias lógica no clásica y has visto algunas demostraciones formales (o puedes decir que una demostración formal sería bastante sencilla de producir) en lógica clásica, puedes reutilizar esas demostraciones para la lógica no clásica en la que todos los axiomas y reglas de inferencia en la demostración de la lógica clásica también se mantienen en la lógica no clásica. Así pues, si la motivación para estudiar lógica clásica reside en parte en estar en mejores condiciones para estudiar lógica no clásica, los sistemas axiomáticos pueden ser preferibles a las tablas de verdad.

Por ejemplo, si usted ha tomado una prueba usual de CCpCqrCCpqCpr en lógica clásica, usted podría encontrar que sólo utiliza los axiomas CpCqp y CCpCqrCCpqCpr. Pero, esa prueba implica que CCpCqrCCpqCpr es también un teorema en lógica intuicionista, lógica mínima, y el cálculo implicacional puro.