¿Qué métodos utilizan las personas para investigar en lógica? ¿Qué tipo de preguntas y objetivos persiguen los investigadores lógicos?

A2A. Esto no es fácil de responder porque la investigación en lógica se lleva a cabo en los departamentos de Matemáticas, Lingüística, Informática y Filosofía. Y cada uno de estos temas tiene su propia cultura y objetivos de investigación. Incluso para las ciencias de la computación, la pregunta no es fácil de responder, quizás la mejor idea sería mirar las actas de conferencias como “Lógica en Ciencias de la Computación (LICS)”, “Lógica de Ciencias de la Computación (CSL) y” Estructuras Fundamentales en Computación y deducción ”(FSCD). El área en la que estoy trabajando se llama Teoría de tipos, que encaja en un área más general que a menudo, pero de alguna manera engañosa, se llama “semántica” para separarse de cosas como la teoría de la complejidad, la teoría de modelos finitos y la teoría de la recursión. Vale la pena mencionar dos cosas: 1) la matemática estructural, es decir, la teoría de categorías es muy popular a diferencia de las matemáticas de la corriente principal, 2) Muchas conferencias ahora permiten la presentación de “artefactos”, son pruebas que se han verificado formalmente en una computadora utilizando un teorema interactivo proverbio como Isabelle o Coq.
Aquí hay una pregunta (abierta): demuestre que los tipos semisimpliciales no son definibles en la Teoría de tipos de homotopía simple (HoTT). Hemos demostrado (http://www.cs.nott.ac.uk/~psztxa…) que puede definirlos usando alguna extensión de HoTT pero permanece abierta si necesita esta extensión.