Pensez à lire la Charte avant de poster !

$\newcommand{\K}{\mathbf K}$


Les-Mathematiques.net - Cours de mathématiques supérieures
 Les-Mathematiques.net - Cours de mathématiques universitaires - Forum - Cours à télécharger

A lire
Deug/Prépa
Licence
Agrégation
A télécharger
Télécharger
191 personne(s) sur le site en ce moment
E. Cartan
A lire
Articles
Math/Infos
Récréation
A télécharger
Télécharger
Théorème de Cantor-Bernstein
Théo. Sylow
Théo. Ascoli
Théo. Baire
Loi forte grd nbre
Nains magiques
 
 
 
 
 

Règles et axiomes des maths

Envoyé par christophe c 
Règles et axiomes des maths
il y a quatre mois
Ce fil n'a rien de "gros", c'est juste que je mets dans cette rubrique ces informations pour les référencer car ça me prend moins de temps que de chercher mes anciens fil.

Les deux seuls connecteurs primitifs sont

$\to$, l'implication
$\forall$.

J'utiliserai $\vdash$, qui ne sera ici qu'un symbole pratique d'abréviation comme suit :

$$A\to (B\vdash C) = A;B \vdash C$$

éventuellement même si liste vide, ie $A\to B=A\vdash B$.

Par exemple $A\to (B\to C) = A\to (B\vdash C) = A;B\vdash C$

Les règles:

0/ Les transformations dues au $\vdash$ sont autorisées

1/ Permuter: la point-virgule est associative et commutative.

2/ Axiomes gratuits: $X\to X$ ainsi que les $(\forall xR(x)) \to R($ ce que vous voulez$)$

3/ Ayant produit $Liste_1\vdash A$ et $B\to C$, vous avez le droit de rajouter à vos productions la phrase :

$$ Liste_1\vdash (A\to B) \to C$$

4/ Si vous avez produit $Liste\vdash R(x)$ et que $x$ n'est pas évoqué dans $Liste$, vous pouvez déduire $Liste\vdash \forall xR(x)$

5/ Si vous avez produit $(A\to A)\to B$, vous pouvez rajouter $B$ à vos productions.


Attention: ce sont les règles de base. Un théorème classique de maths $P$ est tel qu'il existe une liste $L$ composée uniquement d'énoncés de la forme (***) vérifiant $L\vdash P$. Et réciproquement évidemment.

Axiome AUDACIEUX, mais admis:

Poubelle: A\to (B\to A)
Clonage: (A\to (A\to B))\to (A\to B)
RP absurde + symétrisation: $[(A\to \perp)\to \perp]\to A$

en notant $\perp :=(\forall X: X)$

Vous pouvez définir les autres connecteurs comme suit:

$A$ et $B$ est défini comme étant $\forall X[(A\to [B\to X])\to X]$

$A$ ou $B$ est défini comme étant $\forall X: [(A\to X)\to ((B\to X)\to X)]$

$\exists x\in A: R(x)$ est défini comme étant $\forall X: [(\forall y\in A: [R(y)\to X])\to X]$

$u=v$ est défini comme étant $\forall X: u\in X\to v\in X$


Les théorèmes d'éliminations des coupures racontent essentiellement que l'autorisation numéro 5 est inutile, elle ne rajoute pas de théorèmes.

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Règles et axiomes des maths
il y a trois mois
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 B)\to B)\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 B)\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 B): \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é

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Règles et axiomes des maths
il y a trois mois
Je réagis à ton dernier message.
Je ne m'étais jamais rendu compte de ça effectivement - il faut néanmoins garder un modus ponens pour que ça soit intéressant, non ?

Tu as des "applications" de cette remarque ? (je te laisse décider ce que veut dire "application")

"Mathematics, rightly viewed, possesses not only truth, but supreme beauty"-Russell
Re: Règles et axiomes des maths
il y a trois mois
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.

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Règles et axiomes des maths
il y a trois mois
Spécifiquement pour Max, je signale la découverte de Girard et cie des années 80. Je te refais les notations pour que ce soit digeste.

Après moult réflexion, il s'est aperçu que "la clé" des déductions (non réductible jusqu'à ce jour) était une règle assez marrante :

De $a$ et $(b-c)$ déduire $(a+b)-c$. Alors attention, ce ne sont pas les opérations habituelles. Je te donne des définitions complètes :

$E$ est un coolspace quand il est ordonné et doté de 2 applications $+$ et $-$ de $E^2$ dans $E$ toutes deux commutatives et associatives vérifiant, pour tous $x,y..$ :

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

On peut ajouter une application involutive décroissante appelée "no", telle que $no(x+y)=((no(x))-(no(y)))$

Le truc est complètement symétrique, si tu regardes bien la règle.



Le reste est un peu auperflu en fait, dans l'étude de toute ça.

En quoi, son invention (enfin découverte) est bien?
Si tu conçois $$a\to b$ comme $(no(a))-b$, tu es d'un coup toutes les règles naturelles qui étaient plusieurs avant:

$a + (b\to c)$ pouvait aussi bien te donner $(a\to b)\to c$ que te donner $b\to (a+c)$.

Et bien là, une seule règle. Idem en ce qui concerne la contraposée: $a\to b$, c'est $no(a) - b$ alors que $no(b)\to no(a)$ c'est $b-no(a)$

C'est très économique et permet de se concentrer sur l'essentiel.

Et au cas où tu oublierais cette unique règle, je te donne le moyen mnémotechnique:

