Podría haber una disculpa por hacer otra pregunta sobre los requisitos previos, pero estaba confundido acerca de los puntos de partida. Me he encontrado con varios términos como "Lógica modal", "Lógica temporal", "Lógica de primer orden", "Lógica de segundo orden" y "Lógica de orden superior".

¿Qué significa exactamente "Lógica" en este contexto? ¿Cómo definimos rigurosamente la palabra "lógica"?

Después de pasar por las páginas iniciales de algunos libros, puedo concluir aproximadamente que una "lógica es una forma de decidir qué sigue a partir de qué y es importante en el diseño de lenguajes de programación, ya que dicta y facilita el diseño de programas para razonar y comprender programas automáticamente. Quiero comprender el segundo punto de una manera un poco elaborada.

Ahora llegando a estas lógicas.

¿Todas estas lógicas, "Lógica temporal", "Lógica modal", "Lógica de primer orden", "Lógica de orden superior" son independientes unas de otras o necesitamos entender algunas de estas lógicas para entender algunas otras en este grupo? En pocas palabras, ¿cuáles serán los requisitos previos para ellos? (Será genial si puedo obtener sugerencias sobre algunos materiales también).

PD: Muchas gracias por tu amabilidad

Fundamentalmente, una lógica consta de dos cosas.

• La sintaxis es un conjunto de reglas que determinan qué es y qué no es una fórmula.
• La semántica es un conjunto de reglas que determinan qué fórmulas son "verdaderas" y cuáles son "falsas". Para un teórico de modelos , esto se expresa relacionando fórmulas con las estructuras matemáticas en las que son verdaderas; para un teórico de la prueba , la verdad corresponde a la demostrabilidad de un conjunto elegido de axiomas con un conjunto elegido de reglas de prueba (técnicas).

La diferencia entre diferentes lógicas está, más simplemente, en la elección de la sintaxis y la semántica. La mayoría de las lógicas son extensiones de lógica proposicional o lógica de primer orden . En cierto sentido, puede ver estas extensiones como "agregar más funciones" a la lógica. Por ejemplo, la lógica temporal trata con verdades que pueden variar con el tiempo.

En general, estas características podrían expresarse en una lógica más simple, a costa de tener que escribir fórmulas más largas. Por ejemplo, el concepto temporal "  es verdadero desde este punto por la eternidad" se puede expresar de una manera de primer orden agregando un parámetro de tiempo a todas sus proposiciones y diciendo "Para todos los tiempos  , si  es mayor o igual que a la hora actual, entonces  es verdadero en el tiempo  ". En cierto sentido, puede pensar en estas lógicas como agregar bibliotecas a un lenguaje de programación básico para que pueda decir las cosas más fácilmente.$\varphi$$t$$t$$\varphi$$t$

Dado que casi todas las lógicas se basan en una lógica proposicional y de primer orden, recomiendo aprender primero sobre ellas.

Mientras que campos como la informática, las matemáticas y la física están relativamente bien organizados, la lógica tiene una historia caótica. Su organización es realmente confusa, así que creo que es importante leer algo de historia para comprender la estructura densa del campo.

El camino que debe elegir dependerá de sus antecedentes y objetivos .

¿Qué es una lógica?

1. El punto de vista tradicional dice que una lógica es un sistema formal con un lenguaje formal (sintaxis), una semántica (significado externo, pensar en intérpretes de programas) y un conjunto de reglas para deducir declaraciones de otros (piense en las reglas de reducciones de programas). Una lógica se ve puramente como un simple objeto matemático.

2. El punto de vista moderno, dice, a través del famoso isomorfismo de Curry-Howard de que una lógica es un sistema de tipos coherente (las pruebas son programas y los tipos son fórmulas). Más precisamente: un sistema de reglas de inferencias que disfruta del teorema de eliminación de cortes y el teorema de la confluencia / teorema de Church-Rosser que implica que el sistema de programación subyacente se comportará bien.

