Déduction naturelle - Natural deduction

Dans la logique et la théorie de la preuve , la déduction naturelle est une sorte de calcul de preuve dans lequel le raisonnement logique est exprimé par des règles d'inférence étroitement liées au mode de raisonnement « naturel ». Cela contraste avec les systèmes de style Hilbert , qui utilisent plutôt des axiomes autant que possible pour exprimer les lois logiques du raisonnement déductif .

Motivation

La déduction naturelle est née d'un contexte d'insatisfaction vis-à-vis des axiomatisations du raisonnement déductif commun aux systèmes de Hilbert , Frege et Russell (voir, par exemple, le système de Hilbert ). De telles axiomatisations ont été les plus célèbres utilisées par Russell et Whitehead dans leur traité mathématique Principia Mathematica . Poussé par une série de séminaires en Pologne en 1926 par Łukasiewicz qui préconisait un traitement plus naturel de la logique, Jaśkowski a fait les premières tentatives pour définir une déduction plus naturelle, d'abord en 1929 en utilisant une notation schématique, et plus tard en mettant à jour sa proposition dans une séquence d'articles en 1934 et 1935. Ses propositions ont conduit à différentes notations telles que le calcul à la Fitch (ou diagrammes de Fitch) ou la méthode de Suppes pour laquelle Lemmon a donné une variante appelée système L .

La déduction naturelle sous sa forme moderne a été proposée indépendamment par le mathématicien allemand Gerhard Gentzen en 1934, dans une thèse remise à la faculté des sciences mathématiques de l' université de Göttingen . Le terme déduction naturelle (ou plutôt son équivalent allemand natürliches Schließen ) a été inventé dans cet article :

Ich wollte nun zunächst einmal einen Formalismus aufstellen, der dem wirklichen Schließen möglichst nahe kommt. Donc ergab sich ein "Kalkül des natürlichen Schließens" .
(J'ai d'abord voulu construire un formalisme qui se rapproche le plus possible du raisonnement réel. Ainsi est né un "calcul de déduction naturelle".)

Gentzen était motivé par le désir d'établir la cohérence de la théorie des nombres . Il n'a pas pu prouver le résultat principal requis pour le résultat de cohérence, le théorème d'élimination de coupe - le Hauptsatz - directement pour la déduction naturelle. Pour cette raison, il a introduit son système alternatif, le calcul des séquences , pour lequel il a prouvé le Hauptsatz à la fois pour la logique classique et intuitionniste . Dans une série de séminaires en 1961 et 1962, Prawitz a donné un résumé complet des calculs de déduction naturelle et a transporté une grande partie du travail de Gentzen sur les calculs séquentiels dans le cadre de la déduction naturelle. Sa monographie de 1965 Déduction naturelle : une étude théorique de la preuve allait devenir un ouvrage de référence sur la déduction naturelle et incluait des applications pour la logique modale et du second ordre .

En déduction naturelle, une proposition est déduite d'un ensemble de prémisses en appliquant des règles d'inférence à plusieurs reprises. Le système présenté dans cet article est une variation mineure de la formulation de Gentzen ou de Prawitz, mais avec une adhésion plus étroite à la description de Martin-Löf des jugements logiques et des connecteurs.

Jugements et propositions

Un jugement est quelque chose de connaissable, c'est-à-dire un objet de connaissance. C'est évident si on le sait en fait. Ainsi « il pleut » est un jugement, qui est évident pour celui qui sait qu'il pleut réellement ; dans ce cas, on peut facilement trouver des preuves du jugement en regardant par la fenêtre ou en sortant de la maison. Dans la logique mathématique cependant, les preuves ne sont souvent pas aussi directement observables, mais plutôt déduites de jugements évidents plus fondamentaux. Le processus de déduction est ce qui constitue une preuve ; en d'autres termes, un jugement est évident si l'on en a la preuve.

Les jugements les plus importants en logique sont de la forme " A est vrai ". La lettre A représente toute expression représentant une proposition ; les jugements de vérité nécessitent donc un jugement plus primitif : " A est une proposition ". De nombreux autres jugements ont été étudiés ; par exemple, " A est faux " (voir logique classique ), " A est vrai à l'instant t " (voir logique temporelle ), " A est nécessairement vrai " ou " A est éventuellement vrai " (voir logique modale ), " le programme M est de type τ " (voir langages de programmation et théorie des types ), " A est réalisable à partir des ressources disponibles " (voir logique linéaire ), et bien d'autres. Pour commencer, nous nous intéresserons aux deux jugements les plus simples « A est une proposition » et « A est vrai », abrégés respectivement par « A prop » et « A true ».

Le jugement " A prop " définit la structure des preuves valides de A , qui à son tour définit la structure des propositions. Pour cette raison, les règles d'inférence pour ce jugement sont parfois appelées règles de formation . Pour illustrer, si nous avons deux propositions A et B (c'est-à-dire que les jugements " A prop " et " B prop " sont évidents), alors nous formons la proposition composée A et B , écrite symboliquement comme " ". On peut écrire cela sous la forme d'une règle d'inférence : ${\style d'affichage A\coin B}$

${\displaystyle {\frac {A{\hbox{ prop}}\qquad B{\hbox{ prop}}}{(A\wedge B){\hbox{ prop}}}}\ \wedge _{F}}$

où les parenthèses sont omises pour rendre la règle d'inférence plus succincte :

${\displaystyle {\frac {A{\hbox{ prop}}\qquad B{\hbox{ prop}}}{A\wedge B{\hbox{ prop}}}}\ \wedge _{F}}$

Cette règle d'inférence est schématique : A et B peuvent être instanciés avec n'importe quelle expression. La forme générale d'une règle d'inférence est :

${\displaystyle {\frac {J_{1}\qquad J_{2}\qquad \cdots \qquad J_{n}}{J}}\ {\hbox{name}}}$

où chacun est un jugement et la règle d'inférence est nommée "nom". Les jugements au-dessus de la ligne sont appelés prémisses et ceux en dessous de la ligne sont des conclusions . D'autres propositions logiques courantes sont la disjonction ( ), la négation ( ), l'implication ( ) et les constantes logiques vérité ( ) et fausseté ( ). Leurs règles de formation sont ci-dessous. ${\style d'affichage J_{i}}$${\displaystyle A\vee B}$${\style d'affichage \neg A}$${\displaystyle A\supset B}$${\style d'affichage \top }$${\displaystyle \bot }$

