Metamath es un lenguaje formal y un programa informático asociado (un corrector de pruebas ) para archivar, verificar y estudiar pruebas matemáticas. [1] Se han desarrollado varias bases de datos de teoremas probados 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. [2]
Desarrollador (es) | Norman Megill |
---|---|
Escrito en | ANSI C |
Sistema operativo | Linux , Windows , macOS |
Tipo | Comprobación de pruebas asistida por computadora |
Licencia | Licencia pública general GNU ( Dedicación de dominio público de Creative Commons para bases de datos) |
Sitio web | metamath |
A diciembre de 2020, el conjunto de teoremas probados que utilizan Metamath es uno de los cuerpos más grandes de matemáticas formalizadas, que contiene en particular demostraciones de 74 [3] de los 100 teoremas del desafío "Formalizar 100 teoremas" , lo que lo convierte en el tercero después de HOL Light. e Isabelle , pero antes de Coq , Mizar , ProofPower , Lean , Nqthm , ACL2 y Nuprl . Hay al menos 17 verificadores de pruebas para bases de datos que utilizan el formato Metamath. [4]
Este proyecto es el primero de su tipo que permite la navegación interactiva de su base de datos de teoremas formalizados en forma de un sitio web ordinario. [5]
El idioma Metamath
El lenguaje Metamath es un metalenguaje , adecuado para desarrollar una amplia variedad de sistemas formales . El lenguaje Metamath no tiene una lógica específica incrustada en él. En cambio, puede considerarse simplemente como una forma de probar que las reglas de inferencia (afirmadas como axiomas o probadas más tarde) pueden aplicarse. La base de datos más grande de teoremas probados sigue la teoría de conjuntos ZFC convencional y la lógica clásica, pero existen otras bases de datos y se pueden crear otras.
El diseño del lenguaje Metamath se centra en la simplicidad; el lenguaje, empleado para enunciar las definiciones, axiomas, reglas de inferencia y teoremas está compuesto solo por un puñado de palabras clave, y todas las demostraciones se verifican usando un algoritmo simple basado en la sustitución de variables (con condiciones opcionales sobre qué variables deben permanecer distintas después de realizar una sustitución). [6]
Conceptos básicos del idioma
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:
$ (Declare los símbolos constantes que usaremos $) $ c 0 + = -> () término wff | - $.$ (Declare las metavariables que usaremos $) $ vtrs PQ $.
La gramática de las fórmulas se especifica mediante una combinación de $f
(hipótesis flotantes (tipo variable)) y $a
declaraciones (afirmación axiomática); por ejemplo:
$ (Especifique las propiedades de las metavariables $) tt $ f término t $. tr $ f término r $. ts $ f término s $. wp $ f wff P $. wq $ f wff Q $.$ (Defina "wff" (parte 1) $) weq $ a wff t = r $.$ (Defina "wff" (parte 2) $) wim $ a wff (P -> Q) $.
Los axiomas y las reglas de inferencia se especifican con $a
declaraciones junto con ${
y $}
para el alcance del bloque y las $e
declaraciones opcionales (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 $. PS min $ e | - P $. maj $ e | - (P -> Q) $.$ (Defina la regla de inferencia del modus ponens $) mp $ a | - Q $. PS
El uso de un constructo, $a
declaraciones, para capturar reglas sintácticas, esquemas de axiomas y reglas de inferencia tiene la intención de proporcionar un nivel de flexibilidad similar a los marcos lógicos de orden superior sin una dependencia de un sistema de tipos complejo.
Pruebas
Los teoremas (y las reglas de inferencia derivadas) se escriben con $p
enunciados; por ejemplo:
$ (Demuestre 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 PS
Tenga en cuenta la inclusión de la prueba en la $p
declaración. Abrevia la siguiente prueba detallada:
tt $ f término ttze $ a término 01,2 tpl $ un término ( t + 0 )3,1 weq $ a wff ( t + 0 ) = t1,1 weq $ a wff t = t1 a2 $ a | - ( t + 0 ) = t1,2 tpl $ un término ( t + 0 )7,1 weq $ a wff ( t + 0 ) = t1,2 tpl $ un término ( t + 0 )9,1 weq $ a wff ( t + 0 ) = t1,1 weq $ a wff t = t10,11 wim $ a wff ( ( t + 0 ) = t -> t = t )1 a2 $ a | - ( t + 0 ) = t1,2 tpl $ un término ( t + 0 )14,1,1 a1 $ a | - ( ( t + 0 ) = t -> ( ( t + 0 ) = t -> t = t ) )8,12,13,15 mp $ 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 ) = ta2 $ a | - ( t + 0 ) = ta1 $ a | - ( ( t + 0 ) = t -> ( ( t + 0 ) = t -> t = t ) )2,3 mp $ a | - ( ( t + 0 ) = t -> t = t )1,4 mp $ a | - t = t
Sustitución
Todos los pasos de prueba de Metamath usan una sola regla de sustitución, que es simplemente el reemplazo simple de una variable con una expresión y no 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 respaldan, es una construcción derivada en lugar de una construida en el propio lenguaje de Metamath.
La regla de sustitución no hace suposiciones sobre el sistema lógico en uso y solo requiere que las sustituciones de variables se realicen correctamente.
A continuación, se muestra un ejemplo detallado de cómo funciona este algoritmo. Los pasos 1 y 2 del teorema 2p2e4
en 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 usa el teorema opreq2i
. El paso 2 establece que (2 + 2) = (2 + (1 + 1)) . Es la conclusión del teorema opreq2i
. El teorema opreq2i
establece 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 letrada es banal: cuando dos cantidades son iguales, una puede reemplazar una por la otra en una operación. Para comprobar la prueba, Metamath intenta unificar ( CFA ) = ( CFB ) con (2 + 2) = (2 + (1 + 1)) . Solo hay una forma de hacerlo: unificando C con 2 , F con + , A con2 y B con (1 + 1) . Así que ahora Metamath usa la premisa de opreq2i
. Esta premisa estados que A = B . Como consecuencia de su cálculo anterior, Metamath sabe que A debería sustituirse por2 y B por (1 + 1) . La premisa A = B se convierte en 2 = (1 + 1) y así se genera el paso 1. A su vez, el paso 1 se unifica con df-2
. df-2
es la definición del número 2
y 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). Entonces la verificación está terminada y estos dos pasos de la prueba de 2p2e4
son correctos.
Cuando Metamath unifica (2 + 2) con B , debe comprobar que se respetan las reglas sintácticas. De hecho, B tiene el tipo, por class
lo que Metamath tiene que verificar que (2 + 2) también esté escrito class
.
El verificador de pruebas de Metamath
El programa Metamath es el programa original creado para manipular bases de datos escritas en el lenguaje Metamath. Tiene una interfaz de texto (línea de comandos) y está escrito en C. Puede leer una base de datos de 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 17 verificadores de pruebas para bases de datos que usan el formato Metamath. [7]
Bases de datos de metamath
El sitio web de 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 las declaraciones y pruebas 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.
Explorador a prueba de metamath
Tipo de sitio | Enciclopedia en línea |
---|---|
Sede | EE.UU |
Dueño | Norman Megill |
Creado por | Norman Megill |
URL | nosotros |
Comercial | No |
Registro | No |
El Explorador de pruebas de Metamath (registrado en set.mm ) es la base de datos principal y, con mucho, la más grande, con más de 23.000 pruebas en su parte principal a partir de julio de 2019. 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 sea necesario, por ejemplo, en la teoría de categorías ). La base de datos se ha mantenido durante más de veinte años (las primeras pruebas de set.mm están fechadas en agosto de 1993). La base de datos contiene desarrollos, entre otros campos, de la teoría de conjuntos (ordinales y cardinales, recursividad, equivalentes del axioma de elección, la hipótesis del continuo ...), la construcción de los sistemas numéricos reales y complejos, la teoría de órdenes, la teoría de grafos, álgebra abstracta, álgebra lineal, topología general, análisis real y complejo, espacios de Hilbert, teoría de números y geometría elemental. Esta base de datos fue creada por primera vez por Norman Megill, pero a partir de 2019-10-04 ha habido 48 colaboradores (incluido Norman Megill). [8]
El Explorador de pruebas de Metamath hace referencia a muchos libros de texto que se pueden utilizar junto con Metamath. [9] Por lo tanto, las personas interesadas en estudiar matemáticas pueden usar Metamath en relación con estos libros y verificar que las afirmaciones probadas coincidan con la literatura.
Explorador de lógica intuicionista
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 de axiomas de la teoría de conjuntos constructiva .
Explorador de nuevas fundaciones
Esta base de datos desarrolla matemáticas a partir de la teoría de conjuntos New Foundations de Quine .
Explorador de lógica de orden superior
Esta base de datos comienza con lógica de orden superior y deriva equivalentes a axiomas de lógica de primer orden y de teoría de conjuntos ZFC.
Bases de datos sin exploradores
El sitio web de 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 [10] 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 .
Exploradores mayores
El sitio web de Metamath también alberga algunas bases de datos más antiguas que ya no se mantienen, como el "Explorador espacial de Hilbert", que presenta teoremas relacionados con la teoría espacial de Hilbert que ahora se han fusionado en el Explorador de pruebas de Metamath y el "Explorador de lógica cuántica". , que desarrolla la lógica cuántica a partir de la teoría de las celosías ortomodulares.
Deducción natural
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 incrustada en el software, Metamath se puede usar con especies de lógica tan diferentes como las lógicas de estilo Hilbert o sus secuencias. -basadas en lógicas o incluso con cálculo lambda .
Sin embargo, Metamath no proporciona ningún apoyo directo para los 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 ) en su lugar utiliza un conjunto de convenciones que permiten el uso de enfoques de deducción natural dentro de una lógica de estilo Hilbert.
Otras obras relacionadas con Metamath
Comprobadores de pruebas
Usando las ideas de diseño implementadas en Metamath, Raph Levien ha implementado un verificador de pruebas muy pequeño, mmverify.py , en solo 500 líneas de código Python.
Ghilbert es un lenguaje similar, aunque más elaborado, basado en mmverify.py. [11] A Levien le gustaría implementar un sistema en el que varias personas pudieran colaborar y su trabajo enfatiza la modularidad y la conexión entre pequeñas teorías.
Utilizando las obras fundamentales 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 corrector de pruebas en Common Lisp llamado Bourbaki [12] y Marnix Klooster ha codificado un corrector de pruebas en Haskell llamado Hmm . [13]
Aunque todos utilizan el enfoque general de Metamath para la codificación formal del verificador del sistema, también implementan nuevos conceptos propios.
Editores
Mel O'Cat diseñó un sistema llamado Mmj2 , que proporciona una interfaz gráfica de usuario para la entrada de pruebas. [14] El objetivo inicial de Mel O'Cat era permitir al usuario ingresar las pruebas simplemente escribiendo las fórmulas y dejando que Mmj2 encontrara las reglas de inferencia apropiadas para conectarlas. En Metamath, por el contrario, solo puede ingresar los nombres de los teoremas. No puede ingresar las fórmulas directamente. Mmj2 también tiene la posibilidad de ingresar la prueba hacia adelante o hacia atrás (Metamath solo permite ingresar la prueba al revé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 no tienen sentido) y le 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 . [15] Paul Chapman, a su vez, está trabajando en un nuevo navegador de pruebas, que tiene resaltado que le permite ver el teorema al que se hace referencia antes y después de que se realizó la sustitución.
Milpgame es un asistente de pruebas y un verificador (muestra un mensaje solo si 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 a la demostración (prueba) en dos modos: hacia adelante y hacia atrás en relación con la declaración a probar. Milpgame comprueba si una declaración está bien formada (tiene un verificador sintáctico). Puede guardar pruebas inconclusas sin el uso del teorema del 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 escrita en NetBeans IDE).
Ver también
- Comprobación de pruebas automatizada
- Asistente de pruebas
- Sistema Mizar
Referencias
- ^ Megill, Norman; Wheeler, David A. (2 de junio de 2019). Metamath: A Computer Language for Mathematical Proofs (Segunda ed.). Morrisville, Carolina del Norte, EE.UU .: Lulul Press. pag. 248. ISBN 978-0-359-70223-7.
- ^ Megill, Norman. "¿Qué es Metamath?" . Página de inicio de Metamath .
- ^ Metamath 100.
- ^ Megill, Norman. "Verificadores de pruebas conocidos de Metamath" . Consultado el 14 de julio de 2019 .
- ^ TOC de la lista de teoremas - Explorador de prueba de Metamath
- ^ Megill, Norman. "Cómo funcionan las pruebas" . Página de inicio de Metamath Proof Explorer .
- ^ Megill, Norman. "Verificadores de pruebas conocidos de Metamath" . Consultado el 14 de julio de 2019 .
- ^ Wheeler, David A. "Contribuciones de Metamath set.mm vistas con Gource hasta el 2019-10-04" .
- ^ Megill, Norman. "Sugerencias de lectura" . Metamath .
- ^ Liné, Frédéric. "Sistema Metamath basado en deducción natural" . Archivado desde el original el 28 de diciembre de 2012.
- ^ Levien, Raph. "Ghilbert" .
- ^ Arpiainen, Juha. "Presentación de Bourbaki" . Archivado desde el original el 28 de diciembre de 2012.
- ^ Klooster, Marnix. "Presentación de Hmm" . Archivado desde el original el 2 de abril de 2012.
- ^ O'Cat, Mel. "Presentación de mmj2" . Archivado desde el original el 19 de diciembre de 2013.
- ^ Hale, William. "Presentación de mmide" . Archivado desde el original el 28 de diciembre de 2012.
enlaces externos
- Metamath : sitio web oficial.
- Qué piensan los matemáticos de Metamath : opiniones sobre Metamath.