3. Sobre las órdenes, la lógica proposicional puede verse como un sistema de orden 0 (digamos que las variables para las proposiciones se observan ). Se comportan como una función sin argumentos (constantes).$p, q$

   • Cuando pasamos a la lógica de primer orden, las variables para proposiciones se convierten en variables de predicados y toman un objeto como argumento , . Se comportan como funciones que toman objetos (pares, enteros, cadenas) son argumentos. Piensa en el lenguaje C.$P, Q$$P(x_1, ..., x_n)$$Q(x_1, ..., x_n)$
   • En la lógica de segundo orden, la variable para predicados se convierte en una especie de funciones que toman las de primer orden. Se comportan como funciones que toman funciones de primer orden como argumento. Por ejemplo, podemos tener predicados y cuantificación sobre predicados.
   • El mismo razonamiento para el tercer orden, etc. Las lógicas de orden superior aceptan cualquier orden. Piense en Haskell y OCaml que tienen funciones que toman funciones de funciones de funciones, etc. como argumento.

4. En general, no hay consenso sobre qué es una lógica en realidad. Algunos filósofos usan sistemas que no tienen un sistema de programación subyacente coherente. En realidad, diría que cada campo que usa Logic tiene su propia concepción de la lógica. Y a la mayoría de los matemáticos probablemente no les importa lo que es una lógica.

La estructura del campo

La historia de Logic es demasiado grande, así que solo daré la estructura del campo. El campo de la lógica formal se divide en: el uso filosófico, matemático y computacional. La lógica formal comienza en el siglo 19-20.

• Debe estudiar la lógica proposicional y la lógica de primer orden primero. Son los más estándar. Fueron creados para dar una cuenta formal / matemática a la vieja lógica de la época de la antigua Grecia.

  • La teoría de modelos (semántica), estudia las estructuras matemáticas desde la perspectiva de la lógica.
  • La teoría de la prueba (sintaxis), independientemente, estudia las pruebas como un objeto matemático.

• La lógica de segundo orden es una extensión de la lógica de primer orden que es una extensión de la lógica proposicional. Es particularmente interesante porque la aritmética "vive" en el segundo orden (predicados en predicados con inducción). De manera similar, la topología vive en el "tercer orden" (predicados en conjuntos que pueden verse como predicados mismos).

• Luego vino LEJ Brouwer que dividió la lógica en dos:

  • La lógica clásica es la lógica habitual como se definió antes. En particular, para todas las , (excluido el medio).$A$$A \lor \lnot A$
  • La lógica intuicionista es un tipo de lógica que rechaza las leyes intermedias excluidas y todas las leyes equivalentes (por razones técnicas y filosóficas que no explicaré aquí).

• En otro contexto, los filósofos se interesaron en la lógica formal y pensaron que podría responder preguntas filosóficas (filosofía analítica). Crearon sus propios sistemas lógicos independientes (lógicas paraconsistentes, lógicas de relevancia y lógicas modales como lógicas deónticas, lógicas temporales, lógicas epistémicas, ...). La lógica modal no funciona con la verdad sino con modalidades como posibilidad, necesidad, tiempo, conocimiento. Todos son independientes de las lógicas anteriores.

• La correspondencia de Curry-Howard da una correspondencia formal (isomorfismo) entre pruebas y programas. Ahora muchas lógicas podrían verse como sistemas de programación y viceversa. La lógica intuicionista que fue un poco ignorada ahora se ve como un sistema de programación funcional ( -calculus). Conduce al estudio de la teoría de tipos . Es un tema de investigación actualmente activo.$\lambda$

• Los científicos informáticos querían verificar y probar la intensidad de los sistemas de manera formal y parece que las lógicas modales son relevantes. Hoy usan lógicas temporales y lógicas modales para razonar sobre sistemas (ver: métodos formales, verificación de modelos). Los sistemas se modelan a través de la teoría de autómatas (por ejemplo) y se verifican mediante herramientas lógicas. Condujo a la lógica temporal lineal (LTL) y la lógica de árbol computacional (CTL) .

• En la misma motivación, los informáticos querían verificar la solidez y probar las propiedades de los programas. Entonces inventamos la lógica de Hoare para programas imperativos y, en general, las lógicas de separación .

