Implicación Introducción formulada como un teorema?

Mientras hacía una lista de las reglas de inferencia para mis estudiantes de matemáticas, encontré esta lista en Wikipedia:

ingrese la descripción de la imagen aquí

Noté un patrón: para cada regla de introducción , parece haber una regla de eliminación , y viceversa. Por ejemplo, lo que corresponde a la introducción de la conjunción es la eliminación de la conjunción, y lo que corresponde a la introducción de la disyunción es la eliminación de la disyunción.

Me preguntaba si Modus Ponens, que afirma ((P⇒Q)∧P)⇒Q, seguía este patrón. Noté que su artículo de Wikipedia se refería a Modus Ponens como "eliminación de implicación", así que me pregunté si existía otra tautología o teorema conocido como introducción de implicación . Aunque no existe una página en Wikipedia para la "introducción de implicaciones", una búsqueda en Google devolvió esta declaración , formulada en notación secuencial como

(P ⊢ Q) ⊢ (P ⇒ Q)

Es una declaración curiosa, ya que una vez escrita en forma tautológica, parece decir que (P⇒Q)⇒(P⇒Q).

¿He traducido correctamente el enunciado de la notación secuencial a la forma tautológica ? Si es así, el teorema resultante, (P⇒Q)⇒(P⇒Q), me parece bastante trivial. Ciertamente es verdad; Al igual que la eliminación de implicación se puede probar usando una tabla de verdad para mostrar ((P⇒Q)∧P)⇒Q es una tautología, también se puede verificar usando una tabla de verdad que (P⇒Q)⇒(P⇒Q) es una tautología. Sin embargo, debo estar perdiendo lo que hace que esta declaración sea interesante, ya que me parece tan trivial como decir A⇒A.

Tal vez traduje mal la declaración de la notación secuencial a la forma tautológica. La página web mezcla dos símbolos diferentes para la implicación. La definición de "implicación" ⇒ que aprendí es el único conectivo funcional veritativo caracterizado por sus valores booleanos (o tabla de verdad). Es decir, ⇒ es la única función que asigna P y Q a (1,0,1,1):

ingrese la descripción de la imagen aquí

Dado que esta definición de ⇒ es única, ¿qué significaría el otro símbolo de implicación como conectivo veritativo-funcional? ¿Tendría una tabla de verdad diferente? Y, cuando traduje la regla de inferencia de la notación secuencial a la forma tautológica, ¿fue correcto reemplazar todas las instancias de ⊢ con ⇒?

Finalmente, tengo curiosidad por qué la introducción de implicación no se incluye con las otras reglas de inferencia en la tabla de Wikipedia. ¿Hay algo fundamentalmente diferente en este resultado, tal vez su uso de la implicación del torniquete, que hace que este teorema sea de un tipo fundamentalmente diferente a los demás? ¡Gracias por tus pensamientos!

Consulte Deducción natural para conocer la fuente de la formulación simétrica de las reglas de introducción y eliminación.
La regla de introducción es de Γ, A ⊢ B a Γ ⊢ A→B, donde ⊢ significa "deriva lógicamente", consulte la notación de cálculo secuencial . Si desea una simetría completa entre las reglas de introducción y eliminación, la lógica clásica no la tiene, el cálculo secuencial simétrico proporciona una lógica intuicionista .
¡Gracias, @Conifold! Como seguimiento, ¿el símbolo del torniquete ⊢ aquí tiene el mismo significado que el símbolo de vinculación ⊨ o se usan de manera diferente? filosofía.stackexchange.com/questions/12816/…
A menudo se usan indistintamente, pero cuando se distinguen, ⊨ es una consecuencia semántica ("tabla de verdad") y ⊢ es una consecuencia deductiva (teórica de prueba). La diferencia depende de cuestiones sutiles sobre declaraciones "verdaderas pero no demostrables". En cálculo secuencial , la consecuencia deductiva es más natural.
Una introducción de implicación en "forma tautológica" debe ser Q⇒(P⇒Q).

Respuestas (2)

Los dos símbolos diferentes en la página a la que se vincula son de hecho diferentes. El primero es el símbolo del torniquete Ⱶ que puede leerse como 'prueba', mientras que la flecha → es una implicación material. Estos son muy diferentes. La implicación material es un símbolo en el lenguaje objeto definido por la tabla de verdad que proporciona, es decir, T/F/T/T. Torniquete es un símbolo en el metalenguaje que se puede leer como P demuestra Q, o Q es un teorema sobre P.

La regla de introducción condicional puede entenderse en el sentido de que si Q es un teorema sobre P, entonces P → Q es un teorema. Más generalmente, podría escribirse así: si Γ es un conjunto de proposiciones, entonces de Γ,P Ⱶ Q, uno puede deducir Γ Ⱶ P → Q. Si Γ junto con P prueba Q, entonces Γ prueba que P implica materialmente P. Esto se llama el teorema de la deducción.

En la deducción natural, podemos usar la regla de la prueba condicional con el mismo efecto. Puede asumir cualquier P que desee, proceder a demostrar Q a partir de ella y luego descartar la suposición para introducir la implicación material P → Q.

