Estoy haciendo esto exactamente en este momento, tomando un curso introductorio en lógica formal (que he terminado), seguido de un curso en lógica predicativa (actualmente en curso).
El curso introductorio incluyó definiciones básicas en el lenguaje de Sentential Logic (SL), tablas de verdad, un poco de Predicate Logic (PL) y el método de árbol para verificar la validez de ambos. El objetivo principal era aprender a manipular los conectivos y cuantificadores, y traducir el lenguaje natural a los idiomas de SL y PL. Fue interesante, pero no extremadamente útil, ya que muchos de ellos le resultarán muy familiares si está acostumbrado a las matemáticas formales.
El curso que lo siguió de inmediato (el segundo de dos cursos realizados en un semestre) parece ser más útil. El objetivo ya no es principalmente verificar la validez de un argumento, sino usar ciertas reglas para llegar a una conclusión a partir de un conjunto de premisas, que es estructuralmente cómo funcionan las pruebas, tanto matemáticas como lógicas. Además, el curso ha demostrado una prueba de solidez e integridad de la prueba de árbol en SL, y profundizará un poco en la teoría de conjuntos y la teoría de modelos, que creo que será útil para comprender y, a su vez, construir mejor las pruebas matemáticas.
El lenguaje y las herramientas que aprende a usar en un curso de lógica formal pueden no ser las que usa para presentar sus pruebas en un documento, sin embargo, sirven como herramientas bastante útiles para construir y verificar sus pruebas en la fase de investigación.
Ya sea que la lógica sea fácilmente aplicable a las matemáticas o no, depende de su facultad, en nuestra facultad creo que la mayoría de los asistentes al curso introductorio eran del departamento de informática, mientras que la mayoría de los que toman la lógica predicativa son de ciencias cognitivas, nosotros Son solo dos participantes del departamento de matemática. Sin embargo, aunque la lógica presentada utiliza una notación diferente (‘&’ para conjunción en lugar de la ‘v’ invertida, etc.), la única diferencia real es el tempo: nos movemos bastante lentamente, sin embargo, esto es bastante refrescante ya que las cosas tener tiempo para sumergirse, sin tener que poner demasiado trabajo adicional en ello.
- ¿Cuáles son los requisitos previos para estudiar cosas como la verificación formal (software y hardware), la teoría del aprendizaje formal, la demostración automatizada de teoremas y los fundamentos de los lenguajes de programación?
- ¿Qué tan centrales son las pruebas y el conocimiento de las técnicas de prueba para el tema de las matemáticas?
- ¿Sería posible codificar el lenguaje de las leyes para que una computadora pueda compilar y luego razonar sobre ellas?
- ¿Por qué es interesante el isomorfismo de Curry-Howard?
- ¿Cómo se traduciría a lógica la frase en inglés “no haga A y B”?
En general, si usted es el tipo de matemático que incluso considera tomar un curso de lógica formal (la mayoría no lo hace), lo recomendaría según mi propia situación.