CCH et "réalisations logiques"

A la suite d'une demande reçue par MP, j'ouvre un fil pour donner quelques précisions sur les analogies que j'insère parfois dans mes réponses, comme au lien suivant: (à mettre à l'édit)

1.0) Une spécialité de recherche récente (elle a moins de 30ans) est la correspondance de Curry-Howard: elle dit que toute preuve (de science) est un programme (au sens informatique du terme), et moi, personnellement, j'ajoute que tout programme est une preuve (c'est moins souvent signalé à cause des boucles, mais je peux le prouver).

1.1) Ces choses sont développées dans les cours de lambda-calcul (mais ça va beaucoup plus loin évidemment, le LC n'est qu'une "implémentation concrète" du phénomène qui est robuste et ne concerne d'ailleurs pas que "les programmes informatiques", mais tous les trucs de la vie. Les preuves donnent des stratégies automatisables et réciproquement. On peut consulter la page internet de JEAN LOUIS KRIVINE (je préciserai dans les posts ultérieurs sur quels documents cliquer)

2.0) Soit $E$ un ensemble, muni d'un ordre (préférablement complet, mais ce n'est pas une obligation) et d'une application que je note $\to $ qui va de $E^2$ dans $E$, avec un élément neutre à gauche que je note $1$, ie il vérifie $\forall x: (1\to x)=x$. On suppose en outre que $\to$ est croissante à droite et décroissante à gauche et qu'elle est pseudo-commutative, ie $a\to (b\to c)=b\to (a\to c)$ pour tous $a,b,c$. Dernière chose supposée: $a\leq b$ ssi $1\leq (a\to b)$. Théorème: tous les théorèmes de la logique linéaire sont $\geq 1$, tous les éléments jetables sont $\leq 1$ (un élément $x$ est jetable quand $\forall y: y\leq (x\to y)$). Il y a 4 conditions dans la définition, mais elles sont toutes très naturelles, et on peut à bon droit considérer ce genre de structure comme une implémentation de ce qu'on entend par "valeurs de phrases". On y prouve que la borne inférieure des $[a\to (b\to x)]\to x$ quand $x$ parcourt $E$, quand on la note $a\otimes b$, qu'elle est adjointe à $\to$ en ce sens que $\forall a,b,c: [(a\to (b\to c))=((a\otimes b)\to c)]$

2.1) A noter que les théorèmes des autres logiques s'obtiennent aussi très facilement, puisque ce ne sont que les conséquences des axiomes desdites logiques. Par exemple la borne inférieure $LI$ des $x\to (x\otimes x)$ et des $x\to (y\to x)$ quand $x,y$ parcourent $E$ définit la logique intuitionniste (les théorèmes de la logique intuitionniste sont les éléments$\geq LI$, etc

3.0) Un peu d'habitude est on s'aperçoit vite qu'on trouve ce genre de structure partout dans les maths. L'ordre est souvent l'inclusion et la recherche "d'éléments canoniques" équivaut très exactement à la recherche de preuves d'énoncés. Par exemple, si vous écrivez une expression avec des lettres et le signe "=>", il revient très exactement au même d'en cherche une preuve (en logique linéaire) de l'expression vue comme forme propositionnelle ou plutôt de s'imaginer que les lettres désignent des espaces vectoriels et que A=>B désigne $L(A,B)$, et qu'on cherche un vecteur non nul appartenant à l'expression.

3.1) Un autre exemple est celui des anneaux, pour lesquels j'ai publié une classification sur HAL. Les valeurs sont les idéaux et si $J,K$ sont des idéaux, l'idéal J implique K est l'idéal $\{x\in A\mid \forall y\in J: xy\in K\}$. J'ai même appelé "logique annelée" l'ensemble des expressions dont la valeur est l'anneau tout entier quelque soit les valeurs qu'on a attribué aux lettres et quel que soit l'anneau commutatif. Et, par exemple, la logique annelée est strictement comprise entre la logique affine et la logique classique, mais elle est incomparable avec la logique intuitionniste car elle contient un théorème non prouvable en logique intuitionniste qui est Buveur=>TiersExclus. ***

3.2) On a aussi les théorèmes suivants: la logique annelée des anneaux de Von Neumann (tout élément est multiple de son carré) est exactement celle des anneaux qui réalisent la logique intuitionniste et pour ce qui est de la logique classique, un anneau la réalise ssi il est un produit fini de corps.

A suivre, à la faveur des questions techniques et autres. Une manière propre de fonder toutes les maths avec 4 signes et proprement, sans variable, est donnée par la logique dite combinatoire, qui peut servir de mot-clé (c'est un équivalent du lambda-calcul sans utiliser de variables). Je rappelle que le lambda-calcul consiste juste à remplacer ensemble par fonction (ça ne change rien) et à se placer dans la théorie des ensembles originelle (celle qui a provoqué la crise des fondements parce qu'elle est contradictoire), à savoir que toute collection est un ensemble (en LC, toute fonction "intuitive" est une fonction "brute de pomme").

*** Buveur := $\forall R\exists x\forall y: [Rx\to Ry]$ et TiersExclus:= $\forall X: non(non(X))\to X$ où $non(X)$ abrège $\forall Y:[X\to Y]$