Annonce aux shtameurs

@Foys, tout à fait, mais par contre il faut que je précise que mon (enfin mes, car c'est une sorte de famille hétéroclyte) théorème va exactement à l'opposé d'éliminer des coupures. Il en rajoute :-D jusqu'à l'indigestion.

Je rappelle ce qu'est une coupure et pourquoi les enlever permet mal d'afficher l'évidence.

Un coupure c'est en gros dû au modus ponens. (C'est un poil plus subtil, mais je ne vais pas noyer le fil dans ça). Quand vous cherchez "quel bon A" mettre pour prouver B en prouvant A, puis A=>B, vous avez l'embarras du choix. Embarras très concret qui a abouti au théorème de Godel, ce n'est pas rien.

Du coup j'ai inventé un "truc pour parler aux gens" de ça. Les vrais bons raisonnements sans coupures se font comme suit:

De A=>B déjà prouvé et X=>Y déjà prouvé, vous pouvez dire "j'ai prouvé (B=>X)=>(A=>Y)". C'est très naturel et permet de suivre les branchement. Sauf que pour que ce soit fidèle et ne vous prouve pas de théorèmes, il "faut" ajouter une règle qui dit (1=>A) = A, qui est assez profonde.

Vous pouvez alors faire des modus ponens, puisque de A=>B et de A, vous pouvez déduire (A=>A)=>B, mais vous restez gêné par l'hypothèse, certes inoffensive, A=>A.

Les théorèmes d'élimination des coupures disent tous à peu près qu'on peut s'en sortir sans rien rajouter et que les A=>A qui trainent sont des punitions pour avoir coupé. Autrement dit, pas besoin d'une règle qui permet de passer de (A=>A)=>B à B car on peut obtenir les mêmes choses en s'en passant et c'est prouvé. Mais comme dit foys, les contours peuvent obliger à écrire une preuve beaucoup plus longue, qui n'a d'ailleurs guère d'intérêt dans ce que je racontais, puisque je le redis, mon truc à moi part exactement dans l'autre sens, à savoir qui si vous aviez oublié de couper, ma procédure rajoute des coupures à votre place :-D

Cela dit, on aura quand-même le même phénomène de rallongement des preuves (à l'évidence). Sauf qu'en gros, avec mon truc, vous aurez votre théorème P qui sera un cas particulier de A=>A avec A très longue, alors que dans les preuves sans coupures, vous aurez le même théorème P à l'aide d'une très très longue conjonction de $x\ti x$ où $x$ parcourt l'ensemble des toutes petites lettres de rien du tout. Les deux démarches sont différentes.

- Disons qu'une preuve sans coupure ne vous donnera pas "d'évidence" qui généralise le théorème, mais juste une prevue qui se concentrera plus sur l'exécution des noeuds magiques (les duplications) , etc, lors des exécutions de la garantie.

- Mes trucs donne à qui aurait une vue d'avion une "vision immédiate" que le théorème est un truisme, par contre, il ne faut pas oublier que l'exécution de la garantie que A=>A peut être très longue, puisque pour vérifier (A=>B)=>(A'=>B') (les primes ne comptent pas***), il faut vérifier A'=>A et B=>B' et ça peut boucler.

***
je le réécris sans:
puisque pour vérifier (A=>B)=>(A=>B) (les primes ne comptent pas***), il faut vérifier A=>A et B=>B et ça peut boucler.

Voici le lien: http://www.les-mathematiques.net/phorum/read.php?16,2159824,2159824#msg-2159824