Al probar afirmaciones en un sistema lógico, ¿utilizamos una “meta” lógica intuitiva o utilizamos las reglas de deducción del sistema?
Soy nuevo en el tema, pero actualmente estoy leyendo notas de clase sobre lógica proposicional y de predicados. Me interesa especialmente la frontera entre la lógica y el lenguaje. Por favor, corrija, si algunas de las cosas que digo aquí son incorrectas.
Uno puede hacer declaraciones sobre cualquier cosa imaginable en el mundo, y esta declaración (sea lo que sea una declaración en algún idioma) puede ser verdadera o falsa (o posible algo intermedio). Tenemos una comprensión intuitiva sobre la validez de algunas declaraciones que podemos hacer en un idioma, siempre que otras declaraciones ya sean verdaderas.
All cats live on earth.
Simon is a cat.
THEREFOR Simon lives on earth.
Entiendo los sistemas lógicos para formalizar este proceso de determinar la validez de una oración (sin importar si describe a un gato o alguna variedad) - corrígeme si me equivoco aquí.
AFAIK, cuando "inventamos" un sistema lógico, escribimos algunas definiciones (cómo se llaman ciertos objetos, por ejemplo, símbolos lógicos, predicados o fórmulas, o cuál es su estructura). Esto está bien para mí, porque las definiciones son solo un acuerdo sobre cómo llamar a algo. Mi cerebro es lo suficientemente poderoso como para vivir en un mundo donde llamo a los objetos que percibo como quiero llamarlos).
A continuación, escribo cómo se siguen las declaraciones verdaderas y falsas de las oraciones anteriores . Mi entendimiento actual también es que tengo que asumir estas reglas, no se pueden deducir de ningún metalenguaje o principio. Uno simplemente tiene que empezar por alguna parte. ¿Está bien?
En este punto, la mayoría de las notas de conferencias que encontré comienzan a hablar de cosas como la solidez, la integridad o la coherencia, y la equivalencia de las verdades sintácticas y semánticas. Y comienzan a sacar conclusiones sobre el sistema lógico.
Mi pregunta ahora es: para cualquier enunciado del sistema lógico que no sea una definición o una de las reglas de deducción del sistema lógico, ¿solo empleo las reglas de deducción del sistema lógico para probarlas, o tengo que hacerlo? ¿Usas algún tipo de meta lógica intuitiva (de la que hablé al principio) para probarlos?
Respuestas
Entiendo los sistemas lógicos para formalizar este proceso de determinar la validez de una oración (sin importar si describe a un gato o alguna variedad) - corrígeme si me equivoco aquí.
Estás en lo correcto. En particular, un sistema formal simplemente prescribe qué oraciones puede deducir. El sistema no atribuye ningún significado a los símbolos ni a las frases; simplemente le dice lo que puede deducir. Si quiere atribuirles algún significado, por supuesto que no puede hacerlo dentro de ese sistema, pero debe hacerlo fuera de él. En un sistema al estilo de Hilbert, las oraciones que se pueden deducir se prescriben utilizando la regla modus-ponens y los axiomas. Otros sistemas formales (como los sistemas estilo Fitch) tienen diferentes tipos de reglas de inferencia.
AFAIK, cuando "inventamos" un sistema lógico, escribimos algunas definiciones (cómo se llaman ciertos objetos, por ejemplo, símbolos lógicos, predicados o fórmulas, o cuál es su estructura).
Depende de lo que quieras decir exactamente con "sistema lógico". Si se refiere a "sistema fundamental", entonces lo que importa es que las pruebas sean verificables computablemente. Es decir, cada oración que puede ser probada por el sistema tiene ese testigo de probabilidad mediante una cadena (finita) llamada prueba, y hay un único programa de verificación de pruebas que da cualquier par de cadenas de entrada$(p,x)$ siempre se detendrá y su salida será "sí" si $p$ es una prueba válida sobre el sistema de sentencia $x$. Esta es la noción más general de sistema fundacional que los humanos puedan utilizar (hasta donde sabemos).
Tenga en cuenta que las teorías FOL con un conjunto de axiomas computablemente decidibles y un sistema deductivo adecuado están abarcadas por la noción anterior, al igual que todos los demás sistemas fundamentales que se han propuesto en la historia matemática, incluidas las teorías no clásicas y las teorías de tipos.
Sin embargo, si te refieres a un "sistema formal abstracto", como una teoría general de FOL (que quizás tenga un lenguaje o axiomas incontables o incontables), entonces necesariamente debes trabajar dentro de un meta-sistema (que llamaré MS de ahora en adelante ), incluso si no lo hace formalmente. Tenga en cuenta que la EM es invariablemente en sí misma un sistema fundamental según la noción anterior.
A continuación, escribo cómo se siguen las declaraciones verdaderas y falsas de las oraciones anteriores. Mi entendimiento actual también es que tengo que asumir estas reglas, no se pueden deducir de ningún metalenguaje o principio. Uno simplemente tiene que empezar por alguna parte. ¿Está bien?
Sí, estas son las reglas de inferencia que mencioné anteriormente. Pero no es tan exacto decir "cómo las declaraciones verdaderas y falsas se siguen de [...]". Recuerde, un sistema formal simplemente prescribe las reglas sintácticas y no existe la noción de "verdadero" o "falso". Solo puede asignar ese tipo de significado semántico desde el exterior, ya sea dentro de la EM o dentro del lenguaje natural en el mundo real.
Además, sí, las reglas y los axiomas no se pueden "deducir" en ningún sentido significativo. Si lo piensa con mucho cuidado, verá que hay conceptos fundamentales en lógica que no pueden definirse o justificarse de forma no circular, como esbozo en este artículo .
Para cualquier enunciado del sistema lógico que no sea una definición o una de las reglas de deducción del sistema lógico, ¿solo empleo las reglas de deducción del sistema lógico para probarlas, o tengo que usar algún tipo de intuición? meta lógica (de la que hablé al principio) para probarlos?
Esta parte realmente no tiene sentido. Según lo que dije anteriormente, dado cualquier sistema formal computable, ya sea una cadena$x$ es un teorema (es decir, una oración probada) sobre el sistema o no es definitivamente verdadero o falso (si podemos o no averiguar cuál es), y esto es simplemente si hay o no una prueba $p$ de modo que el verificador de pruebas de ese sistema emite "sí" en la entrada $(p,x)$. No importa si puede averiguar si tal$p$ existe, o si puede resolver esto pero no puede encontrar tal $p$o cómo te las arreglas para encontrar $p$(si lo haces). Incluso si usa un razonamiento incorrecto y la posibilidad de tal$p$, puede ejecutar el verificador de pruebas y confirmar que de hecho es una prueba de $x$. La prueba se mantiene independientemente de cómo la obtenga.
Sin embargo, quizás lo que está preguntando es cómo sabemos que un sistema formal es significativo . Bueno, puedes saludar con la mano y decir que parece bueno, o tal vez puedas decir algo como "demuestra teoremas que parecen verdaderos cuando se interpretan de esta manera en particular en el mundo real", por lo que incluso está respaldado empíricamente, como se menciona en el segundo parte de este post sobre axiomatización de naturales .
O puede trabajar en MS y demostrar que un sistema formal $S$es sonido , para alguna definición de "sonido" que define dentro de MS. Es decir, si usted y otra persona están de acuerdo en que la EM elegida es significativa, puede proceder a buscar una prueba de alguna oración sobre la EM que$S$ es sonido, donde "sonido" es una propiedad que puede expresar dentro de la EM.
Por ejemplo, puede probar (dentro de MS) que FOL es sólido, lo que significa que dada cualquier estructura de primer orden $M$ y cualquier conjunto $A$ de oraciones sobre $M$ que son verdad en $M$ (Las estructuras de FOL, las oraciones y la verdad también se definen dentro de la EM), cada oración que se puede probar a partir de $A$ el uso de un sistema deductivo para FOL también es cierto en $M$.
Para otro ejemplo, puede definir la solidez aritmética de un sistema formal $S$ como propiedad de que hay una traducción $t$ a partir de oraciones aritméticas (es decir, oraciones en el lenguaje de PA) de modo que, para cada oración aritmética $Q$, Si $S$ prueba $t(Q)$ luego $Q$ es cierto en $(\mathbb{N},0,1,+,·,<)$ (por supuesto, esta estructura también se construye dentro de MS).
Podría preguntarse, ¿cómo podemos saber que nuestra EM elegida en sí es significativa? No podemos saber de forma no circular, como se mencionó anteriormente. Tampoco podemos hablar de su solidez en términos absolutos. Pero para cualquier MS razonable tenemos una traducción de oraciones aritméticas (porque queremos que MS pueda realizar un razonamiento aritmético básico), por lo que al menos podemos hablar sobre si MS es aritméticamente inconsistente, es decir, si demuestra$t(0=1)$. Esa es una pregunta bien definida, ¡y esperamos que la EM no lo haga! Pero como demostró esencialmente Godel-Rosser, cualquier MS razonable ni siquiera puede probar que es aritméticamente consistente, a menos que sea en realidad aritméticamente inconsistente ... (Este es el teorema de la incompletitud).
Por último, señalaré que la mayoría de los textos lógicos utilizan un MS razonablemente potente como ZFC o al menos ZC. Esto se debe a que quieren probar cosas como el teorema de compacidad para FOL incluso para teorías incontables, y esto necesita un poco de supuestos de teoría de conjuntos. Pero si solo desea probar hechos sobre teorías contables, es posible que pueda arreglárselas con una EM mucho más débil como ACA (consulte esta publicación ).
Podrías pensar en la lógica, por ejemplo, la lógica de primer orden / predicado, como un juego que juegas para producir nuevas proposiciones. Como cualquier juego, necesitas empezar en alguna parte; necesitas piezas iniciales y reglas básicas, por así decirlo. En el caso de Predicate, las piezas iniciales son las proposiciones, construidas a partir de constantes, variables, cuantificadores, predicados y operadores lógicos. Las "reglas del juego" son entonces las reglas de inferencia / deducción. No son dadas por Dios ni son evidentes por sí mismas, es decir, no son canónicas ; las personas eligen las reglas con las que jugar basándose en sus metas y creencias (cf. deducción natural vs cálculo secuencial vs sistema de Hilbert). Como ejemplo, algunas personas permiten que Predicado tenga la Ley del Medio Excluido, mientras que muchas otras la rechazan. En un sistema del primer tipo habrá proposiciones que se siguen de manera no constructiva de los axiomas, mientras que en el segundo podría no haberlo (porque, por ejemplo, un argumento para Q de la forma$(P \vee \neg P) \Rightarrow Q,\, \therefore Q$ podría no agotar todos los casos en $P$).
Entonces, en resumen, como jugar un juego, debe usar las reglas de inferencia establecidas, en cualquier tipo de proposiciones permitidas, para producir nuevas proposiciones que el sistema (Predicado, por ejemplo) acepta / reconoce. De hecho, hay muchas gamificaciones de la lógica que hacen que lo que dije sea bastante literal, una de las cuales está aquí .
Editar (Para abordar mejor la pregunta de si uno solo debe usar los axiomas al producir teoremas): podría "romper las reglas", por así decirlo, y usar una declaración de teorema / no axiomático para "probar" las cosas, pero puede No se puede garantizar que sea una regla de inferencia válida a menos que la acepte como tal o la deduzca posteriormente de los axiomas. Esto condujo, por ejemplo, a la adopción del axioma de elección en el sistema ZF de la teoría de conjuntos (creando ZFC) porque muchas "pruebas" implicaban funciones de elección cuya existencia no podía garantizarse.