¿Cómo encajan las pruebas sobre la lógica en un marco lógico?

Las pruebas deductivas en lógica de primer orden son esencialmente transformaciones de un enunciado del lenguaje en otro. Se comienza con algún enunciado (o varios o ninguno) y luego se produce a partir de él una secuencia ordenada de nuevos enunciados derivados de las sucesivas aplicaciones de las reglas establecidas del sistema. Puede finalizar esta secuencia en cualquier momento y se dice que cualquier declaración nueva producida en este proceso ha sido "derivada" o "probada". Este proceso simple y altamente estructurado es la razón por la cual la demostración de teoremas puede automatizarse: las computadoras son realmente buenas para seguir reglas.

Las pruebas son colecciones de declaraciones en el sistema, y ​​las declaraciones sobre pruebas no son declaraciones en el sistema, son declaraciones en lenguaje natural (por ejemplo, inglés). Por lo tanto, las declaraciones en inglés sobre declaraciones en el sistema no están sujetas a las reglas del sistema y no viven dentro del sistema. Sin embargo, así como es posible decir si $2+2=4$ es correcto o incorrecto dentro del contexto de la aritmética sin usar la aritmética, uno puede determinar si una prueba es válida en el sistema sin usar el sistema para hacerlo. Esto se debe a que cualquier observador imparcial puede consultar el libro de reglas para ver si las reglas se siguieron correctamente o no.

Aquí está el problema: es razonable pensar que la lógica del sistema es también la lógica que usamos para analizar declaraciones sobre el sistema, pero ese simplemente no es el caso. Cuando analizamos el sistema, simplemente estamos revisando el libro de reglas, y las conclusiones que sacamos son objetivamente verdaderas o falsas. Aunque, un sistema diferente con un libro de reglas diferente podría llevar a una conclusión diferente.

Dicho esto, simpatizo con (lo que creo que es) su preocupación, a saber. "Estamos usando la lógica para analizar la lógica, entonces, ¿no es eso circular? ¿Cómo podemos usar la lógica antes de saber cómo funciona?" La respuesta es que la lógica intuicionista natural no se basa necesariamente en un sistema formal porque su verdad es evidente. Déjame ponerlo de esta manera: ¿Por qué crees en la aritmética? ¿Es porque ha estudiado las reglas y parecen internamente consistentes, o es porque sus conclusiones son patentemente obvias? 2 manzanas y 3 manzanas son 5 manzanas, ergo $2+3=5$. No caigas en la trampa de poner el carro delante del caballo. El sistema modela la realidad, no al revés. El modelo es imperfecto, pero usamos el sistema porque el modelo se alinea con nuestras intuiciones.

Como punto final, tomemos por ejemplo el Teorema de Incompletitud. El teorema es esencialmente una prueba de que el enunciado "Este enunciado no es demostrable". existe en el sistema de la aritmética. Esto es importante porque tal declaración es evidentemente verdadera (la alternativa, es decir, ser demostrable, sería una contradicción y, por lo tanto, es imposible), pero no se puede demostrar que sea verdadera (por su propia naturaleza). Sin embargo, su verdad no es obvia dentro de la aritmética ya que eso requeriría una prueba. Es solo dentro de nuestra comprensión intuitiva del significado de la declaración que podemos discernir que debe ser verdad independientemente de lo que el sistema pueda o no pueda decir.

Un sistema lógico formal nunca te dice lo que significa probar algo. Le dice lo que funciona en el modelo. El punto es que necesitas tener fe en que el modelo modela tu pensamiento real, y no otra cosa. De lo contrario, no puede usarlo para discutir la naturaleza del pensamiento.

Sin una prueba de un tipo más casual que las pruebas que usted va a discutir corresponden a nuestra comprensión ordinaria del significado real, no hay razón para el formalismo. Si no tenemos una fe realmente buena de que estamos representando de manera confiable los rudimentos del lenguaje, podemos probar todo tipo de cosas sobre sistemas y modelos, y eso realmente no dirá nada sobre la lógica.

Todo esto es parte del programa de formalismo de Hilbert para divorciar las matemáticas básicas de una interpretación platónica al demostrar que todo lo que realmente hace que la lógica funcione es un conjunto de reglas sobre la manipulación de símbolos. Pero para hacer eso, necesitaríamos encontrar un modelo de lógica que sea consistente y completo. Gödel demuestra que Hilbert está equivocado. No podemos tener tal sistema, si queremos incluir la aritmética en nuestro razonamiento.

Por lo tanto, el razonamiento debe tener una base fuera del método axiomático, para que tenga sentido y capture los límites de la argumentación. O necesita una referencia externa que le brinde una forma de argumentar las virtudes de ambos lados de varias afirmaciones indecidibles. O debe aceptar que los límites de la toma de decisiones se extienden más allá de lo que se puede establecer en un lenguaje preciso a través de una argumentación estricta.