¿Qué paradigma de la demostración automatizada de teoremas es apropiado para la formalización al estilo Principia Mathematica?

11

Estoy en posesión de un libro que, inspirado en los Principia Mathematica (PM) de Russell y el positivismo lógico, intenta formalizar un dominio específico determinando axiomas y deduciendo teoremas de ellos. En resumen, intenta hacer por su dominio lo que PM intentó hacer por las matemáticas. Al igual que PM, fue escrito antes de que fuera posible la prueba automatizada de teoremas (ATP).

Estoy tratando de representar estos axiomas en un sistema ATP moderno e intento deducir teoremas, inicialmente aquellos deducidos por el autor (a mano). No he usado un sistema ATP antes, y dada la gran cantidad de opciones (HOL, Coq, Isabelle y muchas más), cada una con sus fortalezas, debilidades y aplicaciones previstas, está resultando difícil decidir cuál es la adecuada para mi específico propósito.

El formalismo del autor refleja de cerca a PM. Hay clases (¿conjuntos?), Clases de clases, etc., hasta 6 niveles de jerarquía. Hay un primer orden, y posiblemente una lógica de orden superior. Dada la conexión con PM, inicialmente investigué Metamath, ya que otras personas demostraron en MetaMath varios teoremas de PM. Sin embargo, Metamath es, por supuesto, un verificador de prueba y no un sistema ATP.

Al revisar las descripciones de varios sistemas ATP, veo varias características, como implementaciones de la teoría de tipos de Church, teorías de tipos constructivas, teorías de tipos intuicionistas, teoría de conjuntos con y sin tipo, deducción natural, tipos de cálculos lambda, polimorfismo, teoría de funciones recursivas y La existencia de igualdad (o no). En resumen, cada sistema parece implementar un lenguaje muy diferente y debe ser apropiado para formalizar cosas diferentes. Supongo que las bibliotecas existentes para formalizar las matemáticas no son relevantes para mi propósito.

Cualquier consejo con respecto a las características que debo buscar al elegir un ATP, o cualquier otro consejo que pueda tener después de leer esta pregunta, sería muy apreciado. Como referencia, aquí hay una página de muestra del libro. Desafortunadamente, como PM, está en notación de Peano-Russell.

Página del libro

El libro -

"El método axiomático en biología" (1937), JH Woodger, A. Tarski, WF Floyd

Los axiomas comienzan con lo mereológico. Por ejemplo,

1.1.2 es la suma de si está contenida en las partes de , y si es cualquier parte de siempre hay una pertenece a tiene partes en común con las partes de :xααxyxzαy

S=Dfx^α^{αPx:.(y):yPx..(z).zα.PyPzΛ}

Nuevamente, tenga en cuenta que esta es la notación de Peano-Russell (la notación de Principia).

Los axiomas posteriores tienen contenido biológico, como,

7.4.2 Cuando los gametos de dos miembros de una clase mendeliana se unen en pares para formar cigotos, la probabilidad de que un par determinado se una es igual a la del otro par.

Esto, por lo que entiendo, fue un postulado de la genética mendeliana.

Omito la notación para esto porque tiene tres líneas de largo y se basa en contenido previamente definido.

Ejemplo de un teorema -

Teorema

Aparentemente, esto conlleva una interpretación significativa en la genética mendeliana, que, al no ser un historiador de la biología, no entiendo. En el libro, se dedujo a mano.

¡Gracias!

Atriya
fuente
¿Hay interés histórico en seguir exactamente el libro, o podría simplemente extraer la esencia del mismo (la configuración básica y los axiomas) y formalizar la teoría en un sistema moderno disponible?
Andrej Bauer
@andrej: Sí, mi objetivo es extraer y formalizar la esencia de un sistema moderno. No sería necesario deducir cada teorema deducido a mano en el libro. Más bien, sería genial deducir teoremas que no están en el libro, a partir de los axiomas en el libro.
Atriya
55
En ese caso, debe comprender el texto y luego hacerlo en cualquier asistente de prueba y / o probador de teoremas que mejor se adapte a su propósito.
Andrej Bauer

Respuestas:

8

Principia Mathematica fue en gran medida una respuesta a las diversas paradojas descubiertas en la lógica matemática a principios del siglo XX. Sin embargo, el trabajo en sí, que a menudo ha sido elogiado indirectamente como una "obra maestra ilegible", es algo torpe y se han creado bases más modernas. Para describir la mayoría de las matemáticas, tiene varias opciones: la teoría de categorías es una, la teoría de tipos ha sido popular en algunos proyectos como una extensión del cálculo lambda, pero el mejor entendido y más fundamental es probablemente la teoría de conjuntos.

