Las aplicaciones de la lógica matemática a la topología, las ciencias de la computación y la inteligencia artificial, su uso en la investigación de los fundamentos de las matemáticas y su presencia en los debates acerca de la naturaleza de las matemáticas, son sólo algunos ejemplos del lugar que ocupa esta disciplina en la matemática actual. La diversidad de áreas en que se hace presente es un indicativo de la necesidad de abordar muchos de sus problemas en forma multidisciplinaria, de reunir especialistas en distintas áreas que aporten las herramientas requeridas para resolverlos. Este modo de proceder es cada vez más común en el dominio de la lógica matemática por las razones expuestas. En nuestro caso, cada una de las investigaciones propuestas cuenta con la participación de al menos dos académicos que, reuniendo sus conocimientos, estarán en posibilidad de abordar los problemas con mayor profundidad. En el caso de la prueba de Turing modificada, el problema que se intenta resolver es el de la inexistencia de un interrogador-máquina que sea infalible. Esto requiere de las técnicas y métodos de diagonalización propios de la teoría de la computabilidad, y de la exploración del espacio de diálogos posibles entre el interrogador y el interrogado, es decir, del estudio de árboles potencialmente infinitos que podrían modelarse mediante tipos coinductivos. En otras palabras, se requiere de una combinación de técnicas. Respecto a la metodología de Gödel sucede algo similar. Por una parte, es necesario conocer los métodos y las técnicas asociados a los teoremas de incompletud para las teorías axiomáticas, y conocer los debates filosóficos en torno a la naturaleza de las matemáticas; por la otra, es necesario conocer el estado actual de las investigaciones en la teoría de conjuntos, sobre todo con relación a los grandes cardinales y las distintas bases axiomáticas de la teoría. De nuevo una combinación de especialidades que comparten el hecho de desarrollarse en el terreno de la lógica matemática. En cuanto a los sistemas de tipos, la metodología para extender la correspondencia de Curry-Howard precisa del diseño de sistemas deductivos cada vez más complejos. Esto se debe a que los sistemas de tipos que surgen en la práctica capturan nociones y mecanismos de programación cada vez más expresivos y sofisticados. Lo anterior requiere, por tanto, la afluencia de los métodos de la teoría de la demostración y de la teoría de la recursión aplicada a las ciencias computacionales. Finalmente, la aplicación del principio de determinación a la topología exige no sólo amplios conocimientos de topología, sino un extenso dominio de los métodos relativos a las pruebas de consistencia en la teoría de conjuntos. Antes que favorecer la dispersión (desunión) en estos dominios, es necesario fomentar el intercambio de ideas y experiencias entre los especialistas que participan en estas tareas. Es por ello que se plantea la realización de La Primera Escuela Mexicana de Lógica Matemática y del Primer Coloquio Mexicano de Lógica Matemática y su Entorno, donde éstos y otros temas se difundirían y se someterían a la consideración de nuestros colegas provenientes de todo el país y del extranjero. Estos serían dos pasos importantes para estimular el interés de los estudiantes en esta materia y para consolidar, en nuestra universidad y en nuestro país, a la lógica matemática como campo de investigación.

