Ordini dei linguaggi in logica

[otta96]

Se uno si interessa a questioni di logica è abbastanza probabile che avrà a che fare molto presto con i linguaggi del primo e del secondo ordine, in effetti è capitato anche a me, ma ancora non ho ben familiarizzato con questi concetti, scrivo questo post alla ricerca di chiarimenti.
La differenza tra primo e secondo ordine dovrebbe essere che nel primo ordine si quantifica solo su elementi di insiemi, come in tutte le definizioni di strutture algebriche e molte di quelle relazionali che conosco, mentre del secondo ordine vuol dire che si quantifica su sottoinsiemi di insiemi come nella definizione di buon ordine oppure nel quinto assioma di Peano. Solo che leggendo alcune cose di logica mi sembra di capire che riuscire ad esprimere degli assiomi utilizzando solamente il primo ordine sia un grande vantaggio, ad esempio so che l'aritmetica di Peano nonostante avesse un assioma al secondo ordine, si è riusciti a scriverla puramente al primo ordine: https://it.wikipedia.org/wiki/Aritmetica_di_Peano, una altra cosa che me lo fa pensare è la pagina di Wikipedia degli assiomi di Tarski; ecco io volevo capire meglio questa cosa: ad esempio ho pensato "ma se quantifico al secondo ordine su un insieme $X$, non potrei quantificare al primo su $P(X)$ se è così importante il primo ordine?".
P.S. Ma gli assiomi di spazio topologico sarebbero del TERZO ordine in quanto si quantifica sulle famiglie di sottoinsiemi?

[killing_buddha]

Il teorema di Godel vieta alla logica del secondo ordine di avere una teoria della dimostrazione completa.

Ma gli assiomi di spazio topologico sarebbero del TERZO ordine in quanto si quantifica sulle famiglie di sottoinsiemi?

Sì, è tuttavia possibile scendere di un ordine e quantificare su insiemi. Non puoi però esprimere gli assiomi di spazio topologico al primo ordine.

Il fatto è che la definizione stessa di differenza tra primo e secondo ordine non ha molto senso in ZF classica: lì tutto è un insieme, non esiste una distinzione tra ur-elementi e insiemi che li contengono. Vedi qui https://math.stackexchange.com/a/23800/685

[otta96]

Il teorema di Godel vieta alla logica del secondo ordine di avere una teoria della dimostrazione completa.

Potresti spiegarmi cosa vorrebbe dire e quali conseguenze ha all'atto pratico?

Ma gli assiomi di spazio topologico sarebbero del TERZO ordine in quanto si quantifica sulle famiglie di sottoinsiemi?

Sì, è tuttavia possibile scendere di un ordine e quantificare su insiemi. Non puoi però esprimere gli assiomi di spazio topologico al primo ordine.

Davvero? Mi era sembrato di leggere che si potesse arrivare a ridurli fino al primo ordine... Ci sta naturalmente che avessi frainteso o mi ricordi male.

Il fatto è che la definizione stessa di differenza tra primo e secondo ordine non ha molto senso in ZF classica: lì tutto è un insieme, non esiste una distinzione tra ur-elementi e insiemi che li contengono. Vedi qui https://math.stackexchange.com/a/23800/685

E dov'è che ha pienamente senso?
Ho letto la discussione, in particolare la risposta che mi avevi linkato e l'ho trovata molto interessante, in pratica non esistono enunciati del secondo ordine in ZF? A un certo punto ha fatto un discorso un po' vago e non ho capito quanto precise fossero le cose che stava dicendo, cioè che l'assioma di separazione sarebbe del secondo ordine in quanto si quantifica su una proprietà (io ho pensato che lo stesso discorso si potesse applicare all'assioma di rimpiazzamento, anche se si quantifica su due proprietà), ma mi sembra che uno nei commenti dica che in realtà non si può quantificare sulle proposizioni, mi potresti chiarire questa cosa?

[killing_buddha]

Potresti spiegarmi cosa vorrebbe dire e quali conseguenze ha all'atto pratico?

Hai chiesto perché ragionare in FOL e non in SOL. Il motivo è che la logica del primo ordine è completa https://en.wikipedia.org/wiki/G%C3%B6de ... ss_theorem non c'è nulla del genere in logica del secondo ordine (non può esserci per il thm di incompletezza). Un fatto interessante è che FOL è la più potente logica che è completa e compatta. Un altro fatto che vale la pena sottolineare per rispondere a

Il fatto è che la definizione stessa di differenza tra primo e secondo ordine non ha molto senso in ZF classica: lì tutto è un insieme, non esiste una distinzione tra ur-elementi e insiemi che li contengono. Vedi qui https://math.stackexchange.com/a/23800/685

E dov'è che ha pienamente senso?
Ho letto la discussione, in particolare la risposta che mi avevi linkato e l'ho trovata molto interessante, in pratica non esistono enunciati del secondo ordine in ZF? A un certo punto ha fatto un discorso un po' vago e non ho capito quanto precise fossero le cose che stava dicendo, cioè che l'assioma di separazione sarebbe del secondo ordine in quanto si quantifica su una proprietà (io ho pensato che lo stesso discorso si potesse applicare all'assioma di rimpiazzamento, anche se si quantifica su due proprietà), ma mi sembra che uno nei commenti dica che in realtà non si può quantificare sulle proposizioni, mi potresti chiarire questa cosa?

è che esistono diversi sistemi formali che possiedono vari ordini: volta per volta andrebbe specificato qual è il sistema formale che si sta considerando al primo ordine, perché la logica classica, la logica modale, la logica intuizionista, il $\lambda$-calcolo... sono tutti sistemi formali che si possono scrivere al primo e al secondo ordine, e per cui esistono teoremi di (in)completezza del primo e del secondo ordine.

Sì, è tuttavia possibile scendere di un ordine e quantificare su insiemi. Non puoi però esprimere gli assiomi di spazio topologico al primo ordine.

Davvero? Mi era sembrato di leggere che si potesse arrivare a ridurli fino al primo ordine... Ci sta naturalmente che avessi frainteso o mi ricordi male.

Vedi pagina 3 qui.

[otta96]

Hai chiesto perché ragionare in FOL e non in SOL. Il motivo è che la logica del primo ordine è completa https://en.wikipedia.org/wiki/G%C3%B6de ... ss_theorem non c'è nulla del genere in logica del secondo ordine (non può esserci per il thm di incompletezza). Un fatto interessante è che FOL è la più potente logica che è completa e compatta

Che figata!

Vedi pagina 3 qui.

Non sono riuscito a capire se questo conferma quello che avevo letto una volta (tra l'altro forse era proprio quella tesi che mi ero leggiucchiato, o qualcosa di molto simile) o in realtà dice che mi ricordavo male...