Teoria degli insiemi classici e esistenza di almeno un set

Question

Come studente di matematica, accettavo l'argomento secondo cui l'esistenza del set vuoto seguiva dallo schema di comprensione assioma, fintanto che potremmo dimostrare l'esistenza di almeno un set: se a è qualsiasi set, quindi possiamo derivare l'esistenza di {x:a | bot }. Direi quindi di usare l'assioma dell'infinito che è stata stabilita l'esistenza di almeno un set.

Avere una deriva verso la logica e l'informatica, ora mi sembra che l'esistenza di almeno un set possa essere derivata semplicemente dal sistema deduttivo utilizzato, senza un ulteriore assioma teorico di set.

Questo è leggermente deludente per me, poiché mi sarebbe piaciuto l'esistenza di almeno un set per essere una conseguenza degli assiomi teorici impostati, non una conseguenza logica di un sistema deduttivo. Naturalmente, ci sono molti ragionevoli sistemi deduttivi di logica del primo ordine che potremmo considerare, e può darsi che io stia guardando quello sbagliato, che motiva la mia domanda.

Spero che qualcuno conferma che l'esistenza di almeno un set sia effettivamente una conseguenza logica (non una conseguenza teorica impostata), o spiegare i difetti nel prossimo ragionamento o indicare un sistema deduttivo in cui la dichiarazione non regge.

Per precisare il sistema deduttivo che ho in mente, consideriamo il linguaggio in cui le proposizioni primitive sono della forma x in y (dove x e ysdraiarsi in una serie adeguatamente ampia di variabili) e bot, e abbiamo un'implicazione -> così come la quantificazione Ax per ogni variabile x. Questa lingua può essere rappresentata dal tipo di Haskell:

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

o per coloro che preferiscono 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
.

Non c'è nient'altro nella lingua (nessuna costante, nessuna uguaglianza). Sebbene la matematica ordinaria di solito implichi una lingua molto più ricca, la speranza è che tutto possa essere desugardo in termini di questo linguaggio di base.

Ora il sistema deduttivo che ho in mente è un sistema in stile Hilbert con 5 Schema Axiom e 2 regole di inferenza (modus ponens e generalizzazione).

(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)

Date le nostre regole di inferenza, possiamo formalmente rappresentare le nostre prove come alberi di derivazione o specificamente come tipo di dati induttivi di Haskell:

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

E abbiamo in particolare una mappa eval :: Proof v -> Expr v che funge da una sorta di controllo del tipo, restituendo la proposizione (il tipo) effettivamente dimostrato dalla prova (l'espressione). Ora ovviamente, non tutte le prove sono valide (ad esempio la prova Axiom p non è un'invocazione assioma valida se non p è davvero un assioma) nel qual caso il eval La funzione può semplicemente tornare bot -> bot Il che è un modo conveniente per affermare che una prova non valida non dimostra nulla. Quando si implementa la funzione eval (che equivale a precisare il nostro sistema deduttivo), dovremo bisogno isAxiom :: Expr v -> Bool così come Hyp :: Proof v -> [Expr v] (che restituisce l'elenco delle ipotesi coinvolte in una prova). La funzione Hyp è utile decidere se la prova Generalize x P è valido, controllandolo x non è gratuito in nessuna delle proposizioni di Hyp P. Una prova P = ModusPonens P1 P2 non è valido se non eval P2 è della forma eval P1 -> p in quale caso eval P = p.

Avendo descritto le nostre prove, possiamo definire il sequente G |- p come equivalente all'esistenza di una prova P tale che eval P = p e Hyp P <= G (dove il <= IS IS SET inclusi e gli elenchi sono visualizzati come set)

Ok, quindi in questa fase abbiamo una struttura ragionevole di un sistema deduttivo ragionevole per la logica del primo ordine e la teoria dei set. Ora se p è una proposta senza alcuna variabile libera quindi Ax.p e p sono dimostrabilmente equivalenti per qualsiasi variabile x (Ax.p -> p è un assioma, mentre p -> Ax.p non è difficile da dimostrare) e se consideriamo la dichiarazione di esistenza Ex.(bot -> bot) come zucchero sintattico per ~Ax.~(bot->bot) dove ~p è zucchero sintattico per p -> bot, quindi l'esistenza di almeno un set è equivalente a [Ax.((bot -> bot) -> bot)] -> bot che è equivalente a ((bot -> bot) -> bot)-> bot che è esso stesso dimostrabile. Quindi l'esistenza di almeno un set è una conseguenza logica, non teorica.

Tornando allo schema Axiom di comprensione, abbiamo:

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

dove si capisce che p <-> q è zucchero sintattico per (p -> q) /\ (q -> p) mentre p /\ q è zucchero sintattico per ~ (~p \/ ~q) e p \/ q è zucchero sintattico per ~p -> q. Da Eb.Ax[x in b <-> bot] Non ha variabili gratuite, è equivalente a (*) e quindi abbiamo il teorema: Eb.Ax[~ x in b], cioè siamo in grado di dimostrare l'esistenza del set vuoto esclusivamente dallo schema dell'assioma di comprensione e nient'altro (oltre la logica).