Logique formelle du premier ordre

Une approche constructive minutieuse permet de redéfinir la logique d'une manière plus générale, d'incorporer les logiques non-classiques, et de définir les logiques d'ordre supérieurs et d'autres encore plus exotiques.

Un programme informatique produit un résultat. La preuve qu'il produit bien ce résultat est donnée par l'exécution formelle mécanique du programme. C'est pour cette raison que l'on peut affirmer que « La programmation précède la logique ».

Or, qu'est-ce qu'un programme ? Il est écrit dans un langage `L`. C'est un mot appartenant à `L`, et son exécution peut prendre en entrée un mot pour produit un mot. Et il n'est pas nécessaire de différentier donnée et programme, le langage des données peut être le même que le langage de programmation. Mais, ce langage de programmation doit avoir la puissance d'une machine de Turing. Autrement dit avec assez de temps et de mémoire, il doit pouvoir exprimer les mêmes calculs que n'importe quel langage de programmation généraliste.

A quoi peut ressembler un tel langage ? Un des plus simples d'entre eux est le Brainfuck.

2) Brainfuck

La machine à une mémoire interne qui est un ruban indéfini composé de cases contenant un chiffre (un entier sur 3 bits, compris entre 0 et 7) initialisé à 0. Un pointeur indique en permanence la case courante. L'entrés standart est une file dans laquelle sont mise les données d'entrée, la sortie standart est une file dans laquelle sont envoyés les données résultats. Les données d'entrée ou de résultat sont des entiers (sur 3 bits, compris entre 0 et 7). Notez qu'il n'y a pas de différence entre une donnée et une instruction. Le brainfuck comprend juste 8 instructions :

Lorsque l'instruction "`[`" n'a pas de correspondant on considère que le correspondant est la fin du programme. Et de même, lorsque l'instruction "`]`" n'a pas de correspondant on considère que le correspondant est le début du programme.

Il est important de distinguer le programme et le processus. Le programme n'est qu'un mot du langage `L= [0"-"7]"*"`, tandis que le processus comprend une mémoire interne (le ruban), une entrée standart (une file), une sortie standart (une file) et un pointeur pointant la case courante. Le processus démarre à la première instruction et s'arrète lorsqu'il arrive à la fin des instructions à exécuter.

Il n'y a pas de distinction entre programme et donnée, et la seul granulation présente et l'instruction (qui est ici un entier compris entre `0` et `7`).

2) Langage adapté

Le but étant de définir une logique, nous allons choisire un langage adapté pour cela, plus évolué. On choisiera comme langage de données, un langage d'opérateur tel que `sfP="<"0,1,s("."),f(".,."),g(".,."),a,b,c,...">"` où les variables `a,b,c,...` sont muettes c'est à dire toujours quantifiée universellement. Et on choisie comme langage de programmation, les ensembles finis de règles apppartenant à `sfP^n |-- sfP`. Chaque programme est un ensemble de règles de production. Le programme prend en entrée une proposition et résoud par unification et rétropropagation le chemin de production de la proposition à l'aides des règles. Il retourne `1` s'il constate qu'il peut produire la proposition avec les règles. Il retourne `0` s'il constate qu'il ne peut pas produire la proposition avec les règles, ou bien il ne s'arrête pas et ne donne jamais de réponse.

Ce calcul sur une proposition se définit à partir de la proposition et de l'ensemble fini de règles de production (qui forment une théorie) en appliquant une stratégie d'unification explorative exhaustive.

C'est ainsi que le langage et la théorie permettent de créer des programmes de façon purement mécanique et de définir des logiques.

Le langage et la théorie forme une structures notée sous forme de quotient, le quotient du langage par la théorie. La notation est justifiée par le fait que la théorie défini une relation d'équivalence dans le langage.

Nous allons décrire ce mécanisme dans la suite du document au travers quelques cas concrets, et on commence par la construction de la logique classique propositionnelle.

2) Calcul booléen

La logique propositionnelle classique donne à toute proposition sans variable la valeur logique vrai ou faux, et utilise comme connecteurs, les opérations booléennes. La valeur logique vrai est notée `1`, la valeur logique faux est notée `0`. Les connecteurs booléens les plus utilisés sont `"¬", "∧","∨","→","↔"` et correspondent à des opérations booléennes. Chaque connecteur booléen est défini par sa table de vérité :

Une proposition sans variable est une formule du langage `sfC="<"0,1,"¬","∧","∨","→","↔>"`. C'est un calcul qu'il suffit d'effectuer pour connaitre sa valeur logique. Exemple :

