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?