Question naïve sur fondements ensemblistes

Je vais contredire Poirot (gentiment).

Je mets des lettres pour numéroter afin d'utiliser tes numéros sans changer tes questions.

a/ Tout d'abord, lambda-calcul et théorie des ensembles c'est LA MEME CHOSE. Il s'agit d'une réécriture mot à mot de $\{x\mid \dots \}$ en $x\mapsto (\dots)$.

b/ L'invention du signe $\in$ vient juste pour 3 choses:

c1/ l'espace se voit mal dans les textes, donc au lieu de $E\ x$, écrire $E\ni x$, puis finalement $x\in E$ est apparu plus "assumé".

c2/ La volonté très probable que garder un statut privilégié à la notion de phrase. Un texte a dû apparaitre (légitimement) comme risqué dès lors que ses suites de signes autonomisées n'étaient pas des phrases.

c3/ L'extensionalité: si $a\neq b$, il "se doit" d'exister $c$ tel que $(ac)\neq (bc)$ et non pas seulement $c$ tel que $(ca)\neq (cb)$

d/ Bref, tout ça a conduit la science à remplacer $x\mapsto (blabla)$ par $\{x\mid blabla\}$, ainsi que l'évaluation pour deux phrases $P,Q$ "qui aurait normalement due être notée" $(P=Q)$ par $(P\iff Q)$.

e/ Comme tu vois, c'est rudimentaire et syntaxique.

f/ Donc la réponse à ta question1 est clairement non. Et la raison n'a rien de profonde, elle est due aux contraintes matérielles de langage lors des enregistrements des découvertes scientifiques dans les archives de l'académie des sciences.

g/ Ensuite vient ce qu'on pourrait appeler "le fond". Là, il ne faut pas s'y tromper, il s'agit de physique et le fond de l'univers mathématique est un monde "platonicien" peu accessible aux sens, mais supposé exister par 90% des communautaires.

h/ Comme le mot "math" est une abréviation de "recherche de certitudes absolues" (appelés théorèmes) et le mot science de "recherche de "bonnes" certitudes", il ya le problème du passage de la preuve écrite formellement à la garantie qui s'applique dans le monde (physique pour les physiciens, mathématique pour les platoniciens des maths), garantie qui devra affronter la NATURE (qu'elle soit physique pour le monde matériel, ou "athéo-divine" pour le monde platonicien).

j/ Du coup, tu as tout un aspect de "recherche de consistance". On sait depuis Godel que ça n'a pas de sens et depuis la révolution quantique que ça n'en a doublement pas. La consistance est le fait pour une théorie qu'il n'existe pas de preuve de toute phrase.

k/ Le statut lui-même de phrase est venue poser un problème (léger avec Godel, énooooormissime avec la théorie quantique)

m/ Tu es là devant une tout autre affaire. Là encore, la syntaxe reste invariable. il y a de gros efforts (et de gros progrès) qui ont été faits pour ne rien toucher d'autre que la structure dans laquelle évoluent les valeurs des phrases (qui n'est pas forcément $\{vrai; faux\}$). Ces progrès ont été spectaculaires en ce qui concerne le forcing (nom donné à ce principe quand on garde quand-même une algèbre de Boole)

n/ Ne pas confondre avec les probas et tout ce qui y ressemble. Lorsqu'on change la structure de ce qu'on considère comme une phrase, il reste absolument essentiel que les connecteurs soient des images réciproques d'opérations de la structure elle-même. Ce que ne font pas (mais alors pas du tout) les probas.

p/ La réponse à ta question2 est donc "un non nuancé".

q/ L'axiome du choix est puissant dans le cadre uniquement EXTENSIONNEL. Sinon, il est conservatif (on ne peut rien prouver de plus avec un axiome du choix non extensionnel qu'on rajouterait à part les phrases avec des symboles primitifs qui ont servi à le rajouter).

r/ Donc la réponse à ta question3 est là aussi un "non" nuancé.

s/ Concernant l'axiome du choix, et le tiers exclus, ils sont EQUIVALENTS dès lors qu'on regarde le problème "en amont", ie sans tenir compte des bridages artificiels pour tenter de garder des théories consistantes.

Les catégories: elles n'ont rien à voir avec le schmilblick: elles sont un outil qui permet d'unifier des théorèmes de niveau M1,M2 d'algèbre (et un peu d'analyse), ou de booster certaines approches algébriques. C'est unifiant, mais à l'évidence rien à voir avec un côté fondateur (même si une campagne publicitaire, hélas, la politique envahit tout, voudrait tenter de faire un hold up sur ce mot)

Y a-t-il un espoir pour qu'elles soient utiles un jour (en termes fondatoriels)?

La réponse est assez simple: cela dépend de la possibilité ou pas d'associativiser la science. Pour l'instant, rien n'indique que ce soit possible. Qu'entends-je par "associativiser"?

Et bien c'est simple: l'opération $\circ$ est associative alors que $Ap$ ne l'est pas, ie il arrive que :

$$ (a(b))c \neq a(b(c))$$

alors que tu as toujours :

$$ f\circ (g\circ h) = (f\circ g)\circ h $$

Concernant le premier, tu peux aussi penser à $[(a\in b)\in c ] \neq [a\in (b\in c)]$

Tu peux facilement au prix d'un ajout unaire** qui fait passer de $A$ à $1 \to A$ et de $1 \to A$ à $A$ définir $Ap$ (ou $\in$ si tu préfères, ce qui revient au même). Mais rien n'indique que cet ajout soit un petit saut plutôt qu'un grand saut.

En caml par exemple, définir let a() = blabla te permet de REPORTER l'exécution de blabla, alors que si tu définis let a=blabla, l'évaluation de blabla se produit de suite.

De même (aux axiomes non logiques, clonage et jets d'hypothèses près), tous les théorèmes de maths s'obtiennent par modus ponens à partir de :

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

qui est l'incarnation de $\circ$.
MAIS ON A BESOIN DE

$$A\to (1\to A); (1\to A)\to A$$

Autrement dit, le deuxième jeu d'axiomes logiques représente assez bien la difficulté de "tout voir avec une opération associative".

** En notant $K(a)$ la fonction $x\mapsto a$, tu définis :

$$ [a(b) = c] := [K(c) = (a\circ K(b))]$$