Teorie formali(?)
Premetto che non sono ferrato in materia, però mi è sorto un dubbio.
è possibile, in un determinato contesto(analisi, algebra lineare, algebra astratta, ...) sapere a priori se data una formulazione della relativa teoria si possa sapere a priori se all'interno di quella teoria stessa è tutto dimostrabile a partire dalla assiomatizzazione oppure esistano proposizioni non dimostrabili?
Per esempio, studiando matematica mi accorgo sempre di più che la logica proposizionale è una delle teoria formali maggiormente legate a tutte le branche della matematica, visto che viene utilizzata per dimostrare teoremi e quant'altro.
1) tutte le branche matematiche discendono dalla logica proposizionale? Oppure semplicemente ogni teoria formare la so può dotare di un'altra teoria formale per rendere valide le asserzioni in essa?
Per esempio se $L$ è la teoria della logica proposizionale e $V$ è la teoria sui spazi vettoriali allora la coppia $(V,L)$ indica una teoria formale munita delle regole di un'altra teoria formale.
2) prendiamo per esempio la teoria degli spazi vettoriali: una volta stilata la lista assiomatica, è possibile sapere a priori cosa potrò andare a dimostrare e cosa no?
è possibile, in un determinato contesto(analisi, algebra lineare, algebra astratta, ...) sapere a priori se data una formulazione della relativa teoria si possa sapere a priori se all'interno di quella teoria stessa è tutto dimostrabile a partire dalla assiomatizzazione oppure esistano proposizioni non dimostrabili?
Per esempio, studiando matematica mi accorgo sempre di più che la logica proposizionale è una delle teoria formali maggiormente legate a tutte le branche della matematica, visto che viene utilizzata per dimostrare teoremi e quant'altro.
1) tutte le branche matematiche discendono dalla logica proposizionale? Oppure semplicemente ogni teoria formare la so può dotare di un'altra teoria formale per rendere valide le asserzioni in essa?
Per esempio se $L$ è la teoria della logica proposizionale e $V$ è la teoria sui spazi vettoriali allora la coppia $(V,L)$ indica una teoria formale munita delle regole di un'altra teoria formale.
2) prendiamo per esempio la teoria degli spazi vettoriali: una volta stilata la lista assiomatica, è possibile sapere a priori cosa potrò andare a dimostrare e cosa no?
Risposte
"anto_zoolander":
Prendiamo per esempio la teoria degli spazi vettoriali: una volta stilata la lista assiomatica, è possibile sapere a priori cosa potrò andare a dimostrare e cosa no?
Credo te lo vieti una qualche forma del teorema di Godel, ma la domanda mi sembra allo stesso tempo leggermente mal posta.
Consiglio a tal proposito la lettura di questo articolo e di quest'altro articolo. Non si tratta in ogni caso di argomenti facili da affrontare in modo compiuto: stiamo parlando di Logica ad un livello abbastanza avanzato.
@Killing
Infatti ho le idee abbastanza confuse al momento e cercavo qualcosa he le ordini
@G.D
Grazie come sempre
le leggerò con il tempo, perché è una cosa che mi interessa parecchio.
Infatti ho le idee abbastanza confuse al momento e cercavo qualcosa he le ordini
@G.D
Grazie come sempre