${\displaystyle {\frac {A{\hbox{ prop}}\qquad B{\hbox{ prop}}}{A\vee B{\hbox{ prop}}}}\ \vee _{F}\qquad { \frac {A{\hbox{ prop}}\qquad B{\hbox{ prop}}}{A\supset B{\hbox{ prop}}}}\ \supset _{F}}$

${\displaystyle {\frac {\hbox{ }}{\top {\hbox{ prop}}}}\ \top _{F}\qquad {\frac {\hbox{ }}{\bot {\hbox{ prop }}}}\ \bot _{F}\qquad {\frac {A{\hbox{ prop}}}{\neg A{\hbox{ prop}}}}\ \neg _{F}}$

Introduction et élimination

Nous discutons maintenant du jugement « Un vrai ». Les règles d'inférence qui introduisent un connecteur logique dans la conclusion sont appelées règles d'introduction . Pour introduire des conjonctions, c'est -à- dire pour conclure « A et B vrais » pour les propositions A et B , il faut des preuves de « A vrai » et « B vrai ». Comme règle d'inférence :

Il faut comprendre que dans de telles règles les objets sont des propositions. C'est-à-dire que la règle ci-dessus est en réalité une abréviation pour :

Cela peut aussi s'écrire :

Sous cette forme, la première prémisse peut être satisfaite par la règle de formation, donnant les deux premières prémisses de la forme précédente. Dans cet article, nous éluderons les jugements "prop" là où ils sont compris. Dans le cas nul, on ne peut tirer la vérité d'aucune prémisse. ${\displaystyle \wedge _{F}}$

Si la vérité d'une proposition peut être établie de plusieurs manières, le connecteur correspondant a de multiples règles d'introduction.

Notez que dans le cas nul, c'est -à- dire pour le mensonge, il n'y a pas de règles d'introduction. Ainsi, on ne peut jamais déduire le mensonge de jugements plus simples.

Les règles d'introduction duales sont des règles d' élimination décrivant comment déconstruire les informations sur une proposition composée en informations sur ses constituants. Ainsi, à partir de « A ∧ B vrai », on peut conclure « A vrai » et « B vrai » :

Comme exemple d'utilisation des règles d'inférence, considérons la commutativité de la conjonction. Si A ∧ B est vrai, alors B ∧ A est vrai; cette dérivation peut être tirée en composant des règles d'inférence de telle manière que les prémisses d'une inférence inférieure correspondent à la conclusion de la prochaine inférence supérieure.

Les chiffres d'inférence que nous avons vus jusqu'à présent ne sont pas suffisants pour énoncer les règles d' introduction d'implication ou d' élimination de disjonction ; pour ceux-ci, nous avons besoin d'une notion plus générale de dérivation hypothétique .

Dérivations hypothétiques

Une opération omniprésente dans la logique mathématique est le raisonnement à partir d'hypothèses . Par exemple, considérons la dérivation suivante :

Cette dérivation n'établit pas la vérité de B en tant que telle ; il établit plutôt le fait suivant :

Si A (B ∧ C) est vrai alors B est vrai .

En logique, on dit « en supposant que A (B ∧ C) est vrai, on montre que B est vrai » ; en d'autres termes, le jugement " B vrai" dépend du jugement supposé " A (B ∧ C) vrai". Il s'agit d'une dérivation hypothétique , que nous écrivons comme suit :

L'interprétation est : " B vrai est dérivable de A (B ∧ C) vrai ". Bien sûr, dans cet exemple spécifique, nous connaissons en fait la dérivation de " B vrai" à partir de " A (B ∧ C) vrai", mais en général, nous pouvons ne pas connaître a priori la dérivation. La forme générale d'une dérivation hypothétique est :

Chaque dérivation hypothétique a une collection de dérivations antécédentes (le D _i ) écrite sur la ligne du haut, et un jugement successif ( J ) écrit sur la ligne du bas. Chacune des prémisses peut elle-même être une dérivation hypothétique. (Pour simplifier, nous traitons un jugement comme une dérivation sans prémisse.)

La notion de jugement hypothétique est intériorisée comme le connecteur d'implication. Les règles d'introduction et d'élimination sont les suivantes.

Dans la règle d'introduction, l'antécédent nommé u est déchargé dans la conclusion. C'est un mécanisme pour délimiter la portée de l'hypothèse : sa seule raison d'être est d'établir « B vrai » ; il ne peut pas être utilisé à d'autres fins, et en particulier, il ne peut pas être utilisé en dessous de l'introduction. A titre d'exemple, considérons la dérivation de " A ⊃ (B ⊃ (A ∧ B)) true":

Cette dérivation complète n'a pas de prémisses insatisfaites ; cependant, les sous-dérivations sont hypothétiques. Par exemple, la dérivation de " B ⊃ (A ∧ B) true" est hypothétique avec l'antécédent " A true" (nommé u ).

Avec des dérivations hypothétiques, nous pouvons maintenant écrire la règle d'élimination pour la disjonction :

En mots, si A B est vrai, et que nous pouvons dériver « C vrai » à la fois de « A vrai » et de « B vrai », alors C est bien vrai. Notez que cette règle ne s'engage ni sur " A vrai " ni sur " B vrai ". Dans le cas zéro-aire, c'est- à- dire pour le mensonge, on obtient la règle d'élimination suivante :

Cela se lit comme suit : si le mensonge est vrai, alors toute proposition C est vraie.

La négation est semblable à l'implication.

Les décharges de règles d'introduction fois le nom de l'hypothèse u , et succédente p , par exemple , la proposition p ne doit pas se produire dans la conclusion A . Puisque ces règles sont schématiques, l'interprétation de la règle d'introduction est : si de " A vrai " nous pouvons déduire pour chaque proposition p que " p vrai ", alors A doit être faux, c'est -à- dire " pas A vrai ". Pour l'élimination, si A et non A sont montrés vrais, alors il y a une contradiction, auquel cas chaque proposition C est vraie. Parce que les règles d'implication et de négation sont si similaires, il devrait être assez facile de voir que A et A ⊥ ne sont pas équivalents, c'est-à-dire que chacun est dérivable de l'autre.

