Formalisation des maths de DEUG/prépa

[invite22bfc1a6]

Bonjour à tous,

Voici un problème qui me tourne en tête depuis un certain temps... Ce qui suit va sans doute vous paraître très naïf, je m'en excuse par avance.

En prépa, grosso modo, on reconstruit les maths à partir de zéro, et commençant par la logique propositionnelle. On redéfinit précisément des concepts "intuitifs" vus au lycée, comme la notion de limite ou de dérivabilité.

Je me suis donc demandé s'il n'y avait pas moyen de formaliser tout ceci. En gros, être capable de programmer un logiciel qui, à partir de quelques propositions de bases et de quelques règles de construction, permette de recréer toutes les "propositions" qui constituent le programme de prépa.

Plus tard, j'ai entendu parler du théorême de Gödel, de l'indécidabilité, etc... Donc a priori, pas de formalisation possible. Toutefois, cela concerne des cadres mathématiques beaucoup plus généraux que ceux étudiés en prépa. Par exemple, en prépa, on ne définit jamais un ensemble à partir de lui-même, ce qui élimine toute une classe de propositions problèmatiques.

Je demande donc : en se restreignant modestement au programme de prépa, est-il possible de formaliser entièrement le programme de math ? Et si oui, quelles sont les propositions initiales et les règles de construction ?

Merci d'avance pour vos réponses
-----

[Médiat]

Bonjour,

Il existe des logiciels baptisés "assistants de preuve", en particulier COQ développé par l'INRIA (il y en a d'autres bien sur).

[inviteaf48d29f]

Bonjour,

Les maths se formalisent entièrement. D'ailleurs une preuve écrite en mathématiques formelles est tout à fait illisible.
Le fait que des propositions soient indécidables ne pose aucun problème.

Les propositions peuvent tout de même êtres écrites formellement. C'est d'ailleurs un peu le principe du théorème de Gödel, il y aura toujours de proposition qu'on a le droit d'écrire qui sont indécidables.
Une telle proposition P ne peut pas devenir un théorème, pas plus que la proposition non(P). En revanche la proposition P' : "P est indécidable" peut devenir un théorème.

[inviteea028771]

En fait si, une telle proposition peut devenir un théorème... mais dans une théorie plus forte

http://fr.wikipedia.org/wiki/Th%C3%A...e_de_Goodstein

[A voir en vidéo sur Futura]

[invite22bfc1a6]

Bonjour,

Les maths se formalisent entièrement. D'ailleurs une preuve écrite en mathématiques formelles est tout à fait illisible.
Le fait que des propositions soient indécidables ne pose aucun problème.

Les propositions peuvent tout de même êtres écrites formellement. C'est d'ailleurs un peu le principe du théorème de Gödel, il y aura toujours de proposition qu'on a le droit d'écrire qui sont indécidables.
Une telle proposition P ne peut pas devenir un théorème, pas plus que la proposition non(P). En revanche la proposition P' : "P est indécidable" peut devenir un théorème.

En ce cas, quelles sont les propositions de base et les règles de manipulation ?