Ariel Roffé es miembro del grupo BA-Logic group (cuyas reuniones periódicas se realizan en el IIF-Sadaf) y del grupo ANFIBIO. Es becario doctoral del Conicet. Su tema de investigación se encuentra en la intersección entre lógica, filosofía de las ciencias y computación. El motivo de esta entrevista es la publicación de un artículo suyo en el Journal of Applied Non-Classical Logics, sobre uno de los programas que diseñó, llamado Reconstructor.
Mariela Rubin: ¿Qué es Reconstructor? ¿Para qué sirve?
Ariel Roffé: Reconstructor es un programa que tiene como objetivo principal permitir contrastar reconstrucciones formales de teorías empíricas.
Existe una tradición bastante larga en filosofía de las ciencias de intentar reconstruir o representar formalmente el contenido de teorías científicas, usando herramientas de la lógica. Esta tradición empezó con el empirismo lógico y, después de su desaparición, continuó (aunque como tarea menos dominante) en diversas escuelas. Una de ellas es el estructuralismo metateórico, en la que trabajamos desde el Centro de Filosofía e Historia de las Ciencias de la Universidad Nacional de Quilmes.
Pero independientemente de la escuela en la que uno trabaje, hay algo común a todas estas metateorías formales: ninguna contaba, hasta ahora, con métodos sistemáticos para testear sus productos. O sea, uno hacía una reconstrucción de una teoría, y se fijaba más o menos a ojo si la formalización era adecuada. Es decir, si expresaba lo mismo que la teoría target que se estaba reconstruyendo.
Lo que hago en el paper es delinear una metodología para testear reconstrucciones y brindar un programa de computación, capaz de razonar semánticamente, en el que esa metodología se puede llevar a cabo.
MR: ¿En qué consiste esa metodología?
AR: Son varias cosas. Un ejemplo sería este. En la metateoría estructuralista las aplicaciones (exitosas o fallidas) de teorías se representan por medio de modelos (en el sentido lógico del término). Entonces, una de las cosas que propongo es que los modelos que representan aplicaciones paradigmáticamente exitosas de la teoría target tienen que satisfacer la formalización de las leyes. Y lo inverso con las aplicaciones paradigmáticamente fallidas (los modelos que las representan no tienen que satisfacer la formalización de las leyes). Así uno ve que la reconstrucción “se comporta igual” que la teoría target.
Es similar a lo que hacemos en un curso de lógica inicial, cuando le damos como criterio a los alumnos la idea de que una formalización de una oración del lenguaje natural tiene que tener las mismas condiciones de verdad que esa oración. Acá la idea es similar, solo que lo que funciona como “base empírica” para una reconstrucción no es tanto la comprensión intuitiva que suponemos que los alumnos tienen en tanto hablantes competentes del lenguaje, sino los ejemplos paradigmáticos que la comunidad relevante acepta como casos exitosos o fallidos de aplicación de la teoría.
MR: ¿Y por qué sería importante testear una reconstrucción de esta manera?
AR: La respuesta que daría tiene que ver con el modo particular en el que yo concibo a la filosofía de la ciencia (o al menos a esta parte de la filosofía de la ciencia), como formando parte de la ciencia de la ciencia. En particular, diría que el estructuralismo (y las otras metateorías formales) son teorías científicas, que tienen la peculiaridad de que su objeto de estudio son las teorías científicas mismas.
En cualquier otro ámbito de la ciencia, tener una teoría que no podés contrastar rigurosamente sería considerado muy problemático. No veo por qué los metacientíficos deberíamos sentirnos exentos de contrastar las teorías que proponemos para dar cuenta de los fenómenos que queremos explicar. Por supuesto que las teorías (incluidas las teorías acerca de teorías) no se ponen a prueba en abstracto, sino que se contrastan a través de sus aplicaciones. En este caso, las aplicaciones de la metateoría son las reconstrucciones particulares de teorías. Entonces, contrastar una reconstrucción es un modo indirecto de contrastar a la metateoría misma, y de volverla más rigurosamente científica.
MR: ¿Cómo surgió la idea de hacer esto con un programa de computación?
AR: Surgió porque no basta con proponer una metodología, tiene que ser posible llevarla a cabo. Si bien la metodología que propongo se puede llevar a cabo con lápiz y papel, sería extremadamente tedioso hacerlo así. Una formalización de una ley científica real suele tener muchos cuantificadores anidados, presuponer bastante matemática, etc. De hecho, el programa permite ver los procesos de razonamiento internos que hace para ver si un modelo satisface una oración. En los casos de teorías reales que probé, son miles y miles de valuaciones las que hay que chequear para ver si una aplicación satisface o no las leyes.
En lo personal, surgió porque a principios del año pasado yo estaba aprendiendo a programar, probando diseñar funciones que hagan cosas de lógica, y una vez que ya tenía varias hechas se me ocurrió que podía aplicarlas para esto.
MR: ¿A qué público está apuntado?
AR: Está apuntado a diversos públicos. Por un lado, a gente que está trabajando en hacer reconstrucciones formales. Más particularmente, aunque no exclusivamente, a los estructuralistas. La idea sería que puedan chequear si el resultado de ese trabajo de reconstrucción es adecuado o no.
Por otro lado, creo que también le puede ser útil a gente que trabaja en lógica, porque el programa automatiza cálculos en el ámbito de la teoría de modelos, que es uno de los enfoques desde los que usualmente se define a la relación de consecuencia lógica. También porque el software trabaja con una semántica no clásica, de tres valores de verdad, y porque tiene un lenguaje de base bastante rico (que incluye aritmética y teoría de conjuntos), con lo cual se puede incluso codificar y automatizar parte de la metalógica.
MR: ¿Reconstructor usa una lógica no clásica?
AR: Sí, en particular usa una semántica paracompleta. La idea es que uno puede cargar modelos incompletos, con fallas de denotación. En el caso de la ciencia empírica representarían aplicaciones de la teoría en donde no se conoce por adelantado el valor o la extensión de todos los conceptos, por ejemplo antes de hacer una predicción. Para evaluar oraciones en estos modelos incompletos se usan las matrices de la lógica de K3 de Kleene. Estas matrices tienen un tercer valor de verdad que permite representar situaciones de desconocimiento o indeterminación del valor de verdad.
Además el programa incluye la posibilidad de llenar las denotaciones incompletas en un modelo por medio de algoritmos dados por el usuario. Esto es lo que los estructuralistas llaman “métodos de determinación”, que son procedimientos sistemáticos para averiguar la extensión de un concepto (o mejor dicho, un nuevo modo de entender o elucidar la noción de método de determinación). O sea, una vez cargada, la reconstrucción formal puede aplicarse para hacer predicciones automatizadas.
MR: ¿Crees que el programa puede servir para fines educativos?
AR: Sí, claro, es un objetivo que siempre tuve en la cabeza. En el ámbito de la filosofía de las ciencias puede servir para la educación porque es un campo de trabajo multidisicplinario, en donde convive gente con backgrounds muy distintos. Por ejemplo, es tan usual hacer una carrera de grado en ciencias y después especializarse en filosofía como lo inverso. En esa diversidad de backgrounds y de habilidades, quizás algunos vienen con menos conocimientos de lógica y les cuesta más encarar una reconstrucción formal. Creo que el programa puede ayudar especialmente a quienes están aprendiendo a hacer una reconstrucción formal.
En el caso de la lógica la aplicación educativa es más obvia todavía, sirve para aprender semántica formal. Para la enseñanza de la lógica también desarrollé otro sistema, como TAUT, que reúsa parte del código que había desarrollado originalmente para Reconstructor. TAUT también hace cosas en teoría de la prueba y funciona con varios sistemas de lógica más. Ese otro sistema de hecho lo estamos usando en la cátedra de Lógica de la Universidad de Buenos Aires. (NdeE: se puede encontrar otra entrevista sobre TAUT acá))
MR: ¿Qué sigue para el desarrollo del programa?
AR: Últimamente estuve trabajando en agregarle algunas funciones nuevas. Creo que una de las más interesantes es la posibilidad de tener métodos de determinación automáticos. Esto quiere decir que vos le das un modelo incompleto y una ley al programa, y éste infiere las denotaciones que faltan (cuando eso es posible). Para eso, lo que hice fue generalizar el aparato kripkeano de puntos fijos, para que pueda aplicarse a completar la extensión y la anti-extensión de cualquier ítem del lenguaje (no solo del predicado de verdad), e implementar eso computacionalmente. Creo que el resultado es algo así como el equivalente semántico de un probador automático de teoremas.
MR: Por último, ¿Cómo se puede conseguir?
AR: Se puede descargar gratuitamente de mi página. Funciona con todos los sistemas operativos. La versión 2.0, que tiene estas funcionalidades que te mencionaba recién, va a salir dentro de poco.
MR: Gracias.
AR: Gracias a vos.