Lógica proposicional, lógica de primer orden y lógica de orden superior

Question

He estado leyendo un poco sobre los fundamentos de la lógica formal, y he acumulado algunas preguntas en el camino. Soy un completo principiante en este campo, así que agradecería mucho si alguien pudiera aclarar algunos de estos puntos.

1. Una lógica proposicional completa (y consitente) puede definirse de varias maneras, según tengo entendido, que son todas equivalentes. He oído que puede definirse con un axioma y múltiples reglas de inferencia o con múltiples axiomas y una única regla de inferencia (por ejemplo, Modus Ponens) - o en algún punto intermedio. ¿Hay alguna ventaja o desventaja en cualquiera de los dos casos? ¿Cuál es más convencional?

2. La lógica proposicional (de orden zerótico) es simplemente capaz de hacer y verificar enunciados lógicos. Las lógicas de primer orden (y de orden superior) pueden representar pruebas (o complejidad jerárquica creciente) - verdadero/falso, ¿y por qué?

3. Cuál es exactamente la relación entre una lógica de orden n y una lógica de orden (n+1)th, en general. Aquí sería deseable una notación matemática explicativa, siempre que no sea también avanzada.

4. Cualquier lógica formal por encima de (¿o tal vez incluyendo?) el primer orden es lo suficientemente potente como para que el Teorema de Incompletitud de Godel la convierta en inconsistente o incompleta - ¿cierto/falso? ¿Cuáles son las ventajas/desventajas de utilizar lógicas formales de orden inferior/mayor? ¿Existe un límite inferior en el orden de la lógica necesario para demostrar todas las matemáticas conocidas hoy en día, o en teoría habría que utilizar una lógica de orden arbitrariamente alto?

5. ¿Qué papel desempeña la teoría de tipos en la lógica formal? ¿Es simplemente una forma de describir la lógica de enésimo orden en una teoría consolidada (pero ortogonal a la propia lógica formal), o es alguna generalización de la lógica formal que lo explica todo por sí misma?

Espero haber formulado estas preguntas de forma vagamente significativa/comprensible, pero pido disculpas si no es así. Si alguien pudiera proporcionarme algunos detalles sobre los distintos puntos sin asumir demasiados conocimientos previos de los campos, sería estupendo. (Soy un estudiante de Física de grado, con una formación en gran medida en los métodos matemáticos y los fundamentos del análisis matemático, si eso ayuda).

Answer 1

Esta es una larga lista de preguntas. Todas están relacionadas hasta cierto punto, pero podría considerar dividirla en preguntas separadas la próxima vez.

1. Los teóricos de la prueba tienden a preferir sistemas con muchas reglas y pocos axiomas, como los sistemas de deducción natural y los sistemas de Gentzen. La razón es que son mucho más fáciles de manipular y visualizar. (Véase el enunciado y la demostración del Teorema de la Eliminación del Corte para un ejemplo ilustrativo). Los teóricos del modelo tienden a preferir muchos axiomas y sólo modus ponens, como los sistemas de Hilbert. La razón es que la semántica de tales sistemas es fácil de manejar, y la semántica es lo que realmente importa a los teóricos del modelo.

2. La verdadera diferencia entre la lógica proposicional y la de primer orden es la cuantificación. Los cuantificadores son naturalmente más expresivos que las conectivas lógicas.

3. Hay muchos, muchos sabores de la lógica de orden superior. Las dos clasificaciones principales son los sistemas basados en conjuntos y los sistemas basados en funciones. Hay variantes que no encajan realmente en esta división y hay variantes que mezclan ambas. Con una combinatoria interna suficientemente fuerte, todos ellos son equivalentes.

   El sistema basado en conjuntos tiene un conjunto A de objetos de tipo 0, que se consideran atómicos. Los objetos de tipo 1 son elementos de los conjuntos de potencias ℘(A n ). Cuando la teoría base tiene una función de emparejamiento interna (como la aritmética y la teoría de conjuntos), el exponente n puede eliminarse. Entonces, los objetos de tipo 2 son elementos del segundo conjunto de potencias ℘(℘(A)), y de forma similar para los tipos superiores. Los tipos superiores basados en conjuntos son algo inconvenientes sin una función de emparejamiento interna.

   Los sistemas basados en funciones son similares, con funciones A n →A como tipo 1. De nuevo, con una función de emparejamiento interna, los tipos superiores se racionalizan a A → A, (A → A) → A, ((A → A) → A) → A, etc. Sin embargo, es habitual utilizar tipos más complejos en estos sistemas.

4. Cuidado con la lectura del Teorema de Incompletitud de Gödel. Para la lógica de primer orden, las hipótesis establecen que la teoría en cuestión debe ser recusablemente enumerable y que debe ser lo suficientemente potente como para interpretar una cantidad razonable de aritmética. Son hipótesis importantes. (Y explican por qué no existe tal teorema para la lógica proposicional.) Hay muchas variantes para los sistemas de orden superior, pero hay que ser aún más cuidadoso al enunciarlas.

   Puede apreciar la diferencia entre los distintos niveles de la lógica de orden superior leyendo sobre Teoremas de aceleración de Gödel .

   La mayor parte de las matemáticas actuales se basan en la teoría de conjuntos, al menos en un sentido teórico. En la teoría de conjuntos, los tipos superiores se interpretan internamente mediante conjuntos de potencias y conjuntos de funciones. También se extienden transfinitamente y esta jerarquía transfinita de tipos superiores se mostró necesaria para demostrar teoremas muy bajos en la jerarquía, como Teorema de determinación de Borel de Martin .

