Como dije en mi respuesta anterior le regla El modus ponens forma parte del definición de muchos sistemas de pruebas comunes. Sea HPC representan el sistema de Hilbert para la lógica proposicional clásica cuyo sólo regla de inferencia es el modus ponens y cuyos axiomas se enumeran ici después de la de Frege. Se trata de un objeto matemático bien definido. Es un sistema de prueba para la lógica proposicional clásica. En esa página se mencionan literalmente más de una docena de otros, y éstos se limitan a los sistemas de prueba de tipo Hilbert. También hay muchos otros del estilo de la deducción natural o del cálculo secuencial.
En HPC una prueba (formal) es una instancia de uno de los axiomas, o es un uso de la regla modus ponens que combina otras dos pruebas. Esto produce una estructura en forma de árbol binario cuyas hojas son instancias de los axiomas. Esta es la definición de una prueba en HPC . Una fórmula de la lógica proposicional clásica es probado por HPC si podemos construir una prueba que tenga esa fórmula como conclusión (es decir, la raíz del árbol). Este es un ejemplo del enfoque sintáctico de la lógica. Ni siquiera necesitamos formule la idea de las "tablas de verdad" para especificar completamente esto.
Un enfoque alternativo es la semántica. Aquí no hay axiomas ni reglas. En su lugar, necesitamos proporcionar una forma de interpretar las fórmulas como algún objeto matemático (de forma compositiva, pero no me extenderé en ello). Hay muchas semánticas posibles que se pueden utilizar. Una posibilidad es utilizar un Álgebra booleana y, en particular, el álgebra booleana no trivial más sencilla posible construida sobre un conjunto de dos elementos. Cualquier un conjunto de dos elementos será suficiente. Utilicemos $\{\mathsf{cat},\mathsf{dog}\}$ para concretar. Con esta elección de la semántica, las fórmulas con $n$ Las variables proposicionales (distintas) se convierten en $n$ -arias sobre ese conjunto de dos elementos. Ahora bien definir una fórmula para ser " verdadero " si su interpretación es una función que tiene constantemente el valor $\mathsf{dog}$ . A diferencia de lo anterior, podemos especificar completamente esta semántica sin mencionar nunca cualquier noción de prueba formal.
Ahora podemos preguntarnos: ¿son las fórmulas que HPC ¿proba lo mismo que las fórmulas que la semántica del álgebra de Boole llama "verdaderas"? El teorema de solidez para HPC con respecto a esta semántica del álgebra booleana establece que las fórmulas que HPC demuestran que son "verdaderos" en la semántica. El teorema de exhaustividad para HPC con respecto a esta semántica del álgebra de Boole afirma que cada fórmula que es "verdadera" en la semántica tiene una prueba en HPC . Estos (meta)teoremas pueden demostrarse con un razonamiento matemático informal o formalmente dentro de un marco lógico más rico.
En ningún momento hay que aceptar las reglas o axiomas de HPC o están de acuerdo en que la semántica del álgebra booleana que di refleja correctamente alguna noción filosófica de la verdad. Esto no es diferente de estudiar cualquier otro objeto matemático. Si estoy estudiando el anillo de matrices cuadradas, no tengo que rechazar mis nociones previas de suma y multiplicación y aceptar la suma/multiplicación de matrices como el Único Significado Verdadero de la suma y la multiplicación. No necesito tener una explicación de primeros principios de cómo no hay otra manera de sumar y multiplicar matrices. (Hay son otras formas de sumar y multiplicar matrices) Las fórmulas demostradas por HPC son las mismas independientemente de la postura filosófica de cada uno. Las fórmulas que son "verdaderas" con respecto a la semántica del álgebra de Boole son las mismas independientemente de la postura filosófica de cada uno. La postura filosófica de cada uno simplemente no entra en juego. 1
La única vez que necesitaría convencerte de los axiomas/reglas de HPC es si estoy haciendo una afirmación filosófica de que corresponden a alguna noción filosófica de "verdad". Hay muchas razones para estudiar la lógica proposicional clásica aparte de las nociones filosóficas de "verdad", como las aplicaciones a los circuitos digitales. Del mismo modo, hay muchas razones para estudiar la lógica intuicionista sin relación con las nociones filosóficas de la verdad, como la extracción del contenido computacional de las pruebas constructivas o la demostración de teoremas que son válidos para una clase de semántica mucho más amplia y matemáticamente importante que la lógica clásica. Hay buenas razones para estudiar ambas cosas simultáneamente, y no hay disonancia cognitiva en hacerlo.
En cuanto a algunas personas que llaman $(p\land(p\to q))\to q$ "modus ponens", no sería la primera vez en matemáticas que se le da el mismo nombre a dos conceptos distintos pero relacionados. Dicho esto, creo que muchas veces se ve que lo dice alguien que no tiene (o al menos no ha demostrado tener) una comprensión clara de la separación entre lógica y meta-lógica. Al igual que tu pregunta anterior, si intentas formalizar ingenuamente la descripción informal habitual de la regla modus ponens pero no tienes cuidado de separar la sintaxis de la semántica y la lógica de la meta-lógica, entonces obtienes fácilmente la fórmula anterior. Si se tiene cuidado de mantenerlas separadas, es evidente que tratar la fórmula anterior como la formalización de la regla modus ponens es una mezcla de lógica y meta-lógica.
Escribe $\vdash p$ para el meta-lógico afirman que HPC prueba $p$ . La descripción informal típica de la regla modus ponens es: "si $p$ es demostrable y $p\to q$ es demostrable, entonces $q$ es demostrable". Permítanme escribirlo de manera un poco más formal. Para que la distinción entre lógica y meta-lógica sea un poco más clara, escribiré $\curlywedge$ y $\leadsto$ para la conjunción e implicación meta-lógica. El "modus ponens" informal es entonces más formal: $((\vdash p)\curlywedge(\vdash(p\to q)))\leadsto(\vdash q)$ . Esto tiene la forma $(\varphi\curlywedge\psi)\leadsto \chi$ donde $\varphi$ , $\psi$ y $\chi$ son proposiciones atómicas en la meta-lógica. Diciendo $(p\land(p\to q))\to q$ es una tautología es a través de los teoremas de solidez y exhaustividad equivale a decir $\vdash ((p\land(p\to q))\to q)$ . Esta es una proposición atómica de la meta-lógica. Ahora debería quedar claro por qué hablo de una mezcolanza. Ver estas dos proposiciones meta-lógicas como si fueran la misma lleva a $\to$ que se utiliza tanto para el $\to$ conectivo de la lógica y la meta-lógica $\leadsto$ .
Aun así, si alguien quiere llame a $(p\land(p\to q))\to q$ "modus ponens", es su prerrogativa. No es diferente de decir que se va a llamar $A$ . Sin embargo, si lo que pretenden es la formalización de la regla modus ponens, entonces simplemente se equivocan.
1 Esto no es completamente cierto, ya que la postura filosófica de cada uno sobre la verdad influye en su razonamiento informal. Por ejemplo, un ultrafinitista podría rechazar la afirmación de que fórmulas suficientemente grandes de la lógica proposicional clásica puede tienen pruebas en HPC o puede se demuestre que es "verdadera" en la semántica del álgebra de Boole. Sin embargo, un matemático clásico, un ultrafinitista y un intuicionista estarán de acuerdo en que $p\lor\neg p$ es demostrable en HPC y es "verdadero" con respecto a la semántica del álgebra booleana. Sólo que pueden no estar de acuerdo en que HPC es un buen reflejo de su noción (filosófica) de "verdad".
