¿Por qué hay varios sistemas de axiomas para la lógica proposicional?

De hecho, hay muchas presentaciones de la lógica proposicional clásica ¹ .

Si la complejidad se midiera puramente en términos de número de axiomas, entonces sí, el sistema de axiomas de Mendelson sería más "económico". Podríamos ser aún más "económicos" con el sistema de Meredith:

$$((((A\to B)\to(\neg C\to\neg D))\to C)\to E)\to((E\to A)\to(D\to A))$$ Simplemente sale de la lengua. Si bien la minimalidad suele ser un factor determinante, la gente aún necesita descubrir sistemas más mínimos. (De hecho, el anterior no es el sistema más mínimo si incluimos la complejidad del axioma y no solo el número). También está la cuestión de aceptar los axiomas. Idealmente, queremos que los axiomas sean "evidentes" o al menos fáciles de entender intuitivamente. Tal vez sea solo yo, pero el axioma de Meredith no me llama la atención como algo que obviamente debería ser cierto, y mucho menos suficiente para probar todas las demás tautologías clásicas.

Sin embargo, la minimalidad no es el "punto central" de los sistemas axiomáticos. Usted menciona otra razón: a veces realmente quiere probar cosas en qué punto es mejor tener un sistema axiomático más rico e intuitivo. Puede argumentar que podemos derivar cualquier teorema que queramos usar a partir de una base mínima y luego olvidarnos de esa base. Esta es una complejidad verdadera pero innecesaria si no tenemos otra razón para considerar esta base mínima. Cuando comparamos diferentes estilos de sistemas de prueba (p. ej., Hilbert vs. Sequent Calculus vs. Natural Deduction), las traducciones entre ellos (especialmente en sistemas de estilo Hilbert) pueden implicar una gran complejidad mecánica. Esa complejidad a veces puede reducirse significativamente mediante una elección cuidadosa de los axiomas.

Para las leyes del medio excluido (LEM) y la no contradicción, lo primero que debe hacer es definir los conectores. no puedes probar$\neg(P\land\neg P)$en un sistema que no tiene$\land$. Dado$\neg$y$\to$como primitivas, definiciones estándar de$\land$y$\lor$son$P\land Q:\equiv \neg(P\to\neg Q)$y$P\lor Q:\equiv\neg P\to Q$. Con estas definiciones (u otras), entonces sí, el LEM y la no contradicción pueden probarse tanto en los sistemas que mencionas como en cualquier otro sistema de prueba para la lógica proposicional clásica. Su preocupación aquí es una ilustración de que a menudo nos preocupamos por los axiomas que tenemos y no solo por su brevedad y efectividad.

Esto también lleva a otra razón por la que podríamos querer una determinada presentación. Es posible que queramos que esa presentación se alinee con otras lógicas relacionadas. Como está comenzando a darse cuenta, está mal definido decir algo como "la lógica proposicional intuicionista (IPL) es la lógica proposicional clásica (CPL) menos el LEM". Cuando la gente dice cosas como esta, están siendo descuidados. Sin embargo, "CPL es IPL más LEM" no es ambiguo. Cualquier presentación de IPL a la que le agreguemos LEM es una presentación de CPL. Para esa presentación, tiene sentido hablar de eliminar LEM. No tiene sentido hablar de eliminar un axioma sin una presentación de axiomas que contengan ese axioma. También es bastante posible tener una presentación de CPL que contenga LEM que se vuelva mucho más débil que IPL cuando se elimina LEM. De hecho, tú Espero esto porque es probable que una presentación de IPL con LEM agregado sea redundante porque las cosas que son intuitivamente distintas se vuelven identificables cuando se agrega LEM. La historia es la misma para las lógicas paraconsistentes.

Si bien no es un gran impulsor para los sistemas de prueba de estilo Hilbert, para la deducción natural y los cálculos secuenciales, las preocupaciones de la teoría de la prueba estructural a menudo impulsan másaxiomas (o reglas de inferencia, más bien). Por ejemplo, muchos axiomas en un sistema de prueba al estilo de Hilbert mezclan conectivos, por ejemplo, como lo hace Meredith arriba. Esto significa que no podemos entender un conectivo en sus propios términos, sino solo por cómo interactúa con otros conectivos. Una fuerza impulsora en las presentaciones estructurales típicas es caracterizar los conectores mediante reglas que no hacen referencia a ningún otro conector. Esto revela mejor la naturaleza "verdadera" de los conectores y hace que el sistema sea más modular. Se vuelve significativo hablar sobre agregar o eliminar un solo conector que le permite construir una lógica a la carta. De hecho, la teoría de la prueba estructural motiva muchas restricciones sobre cómo debería ser un sistema de prueba, como la armonía lógica .

¹ Y ese enlace solo considera los sistemas de prueba estilo Hilbert.