Le programme de Hilbert est un programme créé par David Hilbert dans le but d'assurer les fondements des mathématiques.
Les conceptions scientifiques de David Hilbert ont une grande influence sur les mathématiciens de son époque. Hilbert s'oppose fermement au pessimisme scientifique prôné en particulier par le physiologiste Emil du Bois-Reymond, pour qui il est des questions en sciences qui resteront toujours sans réponse, une doctrine connue sous le nom d'« Ignorabimus » (du latin ignoramus et ignorabimus : « Nous ne savons pas et nous ne saurons jamais »). Hilbert, pour qui , propose, au contraire, dans une allocution de 1930, de s’appuyer sur un slogan resté célèbre : (Wir müssen wissen. Wir werden wissen).
La découverte de paradoxes dans les théories proposées par Cantor et Frege sur les fondements des mathématiques ébranle la confiance en ceux-ci. Certes, on a de nouvelles théories des ensembles qui sont exemptes des paradoxes connus, mais comment s'assurer qu'on n'en trouverait pas de nouveaux ? Hilbert s'oppose également violemment à l'intuitionnisme du mathématicien néerlandais Brouwer, que promeut ce dernier pour résoudre la crise des fondements, et qui est une remise en cause radicale de ceux-ci.
Brouwer juge que le tiers exclu, un principe logique qui affirme qu'une proposition est soit vraie soit fausse, s'il repose sur une intuition solide quand on manipule le fini, ne peut être un principe du raisonnement, dès que l'on manipule l'infini. Une preuve d'existence doit être effective. Il ne suffit pas, pour montrer telle proposition, de montrer que sa négation entraînerait une contradiction. Cette position, cohérente sur le plan des idées, et qui séduit des mathématiciens de valeur - outre Brouwer lui-même, Hermann Weyl pendant un temps - a pour principal défaut, de remettre en cause des pans entiers des mathématiques.
Pour régler la question des fondements, Hilbert conçoit un programme dont il établit les prémisses en 1900 dans l'introduction à sa célèbre liste de problèmes, le second problème étant celui de la cohérence de l'arithmétique.
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.
Presentation of Wightman's axiomatic framework to QFT as well as to the necessary mathematical objects to their understanding (Hilbert analysis, distributions, group representations,...).Proofs of
A hands-on introduction to interactive theorem proving, proofs as programs, dependent types, and to the Coq proof assistant. Come learn how to write bug-free code!
La logique — du grec , qui est un terme dérivé de signifiant à la fois « raison », « langage » et « raisonnement » — est, dans une première approche, l'étude de l'inférence, c'est-à-dire des règles formelles que doit respecter toute argumentation correcte. Le terme aurait été utilisé pour la première fois par Xénocrate. La logique antique se décompose d'abord en dialectique et rhétorique. Elle est depuis l'Antiquité l'une des grandes disciplines de la philosophie, avec l'éthique (philosophie morale) et la physique (science de la nature).
Gentzen's consistency proof is a result of proof theory in mathematical logic, published by Gerhard Gentzen in 1936. It shows that the Peano axioms of first-order arithmetic do not contain a contradiction (i.e. are "consistent"), as long as a certain other system used in the proof does not contain any contradictions either. This other system, today called "primitive recursive arithmetic with the additional principle of quantifier-free transfinite induction up to the ordinal ε0", is neither weaker nor stronger than the system of Peano axioms.
Gerhard Gentzen ( à Greifswald - à Prague) est un mathématicien et logicien allemand, dont l'œuvre est fondamentale en théorie de la démonstration. Il fut l’un des étudiants de Weyl à l'université de Göttingen de 1929 à 1933. Il est mort dans un camp de prisonniers de guerre en 1945, après avoir été arrêté par les soviets à cause de ses loyautés nazies. Gentzen est un élève de Paul Bernays à l'université de Göttingen. Mais ce dernier ayant été renvoyé comme « non- aryen » en , Hermann Weyl devient formellement son directeur de thèse.
Explore les courbes dans le plan orienté, en discutant de l'orientation, des espaces vectoriels, des relations d'équivalence et de la courbure des courbes régulières.
Games on graphs with omega-regular objectives provide a model for the control and synthesis of reactive systems. Every omega-regular objective can be decomposed into a safety part and a liveness part. The liveness part ensures that something good happens " ...
Current online applications, such as search engines, social networks, or file sharing services, execute across a distributed network of machines. They provide non-stop services to their users despite failures in the underlying network. To achieve such a hi ...
Deciding consistency of constraint networks is a fundamental problem in qualitative spatial and temporal reasoning. In this paper we introduce a divide-and-conquer method that recursively partitions a given problem into smaller sub-problems in deciding con ...