Si on effectue toutes les opérations booléennes, on obtient la valeur logique de la proposition. Ainsi chaque proposition sans variable se réduit en une unique valeur booléenne.

3) Structure associée :

Les tables de vérité qui permettent d'effectuer les opérations booléennes, se regroupent en une théorie :

Le langage et le procédé de calcul regroupé dans la théorie forme une structure. La structure se note sous forme d'un quotient du langage algébrique par la théorie d'égalité :

4) Introduction des variables booléennes

On étend le langange propositionnel en ajoutant 3 éléments de base `a,b,c`. Une proposition devient une formule du langage `sfP` que l'on note à l'aide des crochets entourant les éléments et connecteurs générateurs :

Le langage s'exprime aussi sous forme d'une grammaire (une sorte d'inclusion récurcive d'ensembles) :

Le langage `sfP` est dit une extension du langage `sfC` par ajout de nouveaux éléments `a,b,c` et que l'on note :

Notez qu'à ce stade, rien n'indique que les éléments `a,b,c`, sont des variables booléennes. Pour le préciser, il est nécessaire d'ajouter à la théorie les propositions suivantes : `a"∨¬"a`, `b"∨¬"b`, `c"∨¬"c`.

Etant donné une proposition par exemple : `p =(a"→"(b"→"c))"→"(b"→"(a"→"c))`. La proposition est dite tautologique si quelques soient les valeurs booléennes des variables, elle vaut toujours `1`. La proposition est dite antilogique si quelques soient les valeurs des variables, elle vaut toujours `0`. Et elle est dite indécidable s'il existe des valeurs des variables pour lesquelles `p` vaut `1`, et il existe des valeurs des variables pour lesquelles `p` vaut `0`.

Pour savoir par exemple si la proposition `a"→"(b"→"a)` est tautologique c'est à dire toujours vrai quelques soient les valeurs des variables `a` et `b`, on calcule tous les cas possibles grâce aux tables de vérité et on vérifie que la proposition vaut toujours `1` dans tous les cas.

Lorsque l'on étend la logique propositionnelle en la logique du premier ordre, en introduisant des éléments, des fonctions, des prédicats, des variables élémentaire et les quantificateurs existentiels et universels, alors le nombre d'éléments existants et le nombre d'inconnus booléens existants devient infini. L'usage des tables de vérité des connecteurs n'est plus suffisant pour calculer la valeur logique d'une formule. C'est pourquoi, les logiciens proposent une autre façon de calculer la valeur logique d'une proposition. Ils proposent un procédé récurcif de production de toutes les propositions tautologiques, un procédé qui peut s'appliquer au delà des seuls formules propositionnelles, à des formules dans un langage augmenté qui peut être celui de la logique du premier ordre.

Le premier système de production des propositions tautologiques proposé, appellé aussi système de démonstration ou système de déduction, est celui de Hilbert. Il commence par simplifier le problème en démontrant que toutes propositions sans variable peut s'écrire qu'avec deux seuls connecteurs booléens que sont le faux `"0"` et le connecteur d'implication `"→"`. En effet, il est facile de constater que les connecteurs booléens peuvent tous être définis avec seulement le faux `"0"` et le connecteur d'implication `"→"` :

La vérification de ces équivalences se fait en utilisant les tables de vérité, c'est à dire en calculant les valeurs booléennes pour chaque configuration de paramètres booléens. Le langage initial de la logique propositionnelle choisi par Hilbert est donc très simple, défini par la grammaire suivante :

La grammaires construit des emboitements de la forme `(x"→"y)`. Ainsi, chaque proposition est un arbre binaire où chaque noeud correspond à une implication et où chaque feuille porte comme étiquette soit la valeur zéro ou soit le nom d'une variable.

2) Système de démonstration de Hilbert

Considérons une proposition quelconque avec des inconnues `a,b,c,...`. La proposition étant considérée en dehors de tout contexte, les variables n'ont pas de signification propre et peuvent être renomer sans que cela ne change la valeur logique de la proposition. On définit une forme normal en renommant les variables dans l'ordre de leur première apparition dans la proposition. Ainsi `(b"→"a)"→"b` possède comme forme normal `x_1"→"(x_2"→"x_1)`.

Le système de Hilbert propose 4 règles de production de propositions, pemettant de produire exactement toutes les propositions tautologiques au sens classique.