Cohérence, exhaustivité et formes normales

Une théorie est dite cohérente si le mensonge n'est pas prouvable (à partir d'aucune hypothèse) et est complète si chaque théorème ou sa négation est prouvable en utilisant les règles d'inférence de la logique. Ce sont des déclarations sur l'ensemble de la logique, et sont généralement liées à une notion de modèle . Cependant, il existe des notions locales de cohérence et de complétude qui sont des vérifications purement syntaxiques des règles d'inférence et ne nécessitent aucun recours à des modèles. La première d'entre elles est la cohérence locale, également appelée réductibilité locale, qui dit que toute dérivation contenant une introduction d'un connecteur suivie immédiatement de son élimination peut être transformée en une dérivation équivalente sans ce détour. C'est un contrôle sur la force des règles d'élimination : elles ne doivent pas être si fortes qu'elles incluent des connaissances qui ne sont pas déjà contenues dans leurs locaux. À titre d'exemple, considérons les conjonctions.

────── u   ────── w
A true     B true
────────────────── ∧I
    A ∧ B true
    ────────── ∧E1
      A true

────── u
A true

Doublement, la complétude locale dit que les règles d'élimination sont suffisamment fortes pour décomposer un connecteur en les formes appropriées à sa règle d'introduction. Encore une fois pour les conjonctions :

────────── u
A ∧ B true

────────── u    ────────── u
A ∧ B true      A ∧ B true
────────── ∧E1  ────────── ∧E2
  A true          B true
  ─────────────────────── ∧I
       A ∧ B true

Ces notions correspondent exactement à la -réduction (réduction bêta) et à la -conversion (conversion eta) dans le lambda calcul , en utilisant l' isomorphisme de Curry-Howard . Par complétude locale, nous voyons que chaque dérivation peut être convertie en une dérivation équivalente où le connecteur principal est introduit. En fait, si toute la dérivation obéit à cet ordre d'éliminations suivies d'introductions, alors elle est dite normale . Dans une dérivation normale, toutes les éliminations se produisent au-dessus des introductions. Dans la plupart des logiques, chaque dérivation a une dérivation normale équivalente, appelée forme normale . L'existence de formes normales est généralement difficile à prouver en utilisant la déduction naturelle seule, bien que de tels récits existent dans la littérature, notamment par Dag Prawitz en 1961. Il est beaucoup plus facile de le montrer indirectement au moyen d'une présentation de calcul séquentiel sans coupure . .

Extensions de premier ordre et d'ordre supérieur

Résumé du système de premier ordre

La logique de la section précédente est un exemple de logique à tri unique , c'est -à- dire une logique avec un seul type d'objet : les propositions. De nombreuses extensions de ce cadre simple ont été proposées ; dans cette section, nous l'étendrons avec une deuxième sorte d' individus ou de termes . Plus précisément, nous ajouterons un nouveau type de jugement, " t est un terme " (ou " t terme ") où t est schématique. Nous allons fixer un ensemble dénombrable V de variables , un autre ensemble dénombrable F de symboles de fonction , et construire des termes avec les règles de formation suivantes :

${\displaystyle {\frac {v\in V}{v{\hbox{ term}}}}{\hbox{ var}}_{F}}$

et

${\displaystyle {\frac {f\in F\qquad t_{1}{\hbox{ term}}\qquad t_{2}{\hbox{ term}}\qquad \cdots \qquad t_{n}{\hbox { term}}}{f(t_{1},t_{2},\cdots ,t_{n}){\hbox{ term}}}}{\hbox{ app}}_{F}}$

Pour les propositions, nous considérons un troisième ensemble dénombrable P de prédicats , et définissons des prédicats atomiques sur des termes avec la règle de formation suivante :

${\displaystyle {\frac {\phi \in P\qquad t_{1}{\hbox{ terme}}\qquad t_{2}{\hbox{ terme}}\qquad \cdots \qquad t_{n}{\ hbox{ term}}}{\phi (t_{1},t_{2},\cdots ,t_{n}){\hbox{ prop}}}}{\hbox{ pred}}_{F}}$

Les deux premières règles de formation fournissent une définition d'un terme qui est effectivement la même que celle définie dans l' algèbre des termes et la théorie des modèles , bien que l'objectif de ces domaines d'étude soit assez différent de la déduction naturelle. La troisième règle de formation définit effectivement une formule atomique , comme dans la logique du premier ordre , et encore dans la théorie des modèles.

A celles-ci s'ajoutent une paire de règles de formation, définissant la notation des propositions quantifiées ; un pour la quantification universelle (∀) et existentielle (∃) :

${\displaystyle {\frac {x\in V\qquad A{\hbox{ prop}}}{\forall xA{\hbox{ prop}}}}\;\forall _{F}\qquad \qquad {\frac {x\in V\qquad A{\hbox{ prop}}}{\exists xA{\hbox{ prop}}}}\;\exists _{F}}$

Le quantificateur universel a les règles d'introduction et d'élimination :

${\displaystyle {\begin{matrix}{\cfrac {}{a{\hbox{ term}}}}{\hbox{ u}}\\\vdots \\{\cfrac {[a/x]A{\ hbox{ true}}}{\forall xA{\hbox{ true}}}}\;\forall _{I^{u,a}}\end{matrice}}\qquad \qquad {\frac {\forall xA {\hbox{ true}}\qquad t{\hbox{ term}}}{[t/x]A{\hbox{ true}}}}\;\forall _{E}}$

Le quantificateur existentiel a les règles d'introduction et d'élimination :

${\displaystyle {\frac {[t/x]A{\hbox{ true}}}{\existe xA{\hbox{ true}}}}\;\existe _{I}\qquad \qquad {\cfrac { {\begin{matrice}\\\\\\\\\existe xA{\hbox{ true}}\\\end{matrice}}\qquad {\begin{matrice}{\cfrac {}{a{\hbox { terme}}}}{\hbox{ u}}\qquad {\cfrac {}{[a/x]A{\hbox{ true}}}}{\hbox{ v}}\\\vdots \\C {\hbox{ true}}\\\end{matrix}}}{C{\hbox{ true}}}}\exists _{E^{a,u,v}}}$