5. Tal vez quiera seguir leyendo lógica categórica .

Answer 2

" ¿Cuáles son las ventajas/desventajas de utilizar lógicas formales de orden inferior/superior?"

Parece que las lógicas "fuertes" no se comportan tan bien como la lógica de primer orden. Según el teorema de Lindstrom, FOL es la lógica más fuerte que satisface tanto el teorema de Lowenheim-Skolm hasta Aleph0 como el teorema de compacidad (decimos que una lógica L1 es más fuerte que L2 cuando cada clase elemental de una teoría de L2 es también una clase elemental para una teoría de L1). Como la propiedad de compacidad y la propiedad LS son cruciales para muchas construcciones importantes en la teoría de modelos, parece que es mucho más difícil desarrollar la teoría de modelos para las lógicas más fuertes.

Answer 3

1. Sí, hay ventajas/desventajas en el equilibrio entre el número de reglas de inferencia y el número de axiomas cuando se define una lógica. Como dice François Dorais en su respuesta, depende de lo que se quiera hacer con la lógica.

2. Todas las lógicas sirven para representar pruebas, incluida la lógica proposicional. Cuanto más alto es el orden de la lógica, más potente es en el sentido de que su lenguaje es más expresivo y su deducción más general.

3. El criterio que determina el orden de una lógica está relacionado con los tipos de valor sobre los que se puede cuantificar. En una lógica de orden cero, sólo hay valores y no se admite la cuantificación (por ejemplo, la lógica proposicional, donde los valores son booleanos). En una lógica de primer orden, hay funciones que son distintas de los valores; sólo se puede cuantificar sobre los valores (por ejemplo, la lógica de predicados de primer orden, la aritmética de números naturales). En una lógica de segundo orden, las funciones pueden tomar como argumentos funciones de primer orden, y las funciones de primer orden pueden cuantificarse sobre ellas. En una lógica de tercer orden, las funciones de segundo orden pueden ser a su vez argumentos de funciones y ser cuantificadas sobre ellas, etc., etc. En una lógica de orden superior (este es un concepto distinto del concepto de lógica de enésimo orden), no hay distinción fundamental entre funciones y valores, y todas las funciones pueden ser cuantificadas sobre.

   Obsérvese que el uso de predicados puede considerarse equivalente al uso de conjuntos (algún predicado que devuelva "verdadero" para un valor dado puede considerarse equivalente a que el valor sea un elemento de algún conjunto). Obsérvese también que una lógica dada puede o no distinguir fundamentalmente entre valores generales y valores booleanos, y entre funciones y predicados (funciones que devuelven un valor booleano).

4. El (Primer) Teorema de Incompletitud de Godel sólo se refiere a las lógicas capaces de expresar al menos la aritmética de los números naturales -cualquier lógica de este tipo es incompleta (a menos que sea inconsistente, en cuyo caso es trivialmente completa). Su Segundo Teorema de Incompletitud se refiere a si tales lógicas son capaces de demostrar su propia consistencia.

   La ventaja de una lógica menos potente es que es más fácil de razonar, y que tiende a ser más fácil escribir algoritmos para ella, en el sentido de que (dependiendo de lo que el algoritmo esté destinado a hacer) estos algoritmos tenderán a ser más completos y/o eficientes y/o a terminar (por ejemplo, algoritmos para demostrar declaraciones en la lógica). La ventaja de una lógica más potente es que es más expresiva y, por tanto, capaz de representar y/o demostrar más matemáticas.

   Ciertamente, hay lógicas de orden superior que no son capaces de expresar toda la matemática actual (por ejemplo, no son capaces de expresar completamente la teoría de categorías). Me temo que no sé lo suficiente como para decir si hay/no hay lógicas formales que sean capaces de expresar toda la matemática contemporánea.

5. La teoría de tipos es el estudio de los sistemas de tipos. Es de suponer que su pregunta se refiere al propósito de utilizar un sistema de tipos en una lógica formal. (Pido disculpas si me he equivocado de tema).

   El hecho de que una lógica utilice o no un sistema de tipos es otro atributo distintivo fundamental entre las lógicas. La alternativa es basar la lógica en la teoría de conjuntos. De cualquier manera, la lógica debe evitar de alguna manera los problemas de consistencia, como la Paradoja de Russell que expuso la inconsistencia de la lógica formal de Frege, o la Paradoja de Kleene-Rosser que expuso la inconsistencia del cálculo lambda original de Church.

   El propósito de un sistema de tipos es imponer restricciones adicionales de buena forma en un lenguaje formal, además de las restricciones impuestas por la sintaxis del lenguaje. Es una forma de garantizar que se eviten las paradojas, así como una forma práctica de ayudar al usuario de una lógica a evitar escribir declaraciones sin sentido (como "el número 5 es un espacio vectorial"). De hecho, Russell inventó la teoría de tipos para resolver el problema planteado por su propia paradoja. Church utilizó la teoría de tipos para idear un cálculo lambda alternativo y consistente.

Answer 4

Los artículos de Wikipedia sobre la lógica de primer y segundo orden son bastante buenos. El artículo sobre la lógica de segundo orden cita un artículo de Väänänen que también es informativo: http://www.math.ucla.edu/~asl/bsl/0704/0704-003.ps