• Al estudiar el isomorfismo de Curry-Howard, surgió una nueva lógica: la lógica lineal que restringe las reglas estructurales (debilitamiento y contracción) vistas como el borrado y la duplicación que operan en pruebas y programas. El potencial infinito de la verdad está explícito. Parece que esta lógica es una generalización de la lógica clásica e intuicionista y ofrece una concepción completamente nueva de la lógica basada en la computación y un paradigma de procedimiento. Principalmente es estudiado por informáticos.

• La lógica lineal también proviene de lo que llamamos lógicas subestructurales que rechazan las reglas estructurales de la lógica. Relevant Logic y Affine Logic son ejemplos de tales sistemas.

Resumen y selección de ruta

• Cualquier lógica puede ser: lógica proposicional, primer orden, segundo orden, tercer orden, ..., orden superior (cada uno se extiende al anterior).

• Podemos agregar o eliminar reglas para crear variantes de sistemas existentes:

  • Eliminar excluido-medio: lógica intuicionista
  • Añadir modalidades: lógicas modales
  • Restringir la contradicción y el debilitamiento: lógica lineal
  • Eliminar la contracción: lógica afín
  • Eliminar el debilitamiento: lógica relevante
  • Manejar la negación de manera diferente: lógica paraconsistente

• Aprenda primero la lógica proposicional y de primer orden y:

  • teoría de modelos, segundo orden, orden superior si le interesan las matemáticas
  • teoría de la prueba, lógica intuicionista, segundo orden, lógica lineal si está interesado en los fundamentos de la informática
  • lógicas modales, lógicas hoare, lógicas de separación si está interesado en la verificación de sistemas y programas
  • lógicas modales, lógicas no clásicas en general si te interesa la filosofía

Referencias (libros)

Yo personalmente recomiendo mezclar referencias, si es posible.

• Lógica matemática (Chiswell & Hodges) : libro muy conciso y simple para empezar.
• Un primer curso de lógica (Hedman) : un poco como el anterior pero da más detalles y tiene en cuenta la computabilidad.
• Manual de lógica práctica y razonamiento automatizado (Harrison) : si desea comprender cómo se implementan algunos conceptos relacionados con la lógica en la práctica. Más orientado al razonamiento automatizado.
• Lógica en informática (Huth y Ryan) : muy clara y orientada a los informáticos (verificación de programas y sistemas, lógica Hoare, uso práctico de lógica modal, lógica temporal, verificación de modelos).
• Introducción a la teoría de la prueba (Buss) : una introducción a la teoría de la prueba. Debería ser mejor leer esto después de alguna lógica general.

Referencias (Wikipedia)

• https://en.wikipedia.org/wiki/Philosophical_logic
• https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence
• https://en.wikipedia.org/wiki/Non-classical_logic
• https://en.wikipedia.org/wiki/Intuitionistic_logic
• https://en.wikipedia.org/wiki/Modal_logic
• https://en.wikipedia.org/wiki/Model_theory
• https://en.wikipedia.org/wiki/Proof_theory
• https://en.wikipedia.org/wiki/Linear_temporal_logic
• https://en.wikipedia.org/wiki/Computation_tree_logic
• https://en.wikipedia.org/wiki/Separation_logic
• https://en.wikipedia.org/wiki/Hoare_logic
• https://en.wikipedia.org/wiki/Linear_logic
• https://en.wikipedia.org/wiki/Substructural_logic

Todas estas lógicas están por debajo de la lógica matemática .

La lógica matemática a menudo se divide en los campos de la teoría de conjuntos, la teoría del modelo, la teoría de la recursión y la teoría de la prueba. Estas áreas comparten resultados básicos sobre lógica, particularmente lógica de primer orden y definibilidad. En ciencias de la computación (particularmente en la Clasificación ACM) la lógica matemática abarca temas adicionales no detallados en este artículo; ver Lógica en informática para aquellos.

Además, si desea conocer la lógica en términos generales, este artículo podría ser útil.

La lógica, que originalmente significa "la palabra" o "lo que se habla", pero que viene a significar "pensamiento" o "razón", es un tema relacionado con las leyes más generales de la verdad, y ahora se considera generalmente que consiste en el estudio sistemático de la forma de inferencia válida. Una inferencia válida es aquella en la que existe una relación específica de soporte lógico entre los supuestos de la inferencia y su conclusión.