Dans ces règles, la notation [ t / x ] A représente la substitution de t pour chaque instance (visible) de x dans A , évitant la capture. Comme auparavant, les exposants du nom représentent les composants qui sont déchargés : le terme a ne peut pas apparaître dans la conclusion de ∀I (de tels termes sont appelés variables propres ou paramètres ), et les hypothèses nommées u et v dans ∃E sont localisées à la deuxième prémisse dans une dérivation hypothétique. Bien que la logique propositionnelle des sections précédentes soit décidable , l'ajout des quantificateurs rend la logique indécidable.

Jusqu'à présent, les extensions quantifiées sont du premier ordre : elles distinguent les propositions des types d'objets quantifiés. La logique d'ordre supérieur adopte une approche différente et n'a qu'un seul type de propositions. Les quantificateurs ont comme domaine de quantification exactement le même genre de propositions, comme reflété dans les règles de formation :

${\displaystyle {\cfrac {\begin{matrix}{\cfrac {}{\hbox{ prop}}}}{\hbox{ u}}\\\vdots \\A{\hbox{ prop}}\ \\end{matrice}}{\forall pA{\hbox{ prop}}}}\;\forall _{F^{u}}\qquad \qquad {\cfrac {\begin{matrix}{\cfrac {} {p{\hbox{ prop}}}}{\hbox{ u}}\\\vdots \\A{\hbox{ prop}}\\\end{matrice}}{\existe pA{\hbox{ prop} }}}\;\existe _{F^{u}}}$

Une discussion sur les formes d'introduction et d'élimination pour la logique d'ordre supérieur dépasse le cadre de cet article. Il est possible d'être entre les logiques de premier ordre et d'ordre supérieur. Par exemple, la logique du second ordre a deux types de propositions, un type quantifiant sur des termes et le second type quantifiant sur des propositions du premier type.

Différentes présentations de la déduction naturelle

Présentations arborescentes

Décharge de Gentzen annotations utilisées pour internaliser les jugements hypothétiques peuvent être évités en représentant des preuves comme un arbre de séquent Γ ⊢A au lieu d'un arbre de A vrai jugements.

Présentations séquentielles

Les représentations de Jaśkowski de la déduction naturelle ont conduit à différentes notations telles que le calcul à la Fitch (ou les diagrammes de Fitch) ou la méthode de Suppes , dont Lemmon a donné une variante appelée système L . De tels systèmes de présentation, qui sont décrits plus précisément sous forme de tableaux, comprennent les suivants.

• 1940 : Dans un manuel, Quine a indiqué les dépendances antécédentes par des numéros de ligne entre crochets, anticipant la notation de numéro de ligne de 1957 de Suppes.
• 1950 : Dans un manuel, Quine (1982 , pp. 241-255) a démontré une méthode consistant à utiliser un ou plusieurs astérisques à gauche de chaque ligne de preuve pour indiquer les dépendances. C'est l'équivalent des barres verticales de Kleene. (Il n'est pas tout à fait clair si la notation astérisque de Quine est apparue dans l'édition originale de 1950 ou a été ajoutée dans une édition ultérieure.)
• 1957 : Une introduction à la démonstration du théorème de logique pratique dans un manuel de Suppes (1999 , pp. 25-150). Cela indiquait les dépendances (c'est-à-dire les propositions d'antécédents) par des numéros de ligne à gauche de chaque ligne.
• 1963 : Stoll (1979 , pp. 183-190, 215-219) utilise des ensembles de numéros de ligne pour indiquer les dépendances antécédentes des lignes d'arguments logiques séquentiels basés sur des règles d'inférence de déduction naturelle.
• 1965 : L'ensemble du manuel de Lemmon (1965) est une introduction aux preuves logiques utilisant une méthode inspirée de celle de Suppes.
• 1967 : Dans un manuel, Kleene (2002 , pp. 50-58, 128-130) a brièvement démontré deux types de preuves logiques pratiques, un système utilisant des citations explicites de propositions antécédentes à gauche de chaque ligne, l'autre système utilisant une barre verticale -lignes à gauche pour indiquer les dépendances.

Preuves et théorie des types

La présentation de la déduction naturelle jusqu'ici s'est concentrée sur la nature des propositions sans donner une définition formelle d'une preuve . Pour formaliser la notion de preuve, nous modifions légèrement la présentation des dérivations hypothétiques. Nous étiquetons les antécédents avec des variables de preuve (à partir d'un ensemble dénombrable V de variables), et décorons le successeur avec la preuve réelle. Les antécédents ou hypothèses sont séparés du successeur au moyen d'un tourniquet (⊢). Cette modification passe parfois sous le nom d' hypothèses localisées . Le schéma suivant résume le changement.

──── u1 ──── u2 ... ──── un
 J1      J2          Jn
              ⋮
              J

u1:J1, u2:J2, ..., un:Jn ⊢ J

L'ensemble des hypothèses s'écrira Γ lorsque leur composition exacte n'est pas pertinente. Pour rendre les preuves explicites, on passe du jugement sans preuve " Un vrai " à un jugement : " π est une preuve de (Un vrai) ", qui s'écrit symboliquement comme " π : Un vrai ". Suivant l'approche standard, les preuves sont spécifiées avec leurs propres règles de formation pour le jugement « π preuve ». La preuve la plus simple possible est l'utilisation d'une hypothèse étiquetée ; dans ce cas, la preuve est l'étiquette elle-même.

u ∈ V
─────── proof-F
u proof

───────────────────── hyp
u:A true ⊢ u : A true

Par souci de concision, nous laisserons de côté l'étiquette de jugement true dans le reste de cet article, c'est -à- dire écrivez "Γ ⊢ π : A ". Revoyons quelques-uns des connecteurs avec des preuves explicites. Pour la conjonction, on regarde la règle d'introduction ∧I pour découvrir la forme des preuves de conjonction : elles doivent être une paire de preuves des deux conjoints. Ainsi:

π1 proof    π2 proof
──────────────────── pair-F
(π1, π2) proof

Γ ⊢ π1 : A    Γ ⊢ π2 : B
───────────────────────── ∧I
Γ ⊢ (π1, π2) : A ∧ B

