Lazi

mathématique (lazi,pré-,minimale)

Contexte

En Lazi nous formalisons les mathématiques et raisonnons dessus, nous avons alors besoin de définitions précises et d'un champs large.

Nous avons besoin de la notion de "pré-mathématique" pour plusieurs raisons :

  • car le cadre pré-mathématique influence la mathématique, ne serais-ce par le langage utilisé (qui peut être informatique, par exemple du XML).
  • pour préciser le point d'origine d'un chemin mathématique (absolu ou relatif).

La définition d'une mathématique lazi est ici informelle, une définition formelle est complexe et devrait être donnée plus tard dans les sources quand cela sera nécessaire.

Définitions

une pré-mathématique

C'est un langage et une logique floues ou ne constituant pas forcément une mathématique, permettant néanmoins de définir une mathématique.

Par exemple la langue française accompagnée de la logique de la culture française. Une prémathématique peut aussi être un langage informatique accompagné de la logique de traitement.

une mathématique

En Lazi, une mathématique est un type "déduction".

Remarques :

  • On entent le mot type au sens lazi. (ajouter le lien)
  • Ce type "déduction" est souvent construit avec une union de types simples : les règle de déduction.
  • En lazi les notions de déduction et de preuve sont naturellement unifiées.
  • On peut aussi unifier la notion de déduction et de preuve dans les autres mathématiques, mais il faut alors éventuellement passer par des types plus complexes.
  • Les notions d'axiome et de déduction peuvent être unifiées.
  • Le type des formules est très présent dans toutes les mathématiques (lazi ou autre), mais n'est pas indispensable à la définition d'une mathématique. On peut définir les formules comme le plus petit type calculable de ce qui est déduit par les déductions.

mathématique minimale

On dit qu'une mathématique M est minimale ssi toute mathématique définissant M a une complexité supérieure ou égale.

une mathématique lazi

Une mathématique lazi est lazi.1.0 ou une mathématique extension de lazi.1.0.

@todo (donner le lien pour "voir la documentation lazi sur la notion de type en lazi")