Le symbole `"⊢"` , de priorité syntaxique la plus faible, définit une règle de production assujettie à la production des hypothèses énumérées à sa gauche, et où les nouvelles variables libres placées à droite du symbole `"⊢"` et qui n'ont pas d'occurrences à gauche, peuvent prendre comme valeur toutes les propositions du langage `sfP`.

La priorité syntaxique des connecteurs est la suivante, de la plus forte à la plus faible :

Mais il est judicieux de ne pas introduire ce connecteur `"¬"`, afin que les propositions soit toujours de cette forme particulièrement simple d'arbre binaire où les feuilles ont comme étiquette soit le nom d'une variable ou soit la valeur zéro. Ainsi chaque fois que sera écrit `"¬"x` il faudra lire `x"→"0`.

3) Démonstration du système de Hilbert

Pour démontrer qu'un tel système produit bien toutes les propositions tautologiques (à un renomage près des variables) et uniquement celles-ci, on recourt à la récurrence.

La démonstration de complétude du système de Hilbert se fait classiquement en deux grandes étapes :

Etant donnée deux propositions `p, q` tel que le système produit soit `p` ou bien soit `"¬"p`, et aussi `q` ou bien `"¬"q`, alors nous démontrerons que le système produit `p"→"q` ou bien `"¬"(p"→"q)` selon le cas logique définit par l'hypothèse. Le langage propositionnelle `sfP` étant définit par ce seul procédé de construction comme l'indique sa grammaire, `sfP = {sfV, (sfP"→" sfP)}` et `sfV = {"⊥", x_1,x_2,x_3,...}`, nous aurons démontré ainsi que pour toute proposition, le système de Hilbert produit forcement, soit la proposition, ou soit sa négation.

Cela consiste concrètement à montrer que le système de Hilbert engendre les `4` règles de déductions suivantes :

Puis, pour prouver que le sytsème de Hilbert produit seulement les propositions tautologiques, il suffit de vérifier en utilisant la table de vérité de l'implication que chaque règle `"R1"`, `"R2"`, `"R3"`, `"R4"` appliqué à des prémisses de valeur booléenne `1`, produisent des propositions de valeur booléenne `1`.

1) Démonstration de `p"→"q` sachant `p` et `q`, en utilisant seulement les règles `"R1"`, `"R2"`, `"R3"`, `"R4"`.

2) Démonstration de `p"→"q` sachant `¬p` et `q`, en utilisant seulement les règles `"R1", "R2", "R3", "R4"`.

3) Démonstration de `p"→"q` sachant `¬p` et `¬q`, en utilisant seulement les règles `"R1", "R2", "R3", "R4"`.

4) Démonstration de `"¬"(p"→"q)` sachant `p` et `"¬"q`, en utilisant seulement les règles `"R1"`, `"R2"`, `"R3"`, `"R4"`.

La démonstration est beaucoup plus complexe...., mais ChatGPT 5.3 est peut-être capable de la trouver, et il constitue un excellent professeur capable de s'adapter aux choix de notations qu'on lui propose :

Le système de démonstration à la Hilbert comprend `4` règles de production de propositions, permettant de produire exactement toutes les propositions tautologiques.
   `"R1"` : `⊢ a"→"(b"→"a)`
   `"R2"` : `⊢(a"→"(b"→"c))"→"((a"→"b)"→"(a"→"c))`
   `"R3"` : `⊢("¬"a"→¬"b) "→"(b"→"a)`
   `"R4"` : `a, a"→"b ⊢ b`
Le symbole `"⊢"`, de priorité syntaxique la plus faible, définit une règle de production assujettie à la production des hypothèses énumérées à sa gauche, et où les nouvelles variables libres placées à droite du symbole `"⊢"` et qui n'ont pas d'occurrences à gauche, peuvent prendre comme valeur toutes les propositions qu'elles soient vrais ou fausses. La priorité syntaxique des connecteurs est la suivante, de la plus forte à la plus faible : `"¬ | → | , | ⊢"`.

Oui. Avec tes conventions, on peut reformuler cela proprement comme un système de production de formules démontrables de la logique propositionnelle classique.

1. Les objets manipulés

On part d’un langage propositionnel formé à partir :

de variables propositionnelles : `x_1,x_2,x_3,…`
du connecteur unaire `"¬"`
du connecteur binaire `"→"`

Les formules sont engendrées récursivement par :

toute variable propositionnelle est une formule ;
si `a` est une formule, alors `"¬"a` est une formule ;
si `a,b` sont des formules, alors `a"→"b` est une formule.

