Discesa infinita e teoria degli insiemi formulata al primo ordine.

In alcuni testi ho letto che l'assioma di regolarità

$forall x ne emptyset -> exists y (y in x wedge not exists z (z in x wedge z in y))$

implica che non ci possono essere catene discendenti di insiemi del tipo

1) $x_1 in x_0, x_2 in x_1, x_3 in x_2, ...$

solo che secondo me le dimostrazioni riportate, al primo ordine non si possono usare.
Se c'è una catena discendente di insiemi in un modello della teoria formulata al primo ordine non è detto che ci sia anche l'insieme che li contiene.
Secondo me se si aggiungono un'infinità di costanti $x_0, x_1, x_2, ...$ alla teoria del primo ordine ZF e si aggiungono gli assiomi 1) la teoria non va banalmente in contraddizione anche se contiene l'assioma di regolarità.
Al primo ordine l'assioma di regolarità secondo me risulta incapace di eliminare i modelli degeneri in cui ci sono queste discese infinite, al più si può asserire che non può esistere l'insieme che contiene tutti e soli gli elementi che rappresentano una discesa infinita (perché in tal caso questo insieme avrebbe un elemento in comune con ognuno dei suoi elementi contraddicendo la regolarità), ma questa è una cosa ben diversa dall'affermare che una cosa del genere (discesa infinita) non è compatibile con un certo modello che verifica gli assiomi. Che debba esistere questo insieme qua gli assiomi non lo assicurano affatto.
Che una successione di costanti (o enti di un modello) è indiciata (per comodità) con dei numeri nella metateoria non equivale ad ammettere che c'è sicuramente una funzione tra $omega$ e gli elementi rappresentati da queste costanti nel modello stesso (o in ogni modello).

Qua c'è una dimostrazione di questo tipo (vedi "L'assioma di regolarità implica che non esiste nessuna successione infinita discendente di insiemi")

https://it.wikipedia.org/wiki/Assioma_d ... arit%C3%A0

ma ho trovato dimostrazioni analoghe anche in altri testi, queste dimostrazioni sono inutilizzabili se si usa una teoria formale e non intuitiva di questo tipo.
Che ne pensate?

Nella mia testa, l'assioma di regolarità serve ad assicurare che ogni insieme di ordinali che possiede una proprietà $P$ ammette un elemento minimo.

Detto questo, non ho capito molto bene cosa vuoi fare. L'infinità di costanti che hai aggiunto in (1) è esattamente (l'insieme dei valori del)la funzione che contraddice l'assioma di regolarità.

Detto questo, non ho capito molto bene cosa vuoi fare. L'infinità di costanti che hai aggiunto in (1) è esattamente (l'insieme dei valori del)la funzione che contraddice l'assioma di regolarità.

Perché aggiungere gli assiomi di cui ho parlato lo contraddice? E' questo il punto. Aggiungere infiniti assiomi con infinite costanti ad una teoria del primo ordine non equivale affatto ad aggiungere l'insieme che contiene tutti e soli i referenti di queste costanti.
Anche se asseriamo che esistono, per fare un esempio, $exists x (x = emptyset), exists x (x = {emptyset}), exists x (x = {emptyset, {emptyset}}), ...$ i termini presenti in questi assiomi formano una successione (in cui ogni insieme contiene i precedenti), ma anche se tutti queste asserzioni sono vere questa cosa da sola non implica affatto automaticamente che esiste l'insieme che li contiene tutti e soli (cosa che al primo ordine non si può esprimere in generale, non si riesce ad esprimere la condizione di chiusura - che intuitivamente dovrebbe essere una disgiunzione infinita - e vengono fuori modelli non standard in cui oltre a questi termini ci sono anche altre cose nell'insieme che li contiene), altrimenti non ci sarebbe stato bisogno di alcun assioma dell'infinito che asserisce al minimo che un insieme che li contiene tutti ed è strutturato in certi modi c'è, bisogna assumerlo in qualche modo o mostrare in che modo questa cosa discende dagli assiomi.
La funzione è sempre un insieme nella teoria degli insiemi formale, che questa funzione esista necessariamente tra i referenti delle costanti e $omega$ in base a cosa si può asserire? Se aggiungo certi assiomi che parlano delle relazioni tra certi termini o costanti non aggiungo automaticamente certi insiemi che le contengono.
Se la teoria è formale ed espressa al primo ordine non è che intuitivamente si può asserire che esiste un insieme solo perché metateoricamente costanti e termini si possono ordinare in una successione, bisognerebbe mostrare perché esiste internamente alla teoria in base agli assiomi.
Hai dimestichezza con le teorie del primo ordine con identità? Altrimenti non ci capiamo.

