Morse-Kelley vs cardinaux mondains

Martial, juste un point de vocabulaire (c'est le seul aspect que je me sente en situation de pouvoir commenter ..). Je pense qu'une meilleure traduction de "worldly" serait "mondiaux", non ?

Thierry POMA a écrit:

L'on a donc obtenu le théorème global du choix. C'est juste une esquisse de preuve.

C'est ainsi que le fameux axiome du choix est pleinement un théorème à part entière : sur tout ensemble E, il existe une fonction de choix.

Contrairement à une idée reçue répandue, le "théorème de choix" n'est pas juste une conséquence de l'emploi du tau bourbakiste mais provient du schéma d'axiomes qu'ils ont utilisé à la place des classiques schémas de remplacement et compréhension de ZF habituel (le formalisme à base de $\tau$ contient des formules qui ne sont équivalentes à aucune formule du premier ordre classique).

En fait on peut montrer que la logique du premier ordre avec symbole tau est une extension conservative de la logique du premier ordre tout court.

Il y a des preuves syntaxiques de ça qui sont des usines à gaz (car il faut tenir compte de la façon dont les divers tau sont imbriqués les uns dans les autres. cf le livre de Leisenring de 1969 ou bien l'article de Maehara sur l'élimination des coupures. Une recherche avec votre moteur préféré sur les "premier et deuxième théorèmes epsilon de Hilbert" devrait donner des résultats).

L'argument sémantique est par contre facile (on l'esquisse ci-dessous: les gens qui livrent des preuves syntaxiques de ce que la skolémization marche font exactement la même chose, et franchement ils pourraient parler de l'outil à tout faire général i.e. tau à la place).
Soit $\mathcal L$ un langage du 1er ordre dénombrable (ceux de la vraie vie le sont...).
Soit $B$ une formule (du premier ordre, sans $\tau$) et $(A_d)_{d\in \N}$ une liste de formules sur $\mathcal L$ (sans $\tau$) telles que $B$ n'est pas conséquence prouvable de $(A_d)_{d \in \N}$.
Soit (Lowenheim-Skolem) $M$ un modèle dénombrable de $\neg B, (A_d)_{d\in \N} $. Soient $(m_n)_{n\in \N}$ les éléments du domaine de $M$.
L'interprétation des formules construites avec $\tau$ se fait par induction immédiate et comme d'habitude (et on interprète $\tau_x (P)$ par $P[x:=m_k]$ où $k=0$ s'il n'existe aucun $i$ tel que $M \vDash P[x:=i]$, sinon on prend le plus petit entier $k$ tel que $M \vDash P[x:=m_k]$).
On voit qu'alors toute formule écrite sans $\tau$ a la même valeur de vérité dans $M$ avec cette nouvelle interprétation qu'avec l'interprétation usuelle, de plus toutes les formules de la forme suivante sont également validées:
$Q[x:=t] \Rightarrow Q[x:= \tau_x Q]$
$(\forall x(R \Leftrightarrow S)) \Rightarrow (\tau_y R = \tau_y S)$ (quand $=$ fait partie du langage)
$s = t \Rightarrow P[z:=s] \Rightarrow P[z:=t]$ (il suffit que $=$ soit interprétée comme une relation d'équivalence et que l'interprétation de chaque symbole de base du langage soit compatible avec ça, mais c'est le cas si la théorie de base est supposée égalitaire), de plus pour toute formules $A,B$, $M\vDash (A \Rightarrow $ si et seulement si, si $M\vDash A$ alors $M \vDash B$; on peut donc récupérer tous les syllogismes usuels, et toute conséquence Bourbaki-prouvable de $(A_d)_{d\in \N}$ est validée par $M$, au contraire de $B$.

Bonjour Foys

J'espère que tu vas bien. Voudrais-tu me donner un lien pour le fameux article de Maehara sur l'élimination des coupures, s'il te plait ? Aurais-tu également un exemplaire du livre de Leisenring ? Si tel est le cas, l'on pourra peut-être voir ce que l'on peut faire.

Bien cordialement,

Thierry

British* (pas Britney :-D)

Cela ne viendrait-il pas de ce que $V_{\kappa+1}=\mathfrak{P}\left(V_{\kappa}\right)$ est un modèle prévu pour $\text{MK}$, pour $\kappa$ cardinal inaccessible et $V_{\kappa}\models\text{ZFC}$ ? Comment espérer alors que $V_{\kappa}$ soit un modèle pour $\text{MK}$, pour $\kappa$ cardinal mondain, y compris $1$-mondain ?

Je me pose seulement des questions face à ce que je viens de lire.

@Martial : je ne savais pas que le Cantor's Attic avait disparu, mais il doit en rester des versions sur des sites qui archivent les pages internet comme Wayback Machine.

@Martial : tu trouveras une légère description de ZFC2 ici. Mais peut-être le savais-tu, vu que tu en dresses un portrait dans ton message. La quantification - par exemple $(\forall\,f)$ - aurait pu être plus précise, en utilisant les sortes.

Cf. également ceci.