Le jeu consiste à définir un système de démonstration c'est-à-dire un mécanisme qui produit des démonstrations. On admet comme pemière règle de raisonnement logique, la règle de l'identité qui dit que pour toute formule `A`, la formule `A` démontre la formule `A`. Et on note cette règle comme suit :
`AAA, A|--A`
À ce stade, le système de démonstration ne comprend que cette seule règle de production. On étend le langage logique du premier ordre en introduisant ce nouvel opérateur binaire `|--` auquel on donne une signification bien particulière. `A|--B` signifie que `A` démontre `B` en utilisant les règles du système de démonstration décrite dans l'hypothèse `A`. On pose par exemple `A = (B "et" AAX, X"⊢"X)`
`(B "et" AAX, X"⊢"X) |-- B`
Et cette proposition est vrai car en utilisant la règle `AAX, X"⊢"X` et en se restreignant à `X"="B`, on produit bien `B` à l'aide de l'opérateur `"⊢"`. On peut écrire cette production comme étant ce qui est engendré par toutes les composition possibles de cet élément `B` et de cet opérateur `X"↣"X`.
`"<"B, X"↣"X">" |-- B`
En prenant ce modèle de construction basé sur le passage à la clôture par composition close d'un ensemble d'opérateurs générateurs, la règle d'identité n'est plus nécessaire puisque ce qu'elle produit apparait déjà dans l'engendrement de `"<...>"` comme opérateurs générateurs. On se place dans un paradigme conjonctif, où un ensemble fini de formules est identifié à la conjonction de ces mêmes formules. Cela met en exergue l'associativité et la commutativité de l'opérateur de conjonction. Puis on reprend l'idée de la déduction naturelle, en ajoutant deux règles l'une correspondant à l'introduction de l'implication, l'autre correspondant à son élimination. La règle d'introduction de la l'implication est :
`AAA AABAAC, ((A^^B)"⊢"C) |-- (A"⊢"(B"⇒"C))`
La règle d'élimination de l'implication est :
`AAA AABAACAAD, ((A"⊢"(C"⇒"D))^^(B"⊢"C)) |-- ((A^^B)"⊢"D)`
Où les variables `A,B,C,D`, sont des ensembles de formules, et où l'opérateur de conjonction `^^` se comporte comme l'opérateur d'union d'ensembles, ou d'adjonction d'une formule à un ensemble, ou de groupement de deux formules en un ensemble de formules.
Cela correspond à une lambda-fonction plus perfectionnée qui prend non pas 3 arguments mais 3 ensembles finis d'arguments.
13) Généralisation des lambda-fonctions
f(A,B) = g(B,k(A))
---- 5 juin 2024 ----
"est dérivable par les règles de déduction du système de démonstration. La diffférence entre
Ce système de démonstration manipule des séquents. Un séquent `A|--B` est composé d'une formules `A` appelée hypothèse, et d'une formule `B` appelée conclusion. Le séquent `A|--B ` signifie que l'ensemble des formules `A` démontre `B` en utilisant le système de déduction naturelle".
La somme des connaissances du système raisonnant est un ensemble de formules identitfié comme une conjonction de formules. On étend le langage logique du premier ordre en introduisant un nouvel opérateur `|--` qui signifie "démontre". La diffférence entre
Par convention, à gauche de ce signe on pourra mettre une énumération de formules et d'ensembles finis de formules entre crochet `{}` pour désigner leur réunion. Puis un ensemble vide de formule est représenté par l'absence d'argument. Le séquent `|--alpha` signifie que `alpha` est démontrable à partir de rien.
Une règle de démonstration est composé d'une énumération d'un ou de deux ou de trois séquents d'entrée et d'un séquent de sortie. Elle stipule que si on prouve les séquents en entrée alors on a prouvé le séquent en sortie.
Axiome d'identité : `⮕ alpha"⊢"alpha`
Introduction de la conjonction : `A"⊢"alpha, B"⊢"beta ⮕ {A,B}"⊢"alpha"∧" beta`
Introduction de l'implication : `{A,B}"⊢"alpha ⮕ A"⊢"B"⇒"alpha`
Introduction de la négation : `{A,B}"⊢⊥" ⮕ A"⊢¬"B`
Introduction de la disjonction : `A"⊢"alpha ⮕ A"⊢"alpha"∨"beta`
`A"⊢"alpha ⮕ A"⊢"beta"∨"alpha`
élimination de la conjonction : `{A,B}"⊢"alpha"∧" beta ⮕ A"⊢"alpha`
`{A,B}"⊢"alpha"∧" beta ⮕ A"⊢"beta`
---- 2 juin 2024 ----