Sommaire :
Qu'est ce qu'une théorie au sens le plus général ?. C'est un système de déduction calculable. Pourquoi calculable ? parcequ'une déduction est une construction faisable par une machine, et qu'en déduisant, nous ne faisons que calculer. Remarquez qu'avec cette contrainte qu'est la calculabilité, et en souscrivant à la thèse de Church, nous sommes assurés d'atteindre le plus haut niveau de généralité possible.
Le système de déduction comprend un ensemble de propositions `L` et une relation `"⊢"` sur cet ensemble, qui désigne les déductions entre propositions. Cette relation étant le résultat d'un calcul, elle est énumérable. Et on l'appel la relation de démontrabilité ou la relation de déduction, ou simplement la déduction.
Nous allons construire petit à petit, et en parallèle, le langage des propositions et le système de déduction, en ajoutant un à un les connecteurs au langage des propositions qui permetront de construire des propositions complexes, et une à une les règles que devra satisfaire la relation de déduction. Ainsi nous établirons une méta-théorie des théories.
On commence par le langage propositionnel le plus rudimentaire ne contenant que des propositions atomiques en nombre fini ou énumérable. Notez que rien n'est préciser concernant la sémantique de ces propositions atomiques, c'est à dire leur signification, les modèles qu'elles décrivent. En particulier, ces propositions ne doivent pas être considérées comme des variables booléennes.
Dans un système de déduction, la relation de démontrabilité doit satisfaire deux règles que sont la réflexivité et la transitivité :
`"⊢ est un préordre"` `"⊢ est réflexive"` `a"⊢"a` `"⊢ est transitive"` `a"⊢"b" et " b "⊢"c => a "⊢"c`
Notez que dans ces règles, les propositions atomiques nouvelles `a,b,c` sont implicitement quantifiées universellement sur `L`.
Notez que la priorité syntaxique des connecteurs est ordonnée comme suit, de la plus faible à la plus forte, `=`, `<=>`, `=>`, `"et"`, `↔`, `|--`, ce qui permet d'omettre un certain nombre de parenthèses sans introduire d'ambiguïté. Le principe de ce choix est de donner une priorité faible à l'égalité afin d'éviter de devoir entourer les termes des équations par des parenthèses, puis de donner une priorité plus forte pour la demi-égalité, puis une priorité plus forte pour la conjonction, et une priorité plus forte encore pour les relations étudiées tel que la relation d'équivalence `"↔"` et la relation de déduction `"⊢"`.
Et si la relation de déduction ne satisfait pas ces deux règles que sont la réflexivité et la transitivité, alors on parlera de déduction local `"⊢"_"local"`, la déduction global étant enrichie de ces deux règles pour former une relation plus riche de déduction.
Délors, le langage des démonstrations, que l'on note `D`, va pouvoir se définir à partir de cette relation de déduction locale et des deux règles globales imposées que sont la reflexivité et la transitivité. Une démonstration est une suite de proposition de `L` telle que chaque proposition déduit localement son successeur, et où l''hypothèse est la première proposition et où la conclusion est la derniere proposition.
`D = {(a_i)_(i in{0,1,2...,n}) "/" EEn"∈"NN"*", AA i "∈"{1,2,...,n"-"1}, a_i "∈" A, a_i "⊢"_"local"a_(i+1)}`
Ces deux règles font que la relation de démontrabilité est un pré-ordre partiel. Et à partir du préordre `"⊢"` on définie sa symétrisée `"↔"`, qui constitue une relation d'équivalence :
`a"↔"b <=> a "⊢"b" et "b"⊢"a` `a"↮"b <=> a "⊬"b" ou "b"⊬"a`
Considérons une proposition quelconque `a`. L'ensemble des propositions équivalentes à `a` se note `[a]`. L'ensemble des propositions déductibles de `a` se note `"<"a">"`. Et l'ensemble des propositions déduisant `a` se note `"<"a">"^("-"1)` car correspondand à la relation de déduction inverse.
On divise l'ensemble `L` par la relation d'équivalence `"↔"` pour produire la structure `L"/↔"` regroupant l'ensemble des classes d'équivalences :
Notez que l'on réserve l'usage des braquettes `{}` uniquement pour regrouper des éléments distincts, ce qui explique ici le choix de la notation utilisant l'itérateur d'union.
Dans cette structure `L"/↔"`, le préordre `"⊢"` induit un ordre désigné par le même symbole :
`"dans "L"/↔"``"⊢ est réflexive"` `[a]"⊢"[a]` `"⊢ est antisymétrique "` `[a]"⊢"[b]" et "[b]"⊢"[a] => ([a]"="[b])` `"⊢ est transitive"` `[a]"⊢"[b]" et "[b]"⊢"[c] => [a]"⊢"[c]`
Remarquez qu'un préordre inversé est encore un préordre et donc que la relation inverse `⊣` est encore une relation de déduction, et que ces deux relations de déductions `"⊢", "⊣"` ont les mêmes classes d'équivalences et induisent un même ordre mais inversé dans la structure `ccL"/↔"`.
A ce stade qualifié de prélogique où la négation n'est pas encore définie, on peut quand-même définir les antilogies et les tautologies, et donc d'une certaine manière le faux et le vrai à équivalence près. Une proposition est une antilogie si et seulement si elle démontre toutes les propositions, et elle constitue alors un élément minimal total vis-à-vis du péordre `"⊢"`. Une proposition est tautologie si et seulement si elle est démontrée par n'importe quelle proposition, et elle constitue alors un élément maximal total vis-à-vis du péordre `"⊢"` . Une proposition qui n'est ni une tautologie ni une antilogie est appellé un indécidable. L'ensemble des propositions `L` se partitionne en trois parties :
`a" est une antilogie"` `a" est un minimum total pour ⊢"` `AA x "∈" L, a"⊢"x` `a" est une tautologie"` `a" est un maximum total pour ⊢"` `a" est un indécidable"` `a" n'est pas un bout total pour ⊢"`
On utilise aussi les adjectifs correspondant ; une proposition antilogique est une antilogie, une proposition tautologique est une tautologie, une proposition indécidable est un indécidable.
On peut toujours ajouter deux propositions atomiques, le vrai `"⟙"`, et le faux `"⟘"`, en ajoutant les deux contraintes suivantes sur la relation de démontrabilité.
Et on remarquera que ces deux contraintes n'ont aucune influence sur la relation de déduction restreinte en enlevant ces deux propositions. Il s'agit donc juste d'une commodité d'écriture, pour désigner facilement la classe des tautologies `["⟙"]`, et la classe des antilogies `["⟘"]`.
Un moyen mémothechnique : L'antilogie démontre tout, donc est placée avant tout le monde dans l'ordre de démontrabilité, donc constitue un minimum total représenté par le symbole du sol `"⟘"`. Tandis que la tautologie est démontrer par tout le monde, donc est placée après tous le monde dans l'ordre de démontrabilité, donc constitue un maximum total représenté par le symbole du ciel `"⟙"` qui est également similaire à la lettre T de Tautologie.
L'ensemble des propositions se note `"<"⟘">"= L"` puisque qu'elles sont toutes démontrées par l'antilogie, et l'ensemble des propositions démontrables se note `"<"⟙">"`, et est appelé l'ensemble des tautologies. Et nous avons bien évidemment `⟘⊢⟙`. Et ces deux ensembles sont énumérables puisque la relation `"⊢"` est énumérable.
On définie la notion de cohérence et d'incohérence comme suit :
Le système de déduction `|--` est cohérent `⟙⊬⟘` Le système de déduction `|--` est incohérent `⟙⊢⟘`
Et dans un système incohérent, toute les propositions sont équivalentes.
A l'aide de ces deux propostions `⟙, ⟘` et d'une proposition quelconque `a`, on caractérise 6 sous-ensembles de propositions possibles :
`a` est démontrable `a` est une tautologie `a` est de fausseté démontrable `a` est une antilogie `a` est décidable `a` est une tautologie ou une antilogie `a` est indémontrable `a` est une antilogie ou un indécidable `a` est de fausseté indémontrable `a` est une tautologie ou un indécidable `a` est indécidable `a` est un indécidable
Et si nous avons une proposition `a` qui démontre une proposition `b` alors nous avons ces suites ordonnées :
`"<"⟘">"^("-"1) sube "<"a">"^("-"1) sube "<"b">"^("-"1) sube "<"⟙">"^("-"1)`
Une proposition peut être vue comme un ensemble défini par extension. Il contient alors toutes ses alternatives microscopiques possibles, c'est à dire une disjonction de mondes élémentaires. L'élément minimum est vide et correspond au faux, l'élément maximum est plein et correspond au vrai.
Une proposition peut être vue comme un ensemble définie par compréhension, il contient alors toutes ses déductions, c'est à dire une conjonction de propositions. L'élément minimum est vide et correspond au vrai, l'élément maximum est plein et correspond au faux.
La relation de déductibilité `"⊢"` étant énumérable, il existe un énumérateur de toutes les déductions possibles. Et donc il existe un énumérateur de `"<"a">"`. il existe un énumérateur de `"<"a">"^("-"1)`. Et il existe un énumérateur de `[a]`.
Parcontre les indémontrables peuvent être non énumérable. Il reste à trouver à titre d'exemple, un système de déduction atomique énumérable, le plus simple possible, ayant un ensemble de propositions indémontrables non énumérables.
`ccL = NN`
`"⟘" = 0`
`"⟙" = 1`
`n⊢_"local"f(n)`
L'ensemble des propositions démontrables est :
`"<"1">" = uuu_(ninNN) {f^n(1)}`
L'ensemble des propositions indémontrables est :
`"<"0">"-"<"1">" = NN- uuu_(ninNN) {f^n(1)}`
Ce second ensemble peut être non énumérable. Par exemple en codant les programmes par des entiers, si le premier ensemble comprend tous les programmes qui appliqués à `0` s'arrète en un temps fini, alors le second ensemble qui est son complémentaire comprend tous les programmes qui appliqués à `0` ne s'arrète jamais. Le premier ensemble est énumérable par minimalisation, et le second ensemble est non énumérable à cause du paradoxe de Godel-Turing.
Deux descriptions globales de la relation de déduction peuvent être obtenue ainsi :
`EEx"∈" L, x "⊢"a" et "x"⊬"b`
On définie `"⊢"_E`, la relation de déduction restreinte à un sous-ensemble de propositions `E sube L` :
`EEx"∈" E, x "⊢"a" et "x"⊬"b`
Le sous-ensemble de propositions `E` se partitionne en trois parties :
`A" est une "E"-tautologie"` `a" est un minimum total pour ⊢"_E` `A" est une "E"-antilogie"` `a" est un maximum total pour ⊢"_E` `A" est un "E"-indécidable"` `a" n'est pas un bout total pour ⊢"_E`
On remarque qu'une tautologie dans `L` est une tautologie dans toutes les restrictions de `L`, parcontre l'inverse n'est pas vrai.
De même on remarque qu'une antilogie dans `L` est une antilogie dans toutes les restrictions de `L`, parcontre l'inverse n'est pas vrai.
Nous avons une relation de démontrabilité `"⊢"` reflexive, transitive et énumérable. On construit sa symétrisé `"↔"` qui constitue une relation d'équivalence. La relation de démontrabilité `"⊢"` induit donc une relation d'ordre partiel sur `ccL"/↔"`. Puis nous ajoutons une proposition minimale totale `⟘`, et une proposition maximale totale `⟙`.
L'expression `a"⊢"b` signifie que la proposition `a` démontre la proposition `b`. Mais ce symbole `"⊢"` ne fait pas partie du langage propositionnel. On cherche à l'introduire dans le langage propositionnel sous forme du connecteur logique d'implication. Cet ajout va entrainer de nouvelles règles que devra satisfaire la relation de démontrabilité. Comment trouver ces règles ?
Lorsqu'il y a une proposition minimale ⟙, on pense à une première règle suivante :
Notez la distinction entre les propositions complexes de `ccL` écrites en rouge et la méta-proposition englobante écrite en bleu. Car pour étudier la théorie en toute liberté, il faut se placer à l'extérieur, et donc utiliser un langage distinct qui la complète. Le symbole `=>` a ainsi deux senses. Soit il est utilisé pour construire une proposition complexe appartenant à `ccL` auquel cas il fait partie du langage de la théorie prélogique, ou soit il est utilisé pour décrire la théorie prélogique auquel cas il fait partie du langage de la méta-théorie.
C'est la définition anthique de l'implication, par opposition à la définition booléenne de l'implication. Elle signifie textuellement que si on peut démontrer la proposition `(a"⇒"b)` alors la proposition `a` démontre la proposition `b`, et réciproquement, si la proposition `a` démontre la proposition `b`, alors on peut démontrer la proposition `(a"⇒"b)`. Par contraposé, cela signifie aussi :
C'est à dire textuellement que si la proposition `(a"⇒"b)` est indémontrable, alors la proposition `a` ne peut pas démontrer la proposition `b`, et réciproquement, si la proposition `a` ne peut pas démontrer la proposition `b`, alors on ne peut pas démontrer la proposition `(a"⇒"b)`.
Mais il y a d'autres règles auquel le système de déduction doit se soummettre, telles les shémas d'axiomes de Hilbert, et le modus ponens. Comment les déduisons nous ?
Les shémats d'axiomes de Hilbert
A |- (B => A)
(A => (B => C)) |- ((A => B) => (A => C))
1.2) La règle d'inférence dite du Modus Ponens
A, A=>B --> B
---- 7 août 2018 ----
A ce stade qualifié de prélogique où la négation n'est pas encore définie, on peut quand-même définir le vrai et le faux à équivalence près. Une proposition est fausse si et seulement si elle démontre toutes les propositions, et elle est appelée une antilogie. Une proposition est vrai si et seulement si elle est démontrée par n'importe quelle proposition, et elle est appelée tautologie.
Rien ne nous oblige à ajouter ces deux propositions extrèmes vis-à-vis du préordre `"⊢"`. Et s'il n'y en a pas alors il n'existe pas de tautologies ni d'antilogies. Par contre si on se restreint à un sous-ensemble de propositions `ccE sub ccL` on peut retrouver des totologies et antilogies qui seront délors relatives à ce sous-ensemble `ccE`.
On étend l'usage du symbole de déduction aux ensembles de propositions comme suit :
`ccE"⊢"A <=> AAX"∈" ccE, X"⊢"A` `ccE"⊬"A <=> EEX"∈" ccE, X"⊬"A` `A"⊢"ccE <=> AAX"∈" ccE, A"⊢"X` `A"⊬" ccE <=> EEX"∈" ccE, A"⊬"X` `ccE"⊢"ccF <=> AAX"∈" ccE, AAY"∈" ccF, X"⊢"Y` `ccE"⊬"ccF <=> EEX"∈" ccE, EEY"∈" ccF, X"⊬"Y`
Et nous avons :
`A` est vrai pour `ccE` `A` est indémontrable pour `ccE` `A` est faux pour `ccE` `A` est de fausseté indémontrable pour `ccE` `A` est décidable pour `ccE` `A` est indécidable pour `ccE`
Remarquez qu'il est toujours possible d'ajouter deux propositions atomiques, le vrai `"⟙"_ccE`, et le faux `"⟘"_ccE` relatifs à l'ensemble de propositions `ccE`, en ajoutant les deux contraintes suivantes sur la relation de démontrabilité :
Délors :
A est une `ccE`-tautologie `ccE"⊢"A` A est une `ccE`-antilogie `A"⊢"ccE` A est un `ccE`-indécidable `"⟙"_ccE"⊬"A" et "A"⊬""⟘"_ccE` `ccE"⊬"A" et "A"⊬"ccE`
L'introduction dans le langage propositionnel du symbole d'implication `=>` va entrainer une contrainte sur le système de déduction
la règle de déduction du modus ponens :
Les deux seuls opérations prédéfinies sont le connecteur logique `"et"` qui permet de construire les ensembles finis de propositions appelés théories, et la relation de démontrabilité `"⊢"`, une relation transitive, compatible avec le et, et énumérable puisque devant être produit par le calcul
`"⊢" "énumérable"` `EE f in (NN->ccL^2), f " calculable" et " f(NN="⊢")` `"⊢" "transitive"` `AA (A,B,C) in ccL^3, A"⊢"B " et " B"⊢"C => A"⊢"C `"⊢" "compatible avec le et"` A"⊢"B " et " A"⊢"C => A"⊢"(B" et "C)
L'expression `A" et "B` et égale la théorie `AuuB`. C'est la définition compréhensive du et qui se traduit par l'union d'ensembles de compréhensions.
Le graphe de la relation de démontrabilité `"⊢"` étant énumérable, il existe un énumérateur de toutes les déductions possibles. L'ensemble des propositions déductibles d'une théorie `A` se note `"<"A">"`.
`"<"A"> énumérable"`
A ce stade qualifié de prélogique où la négation n'est pas encore définie, on peut quant-même définir l'implication, l'équivalence, le ou, le vrai et le faux:
où `ccL` représente l'ensemble des propositions. Ainsi, l'ensemble des propositions se note `ccL="<"⟘">"` puisque démontrées par le faux, et l'ensemble des tautologies se note `"<"⟙">"`. Et nous avons bien évidemment `"⟘"=>"⟙"`. Et ces deux ensembles sont énumérables par le processus de construction des démonstrations décrit dans la méta-théorie.
Une théorie `A` implique une théorie `B` si et seulement si `A` démontre `B`, et donc, la relation de démonstration étant transitive, si et seulement si tous ce qui est démontrable par `B` est démontrable par `A`.
`A=>B` si et seulement si `"<"B">"sube"<"A">"`
Et donc pour toutes théorie `A`, nous avons :
`"⟘" => A => "⟙"`
`"<⟙>" sube"<"A">"sube"<"⟘">"`
La théorie `A` est plus riche que la théorie `B` si et seulement si `A=>B`. Et dans ce cas nous avons :
`"⟘" => A => B => "⟙"`
`"<⟙>" sube"<"B">"sube"<"A">"sube"<"⟘">"`
Les 4 ensembles suivants sont à considérer :
démontrées par `A``"<"⟘">"-"<"A">"`
indémontrable par `A`
non énumérable
La méta-théorie est dit contradictoire si et seulement si `"⟘"<=>"⟙"`
On définie la contradiction comme suit. Etant donné deux théories `A` et `B`, elles sont contradictoires si et seulement si `A" et "B =>"⟙"`. Mais la contradiction ainsi définie ne permet pas de définir une négation unique à équivalence près. L'ensemble des négations possibles d'une théorie `A` en prélogique est définie comme suit :
`B` est une négation de `A` si et seulement si, elle est contradictoire avec `A` et que toute proposition démontrée à la fois par `A` et par `B` est une tautologie :
`(A" et "B) => "⟘"` `((A=>C)" et "(B=>C)) => ("⟙"=>C)`
Autrement dit `B` est une négation de `A` si et seulement si :
`"<"A uu B">" = "<⟘>"` `"<"A">"nn"<"B">" = "<"⟙">"`
En l'absence de proposition minimale, la règle se généralise en l'appliquant à toutes les restrictions possibles :
Autrement dit :
Ainsi, l'ensemble des propositions se note `"<"⟘">"` puisque démontrées par le faux, et l'ensemble des tautologies se note `"<"⟙">"`. Et nous avons bien évidemment `"⟘"=>"⟙"`. Et ces deux ensembles sont énumérables par le processus de construction des démonstrations décrit dans la méta-théorie.
---- 4 août 2018 ----
Puis on passe au stade logique en introduisant la négation. La logique classique, comme le calcul booléen, possède une symétrie qu'est la négation notée par l'opérateur `"¬(.)"`. Toutes propositions `P` admet une proposition négative `"¬"P` qui obéït au principe d'exclusion `"¬"(P" et ¬"P)` et au principe du tiers exclu `(P" ou ¬"P)`. Et nous avons `"⟘"<=>"¬⟙"`.
A ce stade il faut supposer que la méta-théorie n'est pas contradictoire.
Et par symétrie, l'ensemble des antilogies `"¬<"⟙">"` est énumérable. De même,
Mais si la méta-théorie est suffisament riche pour pouvoir programmer tout en étant non contradictoire, c'est à dire en termes logique si elle contient l'arithmétique, alors le paradoxe de Godel-Turing fait que l'ensemble des propositions indécidables c'est à dire dont on ne peut pas démontrer ni l'affirmatiion ni la réfutation, n'est pas énumérable. Car sinon tout serait prédictible en temps fini, et en particulier, l'arrêt en un temps fini ou non d'un programme appliqué à une donnée serait prédictible en un temps fini.
Les 7 ensembles suivants sont à considérer :
décidables
non démontrables
de négation non démontrables
indécidables
L'ensemble des indécidables n'est pas énumérable, et donc n'est non vide. La théorie est donc incomplète. Voila pourquoi le paradoxe de Godel-Turing dévoile l'inhérente incomplètude des théories.
Considérons une théorie `T`. L'ensemble des propositions déductibles d'une théorie `T` que l'on note `"<"T">"` est énumérable par un processus de construction des démonstrations décrit dans la méta-théorie et `T`. Parcontre L'ensemble des propositions indécidables par `T` n'est pas énumérable.
Remarquez qu'une théorie `A` implique une théorie `B` si et seulement si tous ce qui est démontrable par `B` est démontrable par `A`.
`(A=>B) <=> ("<"B">"sube"<"A">")`
Et donc pour toutes théorie `T`, nous avons :
`"⟘" => T => "⟙"`
`"<⟙>" sube"<"T">"sube"<"⟘">"`
La théorie `A` est plus riche que la théorie `B` si et seulement si `A=>B`. Et dans ce cas nous avons :
`"⟘" => A => B => "⟙"`
`"<⟙>" sube"<"B">"sube"<"A">"sube"<"⟘">"`
Les 8 ensembles suivants sont à considérer :
affirmées par `A`
réfutées par `A`
décidables par `A`
non démontrables par `A`
de négation non démontrables par `A``"<"⟘">"-("<"A">"+"¬<"A">")`
indécidables par `A`
Considérons les 4 ensembles `"<"⟘">"`, `"<"⟙">"`, `"<"⟘">"^("-"1)`, `"<"⟙">"^("-"1)`. Deux d'entre-eux sont égaux à `ccL` et si la relation de déduction est cohérente, les deux autres sont disjoints.
Ces ensembles vont partitionner `ccL` en 3 parties disjointes :
Ensemble des tautologies Énumérable Ensemble des antilogies Énumérable Ensemble des indécidables Peut-être non énumérable
Et il y a 3 façons de les réunir deux à deux :
Ensemble des propositions décidables Énumérable Ensemble des propositions indémontrables
Peut-être non énumérable Ensemble des propositions de fausseté indémontrable Peut-être non énumérable