"anto_zoolander":
è possibile, in un determinato contesto(analisi, algebra lineare, algebra astratta, ...) sapere a priori se data una formulazione della relativa teoria si possa sapere a priori se all'interno di quella teoria stessa è tutto dimostrabile a partire dalla assiomatizzazione oppure esistano proposizioni non dimostrabili?
Per esempio, studiando matematica mi accorgo sempre di più che la logica proposizionale è una delle teoria formali maggiormente legate a tutte le branche della matematica, visto che viene utilizzata per dimostrare teoremi e quant'altro.
Sostanzialmente questo è il concetto di completezza per le teorie formali, ovvero una teoria è completa se data una qualsiasi proposizione si riesce a dimostrare quella o la sua negazione (ovviamente non è che si possa dimostrare tutto, ma solo le cose vere!

Per farti alcuni esempi, l'aritmetica non è completa, e, dato che ad essa si può ricondurre l'analisi, la teoria degli insiemi, anch'esse non sono complete, che è sostanzialmente cosa dice il primo teorema di Godel, mentre ci sono anche teorie complete, un esempio (secondo me) significativo è la geometria euclidea, ma non nel senso "lo studio di $RR^n$", ma proprio "quella coi triangoli" che faceva Euclide.
1) tutte le branche matematiche discendono dalla logica proposizionale? Oppure semplicemente ogni teoria formare la so può dotare di un'altra teoria formale per rendere valide le asserzioni in essa?
Io non direi che le branche matematiche "discendono" dalla logica proposizionale, ma piuttosto la usano come strumento a cui appoggiarsi, è una base su cui erigere queste teorie.
Per esempio se $L$ è la teoria della logica proposizionale e $V$ è la teoria sui spazi vettoriali allora la coppia $(V,L)$ indica una teoria formale munita delle regole di un'altra teoria formale.
2) prendiamo per esempio la teoria degli spazi vettoriali: una volta stilata la lista assiomatica, è possibile sapere a priori cosa potrò andare a dimostrare e cosa no?
Questo non lo so.
Grazie come semprele leggerò con il tempo, perché è una cosa che mi interessa parecchio.
Anche a me, e moltissimo.
EDIT: Mi ero dimenticato di dire una cosa importantissima!!! Nemmeno io me ne intendo più di tanto, potrei benissimo aver detto una cosa imprecisa/sbagliata/vaga!
1) tutte le branche matematiche discendono dalla logica proposizionale? Oppure semplicemente ogni teoria formare la so può dotare di un'altra teoria formale per rendere valide le asserzioni in essa?
Per esempio se L è la teoria della logica proposizionale e V è la teoria sui spazi vettoriali allora la coppia (V,L) indica una teoria formale munita delle regole di un'altra teoria formale.
Quando formalizzi una teoria hai bisogno di un linguaggio, assiomi logici, regole di inferenza (che ti permettono di fare dimostrazioni a partire dagli assiomi) e assiomi specifici della teoria. Il linguaggio e gli assiomi di solito si considerano quasi sempre al primo ordine (puoi quantificare solo su variabili, per es gli assiomi classici per la def di spazio topologico non sono al primo ordine), poi dipende da quale teoria vuoi formalizzare, in certi casi puoi usare la logica proposizionale, in altri casi si può dimostrare che alcune teorie non sono formalizzabili al primo ordine (per es. i campi Archimedei), ma solo al secondo (quantifico su insiemi). Nota che anche i classici assiomi di Peano per l'aritmetica non sono al primo ordine, visto che il principio di induzione matematica quantifica su sottoinsiemi di $\mathbb{N}$. La famosa teoria PA dell'aritmetica al primo ordine usa una forma più debole del principio di induzione, che infatti non caratterizza $\mathbb{N}$ come unico modello.
2) prendiamo per esempio la teoria degli spazi vettoriali: una volta stilata la lista assiomatica, è possibile sapere a priori cosa potrò andare a dimostrare e cosa no?
Informalmente, diciamo che i nostri assiomi sono quelli soliti di spazio vettoriale formalizzati al primo ordine. Per dimostrare che questa teoria non è completa ti basta trovare una proprietà (esprimibile al primo ordine) che sia vera in un certo spazio vettoriale e falsa in un altro: questo è un enunciato indecidibile, perché se fosse dimostrabile dagli assiomi, sarebbe vero in entrambi gli spazi, se fosse dimostrabile la negazione, dovrebbe essere falso in entrambi.
Grazie di tutto ad entrambi, mi avete comunque dato un'idea 
Ho solo una domanda per @GLNC
cosa si intende per 'considerarle al primo ordine'?
O più in generale di che ordine si parla?

Ho solo una domanda per @GLNC
cosa si intende per 'considerarle al primo ordine'?
O più in generale di che ordine si parla?
"anto_zoolander":
cosa si intende per 'considerarle al primo ordine'?
Questo https://it.wikipedia.org/wiki/Linguaggi ... imo_ordine, anche se è una cosa che non mi è tanto chiara.
Non sono stato super-chiaro in effetti.
In parole povere, un enunciato è al primo ordine quando i quantificatori (per ogni.. esiste..) si riferiscono agli elementi, mentre è al secondo quando si riferiscono a sottoinsiemi.
Per esempio: gli assiomi di spazio vettoriale sono al primo ordine. Perché sono identità soddisfatte da elementi dell'insieme su cui hai la struttura di spazio vettoriale.
Gli assiomi di spazio topologico non sono al primo ordine, perché si riferiscono ai sottoinsiemi dello spazio topologico, non ai punti.
Il principio di induzione non è al primo ordine, perché il "per ogni" si riferisce a sottoinsiemi di $mathbb{N}$.
Gli assiomi di anello sono al primo ordine, un teorema che inizia con qualcosa tipo " per ogni ideale..." non è al primo ordine.
Il motivo per cui ci si prende la briga di parlare di formule al primo ordine è che la logica al primo ordine "si comporta bene", mentre ad esempio già al secondo si perde il teorema di completezza di Godel.
In parole povere, un enunciato è al primo ordine quando i quantificatori (per ogni.. esiste..) si riferiscono agli elementi, mentre è al secondo quando si riferiscono a sottoinsiemi.
Per esempio: gli assiomi di spazio vettoriale sono al primo ordine. Perché sono identità soddisfatte da elementi dell'insieme su cui hai la struttura di spazio vettoriale.
Gli assiomi di spazio topologico non sono al primo ordine, perché si riferiscono ai sottoinsiemi dello spazio topologico, non ai punti.
Il principio di induzione non è al primo ordine, perché il "per ogni" si riferisce a sottoinsiemi di $mathbb{N}$.
Gli assiomi di anello sono al primo ordine, un teorema che inizia con qualcosa tipo " per ogni ideale..." non è al primo ordine.
Il motivo per cui ci si prende la briga di parlare di formule al primo ordine è che la logica al primo ordine "si comporta bene", mentre ad esempio già al secondo si perde il teorema di completezza di Godel.