Teorema di compattezza per linguaggi del primo ordine, dimostrazione costruttiva?
Definizione: un insieme $\Gamma$ di formule di un linguaggio del primo ordine si dice soddisfacibile se esistono una struttura $S$, un'algebra di Boole $B$ ed una valutazione $V$ tali che $V(\phi)=1_B$ per ogni formula $\phi \in \Gamma$.
Teorema di compattezza: un insieme $\Gamma$ di formule di un linguaggio del primo ordine è soddisfacibile se e solo se ogni suo sottoinsieme finito è soddisfacibile.
Sono interessato a capire se può esistere una dimostrazione costruttiva del teorema di compattezza, la dimostrazione classica fa uso del teorema dell'ultrafiltro (ogni filtro proprio in un'algebra di Boole può essere esteso ad un ultrafiltro) che è classicamente equivalente al teorema di compattezza ma che viene solitamente dimostrato utilizzando il lemma di Zorn.
Mi chiedevo quindi...è possibile utilizzare il teorema di compattezza per dimostrare costruttivamente qualche principio che non può valere in matematica costruttiva? Se si, questo mi permetterebbe di concludere che non è possibile dimostrare costruttivamente il teorema di compattezza.
Teorema di compattezza: un insieme $\Gamma$ di formule di un linguaggio del primo ordine è soddisfacibile se e solo se ogni suo sottoinsieme finito è soddisfacibile.
Sono interessato a capire se può esistere una dimostrazione costruttiva del teorema di compattezza, la dimostrazione classica fa uso del teorema dell'ultrafiltro (ogni filtro proprio in un'algebra di Boole può essere esteso ad un ultrafiltro) che è classicamente equivalente al teorema di compattezza ma che viene solitamente dimostrato utilizzando il lemma di Zorn.
Mi chiedevo quindi...è possibile utilizzare il teorema di compattezza per dimostrare costruttivamente qualche principio che non può valere in matematica costruttiva? Se si, questo mi permetterebbe di concludere che non è possibile dimostrare costruttivamente il teorema di compattezza.
Risposte
C'è la questione di cosa intendi di preciso con matematica costruttiva, ma se intendi dimostrabile in ZF, Wikipedia in inglese dice che è equivalente al BPI, una forma più debole dell'assioma della scelta, quindi no.
Per matematica costruttiva non intendo ZF ma CZF.
Io avevo individuato due possibili strade:
1) Il teorema di compattezza implica classicamente il teorema dell'ultrafiltro, lo implica anche costruttivamente? E il teorema dell'ultrafiltro vale costruttivamente?
2) Il teorema di compattezza implica il lemma di König debole, lo implica anche costruttivamente? Tale lemma non vale costruttivamente.
Ora tu mi suggerisci che classicamente il teorema di compattezza implica il teorema dell'ideale primo, anche qui la questione è capire se lo implica anche costruttivamente. Inoltre come si dimostra che il teorema dell'ideale primo non vale costruttivamente?
Io avevo individuato due possibili strade:
1) Il teorema di compattezza implica classicamente il teorema dell'ultrafiltro, lo implica anche costruttivamente? E il teorema dell'ultrafiltro vale costruttivamente?
2) Il teorema di compattezza implica il lemma di König debole, lo implica anche costruttivamente? Tale lemma non vale costruttivamente.
Ora tu mi suggerisci che classicamente il teorema di compattezza implica il teorema dell'ideale primo, anche qui la questione è capire se lo implica anche costruttivamente. Inoltre come si dimostra che il teorema dell'ideale primo non vale costruttivamente?
Ma perchè vuoi sapere se si può dimostrare costruttivamente? Se già non si dimostra non costruttivamente in ZF, figuriamoci se si dimostra in CZF, o sbaglio? Comunque non ti so dire come si dimostra che il teorema dell'ideale primo non vale in ZF.
Non sono convinto che se un teorema non vale in ZF allora sicuramente non valga in CZF.
Comunque in base a cosa dici che il teorema di compattezza non si può dimostrare in ZF?
Comunque in base a cosa dici che il teorema di compattezza non si può dimostrare in ZF?
Io non ne ho visto le dimostrazioni, ma Wikipedia dice che è equivalente al BPI e dice anche che quello non si può dimostrare in ZF.
Io non ho approfondito CZF ma mi sembra strano che se è la versione costruttiva di ZF non sia vero (e chiaro) che si possano dimostrare meno cose che in ZF.
Io non ho approfondito CZF ma mi sembra strano che se è la versione costruttiva di ZF non sia vero (e chiaro) che si possano dimostrare meno cose che in ZF.
Nemmeno io ho approfondito CZF, il fatto che non sono convinto che tutto ciò che vale in CZF valga anche in ZF.
Ad esempio, in ZF si ha che parti di un insieme è anch'esso un insieme, in CZF questo non è in generale vero.
Ora supponiamo di aver dimostrato una proprietà che vale per qualsiasi insieme in CZF, non è detto che questa proprietà valga per tutti gli insiemi in ZF in quanto in ZF ci sono insiemi che non sono insiemi in CZF.
Cosa ne pensi?
Ad esempio, in ZF si ha che parti di un insieme è anch'esso un insieme, in CZF questo non è in generale vero.
Ora supponiamo di aver dimostrato una proprietà che vale per qualsiasi insieme in CZF, non è detto che questa proprietà valga per tutti gli insiemi in ZF in quanto in ZF ci sono insiemi che non sono insiemi in CZF.
Cosa ne pensi?
In effetti non è scontato che valga questa cosa, ma immagino ci sarà un motivo tecnico per cui è vera.
Accedi a tutti gli appunti
Tutor AI: studia meglio e in meno tempo