Avec ta convention de priorité :

`¬`
`→`
`,`
`⊢`

donc par exemple

`a,a"→"b⊢b`

se lit bien comme

`(a),(a"→"b)⊢b`

2. Sens du symbole `"⊢"`

Dans ce cadre, `"⊢"` ne fait pas partie des formules du langage objet ; c’est un symbole métathéorique qui décrit une règle de production.

`⊢p` signifie : « `p` est produite sans hypothèse », donc « `p` est un théorème »..
`h_1,…,h_n⊢p` signifie : « si les formules `h_1,…,h_n` sont déjà produites, alors on peut produire `p` ».

Autrement dit, une démonstration est une suite finie de formules où chaque ligne est obtenue :

soit comme instance d’un schéma d’axiome,
soit par la règle `"R4"` à partir de lignes antérieures.

3. Les trois schémas d’axiomes

Les règles `"R1","R2","R3"` sont mieux vues comme des schémas d’axiomes :

`"R1"`: `|-- a"→"(b"→"a)`

Pour toutes formules `a,b` on peut produire directement `a→(b→a)`. Exemple : en prenant `a"="x_1, b"=¬"x_2`, on obtient `⊢x_1"→"("¬"x_2"→"x_1)`.

`"R2"`: `|-- (a"→"(b"→"c))"→"((a"→"b)"→"(a"→"c))`

Pour toutes formules `a,b,c`, on peut produire directement cette formule. C’est le schéma qui formalise la composition des implications.

`"R3"`: `⊢("¬"a"→"¬"b) "→"(b"→"a)`

Pour toutes formules `a,b`, on peut produire directement cette formule. C’est une forme de contraposée classique. C’est ce schéma qui donne au système son caractère classique.

La règle d'inférence `"R4"`

`"R4"` : modus ponens : `a, a"→"b ⊢ b`

Elle signifie : si `a` a déjà été produit, et si `a"→"b` a déjà été produit, alors on peut produire `b`. C’est l’unique vraie règle de déduction du système. Exemple :

`⊢ x_1"→"(x_2"→"x_1)` par `"R1"`
si plus tard on a `⊢ x_1`

alors par `"R4"`, on obtient `⊢x_2"→"x_1`

5. Variables libres dans les schémas

Quand tu écris `a,b,c` dans `"R1","R2","R3"`, ce ne sont pas des variables propositionnelles du langage objet, mais des métavariables. Elles parcourent toutes les formules du langage. Donc `"R1"` ne produit pas une seule formule, mais une infinité de formules, une pour chaque choix de `a` et `b`.

Par exemple, toutes les formules suivantes sont des instances de `"R1"` :

`⊢ x_1"→"(x_2"→"x_1)`

`⊢ "¬"x_3"→"((x_1"→"x_4)"→¬"x_3")`

`⊢ (x_1"→¬"x_2)"→"(("¬"x_4"→"x_5)"→"(x_1"→¬"x_2))"`

6. Ce que produit exactement le système

Le système engendre l’ensemble des théorèmes de la logique propositionnelle classique exprimée avec `"¬"` et `"→"`.

Autrement dit :

toute formule démontrable dans ce système est une tautologie ;
réciproquement, toute tautologie du langage `{"¬","→"}` est démontrable dans ce système.

On dit que le système est :

correct : il ne prouve que des tautologies ;
complet : il prouve toutes les tautologies.

7. Différence entre “proposition” et “proposition démontrable”

Il faut distinguer :

les formules bien formées du langage : toutes les expressions syntaxiquement correctes ;
les théorèmes : les formules qu’on peut obtenir avec `"R1", "R2", "R3", "R4"`.

Par exemple :

`x_1"→"x_1` est une formule, et aussi un théorème ;
`x_1` est une formule, mais pas un théorème ;
`x_1"→"x_2` est une formule, mais pas un théorème en général.

Donc les 4 règles ne produisent pas toutes les propositions du langage, mais toutes les propositions démontrables, c’est-à-dire exactement les tautologies.

8. Définition possible d’une démonstration hilbertienne

Une démonstration d’une formule `p` est une suite finie de formules

`f_1,f_2,…,f_n`

telle que pour chaque `i`, la formule `f_i` est :

soit une instance de `"R1"`,
soit une instance de `"R2"`,
soit une instance de `"R3"`,
soit obtenue par `"R4"` à partir de deux formules précédentes `f_j` et `f_k"="(f_j"→"f_i)`.