La teoría de conjuntos tiene varias formulaciones diferentes; La teoría de conjuntos de Zermelo Frankel con el axioma de elección es la más ortodoxa, a la que los entusiastas de la teoría de conjuntos refieren con cariño como . La teoría de conjuntos de Tarski-Grothendiek es otra muy similar a que incluye el axioma de Tarski para razonar sobre grandes categorías. Estos son interesantes para la verificación, pero algo más difíciles para la demostración automatizada de teoremas porque el esquema de reemplazo del axioma admite un número infinito de axiomas que representan un desafío para la implementación. Si bien estos fundamentos son perfectamente razonables para los sistemas de verificación de pruebas como Mizar para la teoría de conjuntos Tarski-Grothendiek y Metamath paraZFC ZFCZFC, para un sistema de prueba de teorema real, sería bueno tener axiomatización finita.

La base que probablemente sea más apropiada para eso es la teoría de conjuntos de Von Neumann – Bernays – Gödel, o , que admite la axiomatización finita al ser una teoría de dos tipos que tiene una ontología de clases y conjuntos adecuados. Además, se ha demostrado que es una extensión conservadora de , por lo que cualquier teorema de es un teorema deNBGNBGZFCNBGZFC. La razón por la cual esta teoría es la más apropiada para el razonamiento automatizado en mi opinión es expresable en lógica de primer orden, que admite un cálculo de prueba efectivo, sólido y completo, y la axiomatización finita significa que puede usarse con una resolución de primer orden que nos da la resultado ordenado: si una declaración es decidible, eventualmente se encontrará una prueba.

La lógica proposicional no es lo suficientemente expresiva, y la lógica de orden superior, aunque mucho más expresiva, no admite un cálculo de prueba efectivo, sólido y completo. La lógica de primer orden con la teoría de conjuntos le permite representar y mapear teorías lógicas de orden superior, por lo que para los fundamentos ese es el punto óptimo ... excepto por la posibilidad de enunciados indecidibles (gracias a Gödel), razón por la cual las teorías de primer orden de rango cuantificador suficiente a menudo se describen como semi-decidables.

Art Quaife trabajó en esto en: Desarrollo automatizado de teorías matemáticas fundamentales, donde implementó en lógica de primer orden en forma clausal para que pudiera ser utilizado por un probador de teoremas basado en resolución (Otter) y una excelente referencia para abordar La base de este tipo de trabajo es la Introducción a la lógica matemática de Elliott Mendelson .NBG

Ahora, los asistentes de pruebas modernos a menudo están menos preocupados por los fundamentos del paradigma de Principia Mathematia y son más útiles para probar teoremas para el trabajo diario, por lo que tienen cierto soporte para fragmentos de lógica de orden superior, resolución SAT / SMT, teorías de tipo y otros enfoques más informales y menos fundacionales. Pero si está intentando hacer algo como Principia Mathematica, es ideal un teorema de resolución de primer orden con una teoría de conjuntos de primer orden finitamente axiomatizable.

Para ver algunos ejemplos de cómo los probadores de teoremas automatizados atacan los problemas de estas bases, el sitio de Miles de problemas para los probadores de teoremas ( TPTP ) tiene una buena cantidad de problemas, y notará que muchos de los problemas fundamentales en la teoría de números se encuentran en Teoría de conjuntos . Si tienes tiempo, echa un vistazo a NUM006-1.p en su sitio: la conjetura de Goldbach. Puede intentar ejecutarlo, y si es decidible, eventualmente se encontrará una prueba .NBG

Los teoremas en su libro seguramente serán teoremas de dado que están escritos en el lenguaje de la teoría de conjuntos. Los axiomas de la genética en ese libro seguramente se representarán como definiciones en predicados teóricos establecidos, de la misma manera que la aritmética de Peano se representa en como definiciones de predicados. Desde allí, siga el procedimiento de resolución en cualquier ATP. Elija una declaración que desee probar, anúlela, conviértala a la forma normal de Skolem, luego a la forma clausal y siga la resolución. Cuando encuentre la cláusula vacía, habrá encontrado una contradicción que pruebe la afirmación.NBGNBG

La tarea que tiene a mano si desea intentar definir la teoría en términos de teoría de conjuntos, es encontrar las definiciones de predicados relacionales que están separadas de la teoría de conjuntos, que le permitirán hacer los predicados en términos de teoría de conjuntos. Una vez más, un ejemplo de esto es cómo definimos la aritmética de Peano en la teoría de conjuntos, que por sí misma no tiene definiciones de números, suma, multiplicación o incluso igualdad. Como ejemplo de una definición teórica establecida de una relación como la igualdad, podemos definirla en términos de membresía como tal:

xy ( z (z x z y) x = y)

Un poco de advertencia: la curva de aprendizaje para esto es realmente muy empinada. Si tiene la intención de perseguir esto, puede encontrarse varios años antes de comprender el problema completo, como fue mi experiencia. Es posible que desee examinar la teoría desde un enfoque menos fundamental antes de asumir la enorme tarea de incorporarla en un lenguaje fundamental para todo. Después de todo, no necesariamente tiene que razonar sobre innumerables conjuntos de genes que se mezclan.

