Systèmes à la Hilbert

Systèmes à la Hilbert

Système à la Hilbert

En logique, les systèmes à la Hilbert servent à définir les déductions formelles en suivant un modèle proposé par David Hilbert au début du XXe siècle : un grand nombre d'axiomes logiques exprimant les principales propriétés de la logique que l'on combine au moyen de quelques règles, notamment la règle de modus ponens, pour dériver de nouveaux théorème. Les systèmes à la Hilbert héritent du système défini par Gottlob Frege et constituent les premiers systèmes déductifs, avant l'apparition de la déduction naturelle ou du calcul des séquents.

Sommaire

Définition

Calcul propositionnel

On considère l'ensemble des formules du calcul propositionnel. Rappelons qu'il s'agit des formules finies que l'on peut construire inductivement à partir des variables propositionnelles au moyen des connecteurs logiques.

On se donne un ensemble d'axiomes logiques qui sont des formules valides du calcul propositionnel. Une déduction est une suite de formules telle que chaque formule A apparaissant dans cette suite vérifie l'une des conditions suivantes :

  • A est une instance d'axiome (ou de théorème), c’est-à-dire l'un des axiomes logiques (ou l'un des théorèmes déjà démontrés) dans lequel les variables propositionnelles sont remplacées par des formules ;
  • il existe deux formules précédant A\, qui sont de la forme B\to A et B\, ; on dit alors que A\, est obtenue par modus ponens entre ces deux formules.

On représente une déduction en écrivant les formules ligne par ligne et en adjoignant un commentaire à chaque ligne pour expliquer comment la formule correspondant a été obtenue.

Il existe plusieurs choix possibles de systèmes axiomatiques du calcul propositionnel. On en donne un ici relativement verbeux mais assez intuitif.

  • Axiomes pour l'implication. Le choix de ces deux axiomes un peu étranges se justifie par le fait qu'ils simplifient la démonstration du théorème de déduction :
    • Axiome K : f \to (g \to f) ;
    • Axiome S : (f\to (g\to h))\to ((f\to g)\to (f\to h)).
  • Axiomes pour la négation. On donne deux des principales variantes de ces axiomes ; à titre d'exemple le lecteur pourra choisir l'une d'elles et essayer de trouver une déduction de l'autre :
    • Raisonnement par l'absurde : (\neg f\to g)\to((\neg f\to\neg g)\to f) ;
    • Contraposition : (\neg g\to\neg f)\to (f\to g).
  • Axiomes pour la conjonction :
    • f\to(g\to f\land g) ;
    • f\land g\to f, f\land g\to g.
  • Axiomes pour la disjonction :
    • f\to f\lor g, g\to f\lor g ;
    • Raisonnement par cas : f\lor g\to((f\to h)\to((g\to h)\to h)).

Exemple de déduction

Voici une déduction de l'identité f\to f :

  1. (f\to ((g\to f) \to f))\to ((f\to (g\to f)) \to (f \to f)) (instance de l'axiome S)
  2. f\to ((g\to f)\to f) (instance de l'axiome K)
  3. (f\to (g\to f)) \to (f \to f) (modus ponens entre 1 et 2)
  4. f\to(g\to f) (instance de l'axiome K)
  5. f\to f (modus ponens entre 3 et 4)

Le théorème de déduction

Comme on voit sur l'exemple précédent, il est assez malcommode de démontrer les propriétés les plus simples. C'est pourquoi on étend le système en ajoutant la possibilité d'utiliser des hypothèses, c’est-à-dire des formules non prouvées. Ainsi au lieu de démontrer f\to f, on se contenterait de démontrer f\, en utilisant l'hypothèse f\,, ce qui revient à écrire une démonstration d'une seule ligne.

Un autre exemple de démonstration avec hypothèse est donné par la transitivité de l'implication : en se donnant les hypothèses f\to g, g\to h et f\,, on démontre que h\, :

  1. f\, (hypothèse)
  2. f\to g (hypothèse)
  3. g\, (modus ponens entre 2 et 1)
  4. g\to h (hypothèse)
  5. h\, (modus ponens entre 4 et 3)

La question se pose alors de savoir si à partir d'une preuve avec hypothèses on peut récupérer une preuve sans ; par exemple peut-on à partir de la preuve ci-dessus déduire l'existence d'une preuve de (f\to g)\to ((g\to h) \to (f\to h)) ? La réponse est oui, et c'est ce qu'énonce le théorème de déduction : si on a une démonstration d'une formule A utilisant une hypothèse B alors on peut construire une démonstration de B\to A qui n'utilise plus cette hypothèse, soit si B|- A, alors |- B\to A.

L'utilisation du théorème de déduction permet de simplifier considérablement la recherche de preuves dans les systèmes à la Hilbert. C'est un passage obligé d'une démonstration du théorème de complétude pour un tel système. Dans la déduction naturelle ou le calcul des séquents de Gerhard Gentzen le théorème de la déduction est en quelque sorte intégré comme règle primitive sous la forme d'introduction droite de l'implication.

  • Portail des mathématiques Portail des mathématiques
  • Portail de la logique Portail de la logique
Ce document provient de « Syst%C3%A8me %C3%A0 la Hilbert ».

Wikimedia Foundation. 2010.

Contenu soumis à la licence CC-BY-SA. Source : Article Systèmes à la Hilbert de Wikipédia en français (auteurs)

Игры ⚽ Нужно решить контрольную?

Regardez d'autres dictionnaires:

  • HILBERT (PROBLÈMES DE) — «Qui ne se réjouirait de pouvoir soulever le voile qui cache le futur, de jeter un regard sur le développement des mathématiques, ses progrès ultérieurs, les secrets des découvertes des siècles à venir?...» Prévoir le futur des mathématiques: qui …   Encyclopédie Universelle

  • HILBERT (D.) — Le mathématicien allemand David Hilbert a ouvert la voie à plusieurs générations de chercheurs et a joué un rôle important dans l’élaboration des idées, non seulement dans sa spécialité, mais dans le cadre d’une réflexion générale sur la science …   Encyclopédie Universelle

  • Hilbert space — For the Hilbert space filling curve, see Hilbert curve. Hilbert spaces can be used to study the harmonics of vibrating strings. The mathematical concept of a Hilbert space, named after David Hilbert, generalizes the notion of Euclidean space. It… …   Wikipedia

  • Systeme a la Hilbert — Système à la Hilbert En logique, les systèmes à la Hilbert servent à définir les déductions formelles en suivant un modèle proposé par David Hilbert au début du XXe siècle : un grand nombre d axiomes logiques exprimant les principales… …   Wikipédia en Français

  • Système de Hilbert — Système à la Hilbert En logique, les systèmes à la Hilbert servent à définir les déductions formelles en suivant un modèle proposé par David Hilbert au début du XXe siècle : un grand nombre d axiomes logiques exprimant les principales… …   Wikipédia en Français

  • Système à la hilbert — En logique, les systèmes à la Hilbert servent à définir les déductions formelles en suivant un modèle proposé par David Hilbert au début du XXe siècle : un grand nombre d axiomes logiques exprimant les principales propriétés de la… …   Wikipédia en Français

  • Système à la Hilbert — En logique, les systèmes à la Hilbert servent à définir les déductions formelles en suivant un modèle proposé par David Hilbert au début du XXe siècle : un grand nombre d axiomes logiques exprimant les principales propriétés de la… …   Wikipédia en Français

  • Problèmes de Hilbert — Lors du deuxième congrès international des mathématiciens tenu à Paris en 1900, David Hilbert présenta une liste de problèmes qui tenaient jusqu alors les mathématiciens en échec. Ces problèmes devaient, selon Hilbert, marquer le cours des… …   Wikipédia en Français

  • Problemes de Hilbert — Problèmes de Hilbert Lors du deuxième congrès international de mathématiques tenu à Paris en 1900, David Hilbert présenta une liste de problèmes qui tenaient jusqu alors les mathématiciens en échec. Ces problèmes devaient, selon Hilbert, marquer… …   Wikipédia en Français

  • Problèmes de hilbert — Lors du deuxième congrès international de mathématiques tenu à Paris en 1900, David Hilbert présenta une liste de problèmes qui tenaient jusqu alors les mathématiciens en échec. Ces problèmes devaient, selon Hilbert, marquer le cours des… …   Wikipédia en Français

Share the article and excerpts

Direct link
… Do a right-click on the link above
and select “Copy Link”