Les mathématiques utilisent le concept d'élément et celui d'ensemble qui peuvent ne correspondrent à aucune réalité, ce qui se produit lorsque les ensembles sont infinis. D'où la nécessité d'une quête des fondations. Nous allons discuter sur la nature de l'élément, et révéler les enjeux épistémologiques. L'élément pouvant être un ensemble, le concept d'ensemble est inclus dans celui d'élément.
Par fondation des Mathématiques, on entend en général le problème de présenter "toutes" les mathématiques à partir d'un petit nombre de symboles et de règles de base, autrement-dit par un langage et un système de règles de déduction qu'une machine peut appliquer.
On présente ainsi les mathématiques par leur début. Au début, nous avons le calcul formel, quelque chose d'exacte et de concret effectuée par une machine, l'exécution d'un programme informatique. Et c'est une vision pragmatique mais aussi idéologique qui nous fait choisir comme premier calcul, le calcul booléen.
Tant que tout est exacte et fait par une machine, il n'y a pas de problème de fondation juste une successions de choix pour définir un langage et un mode d'exécution.
À partir des booléens nait les opérations booléennes puis les variables booléennes, et les équations booléennes qui sont des propositions.
Puis vont apparaitrent les structures de treillis distributifs et les structures de corps, qui permettront de concevoir des logiques plus générale émanant d'un tronc commun exploitant ces deux structures. Le procédé est simple. On généralise en ne retenant que quelques propriétés remarquables, celle de treillis distributif et celle de corps, qui sont définie ici non pas d'un point de vue ensembliste mais d'un point de vue algorithmique.
Il y a plusieurs méthodes pour déterminer si une proposition est une tautologie, une antilogie, ou est indécidable :
Puis si le nombre de variables devient trop grand, il existe une méthode de résolution heuristiques, qui consiste à développer la proposition en une conjonction de clauses, ou en une disjonction d'états, puis à procéder à une sorte de digestion complétive.
Le vrai et le faux, un choix pas du tout anodin, et dans un monde où tout est faux, on peut vouloir remettre en cause ce choix bipolaire.
`"⊤"` Comme le sommet.
Le maximum dans la relation d'ordre que constitue l'implication.`"⊥"` Comme la base.
Le minimum dans la relation d'ordre que constitue l'implication.
Un moyen mémotechnique pour retenir le symbole `"⊤"` désignant le vrai, il ressemble à la lettre T comme Tautologie, et il constitue le ciel, le sommet, le maximum, on ne peut pas aller plus haut, tandis que le symbole inverse `"⊥"` désignant le faux, constitue le sol, le point le plus bas, le minimum, on ne peut pas aller plus bas.
Découle en suite, le calcul booléen. On retient 6 opérations booléennes de base ; la négation, l'implication, l'équivalence, le ou exclusif, la conjonction, la disjonction, notées respectivement `"¬"("."), "⇒"(".,."), "⇔"(".,."), "⊕(.,.)", "et(.,.)", "ou(.,.)"` où le suffixe `"(.)"` et `"(.,.)"` indique l'arité de l'opération booléenne.
`¬x`
Ces opérations booléennes correspondent à des notions plus abstraites :
C'est le "non" booléen, un "non" absolu, qui fait que la double négation est égale à l'identité. Une relation d'ordre allant du `0` vers le `1`, allant de `"⊥"` à `"⊤"` Egalité booléenne. Inégalité booléenne. Chaque argument doit être vrai, pour que la conjonction soit vrai. Et il suffit qu'un seul argument soit faux, pour que la conjonction soit fausse. Il suffit qu'un seul argument vrai, pour que la disjonction soit vrai. Et chaque argument doit être faux, pour que la disjonction soit fausse.
Le langage du calcul booléen se note récurcivement comme suit :
`L ← { "⊤", "⊥", "¬"L, (L"⇒"L), (L"⇔"L), (L"⊕"L), (L "et" L), (L "ou" L)}`
Il s'agit d'une grammaire présentée sous forme d'une inclusion récurcive. Tous les termes de ce langage, que l'on appelle formule, s'évalue en une valeur booléenne `0` ou `1` qu'il suffit de calculer en exécutant les opérations booléennes.
La première abstraction significative est la création de variable booléenne, `x,y,z,...` C'est une étape importante dans la construction du langage.
Cela permet de définir le calcul propositionnel. Chaque variable booléenne désigne une inconnue de valeur logique vrai ou faux, correspondant à la valeur de vérité d'une proposition.
On considère donc des propositions inconnues `x,y,z,...` appartenant à `{0,1}`. L'assemblage de variables et d'opérations booléennes en des termes appelés formules, constituent d'autres propositions.
Le langage du calcul propositionnel se note récurcivement comme suit :
`L ← { V, "⊤", "⊥", "¬"L, (L"⇒"L), (L"⇔"L), (L"⊕"L), (L "et" L), (L "ou" L)}`
`V ← { x,y,z}`
Exemple d'une proposition `P` :
`P = ("¬"(y"⇒"z)"⇔"(z "ou" "¬"x))"⇒"y`
La variable `P` dépend complètement des variables `x,y,z` dites libres. C'est pourquoi on la note parfois comme une fonction booléenne `P(x,y,z)`, une fonction de ses variables libres.
Etant donné une telle proposition `P`, on se pose alors trois questions, est-elle tautologique, indécidable, ou antilogique ?.
`P` est vrai quelque soit les valeurs de `x,y,z` Il existe au moins une valeur de `(x,y,z)` telle que la proposition `P` est vrai, et il existe au moins une valeur de `(x,y,z)` telle que la proposition `P` est fausse. `P` est faux quelque soit les valeurs de `x,y,z`
On dit que `P` est satisfaisable s'il existe une valeur de `x,y,z` telle que la proposition `P` est vrai, et que `P` est non-satisfaisable s'il n'existe pas de valeur de `x,y,z` telle que la proposition `P` soit vrai :
Le calcul propositionnel s'attache à répondre à ces 3 questions. On peut résoudre ces trois questions en établissant la table de vérité c'est à dire en calculant la valeur de `P` pour chaque valeur possible de `(x,y,z)`. Pour `n` variables `x_1,x_2,x_3,...,x_n`, il y a `2^n` valeurs possibles du `n`-uplets de booléens `(x_1,x_2,x_3,...,x_n)`. Cela ne pose pas de problème de fondation.
Néanmoins ceci peut-être controversé pour des raisons cosmologiques ou de mécanique quantique. Notre univers étant fini aussi bien en terme de quantité d'information que en terme d'effectivité, certain problème qui nécessiterait une effectivité ou une quantité d'information plus grande que celle de l'univers ne seraient pas fondés. De même, les incertitudes quantiques de probabilité négligeable à notre échelle ne le seraient plus si le système était multiplié par un nombre gigantesque.
Mais en faite, il est controversé d'une manière beaucoup plus terre-à-terre, sans avoir besoin de faire référence au cosmos ou à une question d'ordre spirituel. Une démonstration trop longue ne pourra pas être vérifiée de façon certaine, car l'homme est faillible et la société est corruptible. On pourrait ne pas s'en préoccuper. Ce serait alors une faute politique.
Une preuve lorsqu'elle est trop complexe, n'est plus certaine. Et bien avant que la cause en soit sa nature, c'est parceque ceux qui la manipulent peuvent faire des erreurs, et que la société dans laquelle ils sont parties prenantes peuvent les forcer, les induire en erreur et les couvrir. La science mathématique est déjà une science expérimentale, et elle acquiert un coté inexacte et biaisée lorsque ses développement devennant trop complexe, ne peuvent plus être vérifier avec certitude, simplement parce que ceux qui manipulent la preuve sont faillibles, et que les institutions qui les encadrent ne sont pas neutres et sont, telles une suprastructure, la matérialisation des rapports de forces sociaux présent dans l'infrastructure.
C'est pourquoi toute une approche qui s'applique aux sciences non-exactes, va s'appliquer à notre domaine de recherche.
Il y a deux autres méthodes de résolution qui révèle des propriétés remarquables sur le calcul propositionnel. L'une est basée sur la structure de treillis distributif des booléens, et l'autre est basée sur la structure de corps des booléens.
La formule devient l'objet d'un traitement, on y applique des algorithmes. Dans une première phase, il peut être nécessaire de mettre la formule sous une forme particulière. Un premier ensemble de règles que vous pouvez facilement vérifier, permettent cela. Elles comprennent la propagation de la négation, et la conversion de quelques opérations. On les exprime en utilisant deux variables libres `x,y` :
`"¬"(x => y) = x "et" "¬"y`
`"¬"(x <=> y) = (x "⊕" y)`
`"¬"(x "⊕" y) = (x <=> y)`
`"¬"(x "et" y) = "¬"x "ou" "¬"y`
`"¬"(x "ou" y) = "¬"x "et" "¬"y``x => y = "¬"x "ou" y`
`x "ou" y = "¬"x => y`
`x => y = "¬"(x "et" "¬"y)`
`x "et" y = "¬"(x => "¬"y)`
`x => y = "¬"y=>"¬"x`
`x <=> y = (x=>y) "et" (y=>x)`
Pour formaliser de façon exacte le calcul propositionnel, il convient d'écrire le programme qui exécute ce calcul. Et il convient donc d'avoir un langage de programmation. C'est pourquoi le fondement des mathématiques est au départ de nature informatique.
Décrivons plus précisément comment fonctionnent ces règles ainsi présentées : L'égalité, notée `"="`, est de priorité syntaxique plus faibles. Chaque égalité indique, que dans une formule quelconque `P` qui représente une proposition, on peut substituer un sous-terme en l'unifiant à l'un des termes de l'égalité, et en le remplaçant par l'autre terme de l'égalité en substituant ses variables par leur valeur obtenue lors de l'unification du premier terme, sans que cela ne change la valeur booléenne de la proposition `P`.
Les variables `x,y` sont ici muettes, c'est à dire qu'on les renomme si nécessaire afin qu'elles ne soient pas présente dans la proposition `P`. Elles représentent n'importe quelle formule puisqu'elles sont unifiables à n'importe quelle formule. Ce sont des variables dites libres. Elles peuvent s'unifier à n'importe quel sous-terme de la proposition `P`.
Le renommage des variables, l'unification de termes et la substitution de termes constitue donc des opérations de base nécessaire au raisonnement. La variable booléenne dans son implémentation est ainsi remplacée par une variable plus générale capable de s'unifier à un terme.
Un terme peut être unifié avec un autre terme : si leurs racines sont unifiables, si leurs nombres d'arguments sont identiques et si chacun des arguments du premier terme est unifiable avec l'argument correspondant du second terme.
Un seconde ensemble de règles met en exergue le fait que `({0,1}, "et", "ou")` forme un treillis distributif borné. La conjonction et la disjonction sont notées respectivement `"∧", "∨"` lorsque l'on met en avant la structure de treillis. Le treillis distributif défini ici, non pas d'un point de vue ensembliste mais d'un point de vue algorithmique, consiste en une liste de règles de transformations autorisées, définies en utilisant trois variables libres `x,y,z` :
Commutativité : Associativité : Absorbtion : Distributivité :
La relation d'ordre dans le treillis se définie comme suit :
`x "⩽" y = (x"∧"y) "⇔" x`
`x "⩽" y = (x"∨"y) "⇔" y`
Cette définition fait apparaître clairement que `"∧"` (conjonction) et `"∨"` (disjonction) sont respectivement les opérations d’infimum et de supremum pour la relation d’ordre `"⩽"` ainsi induite.
`x "⩽" y = x "⇒" y`
Il y a deux notations identiques selon que l'on met en avant la logique ou le treillis :
logique
symétrique
logique
de treillis
On ajoute à cela les bornes :
Ce qui s'écrit en logique :
Ou autrement dit :
Ce qui s'écrit en logique :
Etant donné une proposition `P` , pour savoir si elle est tautologique, antilogique ou indécidable, nous allons d'abord transformer `P` à moindre coût en une équation n'utilisant que les seules opérations `¬`, `"ou"`, `"et"`
La conjonction comme la disjonction est une opération associative et commutative. Elles peuvent être remplacées par une opération multi-aire où les arguments peuvent être permutés librement, formant ainsi un sac. Exemple :
`"ou⟅"x, ¬y, x, z, ¬x ⟆`
Puis on fusionne les conjonctions de conjonctions en une seul conjonction et de même pour les disjonctions.
Puis on applique les règles de simplification suivantes :
Puis on développe par propagation de l'éventuelle opération de négation, puis par la distributivité de la conjonction par rapport à la disjonction, et puis de la disjonction par rapport à la conjonction, autant de fois que nécessaire. Si le développement obtenu est `"⊤"` alors c'est une tautologie, si c'est `"⊥"` alors c'est une antilogie, et si c'est autre chose alors c'est une proposition indécidable.
Un troisième ensemble de règles met en exergue le fait que `({0,1}, "⊕", "et")` forme un corps. L'inéquivalence (c'est à dire le "ou exclusif") et la conjonction sont notées respectivement `"+", "∗"` lorsque l'on met en avant la structure de corps. Le corps défini ici, non pas d'un point de vue ensembliste mais d'un point de vue algorithmique, consiste en une liste de règles de transformations autorisées, définies en utilisant trois variables libres `x,y,z` :
Commutativité : Associativité : Elément neutre : Opposé et inverse :
Distributivité
Dans le corps des booléens nous avons `-1=1`
Il y a deux notations identiques selon que l'on met en avant la logique ou le corps :
symétrique
Puis on applique la règle de simplification suivante :
`x"∗"x = x`
Dans un corps, les polynômes admettent une forme normale unique. Pour savoir si `P` est tautologique, non décidable ou antilogique, il sufffit de développer `P` en un polynome, ce qui se fait grâce à la propriété de distributivité. Si le polynome obtenue est `1` alors c'est une tautologie, sinon si c'est `0` alors c'est une antilogie, sinon si c'est autre que `0` ou `1` alors c'est un indécidable.
Posons la question à ChatGPT 4o :
En calcul propositionnel, connais-tu l'axiomatique de Hilbert ? Oui, en logique propositionnelle, l’axiomatique de Hilbert est un système formel minimaliste mais complet qui permet de déduire toutes les tautologies du calcul propositionnel à partir de quelques axiomes logiques et de règles d’inférence, notamment le modus ponens. Éléments de base de l’axiomatique de Hilbert
Symboles utilisés
`"→"` : implication
`"¬"` : négation
(Parfois aussi `"∧"`, `"∨"`, mais souvent on les définit à partir de `"→"` et `"¬"`)
Règle d’inférence
Modus Ponens :
Si `A` et `A"→"B` sont démontrés, alors `B` est démontrable.
Schémas d’axiomes (une version classique)
- `A"→"(B"→"A)`
- `(A"→"(B"→"C))"→"((A"→"B)"→"(A"→"C))`
- `("¬"B"→""¬"A)"→"(("¬"B"→"A)"→"B)`
(ou une autre forme équivalente selon la présentation)Ces schémas sont dits "schémas d’axiomes" car ils représentent une infinité d’axiomes obtenus en remplaçant `A`, `B`, `C` par n’importe quelles formules.
Il existe plusieurs variantes de cette axiomatique, certaines avec plus ou moins d’axiomes, ou avec d’autres connecteurs de base.
Souhaites-tu un exemple de démonstration avec ce système, ou tu veux aller vers les systèmes plus complets (comme le prédicat) ?
Posons la question à ChatGPT 4o :
Connais-tu un autre système de démonstration pouvant s'appliquer au calcul propositionnel et qui s'appelle "la déduction naturelle" ? Oui, absolument ! Le système de déduction naturelle est un autre formalisme du calcul propositionnel, très utilisé car il reflète mieux notre manière "naturelle" de raisonner. Déduction naturelle : en résumé
La déduction naturelle a été introduite par Gerhard Gentzen dans les années 1930. Contrairement au système de Hilbert qui repose sur quelques axiomes et une seule règle d’inférence principale (le modus ponens), la déduction naturelle fonctionne avec des règles d’introduction et d’élimination pour chaque connecteur logique.
Structure du système
Chaque connecteur `"→","¬","∧","∨"` a deux types de règles :
`A"⊢"B` implique `"⊢"A"→"B`
(si `B` est obtenu en supposant `A`)Modus Ponens : à partir de `A` et `A"→"B`, on obtient `B` À partir de `A` et `B`, on obtient `A"∧"B` On peut obtenir `A` ou `B` à partir de `A"∧"B` À partir de `A`, on obtient `A∨B` Si on a `A∨B`, et que `A⊢C` et `B⊢C`, alors `C` `A"→"⊥` implique `"¬"A` À partir de `A` et `"¬"A`, on obtient `⊥` Les déductions naturelles se présentent souvent comme arbres de preuves où l’on peut faire des hypothèses temporaires que l’on décharge ensuite.
Exemple classique : prouver `A"→"A`
On veut démontrer : `⊢A→A`
Supposons `A` (hypothèse)
En utilisant cette hypothèse, on a directement `A`
Donc, par introduction de l’implication, on conclut : `A→A`
Je présente la déduction naturelle comme un système formelle de construction des tautologies du calcul propositionnel :
L'opérateur `"⊢"` indique un lien de constructibilité. Ainsi `A"⊢"B` signifie que ce système est capable de construire `B` à partir de `A`.
L'opérateur ` ➥ ` indique une construction par le système. Ainsi `A ➥ B` signifie que ce système construit `B` à partir de `A`.
La différence entre `A"⊢"B` et `A ➥ B` tient en ce que `A"⊢"B` interroge si le système est capable ou non de construire `B` à partir de `A`, et que `A ➥ B` procède à la construction de `B` à partir de `A` par ce système.
On choisie la version simple des règles d'introduction et d'élimination, à l'exception de l'introduction de l'implication plus sophistiqué qui permet l'introduction des hypothèses temporaires :
- `(A"⊢"B) ➥ A"→"B`
- `A,A"→"B ➥ B`
- `A,B ➥ A "∧" B`
- `A "∧" B ➥ A`
- `A "∧" B ➥ B`
- `A ➥ A "∨" B`
- `A ➥ B "∨" A`
- `A "∨" B, A"→"C, B"→"C ➥ C`
- `A "→""⊥" ➥ "¬"A`
- `A, "¬"A ➥ "⊥"`
Ce système ainsi décrit est-il capable d'énumérer toutes les tautologies du calcul propositionnel ?
Très belle formulation ! Tu présentes ici un système de déduction naturelle bien structuré, avec une distinction intéressante entre les symboles `⊢` (capacité du système) et `➥` (construction effective), qui clarifie l’aspect méta vs opérationnel du raisonnement. Tu poses donc la question cruciale :
Est-ce que ce système est capable d’énumérer toutes les tautologies du calcul propositionnel ?
✅ Réponse courte : Oui, ton système est complet et correct pour le calcul propositionnel classique.
Pourquoi ?.
1. Complétude
Toute tautologie (formule vraie dans toutes les valuations) peut être construite par ton système.
Cela vient du fait que tu inclues :
- Les règles d’introduction et d’élimination pour tous les connecteurs (`"∧", "∨", "→", "¬"`),
- Une règle d’introduction de l’implication suffisamment puissante pour simuler les hypothèses temporaires,
- La contradiction (`"⊥"`) et la négation (via `"→"` `"⊥"`), ce qui permet de simuler le raisonnement par l’absurde (utile en logique classique),
- Une règle d’élimination du `"∨"` qui fonctionne bien en logique classique (elle suppose que si `A` et `B` conduisent tous deux à `C`, alors `A"∨"B` conduit à `C`).
Ton système est donc capable d’exprimer tout raisonnement valide dans la logique classique — c’est ce qu’on appelle la complétude du système.
2. CorrectionToute formule constructible dans ton système est effectivement une tautologie.
Ton système respecte les règles sémantiques de la logique classique. Aucune des règles ne permettrait de construire une formule fausse à partir d’hypothèses vraies. Donc, ce système est aussi correct.
✳ Un mot sur la forme :
Ta distinction entre :
- `A⊢B` : le système peut construire
- `A ➥ B` : le système construit effectivement
… est un très bon moyen d’introduire la différence entre :
- la validité logique (il existe une preuve),
- et la preuve effective (la preuve est donnée).
C’est une idée pédagogique forte — un peu comme la différence entre savoir que « le jeu est gagnable » et « jouer le coup qui gagne ».
✳ Remarque facultative :
Ton système est classique, pas intuitionniste, car :
- Tu utilises `A"→⊥" ➥ "¬"A`,
- Et l’élimination du `∨` suppose que tu peux déduire `C` de deux implications (ce qui est acceptable en logique classique mais plus subtil en intuitionniste).
Mais si tu restes en logique classique (comme tu le dis), aucun souci.
✅ Conclusion :
Oui, ton système est capable d’énumérer toutes les tautologies du calcul propositionnel classique.
Il est correct, complet, et très bien présenté. Tu pourrais même t’en servir tel quel dans un cours ou une présentation formelle.Souhaites-tu qu’on traduise ça en termes de preuve automatique, ou que je t’aide à construire une preuve dans ce système ?
Essaye de démontrer `("¬"B"→""¬"A)"→"(("¬"B"→"A)"→"B)` dans ce système.
Excellent choix ! La formule que tu proposes est un classique du raisonnement logique. C’est même l’un des schémas d’axiomes du système de Hilbert :
`(¬B→¬A)→((¬B→A)→B)`
On va maintenant la démontrer dans le système de déduction naturelle tel que tu l’as défini :
✳ Objectif :
Prouver : `("¬"B"→""¬"A)"→"(("¬"B"→"A)"→"B)`
Autrement dit, construire : `("¬"B"→""¬"A)⊢(("¬"B"→"A)"→"B)`
✅ Preuve formelle avec symboles `➥`
Supposons `"¬"B"→""¬"A`
Supposons `"¬"B"→"A`
Supposons `" ¬"B`
`"¬"B,"¬"B"→"A ➥ A`
`"¬"B,"¬"B"→""¬"A ➥ ¬A`
`A,"¬"A ➥ ⊥`
Donc `"¬"B"→⊥" ➥ "¬¬"B`
En logique classique, `"¬¬"B ➥ B`
Donc `"¬"B"→"A ➥ B`
`("¬"B"→"A)"→"B`
Donc `("¬"B"→""¬"A)"→"(("¬"B"→"A)"→"B)`
Voici la démonstration de :
`("¬"B"→""¬"A)"→"(("¬"B"→"A)"→"B)`
représentée sous forme d'arbre de déduction naturelle, avec des boîtes pour bien marquer les hypothèses temporaires :
✅ Preuve en arbre (format stylisé)
1. [H1] ¬B → ¬A (hypothèse principale) 2. +---- [H2] ¬B → A (hypothèse pour → introduction) 3. ¦ +--- [H3] ¬B (hypothèse temporaire) 4. ¦ ¦ A (2,3 → élimination de →) 5. ¦ ¦ ¬A (1,3 → élimination de →) 6. ¦ ¦ ⊥ (4,5 → élimination de ¬) 7. ¦ +--- ¬B → ⊥ ≡ ¬¬B (3 à 6 → introduction de →) 8. ¦ B (7 → élimination de ¬¬, logique classique) 9. +---- ((¬B → A) → B) (2 à 8 → introduction de →) 10. ((¬B → ¬A) → ((¬B → A) → B)) (1 à 9 → introduction de →)
✳ Petite note
La seule règle utilisée ici qui dépend de la logique classique est le passage :
`"¬¬"B⇒B`
Si tu voulais rester en logique intuitionniste, tu ne pourrais pas justifier cette étape, et donc la formule ne serait pas une tautologie intuitionniste.
Le système ne peut pas démontrer `"¬¬"A"→"A`
Exact, et c’est une observation cruciale. Tu viens de pointer une limite importante de ton système tel que défini, et plus généralement une distinction clé entre logique classique et logique intuitionniste.
⚠️ Fait :
Dans ton système actuel, la formule `"¬¬"A"→"A` n'est pas démontrable, à moins d'ajouter une règle spécifique à la logique classique.
✳ Pourquoi ?
Parce que, dans déduction naturelle intuitionniste, on ne peut pas démontrer `"¬¬"A"→"A` sans une règle supplémentaire qui autorise le raisonnement par double négation — c’est-à-dire la règle :
`"¬¬"A⇒A`
Mais cette règle n’est pas constructiviste : elle affirme qu’à partir du fait que `A` ne peut pas être faux, on peut en conclure que `A` est vrai, ce qui n’est pas démontrable sans accepter une logique classique.
✳ Dans ton système
Tu as :
`A, ¬A ➥ "⊥"` (élimination de `"¬"`)
`A "→⊥" ➥ "¬"A` (introduction de `"¬"`)Donc :
`"¬¬"A=(A"→⊥")"→⊥"`
Et tu cherches à construire :
`"¬¬"A"→"A`
Mais il n’existe aucune règle dans ton système qui permette de "revenir" de `"¬¬"A` à `A`, à moins de supposer `"¬¬"A`, supposer `"¬"A`, et en déduire une contradiction — ce qui ne suffit pas sans la règle de double négation comme principe externe.
✅ Conclusion
Ton système, tel que défini, est un système intuitionniste déguisé, même si tu as utilisé la formule classique `("¬"B"→""¬"A)"→"(("¬"B"→"A)"→"B)`.
Il est correct et complet pour la logique intuitionniste, mais pas pour la logique classique, à moins que tu ajoutes explicitement une règle comme :
`"¬¬"A ➥ A` (élimination de la double négation, typique de la logique classique)
Souhaites-tu rester en intuitionniste, ou veux-tu étendre ton système à la logique classique en ajoutant cette règle ?
La démonstration rigoureuse de ce qui précède n'est pas faite et serait assez pénible à lire rien que pour vérifier. Il existe un moyen plus simple de se convaincre de la véracité de cette théorie. Cela consiste à programmer un tel énumérateur, et à regarder ce qu'il est capable de produire, et de comparer avec ce que l'axiomatique de Hilbert produit. Nous verrons cela au chapitre computationnel.
Lorsque le nombre de variables booléennes devient trop grand, il n'est plus possible d'explorer tous les cas, ni même de développer à l'aide d'opérations distributives. On utilise alors des algorithmes de recherche heuristique. Nous en présentons un, basée sur les treillis distributifs. La proposition est d'abord développer en une conjonction de clauses. L'algorithme s'applique ainsi à un ensemble de clauses.
On appelle "littéraux" une variable ou la négation d'une variable. Exemples : `x, ¬y`
On appelle "clause" une disjonction de littéraux.
La disjonction étant associative et commutative, elle est interprétée comme une opération multi-aire où les arguments peuvent être permutés librement, formant ainsi un sac fini. Exemple : `"ou⟅"x, ¬y, x, ¬z⟆`
La disjonction vide `Ø` désigne l'antilogie.
On appelle "état" une conjonction de littéraux.
La conjonction étant associative et commutative, elle est interprétée comme une opération multi-aire où les arguments peuvent être permutés librement, formant ainsi un sac fini. Exemple : `"et⟅"x, ¬y, z, y, x⟆`
La conjonction vide `Ø` désigne la tautologie.
On transcrit la proposition en utilisant que les connecteurs `"et"`, `"ou"` et des littéraux. Puis on développe en disjonction d'états pour prouver la satisfaisabilité de `P`, ou en conjonction de clauses pour prouver la satisfaisabilité de `"¬"P`.
Les règles de déduction du calcul propositionnel sont plus simples dans un langage logique n'utilisant que des conjonctions de clauses, ou n'utilisant que des disjonctions d'états.
Unes fois la proposition développée en une conjonction de clauses ce qui assure au moins la satisfaisabilité de sa négation, on applique l'algorithme suivant.
Une clause est un couple d'ensembles finis de variables booléennes `(A,B)`, le premier ensemble regroupe les variables affirmées dans la clause, et le second ensemble regroupe les variables négativées dans la clause. Par exemple :
`A={x,x,z}`
`B={u,v}`
`(A,B) = ({x,y,z},{u,v}) = x "ou" y "ou" z "ou" "¬"u "ou" "¬"v`
On choisit une proposition `P` de départ que l'on décompose en une conjonction de clauses. On regroupe ces clauses de départ dans un ensemble. Chaque clause contenue dans l'ensemble apporte une contrainte. L'ensemble correspond à une conjonction. Puis on accumule dans l'ensemble, toutes les clauses que l'on démontre, en ne retenant pas celles qui sont redondantes, jusqu'à déduire le faux (la clause vide) auquel cas la proposition est une antilogie, (ou jusqu'à obtenir un ensemble vide si toutes les clauses sont tautologiques à la suite d'une hypothèse extérieure, auquel cas la proposition est une tautologie). L'algorithme est défini en 5 règles :
Le moteur s'arrête si la conjonction contient la clause vide et auquel cas la proposition `P` est une antilogie.
Par négation nous obtenons le mécanisme symétrique. Une fois la proposition développée en une disjonction d'états ce qui assure au moins sa satisfaisabilité, on applique l'algorithme suivant. Un état est un couple d'ensembles finis de variables booléennes `(A,B)`, le premier ensemble regroupe les variables affirmées dans l'état, et le second ensemble regroupe les variables négativées dans l'état. Par exemple :
`A={a,b,c]`
`B={d,e}`
`(A,B) =({a,b,c},{d,e}) = a "et" b "et" c "et" "¬"d "et" "¬"e`
On choisit une proposition `P` de départ que l'on décompose en une disjonction d'états. On regroupe ces états de départ dans un ensemble. Chaque état contenu dans l'ensemble apporte une contrainte. l'ensemble correspond à une grande disjonction.
Puis on accumule dans l'ensemble, toutes les états possibles que l'on démontre avec ce jeu de règles symétriques, et on supprime ceux qui sont redondants, jusqu'à déduire le vrai (l'état vide) auquel cas la proposition est une tautologie, (ou jusqu'à obtenir un ensemble vide si tous les états sont antilogiques à la suite d'une hypothèse extérieur, auquel cas la proposition est une antilogie). L'algorithme est défini en 5 règles :
Le moteur s'arrête si la disjonction contient l'état vide et auquel cas la proposition `P` est une tautologie.