Desde un punto de vista fundacional, ¿cuál es un buen lenguaje de especificación para sistemas formales?

Question

Supongamos que usted y yo escribimos un libro que desarrolla las matemáticas (clásicas) desde cero.

En el curso de la escritura de este libro, necesitaremos definir una variedad de sistemas formales, como un sistema para la lógica proposicional, uno para la lógica de predicados; un sistema para PA, y un sistema para ZFC.

Ahora. Para llevar a cabo toda esta especificación con la máxima facilidad, probablemente deberíamos establecer un lenguaje de especificación conveniente para los sistemas formales, desde el principio.

Pregunta. Supongamos que damos prioridad a la usabilidad práctica (frente a, por ejemplo, la simplicidad metateórica). ¿Cuál sería un buen lenguaje de especificación para sistemas formales?

Por ejemplo, he oído hablar de Sistemas de puestos . ¿Serían estas una buena opción?

Answer 1

Si quiere una "usabilidad práctica", sospecho que no quiere parecer que está especificando sistemas formales. En su lugar, quieres proporcionar una capa de abstracción que se parezca más a la práctica y al proceso de pensamiento de los matemáticos y a la maquinaria que puede convertirlos en sistemas formales "bajo el capó".

Compárese con la programación de ordenadores; la gente rara vez escribe programas pensando que se convertirán en lenguaje ensamblador o código máquina. Claro, en el fondo de su mente suelen saber que eso ocurre, pero lo consideran irrelevante para la práctica de escribir programas.