En cuanto a las constantes lógicas que tienen sus correspondientes reglas de introducción y eliminación, esto no es casualidad. En el sistema de Fitch, las constantes lógicas están especificadas por estas reglas. La idea de reglas armoniosas de introducción y eliminación fue presentada por Gerhard Gentzen y adoptada por varios otros. La idea es que las reglas I y E correspondientes sean 'inversas' entre sí, para garantizar que no tengan consecuencias ingobernables. En un famoso artículo de 1960, Arthur Prior ("The Runabout Inference Ticket" Analysis 21: 38-9) mostró que definir constantes lógicas sin restricciones podría permitirle probar cualquier cosa.

Esta relación inversa entre las reglas I y E se llama armonía lógica. Michael Dummett argumentó que la lógica clásica no tiene una forma armoniosa de definir las reglas para la negación, mientras que la lógica intuicionista sí, aunque esto ha sido discutido. Si desea continuar con más información sobre la armonía lógica, estos documentos pueden ser útiles:

Steinberger, F. (2011) “Lo que la armonía pudo y no pudo ser”. Revista de Filosofía de Australasia 89: 617-639. Rumfitt, Ian (2016) “Contra la armonía”. Próximamente en Robert Hale, Crispin Wright y Alexander Miller, eds., The Blackwell Companion to the Philosophy of Language, 2ª edición. Oxford: Blackwell.

Creo que ambos documentos se pueden encontrar en philpapers.org.

¡Muchas gracias por la explicación! Entonces, si entiendo esto (corríjame si me equivoco), porque el secuente "→I" (introducción de implicación) involucra símbolos (es decir, el torniquete ⊢) del metalenguaje, por lo tanto, →I no puede ser formulado en términos de un teorema/tautología en el lenguaje objeto matemático? ¿Está bien?
Entonces, parecería que NO hay un resultado de introducción de implicación que sea demostrable dentro del lenguaje objeto como todos los demás resultados de introducción/eliminación, ¿correcto? Y por lo tanto, diríamos que no hay una forma "armoniosa" de definir las reglas I/E para la implicación, ya que →E es demostrable en el lenguaje objeto pero →I no lo es, ¿es correcto?
Las reglas I y E para la implicación material se consideran comúnmente armoniosas, aunque estoy de acuerdo con usted en que la regla I es una rareza, porque se refiere al operador de implicación metalingüística, mientras que otras reglas I no lo hacen. Habiendo dicho eso, podría decirse que la armonía es un criterio demasiado fuerte para lidiar con el problema de la inferencia vagabunda de Prior. Todo lo que necesitamos es que una constante lógica se comporte de tal manera que sea conservadora con respecto a lo que implica. El artículo de Ian Rumfitt que mencioné en la respuesta es bueno en este punto.

Lo que podría considerarse como introducción de implicación, →I , a veces se llama prueba condicional o CP .

La estrategia básica es asumir el antecedente y derivar el consecuente. Una vez que se deriva el consecuente, la suposición puede descartarse. Aquí hay un ejemplo:

{1} 1. (P ∨ Q) → R Prem.
{2} 2. P Suponer.
{2} 3. P ∨ Q 2 ∨I (derecha)
{1,2} 4. R 1,3 PM
{1} 5. P → R 2,4 CP

El antecedente se supone en la línea 2 y el consecuente se deriva en la línea 4. Esto cumple las condiciones para → Introducción o CP en la línea 5.

Con este sistema particular de prueba, los números de dependencia se enumeran a la izquierda. Dondequiera que aparezca el número {2} , eso significa que el número de línea correspondiente depende de la suposición hecha en la línea 2. Observe que una vez que se introduce la implicación, el número de dependencia de la suposición se descarga. Puede ver que la conclusión se basa solo en {1} , que es la premisa.

El otro símbolo:

El artículo de Wikipedia dice:

La regla modus ponens se puede escribir en notación secuencial:

PAG → Q, PAG ⊢ Q

donde ⊢ es un símbolo metalógico que significa que Q es una consecuencia sintáctica de P → Q y P en algún sistema lógico;

El otro símbolo es un torniquete y funciona de manera análoga al símbolo de implicación, pero pertenece a un sistema separado de lógica o metalógica . El torniquete indica que un argumento indicado es sólido y, dado que funciona como una implicación, todas las premisas de un argumento junto con la conclusión se pueden reescribir utilizando la notación lógica normal para formar una tautología.

Como mencioné en mi comentario, la relación expresada por ((A & (A → B)) → B) es el principio que rige tanto la introducción como la eliminación, por lo que la misma tabla de verdad es válida para ambas.

Muchas gracias por tu respuesta. Sin embargo, deja un par de mis preguntas aún sin respuesta... Por ejemplo, ¿cómo se escribiría esta introducción de implicación como un teorema/tautología? ¿Se formularía el enunciado como (P⇒Q)⇒(P⇒Q)? Quiero poder probar el resultado; hasta ahora he podido demostrar todas las demás reglas de inferencia mediante la tabla de verdad.
La relación expresada por la tautología (A & (A → B) → B) es el principio que rige tanto la introducción como la eliminación, por lo que la misma tabla de verdad es válida para ambas. Edité mi respuesta para abordar su pregunta sobre el otro símbolo de implicación, que es un torniquete e indica la solidez del argumento en metalógica.
Implicación Introducción formulada como un teorema?
RespuestasAquíPolítica de privacidad1y, 0v