Système à 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èmes. 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, appelés parfois par opposition systèmes à la Gentzen.

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 :

En prenant l'axiome S: (f\to (g\to h))\to ((f\to g)\to (f\to h)) , et en y remplaçant g par (g\to f) et h par f, on obtient:

  1. (f\to ((g\to f) \to f))\to ((f\to (g\to f)) \to (f \to f)) (instance de l'axiome S)
    Puis en prenant l'axiome K: f \to (g \to f) et en y remplaçant g par (g\to f), on obtient:
  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.


Wikimedia Foundation. 2010.

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

Игры ⚽ Поможем сделать НИР

Regardez d'autres dictionnaires:

  • 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 à 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 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

  • Hilbert — David Hilbert David Hilbert David Hilbert en 1912 Naissance 23 janvier 1862 Königsberg (Prusse Orientale) …   Wikipédia en Français

  • 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 (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

  • Systeme natürlichen Schliessens — Systeme (oder Kalküle) natürlichen Schließens sind ein Kalkültyp, der 1934 von Gerhard Gentzen und etwa zeitgleich von Stanisław Jaśkowski, einem Vertreter der Lemberg Warschau Schule, entwickelt wurde. Der Begriff des Kalküls des natürlichen… …   Deutsch Wikipedia

  • Systeme natürlichen Schließens — Systeme (oder Kalküle) natürlichen Schließens bezeichnen in der mathematischen und philosophischen Logik einen Kalkültyp, der 1934 von Gerhard Gentzen und etwa zeitgleich von Stanisław Jaśkowski, einem Vertreter der Lemberg Warschau Schule,… …   Deutsch Wikipedia

  • HILBERT (ESPACE DE) — La théorie des espaces hilbertiens trouve son origine dans celle des développements de fonctions arbitraires en séries de fonctions orthogonales, lesquelles apparaissent le plus souvent comme fonctions propres de certains opérateurs différentiels …   Encyclopédie Universelle

  • 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… …   Wikipédia en Français

Share the article and excerpts

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