Théorie des ensembles classiques et existence d'au moins un ensemble

Question

En tant qu'étudiant en mathématiques, j'acceptais l'argument selon lequel l'existence de l'ensemble vide suivi du schéma axiome de compréhension, tant que nous pourrions prouver l'existence d'au moins un ensemble: si a est n'importe quel ensemble, alors nous pouvons dériver l'existence de {x:a | bot }. Je dirais ensuite en utilisant l'axiome de l'infini selon lequel l'existence d'au moins un ensemble a été établie.

Ayant dérivé vers la logique et l'informatique, il me semble maintenant que l'existence d'au moins un ensemble peut être dérivée simplement du système déductif utilisé, sans axiome théorique de l'ensemble supplémentaire.

Ceci est légèrement décevant pour moi, car j'aurais aimé l'existence d'au moins un ensemble comme une conséquence des axiomes théoriques définis, et non une conséquence logique d'un système déductif. Bien sûr, il existe de nombreux systèmes déductifs raisonnables de logique de premier ordre que nous pourrions considérer, et il se peut que je regarde le mauvais, ce qui motive ma question.

J'espère que quelqu'un confirmera que l'existence d'au moins un ensemble est en effet une conséquence logique (pas une conséquence théorique définie), ou expliquez les défauts du raisonnement à venir, ou indiquez un système déductif où la déclaration ne tient pas.

Afin d'épeler le système déductif que j'ai en tête, considérons le langage où sont les propositions primitives de la forme x in y (où x et yse trouvent dans un ensemble de variables convenablement large) et bot, et nous avons une implication -> ainsi que la quantification Ax Pour chaque variable x. Cette langue peut être représentée par le type Haskell:

data Expr v  = In v v
             | Bot 
             | Imply (Expr v) (Expr v)
             | Forall v (Expr v)

ou pour ceux qui préfèrent Coq:

Inductive Expr (v:Type) : Type :=
| In    : v -> v -> Expr v
| Bot   : Expr v
| Imply : Expr v -> Expr v -> Expr v
| Forall: v -> Expr v -> Expr v
.

Il n'y a rien d'autre dans la langue (pas constante, pas d'égalité). Bien que les mathématiques ordinaires impliquent généralement une langue beaucoup plus riche, l'espoir est que tout peut être désuguré en termes de cette langue de base.

Maintenant, le système déductif que j'ai en tête est un système de style Hilbert avec 5 schéma axiome et 2 règles d'inférence (modus ponens et généralisation).

(i)     p -> (q -> p)
(ii)    [p -> (q -> r)] -> [(p -> q) -> (p -> r)]
(iii)   [(p -> bot) -> bot] -> p                   (classical mathematics)
(iv)    [Ax.(p -> q)] -> (p -> Ax.q)   (x not free in p)
(v)     Ax.p -> p[y/x]                 (y free for x in p)

Compte tenu de nos règles d'inférence, nous pouvons représenter officiellement nos preuves comme des arbres de dérivation, ou spécifiquement comme le type de données inductives Haskell:

data Proof v  = Axiom (Expr v)
              | Hypothesis (Expr v)
              | ModusPonens (Proof v) (Proof v)
              | Generalize v (Proof v)

Et nous avons de manière cruciale une carte eval :: Proof v -> Expr v qui agit comme une sorte de vérificateur de type, renvoyant la proposition (le type) prouvé par la preuve (l'expression). Maintenant, bien sûr, toutes les preuves ne sont pas valables (par exemple la preuve Axiom p n'est pas une invocation axiome valide sauf si p est en effet un axiome) dans quel cas le eval La fonction peut simplement revenir bot -> bot Ce qui est un moyen pratique de dire qu'une preuve invalide ne prouve rien. Lors de l'implémentation de la fonction eval (ce qui équivaut à épeler notre système déductif), nous aurons besoin isAxiom :: Expr v -> Bool aussi bien que Hyp :: Proof v -> [Expr v] (qui renvoie la liste de l'hypothèse impliquée dans une preuve). La fonction Hyp est utile pour décider si la preuve Generalize x P est valide, en vérifiant que x n'est libre dans aucune des propositions de Hyp P. Une preuve P = ModusPonens P1 P2 n'est valide que sauf eval P2 est de la forme eval P1 -> p dans quel cas eval P = p.

Après avoir décrit nos preuves, nous pouvons définir le séquentiment G |- p comme équivalent à l'existence d'une preuve P tel que eval P = p et Hyp P <= G (où le <= L'inclusion définie et les listes sont affichées comme des ensembles)

OK, à ce stade, nous avons un aperçu raisonnable d'un système déductif raisonnable pour la logique du premier ordre et la théorie des ensembles. Maintenant si p est une proposition sans aucune variable libre alors Ax.p et p sont prouvés équivalents pour toute variable x (Ax.p -> p est un axiome, tandis que p -> Ax.p n'est pas difficile à prouver), et si nous considérons la déclaration d'existence Ex.(bot -> bot) comme sucre syntaxtique pour ~Ax.~(bot->bot) où ~p est du sucre syntaxtique pour p -> bot, alors l'existence d'au moins un ensemble est équivalent à [Ax.((bot -> bot) -> bot)] -> bot qui équivaut à ((bot -> bot) -> bot)-> bot qui est lui-même prouvable. Ainsi, l'existence d'au moins un ensemble est une conséquence logique, pas une conséquence théorique.

Pour en revenir au schéma axiome de compréhension, nous avons:

Aa.Eb.Ax[x in b <-> bot]     (*)

où il est compris que p <-> q est du sucre syntaxtique pour (p -> q) /\ (q -> p) tandis que p /\ q est du sucre syntaxtique pour ~ (~p \/ ~q) et p \/ q est du sucre syntaxtique pour ~p -> q. Depuis Eb.Ax[x in b <-> bot] n'a pas de variable libre, elle équivaut à (*) et nous avons donc le théorème: Eb.Ax[~ x in b], c'est-à-dire que nous sommes capables de prouver l'existence de l'ensemble vide uniquement à partir du schéma axiome de compréhension et rien d'autre (au-delà de la logique).