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 quizás incluyendo?) el primer orden es lo suficientemente poderosa 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/superior? ¿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 o comprensible, pero pido disculpas si no es así. Si alguien pudiera darme 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.

   Puedes 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

1. Sí, hay ventajas y desventajas en donde el equilibrio se encuentra entre el número de reglas de inferencia y el número de axiomas de la definición de una lógica. Como Francois Dorais dice en su respuesta, depende de lo que quieras hacer con la lógica.

2. Todas las lógicas de representación de pruebas, incluyendo la lógica proposicional. El más alto es el orden de la lógica, la más poderosa es en el sentido de su lenguaje más expresivo y su deducción ser más general.

3. El criterio que determina el orden de la lógica se relaciona con el tipo de valor que puede ser cuantificado. En un cero de orden de la lógica, no son sólo los valores y la cuantificación no es compatible (por ejemplo, lógica proposicional, donde los valores son valores booleanos). En una lógica de primer orden, hay funciones que son distintos de los valores; sólo los valores pueden ser cuantificados (por ejemplo, de primer orden de la lī ogica, natural de número de la aritmética). En un segundo orden de la lógica, las funciones pueden tomar de primer orden de las funciones como argumentos, y de primer orden de las funciones pueden ser cuantificados. En un tercer orden de la lógica, de segundo orden de las funciones pueden ser ellos mismos argumentos a funciones y ser cuantificados, etc, etc. En un orden superior de la lógica (esto es un claro concepto de el concepto de un enésimo orden de la lógica), no existe una distinción fundamental entre las funciones y los valores, y todas las funciones pueden ser cuantificados.

   Tenga en cuenta que el uso de los predicados pueden ser considerados como equivalentes para el uso de conjuntos (algunos predicado devuelve "true" para un valor dado puede ser considerado como equivalente al valor de un elemento de un conjunto). Tenga en cuenta también que una determinada lógica puede o no puede distinguir fundamentalmente entre los valores generales y valores booleanos, y entre las funciones y predicados (funciones que devuelven un valor booleano).

4. Gödel (Primera) Teorema de la Incompletitud se refiere sólo a las lógicas capaces de, al menos, que expresan número natural aritmética - cualquier lógicas son incompletos (a menos que sean incompatibles, en cuyo caso son trivialmente completa). Su Segundo Teorema de la Incompletitud se refiere a si tales lógicas son capaces de demostrar su propia consistencia.

   La ventaja de los menos potentes lógica es que es más fácil a la razón, y que se tiende a ser más fácil para escribir algoritmos para, en el sentido de que (dependiendo de lo que el algoritmo es la intención de hacer) estos algoritmos tienden a ser más completa y/o eficiente y/o para terminar (por ejemplo, los algoritmos para la comprobación de las declaraciones en la lógica). La ventaja de una más potente, la lógica es que es más expresivo y por lo tanto capaz de representar y/o de demostrar más de las matemáticas.

   Hay ciertamente de orden superior lógicas que no son capaces de expresar la totalidad de las matemáticas hoy en día (por ejemplo, no es capaz de expresar plenamente la categoría de teoría). Me temo que no sé lo suficiente como para decir si hay/no formal de la lógica que son capaces de expresar todos los de la matemática contemporánea.

5. Tipo de teoría es el estudio de los sistemas de tipo. Presumiblemente, su pregunta se refiere a la finalidad de la utilización de un tipo de sistema en una lógica formal? (Disculpas si me dieron el extremo equivocado del palo.)

   Si es o no una lógica utiliza un tipo de sistema es otro de los fundamentales distinguir atributo entre lógicas. La alternativa es la base de la lógica en la teoría de conjuntos. De cualquier manera, la lógica debe de alguna manera evitar problemas de coherencia, como la Paradoja de Russell que expone la inconsistencia de Frege de la lógica formal, o la Kleene-Rosser Paradoja que expone la inconsistencia de la Iglesia original del cálculo lambda.

   El propósito de un tipo de sistema es la imposición adicional de la correcta forma de restricciones en un lenguaje formal, además de las restricciones impuestas por el lenguaje de sintaxis. Esta es una manera de garantizar que las paradojas pueden ser evitados, así como una manera práctica de ayudar a que el usuario de una lógica de evitar escribir declaraciones sin sentido (como "el número 5 es un espacio vectorial"). Russell inventaron tipo de teoría para resolver el problema planteado por su propia paradoja. La iglesia utiliza el tipo de teoría que venir para arriba con una alternativa, consistente cálculo lambda.

Answer 3

"¿Cuáles son las ventajas/desventajas de la utilización de menor/mayor orden formal de la lógica?"

Parece que el "fuerte" de la lógica no son tan bien educados como de primer orden de la lógica. Por Lindstrom del teorema, FOL es el más fuerte de la lógica, que cumple tanto el Lowenheim-Skolm teorema de abajo a Aleph0 y el teorema de compacidad (decimos que una lógica L1 es más fuerte que el L2 cuando cada clase de primaria de una teoría de la L2 es también en clase de primaria para una teoría de la L1). Como la compacidad de la propiedad y el LS de la propiedad son esenciales para muchos de importantes construcciones en el modelo de la teoría, parece que es mucho más difícil desarrollar el modelo de la teoría más fuerte de la lógica.

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