Teoría de los Testigos: Notas sobre λ-cálculo y lógica

Título original:

Witness Theory: Notes on λ-calculus and Logic

Contenido del libro:

Este libro se ocupa del análisis matemático del concepto de prueba formal en lógica clásica, y registra -en sustancia- un ejercicio más largo de λ-cálculo aplicado.

Siguiendo coloquialismos que se remontan a L. E. J. Brouwer, los objetos de estudio en esta empresa se denominan testigos. Un testigo pretende representar la demostración lógica de una fórmula clásicamente válida, en un contexto de demostración dado. Los formalismos utilizados para expresar los testigos y su comportamiento ecuacional son extensiones del λ-cálculo "tipado puro", consideradas como teorías ecuacionales.

Formalmente, un testigo se genera a partir de variables testigo decoradas -o "tipadas"-, que representan supuestos, y operadores testigo, que representan reglas lógicas de inferencia.

Las especificaciones ecuacionales sirven para definir los operadores de los testigos.

En general, esto puede hacerse ignorando la "tipificación", es decir, las propias fórmulas lógicas.

Model-theoretically, the witnesses are objects of an extensional Scott λ-model.

El planteamiento -denominado, genéricamente, "teoría de los testigos"- se inspira en los trabajos de N. G. de Bruijn, sobre una teoría matemática de la demostración, realizados a finales de los años sesenta y principios de los setenta, en la Universidad de Eindhoven (Países Bajos), y es similar al planteamiento que subyace a la Correspondencia Curry-Howard, familiar de la lógica intuicionista.

En el caso clásico, los decorados -llamados a menudo "tipos"- son fórmulas lógicas clásicas.

En el nivel sin cuantificadores, la teoría ecuacional en cuestión es el λ-cálculo con emparejamiento suryectivo' y algunos subsistemas del mismo, adecuadamente decorados.

La extensión a cuantificadores proposicionales de primer y segundo orden es sencilla.

El libro consiste en una colección de notas y trabajos escritos y difundidos durante los últimos diez años, como continuación de investigaciones previas realizadas por el autor durante los años ochenta.

Entre otras cosas, incluye un estudio de los orígenes de la teoría moderna de la prueba -de Frege a Gentzen- desde un punto de vista teórico-testimonial, así como una aplicación característica de la teoría de los testigos a un problema lógico práctico relativo a la axiomaticidad.