Études-Mathématique/Structure globale

From Lazi wiki
Jump to: navigation, search

Question

Quel est la structure globale de ces fondations mathématiques ?

Étude

/Ajouter un type pour la preuve ? : Non

/Types de mots

Réponse

Le langage de base et les règles simples sont fixées, c'est la partie Lazi-0 : voir http://lazi.bobu.eu/wp-content/uploads/2014/05/definition.pdf

On ajoute une règle signifiant que si on a une représentation d'une preuve dans un certain système (Lazi-1), alors la traduction de la conclusion de la représentation de preuve est une vérité. Ainsi on peut utiliser Lazi-1 pour produire des vérités.

Lazi-1 est une fondation plus sophistiquée que Lazi-0 mais contient les règles de base de Lazi-0.

Lazi-1 définit un système de typage. La fondation définie dépend d'un contexte, ce contexte est un dictionnaire de types. On définira un contexte pour Lazi-1, mais Lazi-1 permettra d'utiliser d'autres contexte ce qui permet par exemple d'utiliser des extensions, des hypothèses etc.

Le contexte des types de base (comme le type des listes) dont deux mathématiques :

  • Le type des formules. En changeant le type des formules on peut par exemple introduire des noms définis, des notations, des variables etc.
  • Le type des déductions. En changeant ce type on peut ajouter de nouvelles règles de déduction.

Par exemple le type des formules contient une union de types: un type pour les mots, un type pour l'application etc. On ajoute le type de mot pour les variables des règles, il contient en lui la liste des mots autorisés, cette liste est une entrée du dictionnaire représentant le type, cette liste peut être modifiée pour ajouter des variables. On obtient ainsi un contexte différent où les formules ont des mots en plus.