Lazi

Contexte mathématique

Introduction

Le "contexte mathématique" est ici pris dans le sens premier (contexte dans le cadre mathématique). Nous allons voir que nous aurons besoin en Lazi d'être plus précis que dans la mathématique standard et pour cela nous aurons besoin de la notion de "contexte mathématique".

Pourquoi nous devons formaliser le contexte en Lazi

Relation entre les définitions mathématiques et les fondations mathématiques

Quand on fait des mathématiques on se place déjà dans un certain contexte qui permet de donner un sens. Par exemple quand on écrit "2 + 2 = 4" on fait référence à la définition usuelle de 2, + et 4. En général le contexte est implicite : on fait références aux mathématiques standards (théorie des ensembles, ZFC etc) et on précise parfois quelques éléments de contexte.

Comme Lazi mathématise entièrement l'activité mathématique, il est nécessaire de pouvoir formaliser entièrement l'activité mathématique. Hors une mathématique qui prouve 2+2=4 est forcément différente d'une mathématique qui ne prouve pas 2+2=4 (c'est le cas par exemple si 2 n'est pas défini).
L'approche des définitions de Principia Mathematica (vol 1 page 11) est standard en informatique : il s'agit d'un système de préprocesseur qui fait les remplacements pour transformer un texte invalide du point de vue de la fondation en texte valide. Avec Lazi il n'est pas question de voir les définitions comme des éléments hors fondation mathématique car un principe important de Lazi est que toute l'activité mathématique soit représentée grâce à la fondation (lazi.1.0). Réaliser tous les remplacements des définitions au préalable et refuser les définitions récursives (comme f = g(h), h = g(f)) seraient des limitations follement gênantes en Lazi.

En Lazi une extension permet d'utiliser des définitions locales à une preuve sans changer de fondation. Mais peut importe le système utilisé, une activité mathématique entièrement formalisée doit toujours préciser le contexte, et celui-ci doit contenir les définitions sur lesquelles on veut s'appuyer.

Le contexte, même relatif à une fondation de départ, n'est pas fait que de définitions

On peut aussi vouloir ajouter des nouveaux axiomes (comme pour l'analyse non standard). En lazi nous aurons besoin d'ajouter des extensions afin d'ajouter des outils mathématiques, ce pourra être par exemple une déduction permettant de réaliser des preuves automatiquement etc.

Comment le contexte est formalisé en Lazi

Comme tout est défini par une mathématique et qu'en Lazi une mathématique est un type, il suffira de donner le nom de ce type pour exprimer le contexte mathématique.
Mais le type est lui-même défini dans un contexte. En Lazi comme en général le contexte a lui même un contexte, par exemple :
— Dans quel contexte êtes vous ici ?
— Pour assister à une réunion sur les récipients alimentaires.
— Et dans quel contexte assistez-vous à cette réunion ?
— Je suis ingénieurs en conception de récipients alimentaires.
etc
Donc si nous voulons être plus précis sur le contexte il nous faut alors donner une liste de mathématiques, c'est ce que l'on appelle le chemin mathématique, par exemple $L[ lazi_1_0 , lazi_1_1 , lazi_1_2 , lazi_1_3 ].

On utilisera les expressions suivantes :

  • Contexte mathématiques : la mathématique xxx
  • Contexte mathématique : le chemin mathématique xxx