Sì, ho capito un po' meglio; non so la risposta.

Il problema sarebbe l'impossibilità di inferire l'esistenza di un insieme che contenga gli x_i, per poterlo usare come codominio per la successione in questione?

Il problema sarebbe l'impossibilità di inferire l'esistenza di un insieme che contenga gli x_i, per poterlo usare come codominio per la successione in questione?

Sì.
Per la verità ho immaginato adesso uno stratagemma per mostrare che in una teoria degli insiemi (formulata al primo ordine) che usa come operazione di successore $s$ in $omega$, $s(x) = x cup {x}$ si può mostrare che deve avere per forza un modello con una discesa infinita.
Si dovrebbero aggiungere a ZF gli assiomi con una nuova costante $a$ di questo tipo
$a ne emptyset$
$a ne {emptyset}$
$a ne {emptyset, {emptyset}}$
$a ne {emptyset, {emptyset}, {emptyset, {emptyset}}}$
...
ed infine l'assioma
$a in omega$

il nuovo sistema al primo ordine non può andare in contraddizione se quello precedente dove non c'era $a$ non ci andava (dato che si possono effettuare inferenze solo da un numero finito di affermazioni). Siccome si dimostra in ZF che l'unico elemento che non ha predecessori in $omega$ è $emptyset$ e si dimostra anche che ogni elemento di $omega$ ha un successore, $a$ non può essere un primo elemento senza predecessore (essendo diverso da $emptyset$) quindi c'è un altro elemento $b$ tale che $s(b) = a$ predecessore di $a$ e così via (sono distinti questi oggetti perché si possono dimostrare in ZF tutte le singole affermazioni $forall x in omega -> (s(...s(s(x)) ne x)$ per un qualsivoglia numero non nullo di applicazioni di $s$.
Siccome per come è definita $s$ è vero che $x in s(x)$ in questa estensione della teoria i modelli hanno una discesa infinita.
Dato che abbiamo aggiunto assiomi non intaccando la coerenza (supposto che il sistema di partenza lo fosse) i modelli della nuova teoria sono inclusi in quelli della precedente. Quindi in ZF (formulata al primo ordine, sia ben chiaro questo, il ragionamento dipende da questo) esistono modelli con discese infinite (sempre se è coerente ).

Si, però questo non contraddice le dimostrazioni che hai trovato sui testi. Se supponi una catena di appartenenza indicizzata da un insieme infinito, gli elementi di questa formano un insieme per l’assioma di rimpiazzamento e questo insieme contraddice l’assioma di fondatezza, assurdo.
Questo non è in contraddizione con il ragionamento che fai nell’ultimo post perché nel modello che hai prodotto $omega$ non è standard, perché il tuo $a$ per costruzione non è un numero naturale standard, quindi la catena che te sai essere infinita da un punto di vista esterno, da un punto di vista interno è finita, perché internamente al modello tutti gli elementi di $omega$ sono numeri “finiti”. Io l’ho capita così.

Si, però questo non contraddice le dimostrazioni che hai trovato sui testi. Se supponi una catena di appartenenza indicizzata da un insieme infinito, gli elementi di questa formano un insieme per l’assioma di rimpiazzamento e questo insieme contraddice l’assioma di fondatezza, assurdo.
Questo non è in contraddizione con il ragionamento che fai nell’ultimo post perché nel modello che hai prodotto $omega$ non è standard, perché il tuo $a$ per costruzione non è un numero naturale standard, quindi la catena che te sai essere infinita da un punto di vista esterno, da un punto di vista interno è finita, perché internamente al modello tutti gli elementi di $omega$ sono numeri “finiti”. Io l’ho capita così.

Non è rilevante che siano infiniti da un punto di vista insiemistico quegli elementi perché formino una discesa del genere (perché potrebbero non essere nemmeno un insieme). Il punto che volevo mettere in evidenza è questo. Se per discesa senza minimo si intende un qualcosa che è già in relazione con omega a monte è un conto, ma non è che prima si mostra la discesa e poi si dice "siccome c'è una funzione con omega allora..." no le due cose sono distinte.