Règles et axiomes des maths

Bon, je ne sais plus où je l'ai dit, mais j'ai oublié de préciser un truc.

Dans un post récent, j'ai raconté qu'ayant A=>B et B=>C, c'était mieux de remarquer que ça nous donnait ((A=>B)=>B)=>C, plutôt que dire que ça nous donne A=>C.

Je précise donc pourquoi.

Un habitant de $A\to C$ est une application de $A$ dans $C$. Si vous n'en déduisez que ça, à l'heure du traçage et de l'écologie, vous perdez que vous aviez en fait bien plus, puisque une habitant de $((A\to \to \to C$ qui contient BIEN PLUS que les éléments de $A$ (traduits par les application triviales $(f\mapsto f(x)$) puisque contient aussi des éléments "complètement échevelés" $\phi$ de $(A\to \to B$ qui ne proviennent pas d'un élément de $a$, ie qui ne sont éventuellement pas cohérents et même s'ils le sont, ne sont pas de la forme $\forall f\in (A\to : \phi(f)=f(a)$ pour un certain $a\in A$.

Or dans l'intrication complexe des preuves, il est dommage de partie en jetant "ce qu'on avait pourtant" au départ et qu'on n'a pas gaspillé

Ah non SURTOUT PAS DE MODUS PONENS. Je dis pourquoi:

1/ On déplace des pointeurs.

2/ Qui te dit que tu ne vas pas avoir les pointeurs suivants: $748\to 78$ pour $A\to B$ et $313132$ pour AUSSI $A$. Le modus ponens exigerait de vérifier que $748 == 313132$

C'est la raison pour laquelle j'ai cantonné ce principe à UNE UNIQUE PLACE DEDIEE qui est la règle 5. On le fait, mais on l'assume.