Les règles d'élimination ∧E ₁ et ∧E ₂ sélectionnent soit la conjointe gauche soit la conjointe droite ; ainsi les preuves sont une paire de projections—première ( fst ) et deuxième ( snd ).

π proof
─────────── fst-F
fst π proof

Γ ⊢ π : A ∧ B
───────────── ∧E1
Γ ⊢ fst π : A

π proof
─────────── snd-F
snd π proof

Γ ⊢ π : A ∧ B
───────────── ∧E2
Γ ⊢ snd π : B

Pour l'implication, la forme d'introduction localise ou lie l'hypothèse, écrite à l'aide d'un ; cela correspond à l'étiquette déchargée. Dans la règle, " , u : A " représente l'ensemble des hypothèses Γ, avec l'hypothèse supplémentaire u .

π proof
──────────── λ-F
λu. π proof

Γ, u:A ⊢ π : B
───────────────── ⊃I
Γ ⊢ λu. π : A ⊃ B

π1 proof   π2 proof
─────────────────── app-F
π1 π2 proof

Γ ⊢ π1 : A ⊃ B    Γ ⊢ π2 : A
──────────────────────────── ⊃E
Γ ⊢ π1 π2 : B

Avec des preuves disponibles explicitement, on peut manipuler et raisonner sur les preuves. L'opération clé sur les preuves est la substitution d'une preuve à une hypothèse utilisée dans une autre preuve. Ceci est communément connu sous le nom de théorème de substitution , et peut être prouvé par induction sur la profondeur (ou la structure) du second jugement.

Théorème de substitution

Si Γ ⊢ π ₁  : A et Γ, u : A ⊢ π ₂  : B , alors Γ ⊢ [π ₁ / u ] π ₂  : B.

Jusqu'à présent, le jugement " ⊢ π : A " a eu une interprétation purement logique. Dans la théorie des types , la vue logique est remplacée par une vue plus computationnelle des objets. Les propositions dans l'interprétation logique sont maintenant vues comme des types , et les preuves comme des programmes dans le lambda calcul . Ainsi l'interprétation de " : A " est " le programme π est de type A ". Les connecteurs logiques reçoivent également une lecture différente : la conjonction est considérée comme un produit (×), l'implication comme la flèche de fonction (→), etc. Les différences ne sont cependant que cosmétiques. La théorie des types a une présentation de déduction naturelle en termes de règles de formation, d'introduction et d'élimination ; en fait, le lecteur peut facilement reconstruire ce que l'on appelle la théorie des types simples à partir des sections précédentes.

La différence entre la logique et la théorie des types est principalement un déplacement de l'attention des types (propositions) vers les programmes (preuves). La théorie des types s'intéresse principalement à la convertibilité ou à la réductibilité des programmes. Pour chaque type, il existe des programmes canoniques de ce type qui sont irréductibles ; celles-ci sont appelées formes ou valeurs canoniques . Si chaque programme peut être réduit à une forme canonique, alors la théorie des types est dite normalisante (ou normalisant faiblement ). Si la forme canonique est unique, alors la théorie est dite fortement normalisante . La normalisabilité est une caractéristique rare de la plupart des théories de type non triviales, ce qui est un grand écart par rapport au monde logique. (Rappelez-vous que presque toutes les dérivations logiques ont une dérivation normale équivalente.) Pour esquisser la raison : dans les théories des types qui admettent des définitions récursives, il est possible d'écrire des programmes qui ne se réduisent jamais à une valeur ; de tels programmes de bouclage peuvent généralement être de n'importe quel type. En particulier, le programme de bouclage a le type ⊥, bien qu'il n'y ait pas de preuve logique de " vrai ". Pour cette raison, les propositions comme types ; les preuves en tant que paradigme des programmes ne fonctionnent que dans un sens, voire pas du tout : interpréter une théorie des types comme une logique donne généralement une logique incohérente.

Exemple : Théorie des types dépendants

Comme la logique, la théorie des types a de nombreuses extensions et variantes, y compris des versions de premier ordre et d'ordre supérieur. Une branche, connue sous le nom de théorie des types dépendants , est utilisée dans un certain nombre de systèmes de preuve assistés par ordinateur. La théorie des types dépendants permet aux quantificateurs de s'étendre sur les programmes eux-mêmes. Ces types quantifiés s'écrivent Π et Σ au lieu de ∀ et ∃, et ont les règles de formation suivantes :

Γ ⊢ A type    Γ, x:A ⊢ B type
───────────────────────────── Π-F
Γ ⊢ Πx:A. B type

Γ ⊢ A type  Γ, x:A ⊢ B type
──────────────────────────── Σ-F
Γ ⊢ Σx:A. B type

Ces types sont des généralisations des types de flèche et de produit, respectivement, comme en témoignent leurs règles d'introduction et d'élimination.

Γ, x:A ⊢ π : B
──────────────────── ΠI
Γ ⊢ λx. π : Πx:A. B

Γ ⊢ π1 : Πx:A. B   Γ ⊢ π2 : A
───────────────────────────── ΠE
Γ ⊢ π1 π2 : [π2/x] B

Γ ⊢ π1 : A    Γ, x:A ⊢ π2 : B
───────────────────────────── ΣI
Γ ⊢ (π1, π2) : Σx:A. B

Γ ⊢ π : Σx:A. B
──────────────── ΣE1
Γ ⊢ fst π : A

Γ ⊢ π : Σx:A. B
──────────────────────── ΣE2
Γ ⊢ snd π : [fst π/x] B

La théorie des types dépendants en pleine généralité est très puissante : elle est capable d'exprimer presque toutes les propriétés imaginables des programmes directement dans les types du programme. Cette généralité a un prix élevé - soit la vérification des types est indécidable ( théorie des types extensionnels ), soit le raisonnement extensionnel est plus difficile ( théorie des types intensionnels ). Pour cette raison, certaines théories des types dépendants n'autorisent pas la quantification sur des programmes arbitraires, mais se limitent plutôt aux programmes d'un domaine d'index décidable donné , par exemple des entiers, des chaînes ou des programmes linéaires.

