Les mathématiques sont les sciences exactes, c'est à dire que chacune de leur déduction est vérifiable par un procédé calculatoire parfaitement défini et ne laissant rien au hasard. Donc, étant donné un langage logique énumérable `ccL`, et étant donnée une théorie énumérable de la démonstration, il existe un programme (dit le grand énumérateur) qui énumère toutes les déductions exprimables dans ce langage logique.
Le système de démonstration se compose d'un ensemble de propositions appartenant à `ccL`, appelées axiomes et qui forment un stock initial de propositions, et d'un ensemble de règles de production permettant de produire à partir du stock d'autres propositions qui seront alors ajoutées au stock.
Le langage logique `ccL` que nous utilisons est classique, c'est à dire que chaque proposition possède une valeur de vérité `0` ou `1`, et les connecteurs logiques utilisés sont booléens. Vous rermarquerais entre autre que la négation y est totale. Nous avons pour toute proposition `P` du langage la propriété suivante :
`¬¬P <=> P`
où le connecteur de négation `¬` a une priorité syntaxique plus forte que celle du connecteur d'équivalence `<=>`. Cette piorité syntaxique permet de réduire le nombre de parenthèses.
Le connecteur d'équivalence `<=>` relie les propositions de même valeurs de vérité, et le connecteur de négation `¬` inverse la valeur de vérité.
La première transformation du langage logique `ccL` que nous mettrons en oeuvre, consistera à y incorporer le connecteur unaire de déduction `"⊢"`. Cela se fera sans avoir à préciser quoique ce soit d'autre puisque ce connecteur est par principe déjà défini complètement mécaniquement par le système de démonstration. Quelque soit une proposition `P` du langage `ccL` nous avons en effet soit `"⊢"P`, ou soit `"¬"("⊢"P)` que l'on note `"⊬"P`. La proposition `"⊢"P` signifie qu'on peut démontrer `P`. La proposition `"⊬"P` signifie qu'on ne peut pas démontrer `P`. Et ces expressions `"⊢"P`, `"⊬"P` possèdent assurement une valeur de vérité `0` ou `1`. Il suffit d'énumérer toutes les déductions possibles à l'aide du grand énumérateur, et si `P` est produit au bout d'un temps fini, nous avons `"⊢"P`, sinon nous avons l'oracle `"⊬"P`, qui est qualifié d'oracle car il faut se placer à la fin des temps pour en être sûr, l'énumération étant infinie.
Ainsi nous pouvons ajouter le connecteur "⊢" au langage `ccL`. Cela produit un langage étendu noté `ccL["⊢"]`. Mais rien ne nous assure qu'il existe dans la théorie de la démonstration des règles de raisonnement s'appliquant à des propositions utilisant ce connecteur de déduction. On va donc ajouter des règles de ce genre. Et on commence par l'identité : Quelque soit une proposition `P` appartenant à `ccL["⊢"]`, si on a la proposition `P` dans notre stoque alors on peut produire la proposition `"⊢"P`, et réciproquement si on a la proposition `"⊢"P` dans notre stoque alors on peut produire la proposition `P`.
modus ponens : Si `"⊢"A` et si `"⊢"(A=>B)` alors `"⊢"B`.
Par contre le connecteur unaire de déduction `"⊢"` que nous voulons ajouter au langage n'est pas un connecteur booléen. Dans le cas ou la théorie de démonstration est complète, ce connecteur de déduction est alors booléen et est identique au connecteur identité :
`("⊢"P)<=>P`
`("⊬"P)<=> "¬"P`
Mais lorsque la théorie de démonstration est incomplète, c'est à dire lorqu'il existe des propositions `P` du langage `ccL` telle que nous n'ayons ni `"⊢"P` ni `"⊢¬"P` c'est à dire telle que nous ayons `("⊬"P)" et "("⊬"P)`, alors le connecteur de déduction `"⊢"` n'est pas un connecteur booléen. Et il se peut qu'il existe des propositions `P` du langage telle que :
`¬ (("⊬""⊬"P) <=> P)`.
L'évaluateur logique
L'évaluateur prélogique
---- 17 septembre 2018 ----
.Par convention, la valeur logique d'une expression est par défaut égale à `1`. Autrement dit, ce qui est affirmé, est affirmé être vrai. L'expression logique `P` signifie exactement l'expression logique `P"="1`.
De même en prélogique, la valeur prélogique d'une expression est par défaut égale à `1`. Autrement dit, ce qui est affirmé, est affirmé être démontrable. L'expression prélogique `P` signifie exactement l'expression prélogique `P "=" 1`, et donc que l'on peut démontrer `P`.
Et qu'est-ce qui permet de dire qu'une expression est logique ou prélogique ? C'est son connecteur racine. Si c'est un connecteur logique alors l'expression est logique. Si c'est un connecteur prélogique alors l'expression est prélogique.
L'expression logique à une valeur logique parmis `{0,1}`.
L'expression prélogique à une valeur prélogique parmis `{0,1,oo}`.
Par exemple que signifie l'expression suivante ? :
`("⊢"P)=>("⊢"Q)`
Le connecteur racine `=>` est un connecteur logique donc c'est une expression logique. Elle possède donc une valeur logique `0` ou `1`. Les sous-expressions `"⊢"P` , `"⊢"Q` sont prélogiques et sont donc interprétées comme ayant une valeur prélogique égale à `1`. L'expression logique est donc équivalente à :
`("⊢"P = 1) => ("⊢"Q=1)`
Et cette expression possède assurement une valeur de vérité `0` ou `1`. Il suffit d'énumérer toutes les déductions possibles à l'aide du grand énumérateur, et les valeurs de vérités de `("⊢"P = 1)` et de `("⊢"Q=1)` seront tranchées parmis `{0,1}` même s'il faut pour cela attendre un temps infini, l'énumération étant infini.
C'est pour cette raison que les expressions de la forme `("⊢"P = 1)` sont des expressions logiques, et que les expressions de la forme `"⊢"P` ne sont pas des expressions logiques mais des expressions prélogiques.
---- 17 septembre 2018 ----
Les mathématiques sont une science exacte, c'est à dire que chacune de leur déduction est vérifiable par un procédé calculatoire parfaitement défini et ne laissant rien au hasard. Donc, étant donné un langage logique énumérable `ccL`, et étant donnée une théorie de la démonstration énumérable, il existe un programme (dit le grand énumérateur) qui énumère toutes les déductions exprimables dans ce langage logique.
La première opération sur le langage logique que nous faisons, consiste à incorporer dans le langage logique le connecteur spécial, appelé connecteur prélogique de déduction `"⊢"`, qui est une application de `ccL -> {0,1,oo}`. Cela se fait sans avoir à préciser quoique ce soit d'autre puisque le connecteur prélogique de déduction `"⊢"` est par principe déjà défini complètement mécaniquement par le système de démonstration. Quelque soit une proposition `P` du langage `ccL` nous avons 3 alternatives possibles, exhaustives et exclusives :
Les connecteurs logiques sont bivalents. Ils peuvent prendre `2` valeurs possibles `1` ou `0` qui signifient respectivement vrai ou faux. Cela est un choix sémantique que nous faisons. C'est le choix de la logique classique.
Par contre, les connecteurs prélogiques sont trivalents. Ils peuvent prendre trois valeurs possibles `1` ou `0` ou `oo`, qui signifient respectivement accepté ou refusé ou indéterminé. Accepté signifie démontrable, Refusé signifie de négation démontrable. Indéterminé signifie que ni l'affirmation ni la négation ne sont démontrables.
Par convention, la valeur logique d'une expression est par défaut égale à `1`. Autrement dit, ce qui est affirmé, est affirmé être vrai. L'expression logique `P` signifie exactement l'expression logique `P"="1`.
De même en prélogique, la valeur prélogique d'une expression est par défaut égale à `1`. Autrement dit, ce qui est affirmé, est affirmé être démontrable. L'expression prélogique `P` signifie exactement l'expression prélogique `P "=" 1`, et donc que l'on peut démontrer `P`.
Et qu'est-ce qui permet de dire qu'une expression est logique ou prélogique ? C'est son connecteur racine. Si c'est un connecteur logique alors l'expression est logique. Si c'est un connecteur prélogique alors l'expression est prélogique.
L'expression logique à une valeur logique parmis `{0,1}`.
L'expression prélogique à une valeur prélogique parmis `{0,1,oo}`.
Par exemple que signifie l'expression suivante ? :
`("⊢"P)=>("⊢"Q)`
Le connecteur racine `=>` est un connecteur logique donc c'est une expression logique. Elle possède donc une valeur logique `0` ou `1`. Les sous-expressions `"⊢"P` , `"⊢"Q` sont prélogiques et sont donc interprétées comme ayant une valeur prélogique égale à `1`. L'expression logique est donc équivalente à :
`("⊢"P = 1) => ("⊢"Q=1)`
Et cette expression possède assurement une valeur de vérité `0` ou `1`. Il suffit d'énumérer toutes les déductions possibles à l'aide du grand énumérateur, et les valeurs de vérités de `("⊢"P = 1)` et de `("⊢"Q=1)` seront tranchées parmis `{0,1}` même s'il faut pour cela attendre un temps infini, l'énumération étant infini.
C'est pour cette raison que les expressions de la forme `("⊢"P = 1)` sont des expressions logiques, et que les expressions de la forme `"⊢"P` ne sont pas des expressions logiques mais des expressions prélogiques.
on garde la signification par défaut le la valeur logique 1 dans les expressions. C'est à dire ce qui est affirmé est affirmé être démontrable. L'expression prélogique `ccQ` signifie exactement l'expression logique `ccQ = 1`
Et cette trivalence est ramenée à une bivalence `0` ou `1` en complétant le connecteur par une égalité avec une de ces 3 valeurs possibles :
(|--P)=0 qui se note
(|--P)=1 qui se note |--P
(|--P)=oo qui se note P?
¡P signifie
Et donc il existe une machine de Turing, `zeta`, appelée l'évaluateur, qui semi-décide les propositions démontrables du langage `ccL`. C'est à dire que, étant donné une proposition `P in ccL`, nous avons toujours les trois alternatives suivantes :
Et on note ces trois alternatives respectivement comme suit `|--"¬"P`, `|--P`, `P?`, à l'aide des connecteurs prélogiques `|--`, `?`.
Et on note ces trois alternatives respectivement comme suit `color(red)("¬")P`, `P`, `¡P`, à l'aide des connecteurs prélogiques `color(red)("¬")`, `¡`, dont certain sont notés en rouge pour les distinguer des connecteurs logiques. En effet la négation prélogique ainsi définie n'est pas la négation logique.
`"¬"P` est l'hypothèse que `P` est faux, tandis que `color(red)("¬")P` signifie que l'on ne peut démonter P
Ainsi nous pouvons avoir le shéma d'axiome logique du tiers exclu `¬P" ou "P` et à la fois le shéma d'axiome prélogique de l'incomplétude `color(red)("¬")P color(red)(" ou ")Pcolor(red)(" ou ")¡P` dans une théorie cohérente.
Etant donné un langage logique de présentation suivante :
`"<"a,b,f"(.)",g"(.,.)>", "=(.,.)", E"(.)", R"(.,.)"`
où le prédicat d'égalité `"=(.,.)"` joue ce rôle particulier qu'est l'égalité entre élément.
On définie la prélogique à partir du langage logique et de l'évaluateur `zeta`. La prélogique possède ses propres connecteurs prélogiques ici écrits en rouge `color(red)(¬, "et", "ou", => , <=>)`, et qui ont une signification différente des connecteurs logiques `¬, "et", "ou", => , <=>`.
---- 16 septembre 2018 ----
La négation prélogique d'une proposition logique `P` signifie que l'on ne peut pas démontrer `P` et donc que la fonction `zeta` appliquée à `P` produit soit `0` ou bien se lance dans un calcul sans fin `oo`.
`color(red)("¬")P` signifie `"⊬"P`
`Acolor(red)("=>")B` signifie `"⊢"(A=>B)`
`color(red)("¬")color(red)("¬")P` signifie `"⊬"("⊬"P)`
à partir de ces deux connecteurs prélogiques, on définie les autres connecteurs
`Acolor(red)(" ou ")B` signifie `("⊢"A)" ou "("⊢"B)`
`Acolor(red)(" et ")B` signifie `("⊢"A)" et "("⊢"B)` et donc signifie `"⊢"(A" et "B)`
`Acolor(red)("=>")B` signifie `"⊢"(A=>B)`
Comparons l'expression `Acolor(red)("=>")B` et l'expression `color(red)("¬")Acolor(red)(" ou ")B`
Les règles de démonstration s'étendent et s'appliquent aussi aux proposition prélogiques. Ce faisant La négation prélogique d'une proposition logique `P` signifie que l'on ne peut pas démontrer `P` et donc que la fonction zeta appliqué à `P` produit soit `0` ou bien se lance dans un calcul sans fin `oo`.
Et en particulier le connecteur `color(red)(=>)` correspond au connecteur de démontrabilité `|--`. Par exemple, les 4 propositions prélogiques suivantes signifient la même chose :
`Acolor(red)(=>)B`
`A|--B`
`|--(A=>B)`
`zeta(A=>B) = 1`
D'autre part :
`color(red)("¬")P = "¬"P " ou " ¡P`
`color(red)("¬")"¬"P = P " ou " ¡P`
`color(red)("¬")¡P = P" ou ¬"P`
La correspondance entre programme et preuve permet de donner un sens cohérent aux connecteurs logiques appliqués aux propositions prélogiques. Les connecteurs logiques sont des programmes calculant une valeur logique en fonction des valeurs logiques des propositions prélogiques passées en argument. Ainsi nous avons :
|
|
|
Cette définition nous permet par exemple de donner un sens exacte à la proposition prélogique suivante :
`(A|--B) => C`
Elle signifie que
qui est assurement non booléenne à cause de l'incomplétude inhérente des théories finis comprenant l'arithmétique,
La calculabilité se définie formellement par rapport à un langage.
Etant donné un langage d'opérateurs tel que par exemple `L="<"a,b,f"(.)",g"(.,.)>"`, l'ensemble des termes exprimables dans ce langage s'appelle le domaine de Herbrand `L`. Un élément `x` est dit calculable si et seulement si il existe un terme de ce langage qui lui est égale, autrement dit si et seulement si il appartient à ce langage, `x in L`
Etant donné par exemple le langage logique de présentation suivante :
`"<"a,b,f"(.)",g"(.,.)>", "=(.,.)", A"(.)", R"(.,.)"`
Ces opérateurs et prédicats sont posés comme étant totalement calculables.
Un élément `x` est dit calculable si et seulement si `x in "<"a,b,f"(.)",g"(.,.)>"`
Un opérateur `h(.)` est dit totalement calculable si et seulement si il existe un programme écrit dans ce langage logique qui prend en entré un élément quelconque `x` du domaine de Herbrand, et produit en un temps fini, un terme du domaine de Herbarnd qui est égale à `h(x)`. Notez que la calculabilité totale de `h` ainsi définie est en fait la caculabilité totale de `h` restreint au domaine de Herbrand, et dont l'image doit nécessairement être inclus dans le domaine de Herbrand.
Puis on introduit la notion de calculabilité (non nécessairement totale) en formalisant le calcul sans fin par le meta-symbole de l'infini de Turing, `color(red)(oo)`.
`h(x, color(red)(oo),y,z) = color(red)(oo)`
`"¬" color(red)(oo) = color(red)(oo)`
`( color(red)(oo) " ou " 1) = 1`
`( color(red)(oo) " ou " 0) = color(red)(oo)`
`( color(red)(oo) " et " 1) = color(red)(oo)`
`( color(red)(oo) " et " 0) = 0`
Mais attention, le méta-langage ainsi défini constitue un langage logique avec ses propres meta-connecteurs logiques `color(red)(¬, "et", "ou", => , <=>)`, qui ont une signification différente des connecteurs logiques `¬, "et", "ou", => , <=>`.
Une proposition `P` possède la valeur logique `oo` si et seulement si on ne peut pas démonter ni `P` ni `"¬"P`, et on note cet état par l'expression `¡P`. Délors, deux éléments `x,y` peuvent être soit égaux, soit distincts, ou soit indiscernables. Ils sont indiscernables lorsque la proposition `x=y` possède la valeur logique `oo`.
{x,y} indiscernables <=> ¡(x=y)
--- 16 septembre 2018 ---
Remarquez que si on fait une interpretation plus étroite de `AAy"(.)"` comme signifiant « quelque soit un opérateur `y"(.)"` calculable », alors cette restriction fait que l'équivalence de Herbrand ne devient qu'une implication :
`EEx AAy, Q(x,y) => AAy"(.)" EEx, Q(x,y(x))`
Remarquez que si on fait une interpretation plus étroite de `EEy"(.)"` comme signifiant « il existe un opérateur `y"(.)"` calculable », alors cette restriction fait que l'équivalence de Skolem ne devient qu'une implication :
`AAx EEy, P(x,y) ⇐ EEy"(.)" AAx, P(x,y(x))`
Mais en logique, tout est exacte, tout est syntaxe, tout est formelle. Quelle est donc l'axiome qui permet d'affirmer l'existence de cet opérateur `y"(.)"` ? on répondra par une périssologie, c'est l'axiome qui permet justement de faire cela, c'est à dire qui permet de faire une infinité de choix en choisissant parmis plusieurs éléments distincts. C'est l'axiome du choix.
Cette axiome permet de faire une infinité de choix arbitraires, et de plus, ces choix peuvent ce faire parmis des éléments dont seul l'existence est affirmée et que l'on peut ne pas pouvoir désigner par des termes. Vous conviendrez que ce pouvoir est exhorbitant, qu'il n'est pas à la porté des simples mortels, et qu'il relève d'une croyance.
Les élémentariens plus terre-à-terre ont proposé une alternative plus modeste à cet axiome. Ils s'en sont tenue à ce qu'ils pouvaient potentiellement produire, à ce que l'homme pouvait potentiellement produire. Ils ont avançer le concept de calculabilité. Toute théorie produite par l'homme, issue d'une logique formelle et exacte est en effet le résultat d'un calcul faisable par une machine parfaite sans jeu et fonctionnant en mécanique classique. Ils ont donc jugé pertinent de se focaliser sur les seuls objects calculables. Dans les univers élémentariens, tous les éléments sont énumérés par un processus de calcul, tous les opérateurs et prédicats sont calculables. L'existence d'un élément satisfaisant un prédicat calculable fait l'objet d'un énumérateur calculable qui énumère les éléments satisfaisant ce prédicat. Mais la revue de tous les éléments nécessite un temp infini. C'est pourquoi les élémentariens s'autorisent à se placer à la fin des temps, ce qui constitue un second axiome litigieux, certe plus modeste que l'axiome du choix, mais dépassant encore la porté des simples mortels. Il existe donc encore une place pour une école encore plus rigide, ... qui considère que l'arithmétique est contradictoire mais dans un calcul qui ne peut pas être atteint dans notre univers trop petit pour cela. Puis en amont, la remise en cause de la mécanique classique, repose la question de ce qu'est la calculabilité et de ce qu'est un calcul exacte.
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.
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 :
`"⊢ est un ordre"` `"⊢ 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 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 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émontrable 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 description 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 pour ⊢"_E`
On remarque que la notion de vrai et de faux est relative à un ensemble de propositions. Une tautologie dans `L` est une tautologie dans toutes les restrictions de `L`, parcontre l'inverse n'est pas vrai. De même une antilogie dans `L` est une antilogie dans toutes les restrictions de `L`, et l'inverse n'est pas vrai.
Nous avons une relation de démontrabilité `"⊢"` reflexive, transitive et énumérable, et sa symétrisé `"↔"` qui constitue une relation d'équivalence. Et donc, la relation de démontrabilité `"⊢"` induit une relation d'ordre partiel sur `ccL"/↔"`. Et nous pouvons toujours ajouter une proposition minimale `⟘`, et une proposition maximale `⟙`.
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, et cette 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 minimal ⟙, 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)`.
En l'absence de proposition minimale, la règle se généralise en l'appliquant à toutes les restrictions possibles :
Autrement dit :
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">" = "<"⟙">"`
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