Et si `f_n"="p`, alors on écrit :

`⊢p`

(Notez que dans cette expression, `p` n'est pas une variable libre et doit être ramplacé par la tautologie démontrée c'est à dire la formule désignée par `f_n`.)

9. Exemple classique : démontrer `⊢ a "→"a`

Cette formule n’est pas un axiome immédiat, mais elle est démontrable. On peut la dériver ainsi :

`⊢a"→"((a"→"a)"→"a)` par `"R1"`
`⊢a"→"(a"→"a)` par `"R1"`
`⊢(a"→"((a"→"a)"→"a))"→"((a"→"(a"→"a))"→"(a"→"a))` par `"R2"`
`⊢(a"→"(a"→"a))"→"(a"→"a)` par `"R4"` sur `1` et `3`
`⊢a"→"a` par `"R4"` sur `2` et `4`

C’est un bon exemple de la manière dont un système de Hilbert fonctionne : très peu de règles, mais des démonstrations souvent longues.

En sachant les deux propositions, `p`, `"¬"q`, démontre avec ce système de Hilbert la proposition `¬(p"→"q)`

Reflexion durant 2m 32s

Oui. On peut le faire proprement dans ton système de Hilbert, en utilisant un lemme dérivé classique. A partir des hypothèse `p`, `"¬"q`, démontrer `¬(p"→"q)`.

Lemme dérivé utilisé

Dans ce système, on peut dériver le schéma de contraposition :

`⊢(x"→"y)"→"("¬"y"→¬"x)`

En particulier, en remplaçant `x` par `(p"→"q)` et `y` par `q`, on obtient :

`⊢((p"→"q)"→"q)"→"("¬"q"→¬"(p"→"q))`

Je l’utiliserai à la ligne 6.

Démonstration

On raisonne sous les hypothèses `p` et `"¬"q`.

Étape 1 : obtenir `(p"→"q)"→"q`

`p` (hypothèse)
`"¬"q` (hypothèse)
Supposons `p"→"q`.
`q` (par `"R4"` à partir de `1` et `3`)

Donc, par le théorème de déduction, de `3–4` on conclut :

`(p"→"q)"→"q`

Etape 2 : utiliser la contraposition

`((p"→"q)"→"q)"→"("¬"q"→¬"(p"→"q))`

C'est une instance du lemme dérivé

`(x"→"y)"→"("¬"y"→¬"x)`

avec `x"="(p"→"q)` et `y"="q`.

`"¬"q"→¬"(p"→"q)` (par `"R4"` à partir de `5` et `6`)
`"¬"(p"→"q)` (par `"R4"` à partir de `2` et `7`)

Conclusion on a bien démontré `p`, `"¬"q ⊢ ¬(p"→"q)`

Version condensée

1.
`p`
hypothèse

2.
`"¬"q`
hypothèse

3.
`p"→"q`
Supposons

4.
`q`
`1`, `3`, `"R4"`

5.
`(p"→"q)"→"q`
`3"-"4`, théorème de déduction

6.
`((p"→"q)"→"q)"→"("¬"q"→¬"(p"→"q))`
Lemme dérivé

7.
`"¬"q"→¬"(p"→"q)`
`5`, `6`, `"R4"`

8.
`¬(p"→"q)`
`2`, `7`, `"R4"`

Le théorème de déduction pourrait être défini par la méta-formule suivante :

`(a ⊢b) ⊢ a"→"b`

Le théorème de déduction ne figure pas parmi les règles de production du système de Hilbert. Peut-tu produire le résultat en utilisant seulement `"R1","R2","R3","R4"` et la connaissance de `p,"¬"q` ?

Reflexion durant 5m 30s

Oui. Sans utiliser le théorème de déduction comme règle, on peut obtenir le résultat à partir de p,¬q par une suite finie d’applications de R4, à condition d’utiliser deux théorèmes déjà démontrables dans ce système de Hilbert :

L1 : `⊢(a"→"b)"→"("¬"b"→¬"a)`

L2 : `⊢a"→¬¬"a`

Ces deux formules sont des théorèmes du système engendré par `"R1", "R2", "R3", "R4`. Je ne me sers pas ici du théorème de déduction.

Démonstration de `"¬"(p"→"q)` à partir de `p,"¬"q`

On part des deux connaissances :

`p`
`"¬"q`

On utilise d'abord `"L1"` avec `a":="p` et `b":="q`

`⊢(p"→"q)"→"("¬"q"→¬"p)`