Puisque les théories des types dépendants permettent aux types de dépendre des programmes, une question naturelle à se poser est de savoir s'il est possible que les programmes dépendent des types, ou de toute autre combinaison. Il existe plusieurs types de réponses à ces questions. Une approche populaire en théorie des types consiste à permettre la quantification des programmes sur des types, également connu sous le nom de polymorphisme paramétrique ; de cela, il y a deux sortes principales : si les types et les programmes sont séparés, alors on obtient un système un peu plus bien comporté appelé polymorphisme prédicatif ; si la distinction entre programme et type est floue, on obtient l'analogue théorique de type de la logique d'ordre supérieur, également connu sous le nom de polymorphisme imprédicatif . Diverses combinaisons de dépendance et de polymorphisme ont été envisagées dans la littérature, la plus connue étant le cube lambda de Henk Barendregt .

L'intersection de la logique et de la théorie des types est un domaine de recherche vaste et actif. Les nouvelles logiques sont généralement formalisées dans un cadre théorique de type général, appelé cadre logique . Les cadres logiques modernes populaires tels que le calcul des constructions et la LF sont basés sur la théorie des types dépendants d'ordre supérieur, avec divers compromis en termes de décidabilité et de pouvoir d'expression. Ces cadres logiques sont eux-mêmes toujours spécifiés comme des systèmes de déduction naturelle, ce qui témoigne de la polyvalence de l'approche de la déduction naturelle.

Logiques classiques et modales

Pour simplifier, les logiques présentées jusqu'ici ont été intuitionnistes . La logique classique étend la logique intuitionniste avec un axiome supplémentaire ou principe du tiers exclu :

Pour toute proposition p, la proposition p ¬p est vraie.

Cette affirmation n'est évidemment ni une introduction ni une élimination ; en effet, il s'agit de deux connecteurs distincts. Le traitement original de Gentzen du tiers exclu prescrivait l'une des trois formulations (équivalentes) suivantes, qui étaient déjà présentes sous des formes analogues dans les systèmes de Hilbert et Heyting :

────────────── XM1
A ∨ ¬A true

¬¬A true
────────── XM2
A true

──────── u
¬A true
⋮
p true
────── XM3u, p
A true

(XM ₃ est simplement XM ₂ exprimé en termes de E.) Ce traitement du tiers exclu, en plus d'être répréhensible du point de vue d'un puriste, introduit des complications supplémentaires dans la définition des formes normales.

Un traitement comparativement plus satisfaisant de la déduction naturelle classique en termes de règles d'introduction et d'élimination a été proposé pour la première fois par Parigot en 1992 sous la forme d'un lambda-calcul classique appelé λμ . L'idée clé de son approche était de remplacer un jugement centré sur la vérité A vrai par une notion plus classique, rappelant le calcul des séquences : sous forme localisée, au lieu de Γ ⊢ A , il a utilisé Γ ⊢ Δ, avec Δ une collection de propositions semblable à Γ. Γ a été traité comme une conjonction et Δ comme une disjonction. Cette structure est essentiellement tirée directement des calculs séquentiels classiques , mais l'innovation dans λμ était de donner un sens informatique aux preuves classiques de déduction naturelle en termes de callcc ou de mécanisme lancer/attraper vu dans LISP et ses descendants. (Voir aussi : contrôle de première classe .)

Une autre extension importante concernait les logiques modales et autres qui nécessitent plus que le simple jugement de base de la vérité. Celles-ci ont été décrites pour la première fois, pour les logiques modales aléthiques S4 et S5 , dans un style de déduction naturelle par Prawitz en 1965, et ont depuis accumulé un grand nombre de travaux connexes. Pour donner un exemple simple, la logique modale S4 requiert un nouveau jugement, " A valide ", qui est catégorique par rapport à la vérité :

Si "A vrai" sous aucune hypothèse de la forme "B vrai", alors "A valide".

Ce jugement catégorique est intériorisé comme un connecteur unaire A (lire « nécessairement A ») avec les règles d'introduction et d'élimination suivantes :

A valid
──────── ◻I
◻ A true

◻ A true
──────── ◻E
A true

Notez que la prémisse « A valide » n'a pas de règles de définition ; au lieu de cela, la définition catégorique de la validité est utilisée à sa place. Ce mode se précise sous la forme localisée lorsque les hypothèses sont explicites. On écrit "Ω;Γ ⊢ A vrai " où Γ contient les hypothèses vraies comme précédemment, et Ω contient les hypothèses valides. A droite il n'y a qu'un seul jugement " A vrai " ; la validité n'est pas nécessaire ici puisque " ⊢ A valid " est par définition identique à " Ω;⋅ ⊢ A true ". Les formulaires d'introduction et d'élimination sont alors :

Ω;⋅ ⊢ π : A true
──────────────────── ◻I
Ω;⋅ ⊢ box π : ◻ A true

Ω;Γ ⊢ π : ◻ A true
────────────────────── ◻E
Ω;Γ ⊢ unbox π : A true

Les hypothèses modales ont leur propre version de la règle d'hypothèse et du théorème de substitution.

─────────────────────────────── valid-hyp
Ω, u: (A valid) ; Γ ⊢ u : A true

Théorème de substitution modale

Si Ω;⋅ ⊢ π ₁  : A vrai et Ω, u : ( A valide ) ; Γ ⊢ π ₂  : C vrai , alors Ω;Γ ⊢ [π ₁ / u ] π ₂  : C vrai .

Ce cadre de séparation des jugements en collections distinctes d'hypothèses, également connu sous le nom de contextes multi-zones ou polyadiques , est très puissant et extensible ; il a été appliqué à de nombreuses logiques modales différentes, ainsi qu'à des logiques linéaires et autres sous-structurales , pour donner quelques exemples. Cependant, relativement peu de systèmes de logique modale peuvent être formalisés directement en déduction naturelle. Donner des caractérisations théoriques de la preuve de ces systèmes, des extensions telles que l'étiquetage ou des systèmes d'inférence profonde.