Remarque : ce ne sera pas trop grave s'il n'y avait pas les duplications (clonage d'hypothèses), donc a priori, par les déplacement les pointeurs changent peu. Mais au delà de la logique affine, c'est le vrai boxon dans les copies de contenus (copie par valeur et non par nom)

Pour les applications de ma remarque que tu évoques, c'est mon slogan "tout théorème est cas particulier d'évidence" qui regroupe ça et ça a plus de 10ans je crois maintenant. Je me suis servi de ces mécanismes pour chercher toujours et encore des nouvelles versions au point que dans le métro il y a quelques années, durant les trajets je tricotais de têtes des nouvelles versions et finalement, je ne pourrais même plus dire laquelle me plait le plus. Disons qu'il faudra un jour que je publie un HAL avec quelques unes.

Mais au sens où tu l'espères peut-être je ne crois pas avoir vraiment beaucoup d'applications que j'aurais enregistrées. C'est vraiment philosophique. J'avais une version "ensembliste" où on voyait que plus on s'autorise à monter moins on avait besoin d'étapes (monter au sens, passer de $A$ à $B^A$, puis à $C^{B^A}$), mais j'ai oublié l'énoncé rigoureux et ça a été pas mal vu par d'autres lors des études de la consistance de AS, donc "assez classiquement".

Mais je n'oublie pas que ça t'intéresse et je posterai si des éléments me reviennent.

Quelques remarques:

je garde le paradigme ci-dessus, c'est à dire un ensemble ordonné doté de 2 opérations croissantes à gauche comme à droite, commutatives et associatives$+,-$ tel que $\forall x,y,z: $

$$ x+(y-z) \leq (x+y)-z$$

et d'une involution décroissante, que je noterai $x\mapsto x'$, pour économiser de l'encre.

Je mets ça dans le cadre plus général des maths.

1/ On peut supposer que l'ordre de $E$ est complet, il a donc un plus petit élément et un plus grand élément.

2/ On peut supposer qu'il a un élément neutre pour chaque opération $0$ pour $+$ et $1$ pour $-$, donc on voit que les notations auront toujours un côté inhabituelle, malgré mes choix pour les opérations, il y a un problème avec les éléments neutres.

3/ La complétude entraine les deux autres opérations naturelles "inf, sup".

Je donne l'état de l'art.

4/ On ne suppose pas que $1$ est le plus grand élément.

L'ensemble des expressions $\geq 1$ (appelé ensemble des théorèmes linéaires) est PSPACE-complet

L'ensemble des expressions $\geq 1$ qui ne contiennent que les symboles $+$ et $-$, mais pas $inf$ et $sup$ est NP-complet

Scoop rigolo: L'ensemble des expressions $\geq 1$ qui ne contiennent que les symboles $+$ et $-$, mais pas $inf$ et $sup$, et qui n'utilisent qu'une seule lettre est NP-complet (informé par Alesha récemment)

5/ On suppose que $1$ est le plus grand élément.

L'ensemble des expressions $\geq 1$ (appelé ensemble des théorèmes affines) est NP-complet (preuve très facile)

Je pense que c'est PSPACE-complet avec inf, sup, mais je ne sais plus par coeur

6/ Je reviens sur un enseignement amusant de ça:

$x'-y$, c'est donc $x\to y$ (noté $x\multimap y$ dans le domaine professionnel, mais je n'utiliserai pas cette notation).

Il y a une manière TRES SIMPLE de retenir la seule règle non triviale: au lieu de se dire que $(x'-y) +z \leq x'-(y+z)$, on se dit que:

$$ (x\to y) + z \geq x\to (y+z) $$

ce qui est une évidence intuitive parfaite mais surtout LA SEULE PRIMITIVE des maths, et je la trouve assez fascinante. Au fond la seule chose qu'on fait c'est d'affaiblir légèrement d'une situation où on dispose d'une garantie de $x\to y$ ainsi que d'une garantie de $z$, on passe à la situation où on ne dispose plus que d'une garantie de $x\to (y+z)$, autrement dit on a perdu la possibilité de consommer $z$ sans avoir payé $x$.

$x\mapsto x'$ ne doit pas être conçu comme la négation habituelle mais comme une simple permutation de joueurs. C'est pourquoi elle est inoffensive et involutive.

Les grosses logiques*** usines à gaz (classique, intuitionniste) sont des productions platoniciennes gratuites dans lesquelles on se permet de suppose autant qu'on veut des $(x+y)\to x$ (autrement dit des $x-x'-y'$), ça encore ce n'est pas trop grave, mais aussi des $x\to (x+x)$, et là c'est du lourd à cause, quand on va considérer les quantificateurs, du fait que $\forall xR(x)$ utilisé une seule fois c'est vraiment rien à côté d'une utilisation multiple.

*** mais l'avantage est qu'elles se définissent de façon très simples à partir de ce qui précède.

Les "exponentielles":

L'ordre étant complet, face à $x$ on peut considérer le plus petit ensemble contenant $1,x$ et stable par $y\mapsto y+y$ et prendre sa borne inférieure qu'on note $x^\infty$, qui vérifie
$x^\infty\leq x$ et
$x^\infty\leq 1$ et
$x^\infty\leq x^\infty+x^\infty$.

Le mot exponentielle vient de ce que $(inf(x,y))^\infty \leq (x^\infty)+(y^\infty)$ (ça se voit mieux en renotant $+:=inf; \times :=+$)

Je ne recommande pas leur utilisation, elles sont un luxe qui ne semble permis que par la complétude de l'ordre, elle-même en conflit avec la notion de liberté (au sens de groupe libre), et on peut le prouver puisque qu'avec un point fixe comme :

$$ a = !(a\to Tout) $$

on obtient $card(E)=1$


Bref, s'il y a une chose à retenir en termes de slogans:

Toutes les maths sont basées sur le fait que

((A=>B) et C) implique (A=>(B et C))

avec une involution inoffensive vérifiant la contraposée dans les deux sens, ie

A=>B implique B'=>A'

A'=>B' => B=>A

Le reste étant l'affirmation d'axiomes audacieux.

Je l'illustre avec des => et des primes:



A + (B=>C) est majoré par
A + (C'=>B') qui est majoré par
C'=>(A + B') qui est majoré par
(A + B')' =>C qui est majoré par
(A' $-$ =>C qui vaut

(A=>B)=>C

Et comprendre ça est un truc énorme car on a "le libre-arbitre" quand on dispose de $A$ et de $(X-Y)$ de passer

plutôt à $(A+X)-Y$
ou plutôt à $X-(A+Y)$

qui n'est plus du tout gommé par l'AUTRE libre-arbitre qui donne le choix entre convertir inf(A,B) en A ou le convertir en B.

A chaque fois j'oublie!! :-X

1/ J'ai répété 1000 fois qu'il y a un théorème qui dit "tout théorème est un cas particulier d'évidence". Et dans la foulée j'oublie un autre théorème, je répare ce matin.

2/ En fait, on peut prouver la chose suivante: tout être vivant qui verrait "en live" en terme de ressentis, l'égalité suivante:

$$ \forall a,b,c : [(a\to (b\to c))=(b\to (a\to c))] $$

considèrerait tout théorème comme évident, ie pourrait dire immédiatement face à n'importe quel proposition si c'est ou pas un théorème, et ce sans se tromper.

Alors, évidemment, chacun dira que personne n'a ces ressentis. Je réponds certes. Mais je signale tout de même qu'en implémentant, pour tous entiers naturels $a,b$ :

$$ (a\to b) := f(a) \times b$$

sur les nombres entiers naturels où $f(a)$ est le a ième nombre premier, on a "naturellement" mis "en dur" cette égalité. Ce qui conduit à :

"n'importe qui "ayant dans les tripes instinctives" où sont les nombres premiers et le calcul de $f$ reconnait immédiatement les théorèmes (qui coincide pour lui avec les évidences"

:-D Je n'ai vraiment pas fait exprès ici de vanter les qualités des arithméticiens, c'est purement factuel et je suis nul en arithmétique pour info :-D

Je vais trier, mais le faire sur plusieurs posts. Pour l'instant, j'importe des phrases qui me paraissent importantes, et je te donne des réponses succinctes. Il y aura un petit désordre. Je numérote quand-même.

1/

foys a écrit:

Les vérités scientifiques sont par nature éternelles, utilisables si l'on veut et reproductibles autant que l'on veut, leur étude ne relève pas des outils d'appréhension des ressources limitées et des déchets non jetables

1.1/ Les "vérités", peut-être, mais elles parlent de "non-vérités" en leur intérieur (sous-formule), mettent devant des $\forall$, etc. Une "vérité" scientifique qui parle d'objets polymorphes et changeant, que l'on va prouver en plein d'étapes qui vont questionner ces objets, il n'y a pas besoin de photo pour voir que ça n'a rien de naturel de parier sur $\forall X: X\to 2X$ à chaque étape.

1.2/ C'est très exactement ce que la logique intuitionniste refuse: les vérités éternelles pour les "grands machins scientifiques". C'est l'opposé, elle n'accorde le statut de clonabilité qu'aux énoncés se trouvant à gauche du =>, autement dit aux hypothèses contingentes. C'est donc rigolo ta déclaration, quand on la met en face de la démarche intuitionniste. Et surtout quand c'est fait dans un contexte temporel proche où tu "défendais subitement" les catégories qui ont beaucoup plus tendance elles-mêmes à défendre l'intuitionnisme.

1.3/ Il n'y a pas d'évidence à pouvoir cloner des objets éternels.

2/ Je lance les détails en donnant des précisions pluss en français que dans les posts précédents:

2.1/ En sciences, en maths, on a 4 "droits". Ils consistent TOUS sauf un (le droit 2.4) à JETER une richesse par la fenètre. Je les liste:

2.2/ Droit de permuter des hypothèses. C'est une "non-règle" puisqu'en fait elle vient palier à notre obligation d'écrire en ligne. Mais la réalité des énoncés est un graphe où les fils d'un sommet ne sont pas ordonnés.

2.3/ Droit de jeter franchement une hypothèse, de ne pas l'utiliser.

2.4/ Droit de CLONER une ressource (autrement dit, on fait une hypothèse une fois et on l'utilise plusieurs fois)

2.5/ Droit de sous-localiser une ressource

J'ai mis exprès un ordre très différent de d'habitude, je redonne les axiomes, sous une forme un peu différente, qui vont avec ces droits:

A2.3 : A=>(B=>A). Son utilisation jettera B à la poubelle.

A2.4 : A=>(A+A). Comme le signe $+$ n'est pas documenté par mes soins, je vous donne la formule légèrement plus lourde qui exprime la même chose en pratique: A=>([A=>(B=>C)] => C)

A2.5 : c'est le plus subtil des droits, car les gens "n'ont pas conscience" de "perdre quelque chose". Elle se réalise en 3 axiomes que je liste, mais qui sont évidemment redondants.

A2.5.1/ (A + (B=>C)) => [(A=>B)=>C]

A2.5.2/ (A + (B=>C)) =>

A2.5.3/ [(A=>B) + (U=>V)] => [(B=>U)=>(A=>V)]

Je ne détaillerai pas leur redondance.

2.6/ A noter qu'ils sont tous irréversibles

2.7/ A noter qu'on ne peut pas "emprunter, puis rembourser" des forces à cette anture logique là. En effet, vous empruntez A, vous le clonez, ça vous donne A+A, vous remboursez un A et il vous en reste un. A partir de rien vous avez gagné A.

2.8/ Pour les gens gênés par le signe $+$ il est définissable par :

$$ (A+B) := inf_X\ [(A\to (B\to X))\to X] $$

où l'ordre veut dire $(X\leq Y) := [Y$ est un cas particulier de $X]$

et vérifie $[A\to (B\to C)] = [(A+B)\to C]$

2.9/ Il faut remarquer une chose: on ne retrouve pas l'ordre à cause du côté "en amont" de ces choses-là. On ne sait pas si $NP=PSPACE$. Il suit qu'il y a deux natures possibles de choix dont on ignore si elles sont "de même nature". Elles le sont ssi $NP=PSPACE$. J'explicite ces choix:

TypeDeChoix1: vous disposez de [(A=>B) + (U=>V)]. Vous pouvez "dégrader" AU CHOIX en :

(B=>U)=>(A=>V) ou bien
(V=>A)=>(U=>B)

et bien une fois votre choix fait (dans le jeu), vous ne pouvez pas revenir en arrière. Il n'est pas considéré comme mobilisant une poubelle, il n'y a pas de "déchet" à jeter comme dans A2.3.

TypeDeChoix2: vous disposez de $inf(A,B)$. Vous avez le choix entre :

l'utiliser comme $A$ ou bien
l'utiliser comme $B$.

On ne sait pas (à ma connaissance) si le deuxième est strictement plus fort que le premier "en pratique". Ce sont juste deux utilisations du libre-arbitre différentes, dont l'une permet l'autre. J'explicite:

on ne sait pas vraiment (du moins, moi, je ne sais pas) si on rajoute vraiment quelque chose de fort en prétendant que:

$\forall A,B\exists X,Y,U,V: ( $

$[(inf(A,B)=[(X\to Y)+(U\to V)])$ et
$(A=[(Y\to U)\to (X\to V)]) $ et
$ (B=[(V\to X)\to (U\to Y)]) ]$

$)$


2.10/ Sans le clonage, toutes les maths sont calculables au sens que vous disposez d'un algorithme qui vous dit si un énoncé est ou n'est pas un théorème. Cela tient bêtement au fait qu'une preuve a "par avance" une longueur limitée, puisque chaque étape va consommer une ressource ou permuter sans rallonger ou raccourcir des configurations.

A SUIVRE.

Bien sûr qu'il en existe. Mais on n'irait pas loin, la quasi-totalité des preuves rédigées actuellement clonent alors même que dans une partie des cas ce n'est même pas nécessaire. Avec un tel stop, tu bloquerais tous les processus.

Par ailleurs, on fait même infiniment mieux : on sait EXACTEMENT où on clone quand on traduit la preuve en terme (en programme si tu préfères), puisqu'il s'agit juste de la présence d'un combinateur appelé $W$ qui agit comme suit:

$$ \forall x,y: W(x)(y) := x(y)(y)$$

et on peut très bien ne pas l'exécuter (je me suis amusé plein de fois à le faire.

Tu obtiens alors un théorème épouvantable précédé par des dizaines d'hypothèses de la forme $(A\to (A\to )\to (A\to $ qui sont illisibles.

En fait, on peut faire mieux (je ne'ai toujours pas terminé l'article, mais je l'avais commencé pour alesha) : ne jamais utiliser $W$, donc ne jamais rien cloner et ainsi toutes les preuves terminent. SAUF QUE : on utilise un très grand nombre de fois l'axiome d'extensionalité. Autement dit, on passe d'une preuve où on a cloné à une preuve où on a répété à en dégueuler partout un appel à la main invisible en grattant la lampe d'Aladin.

L'axiome d'extensionalité permet de déduire les axiomes puissants en "Foy-ssisant" l'argument platonicien que j'ai cité. A chaque fois tu dis: "ô vérité scientifique éternelle et immuable, montre ta pérénité et reproduis ta garantie"

On va dire qu'à l'époque actuelle, c'est mieux de ne pas faire de publicité à cette démarche, même si elle renvoie le clonage, l'axiome du choix et le tiers-exclus à des conséquences de l'axiome d'extensionalité.

(L'axiome d'extensionalité dit que quand on demande à $a$ s'il contient $b$, ce $a$ est capable de "passer outre" la FORME sous laquelle on lui présente $b$ et de ne répondre qu'en fonction des réponses que $b$ lui-même fournirait quand on lui demande s'il contient $c,d,e,etc$. Autrement dit il "lit dans les pensées" de $b$ avant de répondre et ne fournit une réponse qu'en fonction de qui est $b$ et non pas de comment on l'évoque). Son énoncé formel est $\forall a,b:$

De toute faàon, dans ce domaine, je ne pense pas que les recherches "soient terminées". On les aura terminées quand on aura classé quel est "l'atome" indivisible de pensée qui va chercher les réponses à l'infini.

Actuellement bien sûr on sait qu'il y a $W$. Mais les autres trucs génèrent du NP-complet à minima, quand ce n'est pas du PSPACE-complet. C'est encore un peu fouillis.

Bon, on sait tout de même mettre les choses "sur une ligne", ie identifier le X tel que on attend la réponse de $X^n$ sans contrôler $n$ (c'est ça que j'appelle "aller chercher la réponse à l'infini")