Metamath

L'ensemble des symboles qui peuvent être utilisés pour construire des formules est déclaré en utilisant $c (déclaration de constante) et $v (déclaration de variable) déclarations. Par exemple :

$( Declare the constant symbols we will use $)
    $c 0 + = -> ( ) term wff |- $.
$( Declare the metavariables we will use $)
    $v t r s P Q $.

La grammaire pour les formules est spécifiée en utilisant une combinaison de déclarations $f (hypothèse flottante) et $a (assertion axiomatique). Par exemple :

$( Specify properties of the metavariables $)
    tt $f term t $.
    tr $f term r $.
    ts $f term s $.
    wp $f wff P $.
    wq $f wff Q $.
$( Define "wff" (part 1) $)
    weq $a wff t = r $.
$( Define "wff" (part 2) $)
    wim $a wff ( P -> Q ) $.

Axiomes et règles d'inférence sont spécifiés avec les expressions $a avec $ { et $} pour la structure de blocs et optionnellement des expressions $e (hypothèses essentielles). Par exemple :

$( State axiom a1 $)
    a1 $a |- ( t = r -> ( t = s -> r = s ) ) $.
$( State axiom a2 $)
    a2 $a |- ( t + 0 ) = t $.
    ${
       min $e |- P $.
       maj $e |- ( P -> Q ) $.
$( Define the modus ponens inference rule $)
       mp  $a |- Q $.
    $}

Utiliser un seul type d'expression, $a, pour définir les règles syntaxiques, les schémas axiomatiques et mes règles d'inférence doit fournir un niveau de flexibilité similaire aux cadres logiques d'ordre supérieur sans dépendre d'un système complexe de types.