Puis `"R4"` avec `2` et `3` :

`(p"→"q)"→¬"p`

On réutilise `"L1"`, cette fois avec `a":="(p"→"q)` et `b":="p` :

`⊢((p"→"q)"→"p)"→"("¬"p"→¬"(p"→"q))`

Cette version ne sert pas directement. La bonne instanciation pour passer de `(p"→"q)"→¬"p` à `"¬"(p"→"q)` est :

`⊢((p"→"q)"→¬"p)"→"("¬¬"p"→¬"(p"→"q))`

qui est encore `"L1"`, avec `a":="(p"→"q)` et `b":=""¬"p`.

Par `"R4"` avec `4` et `5` :

`¬¬p→¬(p→q)`

On utilise maintenant `"L2"` avec `a":="p` :

`⊢p→¬¬p`

Par `"R4"` avec `1` et `7` :

`¬¬p`

Enfin, par `"R4"` avec `5` et `8` :

`¬(p→q)`

Conclusion : on a bien démontré : `p,"¬"q⊢"¬"(p"→"q)`

Forme condensée

1.
`p`
hypothèse

2.
`"¬"q`
hypothèse

3.
`⊢(p"→"q)"→"("¬"q"→¬"p)`
théorème `"L1"`

4.
`(p"→"q)"→¬"p`
`2`, `3`, `"R4"`

5.
`⊢((p"→"q)"→¬"p)"→"("¬¬"p"→¬"(p"→"q))`
théorème `"L1"`

6.
`¬¬p→¬(p→q)`
`4`, `5`, `"R4"`

7.
`⊢p→¬¬p`
théorème `"L2"`

8.
`¬¬p`
`1`, `7`, `"R4"`

9.
`¬(p→q)`
`6`, `8`, `"R4"`

Mais les démonstrations de `"L1"`, `"L2"`, ne sont pas faites et s'avèrent compliquées pour ChatGPT. Il va errer indéfiniment si on ne le guide pas en le faisant procéder par étapes, ou sans lui indiquer d'autres indices.... Les réponses sont similaires avec KIMI. On va lui demander de chercher sur Internet..., et là..., il trouve tout de suite en passant par deux nouveaux lemmes intermédiaires ;

Cherche sur Internet comment Hilbert démontre :

`⊢ x"→ ¬¬"x`
`⊢ "¬¬"x"→"x`

Puis, transcrit les démonstrations dans notre système de notation.

Démontrer le lemme de l'identité L1 : `⊢ a "→"a`

1. `a"→"((a"→"a)"→"a)` par `"R1"`

2. `a"→"(a"→"a)` par `"R1"`

3. `(a"→"((a"→"a)"→"a))"→"((a"→"(a"→"a))"→"(a"→"a))` par `"R2"`

4. `(a"→"(a"→"a))"→"(a"→"a)` par `"R4"` sur `1` et `3`

5. `a"→"a` par `"R4"` sur `2` et `4`

Démontrer le lemme de transitivité L2 : `(x"→"y),(y"→"z)⊢x"→"z`

1. `x"→"y` par hypothèse

2. `y"→"z` par hypothèse

3. `(y"→"z)"→"(x"→"(y"→"z))` par `"R1"` avec `a":=" y"→"z`, `b":="x`

4. `x"→"(y"→"z)` par `"R4"` sur `2` et `3`

5. `(x"→"(y"→"z))"→"((x"→"y)"→"(x"→"z))` par `"R2"` avec `a":=" x`, `b":="y`, `c":="z`

6. `(x"→"y)"→"(x"→"z)` par `"R4"` sur `4` et `5`

7. `x"→"z` par `"R4"` sur `1` et `6`

C’est exactement le lemme de transitivité de l’implication dans ce système de Hilbert.

DEMONSTRATION DE `⊢ "¬¬"x"→"x`