Dezakin
fuente
1
¡Muchas gracias por esta respuesta detallada y esclarecedora! Algunas preguntas: 1. Wikipedia afirma que "El esquema de reemplazo del axioma no es necesario para las pruebas de la mayoría de los teoremas de las matemáticas ordinarias", y que no era uno de los axiomas originales de Z (fue agregado por F). ¿Es posible que mis teoremas puedan ser demostrables sin él, negando así la necesidad de NBG? Por supuesto, supongo que ningún comprobador de teoremas automatizado permitiría el uso de {ZFC - esquema de reemplazo del axioma}, si eso fuera posible?
Atriya
2. Dado que la lógica de primer orden + la teoría de conjuntos es la mejor para los fundamentos, supongo que HOL / Isabelle / PVS / etc. (todos de orden superior) ¿son excesivos para mi propósito? Además, ¿todo lo basado en la teoría de tipos (Coq et al.) No es apropiado? En consecuencia, ¿los gustos de Prover9 / Vampire / SNARK serían apropiados? Tengo experiencia previa con SNARK. Puede manejar la lógica de primer orden de muchos tipos con igualdad, por resolución, pero no estoy seguro de cómo representar la teoría de conjuntos en ella.
Atriya
1
Los probadores de teoremas automatizados pueden usar esquemas de axiomas, pero dificulta la implementación. Prover9 no los admite. HOL, Isabelle, Coq apoyan la teoría de conjuntos de primer orden hasta donde puedo recordar, y probablemente estén perfectamente bien para su proyecto. Aunque puede incorporar otras teorías en NBG, no es absolutamente necesario. No tenemos que incorporar la aritmética de Peano en NBG para probar cosas sobre los números ... pero ayuda a aprender y comprender la estructura lógica.
dezakin
Siempre puede insertar su teoría en la teoría de conjuntos después, definiendo los predicados de la teoría en términos del predicado de membresía. No me preocuparía hacer que su proyecto sea absolutamente fundamental de inmediato. Se puede ajustar más tarde.
dezakin
Parece entonces que prácticamente cualquier probador, incluso aquellos tan diferentes como Coq, HOL y Prover9, pueden usarse para mi proyecto. En tales casos, ¿cuál sería una estrategia de decisión inteligente? No estoy familiarizado con todos menos SNARK. El "ideal" es el descubrimiento de nuevos teoremas en el sistema de axiomas proporcionado.
Atriya
8

Varios puntos:

  1. Hasta donde yo sé, Principia Mathematica usa esencialmente una formalización de la teoría de conjuntos usando una lógica de primer orden escrita. Por lo tanto, sería tentador utilizar un probador de teoremas automatizado de primer orden como Prover 9 o posiblemente ACL2 para formalizar sus declaraciones. Sin embargo, veo varias construcciones teóricas de conjuntos (como , ) allí, que generalmente no funcionan muy bien con ATP de primer orden.,

  2. Cualquier asistente de prueba interactivo moderno seguramente tendrá la expresividad para formalizar y probar sus declaraciones, como Andrej ha sugerido. De hecho, dado que parece haber algunas afirmaciones que incluyen la aritmética, sería aconsejable utilizar un sistema como Isabelle , Coq o HOL que ya tienen teorías extensas para tratar las afirmaciones de la aritmética. Mi énfasis en lo moderno no es una coincidencia: se han hecho grandes avances en la usabilidad desde Automath, y honestamente creo que te harías un mal servicio al usar cualquier cosa que no se haya desarrollado activamente desde los años 90 (si incluso pudieras obtener uno ¡trabajar!)

  3. Finalmente, ITP y ATP tienen curvas de aprendizaje bastante desafiantes, y no debe esperar poder ingresar estos teoremas en un sistema como si estuviera escribiendo una prueba . Espere frustración severa y tiempo perdido, especialmente en los primeros meses (sí, meses). Definitivamente, debe trabajar con algunos tutoriales al principio antes de llegar a la formalización principal.LATEX

cody
fuente
¡Gracias! Este es el tipo de consejo general que estaba buscando. Marcar esta respuesta como aceptada. Probablemente tendré preguntas más específicas / técnicas a medida que avance.
Atriya
La teoría de conjuntos está hecha para la lógica de primer orden. Puede reducir todas las matemáticas a una teoría de primer orden con un solo predicado: membresía. A partir de ahí, puede construir definiciones de unión, intersección, subconjunto, subconjunto adecuado y otras relaciones. Prover9 es completamente apropiado.
dezakin
¿En teoria? Si. ¿En la práctica? Si define, digamos, los números naturales usando la teoría de conjuntos, un sistema como Prover9 no podría probar las declaraciones más básicas como el ordenamiento total de . Por naturaleza, los sistemas como la teoría de conjuntos requieren una serie de heurísticas específicas para ser manejados eficientemente por los sistemas ATP. N
cody
Prover9 utiliza a menudo construcciones teóricas establecidas de los números naturales. Verifique los problemas de teoría de números y los axiomas de teoría de números en TPTP. Definen la teoría de números como definiciones de la teoría de conjuntos. Las heurísticas requeridas por ATP para los probadores de teoremas de resolución son exactamente qué cláusula elegir para la lista utilizable cuando se busca la cláusula vacía, y la teoría de conjuntos no es una excepción especial a eso. Otras teorías se definen en la teoría de conjuntos por predicados relacionales.
dezakin