Langage formel

Dans les Principia Mathematica, cette preuve apparaît à la moitié du Volume II, tout ce qui précède ne sert pas qu'à cela bien sûr, mais même si c'était le cas , cela ne ferait pas des milliards de milliards:-D (facile à estimer)

Médiat a écrit:

Dans les Principia Mathematica, cette preuve apparaît à la moitié du Volume II, tout ce qui précède ne sert pas qu'à cela bien sûr, mais même si c'était le cas , cela ne ferait pas des milliards de milliardsgrinning smiley (facile à estimer)

Sauf erreur les Principia contiennent un opérateur de description définie: un symbole $i$ tel que si $\psi$ est une formule, $i(\psi)$ désigne "l'unique objet satisfaisant $\psi$", ouvrant la possibilité d'introduire des définitions d'objets comme des abréviations, et donc des formules de mathématiques.

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]

voir Bourbaki

Merci Poirot. Et encore tu n'as là que la définition du nombre $1$. Donc, pour $1+1=2$ je dois être dans le bon ordre de grandeur.

Evidemment il faut préciser de quoi on parle. La preuve de $1+1=2$ dans Peano prend deux lignes.

Si on a droit aux

" := "

et contrairement à un préjugé répandu,

l'informel est en moyenne même plus long que le formel.

Comment appelle-t-on ces constructions en informatique déjà? (let; := ...) Je n'arrive plus à retrouver le nom technique depuis plusieurs jours :-X

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.

Dreamer a écrit:

Au hasard, l'affectation ?

Merci Dreamer; mais il me semble qu'il y avait un autre terme (ou peut-être que je me fais des films).

Bonsoir.

Si je peux me permettre, il me semble que ce sont des synonymes.

À bientôt.