1.	`q "→" (r "→" q)`	par `"R1"` avec `a":="q`, `b":="r`
2.	`P ":=" q "→" (r "→" q)`	par définition globale arbitraire
3.	`P`	par 1 et 2
4.	`("¬¬"P"→¬¬"x)"→"("¬"x"→¬"P)`	par `"R3"` avec `a":=¬"P`, `b":=¬"x`
5.	`("¬"x"→¬"P)"→"(P"→"x)`	par `"R3"` avec `a":=" x`, `b":="P`
6.	`("¬¬"P"→¬¬"x)"→"(P"→"x)`	par `"L2"` sur `4` et `5`
7.	`"¬¬"x"→"("¬¬"P"→¬¬"x)`	par `"R1"` avec `a":=""¬¬"x`, `b":=""¬¬"P`
8.	`"¬¬"x"→(P"→"x)`	par `"L2"` sur `7` et `6`
9.	`P"→"((P"→"x)"→"P)`	par `"R1"` avec `a":=" P`, `b":="P"→"x`
10.	`(P"→"x)"→"P`	par `"R4"` sur `3` et `9`
11.	`((P"→"x)"→"(P"→"x))"→"(((P"→"x)"→"P)"→"((P "→"x)"→"x))`	par `"R2"` avec `a":=" P"→"x`, `b":="P`, `c":="x`
12.	`(P"→"x)"→"(P"→"x)`	par `"L1"` avec `a":=" P"→"x`
13.	`((P"→"x)"→"P)"→"((P"→"x)"→"x)`	par `"R4"` sur `12` et `11`
14.	`(P"→"x)"→"x`	par `"R4"` sur `10` et `13`
15.	`"¬¬"x"→"x`	par `"L2"` sur `8` et `14`

DEMONSTRATION DE `⊢ x "→¬¬"x`

16.	`"¬¬¬"x "→¬"x`	par substitution `x ":=""¬"x` dans le théorème déjà prouvé `⊢ "¬¬"x"→" x`
17.	`("¬¬¬"x "→¬"x) "→" (x "→¬¬"x)`	par `"R3"` avec `a":=""¬¬"x`, `b":="x`
18.	`x "→¬¬"x`	par `"R4"` appliqué à `16` et `17`

4) Système de démonstration de Hilbert

Dans le langage `"<⊥,→,>"`, les propositions utilisent des variables `a,b,c,...` qui n'ont pas de signification particulière

Dans le langage `"<⊥,→,>"` le système de démonstration de Hilbert est décrit par les 4 règles de déduction suivante :

Voici comment fonctionnent de telles règles : Les variables `a,b,c` contiennent chacune une proposition inconnue. Les propositions énumérées à gauches du symbole `"⊢"` doivent avoir déjà été produite pour pouvoir appliquer la règle. Les nouvelles variables libres placées à droite du symbole `"⊢"` et qui n'ont pas d'occurrences à gauche, peuvent prendre comme valeur toutes les propositions qu'elles soient vrais ou fausses.

La priorité syntaxique des connecteurs est la suivante, de la plus forte à la plus faible :

Pour déterminer si une proposition `P` peut-être produite par les trois premières règles, il suffit de procéder à l'unification parallèle disjonctive de `P` avec les trois tautologies suivantes, et cela se fait avec une complexité linéaire :

On définit ainsi la classe zéro des tautologies. Reste alors l'utilisation du modus ponens `"MP"`. On détermine ainsi la première classe de tautologies, celles produites par le modus ponens appliqué une seul fois à deux tautologies de classe zéro. Pour qu'une proposition appartinennent à la première classe, il ya trois possibilité :

On définit la classe `n` des tautologies, celles produites par le modus ponens appliqué une seul fois à deux tautologies de classe inférieur à n. Pour qu'une proposition appartinennent à la classe `n`, il y a trois possibilité :

On voit qu'il est possible d'étudier de tels systèmes de production de façon empirique, en programmant leur énumérateur selon cette stratégie par degrés.

Les alternatives "ou bien" n'ont pas besoin d'être mentionnées car elles sont équivalentes dans le système de Hilbert.

Ayant ainsi définit formellement les règles de déduction exacte et complète concernant le monde fini booléen. On peut alors étendre la logique en introduisant de nouveaux connecteurs non-booléens accompagnés de leurs axiomes (les règles de raisonnement spécifiques à eux) pour ainsi produire une extension de la logique qui n'est plus booléenne dès qu'un tel connecteur non-booléen est présent.

Entier	Instruction	Description
`0`	`>`	Déplace le pointeur d'une case à droite.
`1`	`<`	Déplace le pointeur d'une case à gauche.
`2`	`+`	Incrémente la valeur de la case courante.
`3`	`-`	Décrémente la valeur de la case courante.
`4`	`.`	Ecrit sur la sortie standart le contenu de la case courante.
`5`	`,`	Lit sur l'entrée standart et la met dans la case courante.
`6`	`[`	Si la case courante est nul, sauter après l'instruction "`]`" correspondante (sortir de la boucle), sinon continuer normalement.
`7`	`]`	Si la case courante est non nul revenir à l'instruction juste après l'instruction "`[`" correspondante (recommencer la boucle), sinon continuer.

