Armonía lógica

La armonía lógica , término acuñado por Michael Dummett , es una propiedad de las reglas de inferencia que un sistema lógico dado puede satisfacer.

El lógico Gerhard Gentzen propuso que el significado de los conectores lógicos no necesita ser definido por un mundo externo a la lógica, sino que puede derivarse de las reglas para su uso dentro de la propia lógica. Por ejemplo, si uno cree que el cielo es azul y también cree que la hierba es verde , entonces puede introducir el conector " y " de la siguiente manera: "El cielo es azul Y la hierba es verde" . La idea de Gentzen era que tales reglas otorgan significado a las palabras, o al menos a los conectores lógicos. Esta idea también se ha asociado con la noción wittgensteiniana de que, en muchos casos, podemos decir que el significado es el uso . También se la conoce como semántica de roles inferenciales o inferencialismo.

En un sistema de deducción natural, cada conector lógico tiene dos tipos de reglas: las reglas de introducción y las reglas de eliminación . En este caso, y se introduce y elimina mediante las siguientes reglas:$${\displaystyle {\frac {P\quad Q}{P\land Q}},\quad {\frac {P\land Q}{P}},\quad {\frac {P\land Q}{Q}}}$$Arthur Prior señaló un problema aparente con esto : ¿Por qué no podemos tener una expresión (llamémosla " tonk ") cuya regla de introducción sea la de OR (de "p" a "p tonk q") pero cuya regla de eliminación sea la de AND (de "p tonk q" a "q")? Esto nos permite deducir cualquier cosa a partir de cualquier punto de partida. Prior sugirió que esto significaba que las reglas inferenciales no podían determinar el significado, es decir, el inferencialismo es falso. ^{[ 1 ]}

Nuel Belnap respondió que las reglas de introducción y eliminación pueden constituir significado, siempre que cumplan ciertas restricciones, como no permitirnos deducir nuevas verdades en el vocabulario antiguo. ^{[ 2 ] [ 3 ]}

El concepto de armonía formaliza esto. Las reglas de introducción y eliminación de un conector lógico están en armonía si, en cualquier demostración, las fórmulas máximas pueden eliminarse normalizando la demostración. Una fórmula máxima es aquella que se introduce y luego se elimina. La idea es que dichas fórmulas máximas se comportan de forma similar a los lemas y, si bien pueden facilitar la redacción y acortar la demostración, no son estrictamente necesarias. Una demostración normalizada solo debe introducir conectores lógicos y nunca eliminarlos.

La razón más profunda de tal demanda es que, idealmente, las reglas de introducción para un conector describen las condiciones que pueden justificar el conector. Por ejemplo,${\displaystyle A\land B}$se justifica dada una prueba de${\displaystyle A}$y una prueba de${\displaystyle B}$Por otro lado, las reglas de eliminación para un conector describen las condiciones que el conector puede justificar. Por ejemplo, una prueba de${\displaystyle A\land B}$justifica${\displaystyle A}$y también justifica${\displaystyle B}$La idea de armonía es que aquello que justifica un conector debe ser exactamente lo mismo que lo justifica. Esta es la idea principal del «Principio de Inversión» de Prawitz . ^{[ 4 ] [ 5 ]}

La aplicación de la armonía a la lógica matemática puede considerarse un caso particular del concepto filosófico. Resulta pertinente hablar de armonía no solo en relación con los sistemas inferenciales, sino también con los sistemas conceptuales de la cognición humana y con los sistemas de tipos en los lenguajes de programación.

La semántica de esta forma no ha supuesto un gran desafío para la esbozada en la teoría semántica de la verdad de Tarski , pero muchos filósofos interesados ​​en reconstituir la semántica de la lógica de una manera que respete el significado en el uso, según Ludwig Wittgenstein, han considerado que la armonía es la clave.

• armonía en la wiki de Greg Restall , Proof and Consequence (copia de archivo, julio de 2012)