L'ajout d'étiquettes aux formules permet un contrôle beaucoup plus fin des conditions dans lesquelles les règles s'appliquent, permettant d'appliquer les techniques plus flexibles des tableaux analytiques , comme cela a été fait dans le cas de la déduction étiquetée . Les étiquettes permettent également de nommer des mondes dans la sémantique de Kripke ; Simpson (1993) présente une technique influente pour convertir les conditions de cadre des logiques modales dans la sémantique de Kripke en règles d'inférence dans une formalisation de déduction naturelle de la logique hybride . Stouppa (2004) examine l'application de nombreuses théories de la preuve, telles que les hyperséquents d' Avron et Pottinger et la logique d'affichage de Belnap à des logiques modales telles que S5 et B.

Comparaison avec d'autres approches fondamentales

Calcul séquentiel

Le calcul des séquences est la principale alternative à la déduction naturelle comme fondement de la logique mathématique . En déduction naturelle, le flux d'information est bidirectionnel : les règles d'élimination font circuler l'information vers le bas par déconstruction, et les règles d'introduction font circuler l'information vers le haut par assemblage. Ainsi, une preuve par déduction naturelle n'a pas de lecture purement ascendante ou descendante, ce qui la rend impropre à l'automatisation dans la recherche de preuves. Pour remédier à ce fait, Gentzen a proposé en 1935 son calcul des séquences , bien qu'il l'ait initialement conçu comme un dispositif technique pour clarifier la cohérence de la logique des prédicats . Kleene , dans son livre fondateur de 1952 Introduction to Metamathematics , a donné la première formulation du calcul des séquences dans le style moderne.

Dans le calcul des séquences, toutes les règles d'inférence ont une lecture purement ascendante. Les règles d' inférence peuvent s'appliquer aux éléments des deux côtés du tourniquet . (Pour différencier de la déduction naturelle, cet article utilise une double flèche au lieu de la pointe de droite ⊢ pour les séquences.) Les règles d'introduction de la déduction naturelle sont considérées comme des règles correctes dans le calcul des séquences et sont structurellement très similaires. Les règles d'élimination, quant à elles, se transforment en règles de gauche dans le calcul des séquences. Pour donner un exemple, considérons la disjonction ; les bonnes règles sont familières :

Γ ⇒ A
───────── ∨R1
Γ ⇒ A ∨ B

Γ ⇒ B
───────── ∨R2
Γ ⇒ A ∨ B

À gauche:

Γ, u:A ⇒ C       Γ, v:B ⇒ C
─────────────────────────── ∨L
Γ, w: (A ∨ B) ⇒ C

Rappelons la règle de déduction naturelle ∨E sous forme localisée :

Γ ⊢ A ∨ B    Γ, u:A ⊢ C    Γ, v:B ⊢ C
─────────────────────────────────────── ∨E
Γ ⊢ C

La proposition A ∨ B , qui succède à une prémisse dans ∨E, se transforme en hypothèse de conclusion dans la règle de gauche ∨L. Ainsi, les règles de gauche peuvent être vues comme une sorte de règle d'élimination inversée. Cette observation peut être illustrée comme suit :

 ────── hyp
 |
 | elim. rules
 |
 ↓
 ────────────────────── ↑↓ meet
 ↑
 |
 | intro. rules
 |
 conclusion

 ─────────────────────────── init
 ↑            ↑
 |            |
 | left rules | right rules
 |            |
 conclusion

Dans le calcul des séquences, les règles de gauche et de droite sont exécutées en lock-step jusqu'à ce que l'on atteigne la séquence initiale , qui correspond au point de rencontre des règles d'élimination et d'introduction en déduction naturelle. Ces règles initiales sont superficiellement similaires à la règle d'hypothèse de la déduction naturelle, mais dans le calcul des séquences, elles décrivent une transposition ou une poignée de main d'une proposition à gauche et à droite :

────────── init
Γ, u:A ⇒ A

La correspondance entre le calcul des séquents et la déduction naturelle est une paire de théorèmes de solidité et de complétude, qui sont tous deux prouvables au moyen d'un argument inductif.

Solidité de ⇒ wrt. ??

Si Γ ⇒ A , alors Γ ⊢ A .

Intégralité de ⇒ wrt. ??

Si Γ ⊢ A , alors Γ ⇒ A .

Il est clair par ces théorèmes que le calcul des séquences ne change pas la notion de vérité, car la même collection de propositions reste vraie. Ainsi, on peut utiliser les mêmes objets de preuve que précédemment dans les dérivations de calcul séquentiel. A titre d'exemple, considérons les conjonctions. La règle de droite est pratiquement identique à la règle d'introduction

Γ ⇒ π1 : A     Γ ⇒ π2 : B
─────────────────────────── ∧R
Γ ⇒ (π1, π2) : A ∧ B

Γ ⊢ π1 : A      Γ ⊢ π2 : B
───────────────────────── ∧I
Γ ⊢ (π1, π2) : A ∧ B

La règle de gauche, cependant, effectue certaines substitutions supplémentaires qui ne sont pas effectuées dans les règles d'élimination correspondantes.

Γ, u:A ⇒ π : C
──────────────────────────────── ∧L1
Γ, v: (A ∧ B) ⇒ [fst v/u] π : C

Γ ⊢ π : A ∧ B
───────────── ∧E1
Γ ⊢ fst π : A

Γ, u:B ⇒ π : C
──────────────────────────────── ∧L2
Γ, v: (A ∧ B) ⇒ [snd v/u] π : C

Γ ⊢ π : A ∧ B
───────────── ∧E2
Γ ⊢ snd π : B

Les sortes de preuves générées dans le calcul des séquents sont donc assez différentes de celles de la déduction naturelle. Le calcul des séquences produit des preuves sous la forme dite -normale η-longue , qui correspond à une représentation canonique de la forme normale de la preuve par déduction naturelle. Si l'on tente de décrire ces preuves en utilisant la déduction naturelle elle-même, on obtient ce qu'on appelle le calcul d'intercalation (décrit pour la première fois par John Byrnes), qui peut être utilisé pour définir formellement la notion de forme normale pour la déduction naturelle.

Le théorème de substitution de la déduction naturelle prend la forme d'une règle structurelle ou théorème structurel dit coupé dans le calcul des séquences.

Couper (remplacement)

Si Γ ⇒ π ₁  : A et Γ, u : A ⇒ π ₂  : C , alors Γ ⇒ [π ₁ /u] π ₂  : C .