Avec $a$ + $u\to v$, on voit bien que j'ai un peu plus qu'avec $u\to (a+v)$, puisque dans le deuxième cas, je dois acheter d'abord $u$ pour recevoir $a$ (ainsi que $v$) en retour alors que dans le premier, le $a$ je l'ai d'office.

L'activité mathématique consiste à trouver les $expression1\leq expression2$ qui sont prouvables avec cette unique règle. C'est hélas "encore" NP-complet, mais y a du progrès.

En outre, tout théorème est toujours cas particulier d'une évidence de manière absolument non inflationniste: X est cas particulier de Y ssi on obtient X en remplaçant parfois dans Y des lettres différentes par des lettres égales.

Or "il se trouve" que toute théorème dans lequel chaque lettre figure exactement 2 fois une en occurrence positive et l'autre négative est évident.

Ces mécanismes marchent aussi pour la logique affine. Après évidemment, pour cause de clonage, ça ne marche plus de la même façon car cloner est un axiome pur et dur au même titre que l'extensionalité. Dans les deux cas, c'est supposer l'immuabilité et l'éternité des vérités mathématiques et ça coute cher évidemment en axiome.

Pour info, les vraies notations sont

$\otimes$ à la place de $+$

et un machin qui s'appelle "par" je ne sais pas le faire en latex pour le $-$

la borne inf s'appelle "avec" (idem, je ne sais pas faire le symbole en latex)

la borne sup s'appelle $\oplus$.

C'est appelé "logique linéaire" car il y a égalité entre ensemble expressions représentant des espaces vectoriels où vit un objet canonique et théorèmes linéaires.

le "no" est le $\perp$ (ou le $^*$ quand besoin), le $\oplus$ le produit simple (ou la somme) et le $\otimes$ le produit tensoriel. Evidemment, l'involutivité du $no$, c'est exclusif à la dimension finie, mais ici il n'y a pas du tout de dimension infinie, c'est propositionnel. Il y a des limites à cette "isomorphie" informelle qui est qu'en algèbre linéaire ces opérations sont réelles et non sur "des expressions". Mais je te sais capable de comprendre.

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Règles et axiomes des maths
il y a trois mois
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' $-$ B) =>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.

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Règles et axiomes des maths
il y a trois mois
Précision : dans le libre-arbitre quej'évoque ci-dessus, je veux bien insister qu'on ne sait pas les distinguer "psychologiquement", mais qu'on a une distinction mathématique pour l'heure très clair:

1/ Dans le cas des choix itérés entre a-(x+b) et (x+a)-b, on reste dans la logique linéaire dite multiplicative qui est NP-complète seulement (et en plus d'une manière assez exotique, puisque l'ensemble de ses théorèmes maximaux est P (ce sont les évidences) et qu'on obtient tous les autres par des remplacement de couples $(x,y)$ par des couples $(z,z)$.

2/ Dans le cas des choix itérés entre passer de inf(a,b) à a et passer de inf(a,b) à b, on peut prouver que c'est PSPACE-complet.

3/ Or on ne sait pas actuellement si PSPACE = NP (loin s'en faut!! Un énoncé comme PSPACE = NP est quasi la même chose que P+NP, il ne rapporte juste pas 1000000 dollars)

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Règles et axiomes des maths
il y a trois mois
A chaque fois j'oublie!! angry smiley

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"

grinning smiley 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 grinning smiley

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Règles et axiomes des maths
il y a deux mois
Je développerai ici des réponses détaillées aux posts de Foys dans d'autres fils où je mettrai un lien qui redirigent vers le présent post et les suivants. En effet, une classification un peu longue est nécessaire pour éviter les flous et ça encombrerait les fils initiaux.

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Règles et axiomes des maths
il y a deux mois
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/

Citation
foys
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)) => [B=>(A+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.

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Règles et axiomes des maths
il y a deux mois
avatar
Bonjour.

Juste une petite demande de clarification : si le clonage est la seule opération qui pose problème, pourquoi n'existe-t-il pas d'algorithme (c'est ce que j'entends souvent) qui puisse reconnaître cette configuration et 'arrêter' la preuve ?

Désolé si ma question est à côté de la plaque.

Cherche livres & objets du domaine mathématique : intégraphes, règles log & engins [électro]méca ou analog
Re: Règles et axiomes des maths
il y a deux mois
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 B))\to (A\to B)$ 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:$

$a(b)$ ne dépend que de $x\mapsto (b(x))$


Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Règles et axiomes des maths
il y a deux mois
avatar
Merci pour l'éclairage.

C'est quand même rageant ces explosions déclaratives.
Re: Règles et axiomes des maths
il y a deux mois
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")

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Seuls les utilisateurs enregistrés peuvent poster des messages dans ce forum.

Cliquer ici pour vous connecter

Liste des forums - Statistiques du forum

Total
Discussions: 149 229, Messages: 1 507 001, Utilisateurs: 27 661.
Notre dernier utilisateur inscrit ibra.


Ce forum
Discussions: 2 517, Messages: 51 078.

 

 
©Emmanuel Vieillard Baron 01-01-2001
Adresse Mail:

Inscription
Désinscription

Actuellement 16057 abonnés
Qu'est-ce que c'est ?
Taper le mot à rechercher

Mode d'emploi
En vrac

Faites connaître Les-Mathematiques.net à un ami
Curiosités
Participer
Latex et autres....
Collaborateurs
Forum

Nous contacter

Le vote Linux

WWW IMS
Cut the knot
Mac Tutor History...
Number, constant,...
Plouffe's inverter
The Prime page