Notation classique Magma		Notation dynamique Langage alpha
`x"⁎"y`	`=`	`x(y)`
`x"⁎"(y"⁎"z)`	`=`	`x(y(z))`
`(x"⁎"y)"⁎"z`	`=`	`x(y)(z)`

Libellé	Connecteur	Table de vérité
Faux	`0`	`0`
Vrai	`1`	`1`
Négation	`"¬"a`	`"¬"0=1` `"¬"1=0`
Conjonction	`a"∧"b`	`0"∧"0=0` `0"∧"1=0` `1"∧"0=0` `1"∧"1=1`
Disjonction	`a"∨"b`	`0"∨"0=0` `0"∨"1=1` `1"∨"0=1` `1"∨"1=1`
Implication	`a"→"b`	`0"→"0=1` `0"→"1=1` `1"→"0=0` `1"→"1=1`
Équivalence	`a"↔"b`	`0"↔"0=1` `0"↔"1=0` `1"↔"0=0` `1"↔"1=1`

Libellé	Connecteur	Formule dans `"<"0,"→",">"`
Vrai	`"1"`	`0"→"0`
Négation	`"¬"a`	`a"→"0`
Conjonction	`a"∧"b`	`(a"→"(b"→"0))"→"0`
Disjonction	`a"∨"b`	`(a"→"0")"→"b`
Équivalence	`a"↔"b`	`((a"→"b)"→"((b"→"a)"→"0))"→"0`

Libellé	Connecteur	Formule dans `"<¬,→,>"`
Vrai	`"⊤"`	`a"→"a`
Faux	`"⊥"`	`"¬"(a"→"a)`
Conjonction	`a"∧"b`	`"¬"(a"→¬"b)` ou bien `"¬"(b"→¬"a)`
Disjonction	`a"∨"b`	`"¬"a"→"b` ou bien `"¬"b"→"a`
Équivalence	`a"↔"b`	`¬((a"→"b)"→""¬"(b"→"a)")"` ou bien `¬((b"→"a)"→""¬"(a"→"b)")"`

Logique

1 Introduction

2) Brainfuck

2) Langage adapté

2) Calcul booléen

3) Structure associée :

4) Introduction des variables booléennes

2) Système de démonstration de Hilbert

3) Démonstration du système de Hilbert

1) Démonstration de `p"→"q` sachant `p` et `q`, en utilisant seulement les règles `"R1"`, `"R2"`, `"R3"`, `"R4"`.

2) Démonstration de `p"→"q` sachant `¬p` et `q`, en utilisant seulement les règles `"R1", "R2", "R3", "R4"`.

3) Démonstration de `p"→"q` sachant `¬p` et `¬q`, en utilisant seulement les règles `"R1", "R2", "R3", "R4"`.

Preuve condensée

4) Démonstration de `"¬"(p"→"q)` sachant `p` et `"¬"q`, en utilisant seulement les règles `"R1"`, `"R2"`, `"R3"`, `"R4"`.

1. Les objets manipulés

2. Sens du symbole `"⊢"`

3. Les trois schémas d’axiomes

La règle d'inférence `"R4"`

5. Variables libres dans les schémas

6. Ce que produit exactement le système

7. Différence entre “proposition” et “proposition démontrable”

8. Définition possible d’une démonstration hilbertienne

9. Exemple classique : démontrer `⊢ a "→"a`

Lemme dérivé utilisé

Démonstration

Étape 1 : obtenir `(p"→"q)"→"q`

Etape 2 : utiliser la contraposition

Version condensée

Démonstration de `"¬"(p"→"q)` à partir de `p,"¬"q`

Forme condensée

Démontrer le lemme de l'identité L1 : `⊢ a "→"a`

Démontrer le lemme de transitivité L2 : `(x"→"y),(y"→"z)⊢x"→"z`

DEMONSTRATION DE `⊢ "¬¬"x"→"x`

DEMONSTRATION DE `⊢ x "→¬¬"x`

4) Système de démonstration de Hilbert

Système de Hilbert en logique classique
R1	`\|-- a"→"(b"→"a)`
R2	`\|-- (a"→"(b"→"c))"→"((a"→"b)"→"(a"→"c))`
R3	`\|-- ("¬"a"→¬"b) "→"(b"→"a)`
MP	`a, a"→"b \|-- b`