Dans la plupart des logiques bien conduites, la coupe est inutile en tant que règle d'inférence, bien qu'elle reste prouvable en tant que méta-théorème ; le caractère superflu de la règle de coupe est généralement présenté comme un processus de calcul, connu sous le nom d' élimination de coupe . Ceci a une application intéressante pour la déduction naturelle ; il est généralement extrêmement fastidieux de prouver certaines propriétés directement en déduction naturelle à cause d'un nombre illimité de cas. Par exemple, envisagez de montrer qu'une proposition donnée n'est pas prouvable en déduction naturelle. Un argument inductif simple échoue à cause de règles comme ∨E ou E qui peuvent introduire des propositions arbitraires. Cependant, nous savons que le calcul des séquences est complet par rapport à la déduction naturelle, il suffit donc de montrer cette indémontrabilité dans le calcul des séquences. Maintenant, si cut n'est pas disponible en tant que règle d'inférence, alors toutes les règles séquentielles introduisent un connecteur à droite ou à gauche, de sorte que la profondeur d'une dérivation séquentielle est entièrement limitée par les connecteurs dans la conclusion finale. Ainsi, montrer l'unprouvabilité est beaucoup plus facile, car il n'y a qu'un nombre fini de cas à considérer, et chaque cas est composé entièrement de sous-propositions de la conclusion. Un exemple simple de ceci est le théorème de cohérence globale : " ⋅ ⊢ ⊥ true " n'est pas prouvable. Dans la version du calcul des séquences, c'est manifestement vrai car il n'y a pas de règle qui puisse avoir « ⋅ ⇒ ⊥ » comme conclusion ! Les théoriciens de la preuve préfèrent souvent travailler sur des formulations de calculs séquentiels sans coupure en raison de ces propriétés.

Voir également

Remarques

Les références

• Barker-Plummer, Dave; Barwise, Jon ; Etchemendy, John (2011). Preuve de langage et logique (2e éd.). Publications CSLI. ISBN 978-1575866321.
• Gallier, Jean (2005). "Logiques constructives. Partie I: Un didacticiel sur les systèmes de preuve et les λ-calculs typés" . Consulté le 12 juin 2014 .
• Gentzen, Gerhard Karl Erich (1934). "Untersuchungen über das logische Schließen. I" . Mathematische Zeitschrift . 39 (2) : 176-210. doi : 10.1007/BF01201353 . S2CID  121546341 . (Traduction anglaise Investigations into Logical Deduction in ME Szabo. The Collected Works of Gerhard Gentzen. North-Holland Publishing Company, 1969.)
• Gentzen, Gerhard Karl Erich (1935). "Untersuchungen über das logische Schließen. II" . Mathematische Zeitschrift . 39 (3) : 405-431. doi : 10.1007/bf01201363 . S2CID  186239837 .
• Girard, Jean-Yves (1990). Preuves et types . Cambridge Tracts en informatique théorique. Cambridge University Press, Cambridge, Angleterre. Archivé de l'original le 2016-07-04 . Récupéré le 20-04-2006 . Traduit et avec annexes par Paul Taylor et Yves Lafont.
• Jaśkowski, Stanislaw (1934). Sur les règles de suppositions en logique formelle .Réimprimé en logique polonaise 1920-1939 , éd. Storrs McCall.
• Kleene, Stephen Cole (1980) [1952]. Introduction aux métamathématiques (onzième éd.). Hollande du Nord. ISBN 978-0-7204-2103-3.
• Kleene, Stephen Cole (2009) [1952]. Introduction aux métamathématiques . Ishi Press International. ISBN 978-0-923891-57-2.
• Kleene, Stephen Cole (2002) [1967]. Logique mathématique . Mineola, New York : Publications de Douvres. ISBN 978-0-486-42533-7.
• Lemmon, Edward John (1965). Logique de départ . Thomas Nelson. ISBN 978-0-17-712040-4.
• Martin-Löf, Per (1996). « Sur les significations des constantes logiques et les justifications des lois logiques » (PDF) . Journal nordique de logique philosophique . 1 (1) : 11-60. Notes de cours pour un cours abrégé à l'Università degli Studi di Siena, avril 1983.
• Pfenning, Frank; Davies, Rowan (2001). « Une reconstruction de jugement de la logique modale » (PDF) . Structures mathématiques en informatique . 11 (4) : 511-540. CiteSeerX  10.1.1.43.1611 . doi : 10.1017/S0960129501003322 . S2CID  16467268 .
• Prawitz, Dag (1965). Déduction naturelle: Une étude de preuve-théorique . Acta Universitatis Stockholmiensis, Stockholm études de philosophie 3. Stockholm, Göteborg, Uppsala : Almqvist & Wicksell.
• Prawitz, Dag (2006) [1965]. Déduction naturelle: Une étude de preuve-théorique . Mineola, New York : Publications de Douvres. ISBN 978-0-486-44655-4.
• Quine, Willard Van Orman (1981) [1940]. Logique mathématique (éd. révisé). Cambridge, Massachusetts : Harvard University Press. ISBN 978-0-674-55451-1.
• Quine, Willard Van Orman (1982) [1950]. Méthodes de logique (quatrième éd.). Cambridge, Massachusetts : Harvard University Press. ISBN 978-0-674-57176-1.
• Simpson, Alex (1993). La théorie de la preuve et la sémantique de la logique modale intuitionniste (PDF) . Université d'Édimbourg. Thèse de doctorat.
• Stoll, Robert Roth (1979) [1963]. Théorie des ensembles et logique . Mineola, New York : Publications de Douvres. ISBN 978-0-486-63829-4.
• Stouppa, Phiniki (2004). La conception des théories de la preuve modale : le cas de S5 . Université de Dresde. CiteSeerX  10.1.1.140.1858 . Thèse de maîtrise.
• Suppes, Patrick Colonel (1999) [1957]. Introduction à la logique . Mineola, New York : Publications de Douvres. ISBN 978-0-486-40687-9.

Liens externes

• Laboreo, Daniel Clemente, " Introduction à la déduction naturelle. "
• Domino à l'acide. Déduction naturelle visualisée comme un jeu de dominos.
• Pelletier, Jeff, " Une histoire de la déduction naturelle et des manuels de logique élémentaire. "
• Levy, Michel, Un prouveur propositionnel.