Langage formel
Bonjour,
A-t-on une idée de l'ordre de grandeur du nombre de symboles qu'il faudrait utiliser pour traduire une proposition mathématique "usuelle" dans un langage formel ?
Ma question est très vague mais c'est surtout pour amener à discuter. J'aimerais notamment savoir s'il existe des mathématiciens qui ont tenté d'écrire des mathématiques en se restreignant à utiliser le moins de symboles possible. Merci d'avance
A-t-on une idée de l'ordre de grandeur du nombre de symboles qu'il faudrait utiliser pour traduire une proposition mathématique "usuelle" dans un langage formel ?
Ma question est très vague mais c'est surtout pour amener à discuter. J'aimerais notamment savoir s'il existe des mathématiciens qui ont tenté d'écrire des mathématiques en se restreignant à utiliser le moins de symboles possible. Merci d'avance
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
Après on peut consulter des prouveurs formels pour regarder comment c'est fait (dans Metamath il me semble que tout est documenté).
L'informatique a fait considérablement évoluer ces débats dans le bon sens, ce qui était autrefois un argumentaire sur papier à peine digeste est devenu un ensemble de programmes informatiques et d'implémentations bas-niveau de concepts. Les maths sont totalement formalisables par exemple, contrairement à certains clichés répandus.
Cependant l'emblématique ZF(C) qui est souvent réputée héberger toutes les mathématiques, est entièrement écrite en logique du premier ordre à partir des seuls symboles de relation $\in,=$ (ce dernier pouvant être enlevé à la rigueur via $p=q:= \forall x (x\in p \leftrightarrow x \in q)$). Ceci est à prendre au sens littéral puisque de nombreux développements (métathéoriques on va dire) de théorie des ensembles se réfèrent explicitement à ladite syntaxe (formules $\Delta_0$; absoluité; hiérarchie analytique/de Lévy; ensembles des formules et ensembles contructibles, (*) etc).
Or dans ce langage, en contraste saisissant avec la pratique mathématique normale, il n'y a aucun symbole de constante, et surtout aucun symbole de fonction.(**)
Autrement dit "$1+1=2$" doit être traduit en quelque chose comme $\forall x \forall y \forall z \left [\left (F(x)\wedge G(y) \wedge H(x,x,z) \right )\Rightarrow (z=y)\right ]$ où $F,G,H$ sont des formules à rallonge incluant toutes les définitions intermédiaires et dont les significations respectives sont:
$F(a):=$ "$a$ est l'ordinal successeur de l'ensemble vide"
$G(b):=$ "$b$ est le successeur du successeur de l'ensemble vide"
$H(c,d,e):=$ "$e$ est la somme de ordinaux $c$ et $d$".
Bref il est possible que la version Principia Mathematica de "$1+1=2$" soit en fait plus courte que sa contrepartie dans ZF!
Bon, on est dans les deux cas bien au delà de ce qui est acceptable en termes de lisibilité :-D.
[size=x-small](**)Si on se place dans une extension conservatrice de cette théorie avec des symboles de fonctions, il faut expliquer comment les notions abordées dans la parenthèse (*) se comportent.[/size]
Bien d'accord, et on pourrait mettre Bourbaki dans le même sac (sur ce sujet) (:D
Evidemment il faut préciser de quoi on parle. La preuve de $1+1=2$ dans Peano prend deux lignes.
Ca passerait chez un auteur béotien mais vu les accomplissements techniques de Mathias celui-ci se comporte en manipulateur et en voyou et cet article est une honte. Rien de bon à retirer de ces propagandes.
" := "
et contrairement à un préjugé répandu,
l'informel est en moyenne même plus long que le formel.
Poirot: c'est normal, les lambda-termes $(\lambda x. F)t$ et $F[x:=t]$ sont (beta) équivalents mais le deuxième est bien plus gros que le premier souvent.
Au hasard, l'affectation ?
À bientôt.
Cherche livres et objets du domaine mathématique :
Intégraphes, règles log et calculateurs électromécaniques.
Si je peux me permettre, il me semble que ce sont des synonymes.
À bientôt.
Cherche livres et objets du domaine mathématique :
Intégraphes, règles log et calculateurs électromécaniques.
Mais quel intérêt à devenir nous-mêmes des machines ? Les machines peuvent nous servir...l'inverse est à bannir.