Presentamos de forma detallada las contribuciones de cada investigación propuesta. Contribuciones de la investigación “Sistemas de Tipos y extensiones al Paradigma de Programación con Pruebas” (1er año, Favio E. Miranda Perea, Carlos Torres Alcaraz) - Extender el isomorfismo de Curry-Howard en lo que respecta a logicas y sistemas de tipos que incluyan mecanismos de definicion de funciones mediante distintos principios de recursion y correcursion, en particular nos interesan los principios de recursión y correcursión por curso de valores el cual generaliza al principio de iteración convencional al permitir que el valor de una función en un argumento dado dependa no sólo de los valores inmediatos anteriores sino también de resultados recursivos de cualquier valor anterior. Dualmente, el principio de correcursión por curso de valores permite especificar argumentos a níveles arbitrarios para la construcción de las partes de una estructura coinductiva en lugar de forzar la especificación para el nivel inmediato siguiente. La definición de sistemas de tipos robustos que modelen estos principios así como su relación con técnicas de programación dinámica, como la memoización (ver [AHB02],[MGxx]), constituiran una contribución al llamado enfoque calculacional de la programación, donde la implementación de un problema se deriva de una especificación particular mediante la manipulación algebráica de ecuaciones. Este enfoque es relevante para el paradigma de programación funcional donde las expresiones de un lenguaje se conmportan como funciones matemáticas debido a la ausencia de efectos laterales. - Extender el paradigma de programacion con pruebas a lógicas que permitan la extraccion de programas que involucren tipos de datos coinductivos, los cuales implementan estructuras potencial o estrictamente infinitas como son flujos (listas infinitas) y arboles infinitos. Si bien existen intentos previos para manejar este tipo de datos, nuestra contribución sería relevante en al menos dos aspectos: La extensión del método de extracción de programas a especificaciones que involucran no sólo definiciones coiterativas simples sino también correcursivas primitivas y correcursivas de Mendler. Por otra parte, la definición de sistemas de deducción natural con un mecanismo primitivo para la definición de tipos de datos inductivos y coinductivos, a diferencia de las extensiones existentes donde la definición de tipos de datos se hace mediante la codificación impredicativa en lógica de segundo orden, lo cual trae consigo dificultades en la práctica. Contribuciones de la investigación “Aplicaciones del principio de determinación en la topología” (1er año, Diego Rojas Rebolledo, David Meza Alcantara, Favio E. Miranda Perea) - El Juego de comparación clasifica los ideales borelianos en un modo similar al orden de Wadge y al orden monótono de Tukey. Una contribución relavante sería extender los resultados sobre esta clase de ideales (Borel) a clases más amplias suponiendo principios de determinación. - Se pretende estudiar las propiedades intrínsecas que permiten que se aplique el argumento de determinación presentado en [Ro07], para así generalzar los métodos hacia otros espacios polacos, más allá de los espacios cero dimensionales. - El estudio de cofinalidades para ideales F_sigma sobre omega desarrollado en [HRZ09] en colaboración con M.Hrusak (UNAM) y J. Zapletal (University of Florida), plantea, entre otros, el problema de decidir si la cofinalidad de ideales borelianos sobre omega, es preservada bajo la iteración con soporte numerable del forcing de Sacks. Contribuciones de la investigación "La metodología de Gödel para las matemáticas" (2do año, Carlos Torres Alcaraz, Diego Rojas Rebolledo) Al respecto, y a pesar de la vasta literatura sobre el tema, aún queda mucho por decir en este dominio. Uno de los propósitos de este proyecto es precisar qué tanto se ha logrado en la evaluación de las extensiones de la teoría axiomatica de los conjuntos siguiendo la metodología propuesta por Gödel, es decir, hasta dónde se ha avanzado con este criterio de verdad para los axiomas de orden superior en la teoría de conjuntos. Otro tema de interés en el proyecto es el de examinar hasta qué punto podemos aceptar la metodología propuesta por Gödel sin tener que admitir su realismo conceptual. Esto implica poner a discusión el valor heurístico de su postura incluso para el nominalismo, el formalismo y otras escuelas que encuentran insostenible la posición filosófica de Gödel. En este sentido, creemos que es mucho lo que se puede reivindicar de su metodología sin tener que tomar una decisión acerca de la naturaleza de las matemáticas, es decir, sin tener que “resolver” una cuestión ontológica que no preocupa a todos. Esto, sin olvidar que fue la creencia de Gödel en la existencia de los conjuntos infinitos lo que lo llevó a predecir correctamente la indecidibilidad de la hipótesis del continuo y a concebir su metodología. Simplemente, lo que creemos es que la metodología propuesta por Gödel resulta exitosa no porque diga a los matemáticos qué deben hacer, creer o pensar, sino porque de algún modo refleja la práctica matemática. Esta es la conclusión a la que apuntaría nuestro trabajo. Contribuciones de la investigación "Una variante de la prueba de Turing: La máquina como interrogador" (2do año, Carlos Torres Alcaraz, Favio E. Miranda Perea) Al respecto, nos proponemos demostrar con base en los métodos utilizados por Gödel en sus pruebas de incompletud, la inexistencia de una máquina interrogadora infalible, y explorar esta cuestión considerando la complejidad de los algoritmos que serían necesarios para hacer la identificación correcta por parte de la máquina interrogadora, viendo si ello es suficiente para establecer la limitación señalada. Considerando que los humanos somos capaces de realizar todo lo que una máquina de Turing puede hacer, habríamos probado que la posibilidad de un interrogador (humano) perfecto requeriría de habilidades no mecanizables, al menos en el sentido actual del término “mecanizable”. Esto realzaría la importancia del interrogador en la prueba de Turing, es decir, daría el mismo peso al interrogador que a la máquina.