Les théorèmes (et les règles d'inférence dérivées) sont définis avec les expressions $p. Par exemple :

$( Prove a theorem $)
    th1 $p |- t = t $=
  $( Here is its proof: $)
       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
     $.

Notez l'inclusion de la preuve dans l'expression $p. Cela permet une représentation compacte de la preuve sous forme détaillée suivante :

tt            $f term t
tze           $a term 0
1,2 tpl       $a term ( t + 0 )
3,1 weq       $a wff ( t + 0 ) = t
1,1 weq       $a wff t = t
1 a2          $a |- ( t + 0 ) = t
1,2 tpl       $a term ( t + 0 )
7,1 weq       $a wff ( t + 0 ) = t
1,2 tpl       $a term ( t + 0 )
9,1 weq       $a wff ( t + 0 ) = t
1,1 weq       $a wff t = t
10,11 wim     $a wff ( ( t + 0 ) = t -> t = t )
1 a2          $a |- ( t + 0 ) = t
1,2 tpl       $a term ( 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 forme « essentielle » de la preuve masque les détails syntaxiques et conduit à une présentation plus conventionnelle :

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

Toutes les étapes des preuves de Metamath utilisent une seule règle de substitution, qui est simplement le remplacement d'une variable avec une expression et non la substitution définie formellement dans le domaine du calcul de prédicats. La substitution formelle, dans les bases de données de Metamath qui la gèrent, est une construction dérivée et non une fonctionnalité intégrée au langage.

La règle de substitution ne dépend pas du système logique utilisé et ne requiert que les remplacements de variables soient faits correctement.

Une preuve étape par étape

Voici un exemple détaillé de la façon dont cet algorithme fonctionne. Les étapes 1 et 2 du théorème 2p2e4 dans le Metamath Proof Explorer (set.mm) sont représentées à gauche. Nous allons expliquer comment Metamath utilise son algorithme de remplacement pour vérifier que l'étape 2 est la conséquence logique de l'étape 1 lorsque vous utilisez le théorème opreq2i. L'étape 2 indique que (2 + 2) = (2 + (1 + 1). C'est la conclusion du théorème opreq2i. Le théorème opreq2i affirme que si A = B = A = B, puis ((C F A) = (C F B)) = ((C F A) = (C F B)). Ce théorème n'apparaîtrait jamais sous cette forme cryptique dans un manuel, mais sa formulation littéraire est banale: lorsque deux quantités sont égales, il peut être remplacé l'un par l'autre dans une opération. Pour vérifier la preuve Metamath essaie d'unifier ((C F A) = (C F B)) = ((C F A) = (C F B)) avec (2 + 2) = (2 + (1 + 1). Il n'y a qu'une seule FAçon de le faire: unifier C avec 2, F avec +, A avec 2 et B avec (1 + 1). Alors maintenant Metamath utilise la prémisse de opreq2i. Cette prémisse indique que A = B. En rA = Bison de son calcul précédent, Metamath sait que A doit être remplacé par 2 et A = B par 1 + 1). Le A = B prémisse A = A = B devient 2=(1 + 1) et donc l'étape 1 est générée. Dans son étape 1 il est unifié avec df-2. df-2 est la définition du nombre 2 et indique que 2 = (1 + 1). Ici l'unification est simplement une question de constantes et est directe (sans problème des variables à remplacer). La vérification est terminée et ces deux étapes de la preuve2p2e4 sont correctes.

Lorsque Metamath unifie (2 + 2) avec B, il faut vérifier que les règles de syntaxe sont respectées. En fait B est de type classdonc Metamath doit vérifier que (2 + 2) est également de type class.

Adresse	us.metamath.org/mpeuni/mmset.html
Commercial	No
Type de site	Online encyclopedia

Le Metamath Proof Explorer (et son fichier set.mm) est la principale et de loin la plus grande base de données, avec plus de 23.000 preuves dans sa partie principale en juillet 2019. Il est basé sur la logique classique de premier ordre et la théorie des ensembles ZFC (avec l'ajout de Tarski-Grothendieck théorie des ensembles si nécessaire, par exemple dans la théorie de la catégorie). La base de données a été maintenue pendant plus de vingt ans (les premières preuves en set.mm datent d'août 1993). La base de données contient des développements, entre autres, de théorie des ensembles (ordinaux et cardinaux, récursion, équivalents de l'axiome de choix, l'hypothèse continue…), la construction des systèmes de nombres réels et complexes, la théorie de l'ordre, la théorie des graphiques, l'algèbre abstraite, 'algèbre linéaire, topologie générale, analyse réelle et complexe, les espaces Hilbertiens, la théorie des nombres et la géométrie élémentaire. Cette base de données a été créée pour la première fois par Norman Megill, mais au 04/10/2019 on compte 48 collaborateurs (en incluant Norman Megill[7]).

Le Metamath Proof Explorer fait référence à de nombreux manuels pouvant être utilisés conjointement avec Metamath[8]. Ainsi, les personnes intéressées à étudier les mathématiques peuvent utiliser Metamath en relation avec ces livres et vérifier que les affirmations prouvées correspondent à la littérature.

Cette base de données développe les mathématiques d'un point de vue constructif, en commençant par les axiomes de la logique intuitionniste et en continuant avec les systèmes axiomes de théorie constructive de l'ensemble.

Cette base de données développe les mathématiques issus de la théorie New Foundation de Quine.

Cette base de données commence par la logique d'ordre supérieur et dérive des équivalents aux axiomes de la logique de premier ordre et de la théorie des ensembles ZFC .

Le site Web de Metamath héberge quelques autres bases de données qui ne peuvent être consultées en ligne, mais restent néanmoins remarquables. La base de données peano.mm écrite par Robert Solovay formalise l'arithmétique de Peano. La base de données nat.mm formalise la déduction naturelle[9]. La base de données miu.mm formalise le puzzle MU basé sur le système formel MIU présenté dans Gödel, Escher, Bach.

Le site Web de Metamath abrite également des bases de données plus anciennes qui ne sont plus maintenues, comme le "Hilbert Space Explorer", qui présente des théorèmes appartenant à la théorie des espaces hilbertiens qui a maintenant rejoint la base principale, et le "Quantum Logic Explorer", qui développe la logique quantique à partir de la théorie des lattices orthomodulaires.

En utilisant les idées de conception mises en œuvre dans Metamath, Raph Levien a réalisé un très petit vérificateur, mmverify.py, en seulement 500 lignes de code Python.

Ghilbert est un langage plus élaboré basé sur mmverify.py[10]. Levien cherche à obtenir un système qui permettrait la collaboration entre plusieurs utilisateurs et son travail promeut la modularité et l'interconnection des modules théoriques.

Sur la base de ces travaux originaux, de multiples réimplémentations de l'architecture Metamath ont vu le jour dans de nombreux langages de programmation : Juha Arpiainen a réalisé son vérificateur Bourbaki[11] en Common Lisp et Marnix Klooster a codé le sien en Haskell called Hmm[12].

Bien que tous utilisent l'approche commune de Metamath pour le mécanisme de vérification formelle, ils apportent également leurs propres concepts originaux.

Mel O'Cat a conçu un système nommé Mmj2, qui propose une interface utilisateur graphique pour la saisie des preuves[13]. L'objectif initial de Mel O'Cat était de permettre à l'utilisateur de saisir les preuves en écrivant simplement les formules et en laissant Mmj2 trouver les règles d'inférence appropriées pour les relier. Dans Metamath au contraire ne peut entrer dans les noms des théorèmes. Vous ne pouvez pas entrer les formules directement. Mmj2 permet également de saisir une preuve dans les deux sens alors que Metamath permet seulement de saisir une preuve en partant du résultat. De plus, Mmj2 possède un vrai analyseur grammatical, ce qui n'est pas le cas pour Metamath. Cette différence technique apporte plus de confort à l'utilisateur. En particulier, Metamath hésite parfois entre plusieurs formules et demande à l'utilisateur de choisir. Avec Mmj2, cette limitation n'existe plus.

Le projet Mmide[14] de William Hale ajoute lui aussi une interface utilisateur graphique à Metamath. Paul Chapman travaille sur un nouvel explorer, qui peut mettre en évidence un théorème appliqué avant et après l'action de substitution..

Milpgame est un assistant de preuve et un vérificateur (un message s'affiche en cas d'erreur) avec une interface utilisateur graphique pour le langage de Metamath (set.mm), écrit par Filip Cernatescu, et distribué sous forme d'application Java open source (licence MIT) (application multi-plateforme: Windows, Linux, Mac OS). L'utilisateur peut introduire la démonstration dans le deux sens. Milpgame vérifie si une déclaration est bien formée (présence d'un vérificateur syntaxique). Vous pouvez enregistrer des preuves inachevées sans l'utilisation du théorème dummylink. La preuve s'affiche sous forme d'arbre, les déclarations sont affichées à l'aide des définitions html. Milpgame est distribué sous forme d'archive .jar Java (JRE version 6u24 requis, développé avec l'IDE NetBeans ID.