Metamath es un lenguaje formal y un programa informático asociado (un asistente de pruebas ) para archivar y verificar pruebas matemáticas. [2] Se han desarrollado varias bases de datos de teoremas demostrados utilizando Metamath que cubren resultados estándar en lógica , teoría de conjuntos , teoría de números , álgebra , topología y análisis , entre otros. [3]
En 2023, Metamath se había utilizado para demostrar 74 [4] de los 100 teoremas del desafío "Formalizar 100 teoremas". [5] Al menos 19 verificadores de pruebas utilizan el formato Metamath. [6] El sitio web de Metamath ofrece una base de datos de teoremas formalizados que se pueden explorar de forma interactiva. [7]
El lenguaje Metamath es un metalenguaje para sistemas formales . El lenguaje Metamath no tiene una lógica específica incorporada. En cambio, puede considerarse como una forma de demostrar que las reglas de inferencia (afirmadas como axiomas o demostradas posteriormente) pueden aplicarse. La base de datos más grande de teoremas demostrados sigue la lógica convencional de primer orden y la teoría de conjuntos ZFC . [8]
El diseño del lenguaje Metamath (empleado para enunciar las definiciones, axiomas, reglas de inferencia y teoremas) se centra en la simplicidad. Las demostraciones se verifican utilizando un algoritmo basado en la sustitución de variables . El algoritmo también tiene condiciones opcionales para determinar qué variables deben permanecer distintas después de que se realiza una sustitución. [9]
El conjunto de símbolos que se pueden utilizar para construir fórmulas se declara mediante declaraciones $c(símbolos constantes) y $v(símbolos variables); por ejemplo:
$(Declara los símbolos constantes que usaremos $) $c 0 + = -> ( ) término wff |- $.$(Declara las metavariables que utilizaremos $) $vtrs PQ $.
La gramática de las fórmulas se especifica utilizando una combinación de declaraciones $f(hipótesis flotantes (de tipo variable)) y $a(afirmaciones axiomáticas); por ejemplo:
$(Especifica propiedades de las metavariables $) tt $f término t $. tr $f término r $. ts $f término s $. que es $f que es P $. que significa $f que significa Q $.$(Definir "wff" (parte 1) $) weq $a wff t = r $.$(Definir "wff" (parte 2) $) con $a wff ( P -> Q ) $.
Los axiomas y las reglas de inferencia se especifican con $adeclaraciones junto con ${y $}para el alcance de bloque y declaraciones opcionales $e(hipótesis esenciales); por ejemplo:
$( Axioma de estado a1 $) a1 $a |- ( t = r -> ( t = s -> r = s ) ) $.$( Axioma de estado a2 $) a2 $a |- ( t + 0 ) = t $. ${ mín $e |- P $. mayor $e |- ( P -> Q ) $.$(Definir la regla de inferencia modus ponens $) mp $a |- Q $. $}El uso de un constructo, $adeclaraciones, para capturar reglas sintácticas, esquemas axiomáticos y reglas de inferencia tiene como objetivo proporcionar un nivel de flexibilidad similar a los marcos lógicos de orden superior sin depender de un sistema de tipos complejo.
Los teoremas (y las reglas de inferencia derivadas) se escriben con $penunciados; por ejemplo:
$(Demostrar un teorema) th1 $p |- t = t $= $(Aquí está su prueba: $) tt tze tpl tt weq tt tt weq tt a2 tt tze tpl tt weq tt tze tpl tt weq tt tt weq wim tt a2 tt tze tpl tt tt a1 mp mp $.
Obsérvese la inclusión de la prueba en el $penunciado. Se abrevia la siguiente prueba detallada:
tt $ f término t tze $ un término 0 1,2 tpl $ un término ( t + 0 ) 3,1 wq $ una wff ( t + 0 ) = t 1,1 wq $ a wff t = t 1a2 $ a | - ( t + 0 ) = t 1,2 tpl $ un término ( t + 0 ) 7,1 wq $ una wff ( t + 0 ) = t 1,2 tpl $ un término ( t + 0 ) 9,1 wq $ una wff ( t + 0 ) = t 1,1 wq $ a wff t = t 10,11 wim $ una función fb ( ( t + 0 ) = t -> t = t ) 1a2 $ a | - ( t + 0 ) = t 1,2 tpl $ un término ( t + 0 ) 14,1,1 a1 $ a |- ( ( t + 0 ) = t -> ( ( t + 0 ) = t -> t = t ) ) 8,12,13,15 p.p. $ a |- ( ( t + 0 ) = t -> t = t ) 4,5,6,16 mp $ a |- t = t La forma "esencial" de la prueba elude los detalles sintácticos, dejando una presentación más convencional:
a2 $ a |- ( t + 0 ) = t a2 $ a |- ( t + 0 ) = t a1 $ a |- ( ( t + 0 ) = t -> ( ( t + 0 ) = t -> t = t ) ) 2,3 mp $ a |- ( ( t + 0 ) = t -> t = t ) 1,4 mp $ a |- t = t Todos los pasos de prueba de Metamath utilizan una única regla de sustitución, que consiste simplemente en reemplazar una variable por una expresión y no en la sustitución adecuada descrita en los trabajos sobre cálculo de predicados . La sustitución adecuada, en las bases de datos de Metamath que la admiten, es una construcción derivada en lugar de una incorporada al lenguaje Metamath en sí.
La regla de sustitución no hace ninguna suposición sobre el sistema lógico en uso y sólo requiere que las sustituciones de variables se realicen correctamente.
Aquí hay un ejemplo detallado de cómo funciona este algoritmo. Los pasos 1 y 2 del teorema 2p2e4en el Explorador de pruebas de Metamath ( set.mm ) se muestran a la izquierda. Expliquemos cómo Metamath usa su algoritmo de sustitución para verificar que el paso 2 es la consecuencia lógica del paso 1 cuando se usa el teorema opreq2i. El paso 2 establece que ( 2 + 2 ) = ( 2 + ( 1 + 1 ) ) . Es la conclusión del teorema opreq2i. El teorema opreq2iestablece que si A = B , entonces ( CFA ) = ( CFB ) . Este teorema nunca aparecería bajo esta forma críptica en un libro de texto, pero su formulación culta es banal: cuando dos cantidades son iguales, una puede reemplazar una por la otra en una operación. Para verificar la prueba, Metamath intenta unificar ( CFA ) = ( CFB ) con ( 2 + 2 ) = ( 2 + ( 1 + 1 ) ) . Sólo hay una manera de hacerlo: unificando C con 2 , F con + , A con2 y B con ( 1 + 1 ) . Ahora Metamath utiliza la premisa de opreq2i. Esta premisa establece que A = B . Como consecuencia de su cálculo anterior, Metamath sabe que A debe sustituirse por2 y B por ( 1 + 1 ) . La premisa A = B se convierte en 2=( 1 + 1 ) y, por lo tanto, se genera el paso 1. A su vez, el paso 1 se unifica con df-2. df-2es la definición del número 2y establece que 2 = ( 1 + 1 ). Aquí la unificación es simplemente una cuestión de constantes y es sencilla (no hay problema de variables para sustituir). Por lo tanto, la verificación está terminada y estos dos pasos de la prueba de 2p2e4son correctos.
Cuando Metamath unifica (2+2) con B, debe comprobar que se respeten las reglas sintácticas. De hecho, B tiene el tipo class, por lo que Metamath debe comprobar que (2+2) también esté tipificado class.
El programa Metamath es el programa original creado para manipular bases de datos escritas con el lenguaje Metamath. Tiene una interfaz de texto (línea de comandos) y está escrito en C. Puede leer una base de datos Metamath en la memoria, verificar las pruebas de una base de datos, modificar la base de datos (en particular, agregando pruebas) y volver a escribirlas en el almacenamiento.
Tiene un comando de prueba que permite a los usuarios ingresar una prueba, junto con mecanismos para buscar pruebas existentes.
El programa Metamath puede convertir declaraciones a notación HTML o TeX ; por ejemplo, puede generar el axioma modus ponens de set.mm como:
Muchos otros programas pueden procesar bases de datos Metamath, en particular, hay al menos 19 verificadores de pruebas para bases de datos que utilizan el formato Metamath. [10]
El sitio web Metamath alberga varias bases de datos que almacenan teoremas derivados de varios sistemas axiomáticos. La mayoría de las bases de datos ( archivos .mm ) tienen una interfaz asociada, llamada "Explorador", que permite navegar por los enunciados y las demostraciones de forma interactiva en el sitio web, de una manera fácil de usar. La mayoría de las bases de datos utilizan un sistema de deducción formal de Hilbert, aunque esto no es un requisito.
El Metamath Proof Explorer (registrado en set.mm ) es la base de datos principal. Se basa en la lógica clásica de primer orden y la teoría de conjuntos ZFC (con la adición de la teoría de conjuntos de Tarski-Grothendieck cuando es necesario, por ejemplo en la teoría de categorías ). La base de datos se ha mantenido durante más de treinta años (las primeras demostraciones en set.mm datan de septiembre de 1992). La base de datos contiene desarrollos, entre otros campos, de la teoría de conjuntos (ordinales y cardinales, recursión, equivalentes del axioma de elección, la hipótesis del continuo...), la construcción de los sistemas de números reales y complejos, la teoría del orden, la teoría de grafos, el álgebra abstracta, el álgebra lineal, la topología general, el análisis real y complejo, los espacios de Hilbert, la teoría de números y la geometría elemental. [11]
El Metamath Proof Explorer hace referencia a muchos libros de texto que pueden usarse junto con Metamath. [12] Por lo tanto, las personas interesadas en estudiar matemáticas pueden usar Metamath en conexión con estos libros y verificar que las afirmaciones probadas coinciden con la literatura.
Esta base de datos desarrolla las matemáticas desde un punto de vista constructivo, comenzando con los axiomas de la lógica intuicionista y continuando con los sistemas axiomáticos de la teoría de conjuntos constructiva .
Esta base de datos desarrolla las matemáticas a partir de la teoría de conjuntos Nuevos Fundamentos de Quine .
Esta base de datos comienza con la lógica de orden superior y deriva equivalentes a los axiomas de la lógica de primer orden y de la teoría de conjuntos ZFC.
El sitio web Metamath alberga algunas otras bases de datos que no están asociadas con exploradores pero que, no obstante, son dignas de mención. La base de datos peano.mm escrita por Robert Solovay formaliza la aritmética de Peano . La base de datos nat.mm [13] formaliza la deducción natural . La base de datos miu.mm formaliza el rompecabezas MU basado en el sistema formal MIU presentado en Gödel, Escher, Bach .
El sitio web de Metamath también alberga algunas bases de datos antiguas que ya no se mantienen, como el "Hilbert Space Explorer", que presenta teoremas relacionados con la teoría del espacio de Hilbert que ahora se han fusionado en el Metamath Proof Explorer, y el "Quantum Logic Explorer", que desarrolla la lógica cuántica comenzando con la teoría de redes ortomodulares.
Debido a que Metamath tiene un concepto muy genérico de lo que es una prueba (es decir, un árbol de fórmulas conectadas por reglas de inferencia) y no hay una lógica específica incorporada en el software, Metamath se puede utilizar con especies de lógica tan diferentes como lógicas de estilo Hilbert o lógicas basadas en secuencias o incluso con cálculo lambda .
Sin embargo, Metamath no ofrece soporte directo para sistemas de deducción natural . Como se señaló anteriormente, la base de datos nat.mm formaliza la deducción natural. El Explorador de pruebas de Metamath (con su base de datos set.mm ) utiliza, en cambio, un conjunto de convenciones que permiten el uso de enfoques de deducción natural dentro de una lógica de estilo Hilbert.
Utilizando las ideas de diseño implementadas en Metamath, Raph Levien ha implementado un verificador de pruebas muy pequeño, mmverify.py , de solo 500 líneas de código Python.
Ghilbert es un lenguaje similar aunque más elaborado basado en mmverify.py. [14] A Levien le gustaría implementar un sistema donde varias personas pudieran colaborar y su trabajo enfatiza la modularidad y la conexión entre pequeñas teorías.
Utilizando el trabajo seminal de Levien, se han implementado muchas otras implementaciones de los principios de diseño de Metamath para una amplia variedad de lenguajes. Juha Arpiainen ha implementado su propio verificador de pruebas en Common Lisp llamado Bourbaki [15] y Marnix Klooster ha codificado un verificador de pruebas en Haskell llamado Hmm . [16]
Si bien todos utilizan el enfoque general de Metamath para la codificación del verificador de sistemas formales, también implementan nuevos conceptos propios.
Mel O'Cat diseñó un sistema llamado Mmj2 , que proporciona una interfaz gráfica de usuario para la entrada de pruebas. [17] El objetivo inicial de Mel O'Cat era permitir al usuario introducir las pruebas simplemente escribiendo las fórmulas y dejando que Mmj2 encuentre las reglas de inferencia adecuadas para conectarlas. En Metamath, por el contrario, solo se pueden introducir los nombres de los teoremas. No se pueden introducir las fórmulas directamente. Mmj2 también tiene la posibilidad de introducir la prueba hacia adelante o hacia atrás (Metamath solo permite introducir la prueba hacia atrás). Además, Mmj2 tiene un analizador gramatical real (a diferencia de Metamath). Esta diferencia técnica aporta más comodidad al usuario. En particular, Metamath a veces duda entre varias fórmulas que analiza (la mayoría de ellas sin sentido) y pide al usuario que elija. En Mmj2 esta limitación ya no existe.
También hay un proyecto de William Hale para agregar una interfaz gráfica de usuario a Metamath llamada Mmide . [18] Paul Chapman a su vez está trabajando en un nuevo navegador de pruebas, que tiene resaltado que le permite ver el teorema referenciado antes y después de que se realizó la sustitución.
Milpgame es un asistente de pruebas y un verificador (muestra un mensaje solo cuando algo salió mal) con una interfaz gráfica de usuario para el lenguaje Metamath (set.mm), escrito por Filip Cernatescu, es una aplicación Java de código abierto (licencia MIT) (aplicación multiplataforma: Windows, Linux, Mac OS). El usuario puede ingresar la demostración (prueba) en dos modos: hacia adelante y hacia atrás en relación con la declaración a probar. Milpgame verifica si una declaración está bien formada (tiene un verificador sintáctico). Puede guardar pruebas inacabadas sin el uso del teorema de enlace ficticio. La demostración se muestra como un árbol, las declaraciones se muestran usando definiciones html (definidas en el capítulo de composición tipográfica). Milpgame se distribuye como Java .jar (JRE versión 6 actualización 24 escrito en NetBeans IDE).
