Intuitionnisme

Je ne me souviens plus exactement: Ageron, c'est le bouquin soigné avec les théorèmes d'Hartog, et compagnie?

Le problème, généralement, pour obtenir des "oeuvres" intuitionnistes c'est qu'on enlève l'axiome non non A implique A, mais on n'en rajoute pas.

Toutes les preuves classiques (de P) sont donc des preuves intuitionnistes de (conjonction de (nonnonA implique A) implique P) ce qui fait des théories intuitionnistes des théories qui disent à peu près les mêmes choses que les théories classiques (je caricature!), en ce qu'elles expriment autant de choses.

Les résultats "négatifs" (du genre "on ne connait pas de preuves intuitionnistes de..." ou même "on peut prouver qu'il n'y a pas de preuves intuitionnistes de..." sont "galère" et difficiles à établir, en général

Du coup, je crois que ce que tu demandes, tu le trouverais dans des vieux ouvrages du début du siècle. Quand on a compris ce qu'était "l'intuitionnisme" (correspondance de Curry Howard, théorème de Statman, complétude, élimination des coupures, etc), on s'est "détourné" des "théories intuitionnistes" proprement dites pour étudier les systèmes déductifs dans leur intégralité.

En effet, l'idée même de "théorie" va plutôt avec la logique classique. ie, quand on enlève des axiomes (non logiques) c'est pour en rajouter d'autres. Avec les affaiblissements logiques (enlever des axiomes logiques) c'est tout l'édifice qui s'ébranle, et la déontologie veut que, plutôt que parler d'axiomes, on parle de système déductif tout entier.

Donc, today, tu devrais chercher un livre qui précise de A à Z dans son chapitre1 pas seulement les axiomes, mais aussi les règles d'inférence, et la "géométrie" des preuves (comment on les présente, sur quel "papier", selon quelle structure)!

Ageron (si je me gourre pas sur le livre que tu évoques FIXE l'intuitionnisme comme système d'arrière plan (mais n'est pas toujours très clair dessus), et se contente de préciser quand il use de l'absurde.

Cela dit, je crois qu'il y a un livre qui te plairait beaucoup. Hélas, je ne me rappelle plus l'auteur.

Par contre son titre doit être "géométrie simplectique" ou un truc dans le genre. En gros, dans son livre, (je l'ai parcouru vite fait) toutes les applications sont localement affines, il suppose l'existence d'un réel e tel que e×e=0, dérive en divisant bêtement f(x+e)-f(x) par e, (et généralise l'idée aux développements limités) et c'est parti pour 150-200 pages. Je crois qu'il torche la (une remixée) formule de Stokes en 5 lignes, sans problème.

Avec ces infos peut-être trouveras-tu ton bonheur...