Logiche del primo ordine
La regola di $\forall$-formazione dice
$\Gamma, z \in D \vdash A(z) \implies \Gamma \vdash (\forall x \in D)A(x)$, con $z$ non libera nel dominio $D$. Poi Wikipedia dice
"Ciò significa che z non deve già comparire in qualche proposizione del sequente altrimenti si avrebbe un sistema inconsistente: asserire che, dato A per una certa variabile, valga A per tutti gli elementi del dominio è assolutamente folle."
Ok, ma non è quello che si sta facendo, quando si scrive $(\forall x \in D)A(x)$? Oppure $x$ ha qualche altra proprietà implicita?
$\Gamma, z \in D \vdash A(z) \implies \Gamma \vdash (\forall x \in D)A(x)$, con $z$ non libera nel dominio $D$. Poi Wikipedia dice
"Ciò significa che z non deve già comparire in qualche proposizione del sequente altrimenti si avrebbe un sistema inconsistente: asserire che, dato A per una certa variabile, valga A per tutti gli elementi del dominio è assolutamente folle."
Ok, ma non è quello che si sta facendo, quando si scrive $(\forall x \in D)A(x)$? Oppure $x$ ha qualche altra proprietà implicita?
Risposte
Usando la semantica di Kripke, per dimostrare che $\neg(\neg A \wedge \neg B) \vdash A \vee B$ non è valido in LJ, prendo un albero con 3 nodi, $x_0,x_1,x_2$, e faccio forzare $\neg A$ a $x_1$ e $\neg B$ a $x_2$. Ora è chiaro che il conseguente è falso. Lo è anche per l'antecedente (almeno intuitivamente), e per dimostrarlo basta far vedere che $V(\neg A) \cap V(\neg B) \subseteq \emptyset$, banale. Corretto?
"TomSawyer":
Era un esercizio dell'inizio del corso. Ora bisogna trovare i contromodelli usando gli alberi di Kripke. O c'è una prova ancora più rigorosa?
Proprio quello che intendevo. I sequenti di LJ si falsificano appunto usando la semantica di Kripke.
Purtroppo ho davvero poco tempo, però ho trovato il file che avevo dato in input a Otter. Tanto per darti l'idea di come si traduceva il teorema di Dedekind nel caso di tre omomorfismi $f_1,f_2,f_3$
all x (G(x) | C(x)).
all x (x=x).
all x (-(G(x) & C(x))).
all x y z (G(x) & G(y) & G(z) -> f(e1,x) = x &
f(f(x,y),z) = f(x,f(y,z))).
(all x y z (C(x) & C(y) & C(z) -> (s(e2,x) = x &
s(s(x,y),z) = s(x,s(y,z))))).
all x y ((C(x) & C(y)) -> s(x,y)=s(y,x)).
(all x ( C(x) -> (exists y (C(y) & s(x,y)=e2)))).
all x y z (C(x) & C(y) & C(z) -> (m(e3,x) = x)).
all x y z ( (C(x) & C(y) & C(z)) -> ( m(m(x,y),z) = m(x,m(y,z)) & m(x,y)=m(y,x) ) ).
(all x ( (C(x) & x!=e2) -> (exists y (C(y) & m(x,y)=e3)))).
all x y (G(x) & G(y) -> G(f(x,y))).
all x y (C(x) & C(y) -> (C(s(x,y)) & C(m(x,y)))).
all x y z (C(x) & C(y) & C(z) -> (m(x,s(y,z))=s(m(x,y),m(x,z)))).
all x y ( (G(x) & G(y)) -> (f1(f(x,y))=m(f1(x),f1(y))) ).
all x y ( (G(x) & G(y)) -> (f2(f(x,y))=m(f2(x),f2(y))) ).
all x y ( (G(x) & G(y)) -> (f3(f(x,y))=m(f3(x),f3(y))) ).
all x (G(x) -> C(f1(x))).
all x (G(x) -> C(f2(x))).
all x (G(x) -> C(f3(x))).
G(e1) & C(e2) & C(e3).
f1(e1)=e3.
f2(e1)=e3.
f3(e1)=e3.
all x ( G(x) -> (f1(x)!=e2 & f2(x)!=e2 & f3(x)!=e2) ).
e2!=e3.
exists x (G(x) & (f1(x)!=f2(x))).
exists x (G(x) & (f1(x)!=f3(x))).
exists x (G(x) & (f2(x)!=f3(x))).
exists a1 a2 a3 ((C(a1) & a1!=e2 & C(a2) & a2!=e2 & C(a3) & a3!=e2) & (all x ( G(x) -> ( s(s(m(a1,f1(x)),m(a2,f2(x))),m(a3,f3(x)))=e2 ) ))).
Non sono sicuro che la traduzione sia perfetta, perché non mi ricordo quale era il file giusto fra i vari che avevo. Comunque il teorema di Dedekind vale anche quando gli omomorfismi sono da un semigruppo G al gruppo moltiplicativo di un campo C. Sostanzialmente ho definito G e C e gli omomorfismi
ps: la sbarra | è $\vee$ e il - è il $\not$
"fields":
[quote="TomSawyer"]Ma non dovrebbe essere sufficiente rendere vero, in qualche caso particolare, l'antecedente e falso il conseguente? Nel caso in cui $B=\neg A$ (non $B\equiv \neg A$, come ho scritto) questo succede. Viene anche dato come suggerimento.
Ah sì, ora ho capito cosa intendi, ok. Solo che non vedo come la tua prova possa essere rigorosa se non ti è stata definita la semantica di LJ. Forse volevano solo un argomentazione "intuitiva" e in questo caso va bene. [/quote]
Era un esercizio dell'inizio del corso. Ora bisogna trovare i contromodelli usando gli alberi di Kripke. O c'è una prova ancora più rigorosa?
"fields":
[quote="TomSawyer"][quote="fields"]In ogni caso ho dovuto definire gli omomorfismi, e i due campi che sono dominio e immagine degli omorfismi (in poche parole tutte le ipotesi e la negazione della conclusione)
Lavoro lungo e noioso?
[/quote]
Be', sì, è noioso e abbastanza lungo (1 oretta) scrivere per bene tutte le formule. In ogni caso la dimostrazione rigorosa con i sequenti non è fattibile con carta e penna: troppe formule. In realtà, però, essa è semplice: consiste in un paio di passaggi algebrici, anche se non ovvi.[/quote]
Magari, quando una volta avrai voglia, posta l'impostazione, o una psuedotale.
"TomSawyer":
Ma non dovrebbe essere sufficiente rendere vero, in qualche caso particolare, l'antecedente e falso il conseguente? Nel caso in cui $B=\neg A$ (non $B\equiv \neg A$, come ho scritto) questo succede. Viene anche dato come suggerimento.
Ah sì, ora ho capito cosa intendi, ok. Solo che non vedo come la tua prova possa essere rigorosa se non ti è stata definita la semantica di LJ. Forse volevano solo un argomentazione "intuitiva" e in questo caso va bene.
"TomSawyer":
[quote="fields"]In ogni caso ho dovuto definire gli omomorfismi, e i due campi che sono dominio e immagine degli omorfismi (in poche parole tutte le ipotesi e la negazione della conclusione)
Lavoro lungo e noioso?
[/quote]
Be', sì, è noioso e abbastanza lungo (1 oretta) scrivere per bene tutte le formule. In ogni caso la dimostrazione rigorosa con i sequenti non è fattibile con carta e penna: troppe formule. In realtà, però, essa è semplice: consiste in un paio di passaggi algebrici, anche se non ovvi.
"fields":
[quote="TomSawyer"]Per dimostrare che $\neg(\neg A \wedge \neg B) \vdash A \vee B$ non è derivabile in LJ, ho considerato il caso in cui $B\equiv \neg A$ e ho $\neg(\neg A \wedge \neg\neg A) \vdash A \vee \neg A$. Ora l'antecedente è dimostrabile in LJ, perché si ha
...
$\neg A \vdash \neg A \quad _|_ \vdash _|_$
$\neg A, \neg A \to _|_ \vdash$
$\neg A \wedge \neg\neg A \vdash$
$\vdash \neg(\neg A \wedge \neg\neg A)$
e il conseguente è sempre falso in LJ.
Se parli di verità o falsità devi avere una nozione di semantica, modelli e verità per LJ. Non mi sembra che tu abbia trattato la semantica di LJ... Comunque, suppore che $B\equiv \not A$ e' un po' troppo restrittivo, o no?
Io credo che dovresti mostrare che l'applicazione di ogni possibile regola non produce nessuna derivazione del tuo sequente, il che e' facile perche di fatto puoi applicare solo $\vee R$, e poi ti blocchi.[/quote]
Ma non dovrebbe essere sufficiente rendere vero, in qualche caso particolare, l'antecedente e falso il conseguente? Nel caso in cui $B=\neg A$ (non $B\equiv \neg A$, come ho scritto) questo succede. Viene anche dato come suggerimento.
"fields":
In ogni caso ho dovuto definire gli omomorfismi, e i due campi che sono dominio e immagine degli omorfismi (in poche parole tutte le ipotesi e la negazione della conclusione)
Lavoro lungo e noioso?
"fields":
Comunque il mio esperimento era volto a qualcosa di piu' sottile. Immagina: io avevo da dimostrare il teorema di Dedekind. La prima cosa che mi sono chiesto era: che strategia adottare? Ho allora notato che il teorema poteva tradursi in logica dei predicati: dunque doveva esserci per forza una dimostrazione del teorema super elementare, fatta di sole manipolazioni algebriche e che tale prova doveva essere per assurdo (essendo in linea di principio, nel caso $t=4$, dimostrabile con i sequenti)
E' lunga la dimostrazione elementare nella logica dei predicati? Una volta ben definito tutto quanto (cosa che non credo di saper fare rigorosamente) potrei farla anch'io, per dire?
PS: la derivazione di $A\to B, \neg(\neg A \vee B) \vdash _|_$ era in LJ, naturalmente, dato che in LK è banale.
"TomSawyer":
Derivare $A\to B, \neg(\neg A \vee B) \vdash _|_$ dovrebbe essere un po' difficile. Io ho fatto così:
$\quad \quad \quad \quad \quad \quad B \vdash B$
$\quad \quad \quad \quad \quad \quad B \vdash \neg A \vee B$
$A \vdash A \quad quad \neg(\neg A \vee B), B \vdash$
$A, \neg(\neg A \vee B), A \to B \vdash$
$\neg(\neg A \vee B), A \to B \vdash \neg A$
$\neg(\neg A \vee B), A \to B \vdash \neg A \vee B$
$\neg(\neg A \vee B), \neg(\neg A \vee B), A \to B \vdash$
$A\to B, \neg(\neg A \vee B) \vdash _|_$
E' giusto?
Ok.
"TomSawyer":
Mi sa che sono proprio cieco.
???
$A\to B \vdash \neg A \quad \quad B\vdash B$
$(A\to B), (\neg A \to B) \vdash B$
$(A\to B) \wedge (\neg A \to B) \vdash B$
Se sei in LK il sequente più in alto a sinistra è: $A\to B \vdash \neg A,B$.
"TomSawyer":
Per dimostrare che $\neg(\neg A \wedge \neg B) \vdash A \vee B$ non è derivabile in LJ, ho considerato il caso in cui $B\equiv \neg A$ e ho $\neg(\neg A \wedge \neg\neg A) \vdash A \vee \neg A$. Ora l'antecedente è dimostrabile in LJ, perché si ha
...
$\neg A \vdash \neg A \quad _|_ \vdash _|_$
$\neg A, \neg A \to _|_ \vdash$
$\neg A \wedge \neg\neg A \vdash$
$\vdash \neg(\neg A \wedge \neg\neg A)$
e il conseguente è sempre falso in LJ.
Se parli di verità o falsità devi avere una nozione di semantica, modelli e verità per LJ. Non mi sembra che tu abbia trattato la semantica di LJ... Comunque, suppore che $B\equiv \not A$ e' un po' troppo restrittivo, o no?
Io credo che dovresti mostrare che l'applicazione di ogni possibile regola non produce nessuna derivazione del tuo sequente, il che e' facile perche di fatto puoi applicare solo $\vee R$, e poi ti blocchi.
"TomSawyer":
E come hai trascritto simbolicamente il teorema di Dedekind? Hai dovuto dargli in input un'unica formula, in cui definivi anche gli omomorfismi e i domini o li hai definiti a parte? Tipo una roba del genere $\exists \sigma_1...\exists \sigma_4 (\sigma_1\ne...\ne\sigma_4) \to \forall \alpha_1 ... \forall \alpha_4 (\alpha_1\...\alpha_4\ne0)\exists (u \in E) (\alpha_1\sigma_1(u)+...+\alpha_4\sigma_4(u)\ne0)$, con gli omomorfismi già definiti?
Innanzitutto se vuoi dare in pasto ad un dimostratore un teorema che dice che dalle ipotesi $A$ segue $B$ devi dargli in input $A$ e $\not B$. Il dimostratore sara' in grado, eventualmente tra qualche miliardo di anni, di fornirti una dimostrazione per assurdo. (per inciso, la logica del prim'ordine dimostra che ogni teorema puo' essere dimostrato per assurdo
)In ogni caso ho dovuto definire gli omomorfismi, e i due campi che sono dominio e immagine degli omorfismi (in poche parole tutte le ipotesi e la negazione della conclusione)
Comunque il mio esperimento era volto a qualcosa di piu' sottile. Immagina: io avevo da dimostrare il teorema di Dedekind. La prima cosa che mi sono chiesto era: che strategia adottare? Ho allora notato che il teorema poteva tradursi in logica dei predicati: dunque doveva esserci per forza una dimostrazione del teorema super elementare, fatta di sole manipolazioni algebriche e che tale prova doveva essere per assurdo (essendo in linea di principio, nel caso $t=4$, dimostrabile con i sequenti)
Dunque mi sono creato una strategia che sapevo necessariamente vincente, grazie alla mia conoscenza della logica. Poi ho deciso di vedere come se la cavava Otter, ma lui si e' piantato.
Derivare $A\to B, \neg(\neg A \vee B) \vdash _|_$ dovrebbe essere un po' difficile. Io ho fatto così:
$\quad \quad \quad \quad \quad \quad B \vdash B$
$\quad \quad \quad \quad \quad \quad B \vdash \neg A \vee B$
$A \vdash A \quad quad \neg(\neg A \vee B), B \vdash$
$A, \neg(\neg A \vee B), A \to B \vdash$
$\neg(\neg A \vee B), A \to B \vdash \neg A$
$\neg(\neg A \vee B), A \to B \vdash \neg A \vee B$
$\neg(\neg A \vee B), \neg(\neg A \vee B), A \to B \vdash$
$A\to B, \neg(\neg A \vee B) \vdash _|_$
E' giusto?
$\quad \quad \quad \quad \quad \quad B \vdash B$
$\quad \quad \quad \quad \quad \quad B \vdash \neg A \vee B$
$A \vdash A \quad quad \neg(\neg A \vee B), B \vdash$
$A, \neg(\neg A \vee B), A \to B \vdash$
$\neg(\neg A \vee B), A \to B \vdash \neg A$
$\neg(\neg A \vee B), A \to B \vdash \neg A \vee B$
$\neg(\neg A \vee B), \neg(\neg A \vee B), A \to B \vdash$
$A\to B, \neg(\neg A \vee B) \vdash _|_$
E' giusto?
Mi sa che sono proprio cieco.
???
$A\to B \vdash \neg A \quad \quad B\vdash B$
$(A\to B), (\neg A \to B) \vdash B$
$(A\to B) \wedge (\neg A \to B) \vdash B$
E neanche indebolendo una tra $(A\to B)$ e $(\neg A \to B)$ non si fa niente.
Per dimostrare che $\neg(\neg A \wedge \neg B) \vdash A \vee B$ non è derivabile in LJ, ho considerato il caso in cui $B\equiv \neg A$ e ho $\neg(\neg A \wedge \neg\neg A) \vdash A \vee \neg A$. Ora l'antecedente è dimostrabile in LJ, perché si ha
...
$\neg A \vdash \neg A \quad _|_ \vdash _|_$
$\neg A, \neg A \to _|_ \vdash$
$\neg A \wedge \neg\neg A \vdash$
$\vdash \neg(\neg A \wedge \neg\neg A)$
e il conseguente è sempre falso in LJ.
E come hai trascritto simbolicamente il teorema di Dedekind? Hai dovuto dargli in input un'unica formula, in cui definivi anche gli omomorfismi e i domini o li hai definiti a parte? Tipo una roba del genere $\exists \sigma_1...\exists \sigma_4 (\sigma_1\ne...\ne\sigma_4) \to \forall \alpha_1 ... \forall \alpha_4 (\alpha_1\...\alpha_4\ne0)\exists (u \in E) (\alpha_1\sigma_1(u)+...+\alpha_4\sigma_4(u)\ne0)$, con gli omomorfismi già definiti?
???
$A\to B \vdash \neg A \quad \quad B\vdash B$
$(A\to B), (\neg A \to B) \vdash B$
$(A\to B) \wedge (\neg A \to B) \vdash B$
E neanche indebolendo una tra $(A\to B)$ e $(\neg A \to B)$ non si fa niente.
Per dimostrare che $\neg(\neg A \wedge \neg B) \vdash A \vee B$ non è derivabile in LJ, ho considerato il caso in cui $B\equiv \neg A$ e ho $\neg(\neg A \wedge \neg\neg A) \vdash A \vee \neg A$. Ora l'antecedente è dimostrabile in LJ, perché si ha
...
$\neg A \vdash \neg A \quad _|_ \vdash _|_$
$\neg A, \neg A \to _|_ \vdash$
$\neg A \wedge \neg\neg A \vdash$
$\vdash \neg(\neg A \wedge \neg\neg A)$
e il conseguente è sempre falso in LJ.
E come hai trascritto simbolicamente il teorema di Dedekind? Hai dovuto dargli in input un'unica formula, in cui definivi anche gli omomorfismi e i domini o li hai definiti a parte? Tipo una roba del genere $\exists \sigma_1...\exists \sigma_4 (\sigma_1\ne...\ne\sigma_4) \to \forall \alpha_1 ... \forall \alpha_4 (\alpha_1\...\alpha_4\ne0)\exists (u \in E) (\alpha_1\sigma_1(u)+...+\alpha_4\sigma_4(u)\ne0)$, con gli omomorfismi già definiti?
Alle prime 3 domande, la risposta e': Ok.
Uhm.. forse avrai avuto qualche svista, perche' la derivazione e' immediata: applichi $\wedgeL$ e poi $\to L$ due volte: non puoi fare altro
http://eom.springer.de/d/d120070.htm Semplificato al caso $t=4$ per Otter: gli ho dato l'handicap
Mi domando se mai si riuscira' a scrivere un theorem prover piu' bravo di un essere umano: sarebbe fico 
"TomSawyer":
Poi, non riesco a trovare una derivazione in LK di $(A\to B) \wedge (\neg A \to B) \vdash B$, che non faccia uso della sostituzione $A\to B \equiv \neg A \vee B$.
Uhm.. forse avrai avuto qualche svista, perche' la derivazione e' immediata: applichi $\wedgeL$ e poi $\to L$ due volte: non puoi fare altro
Qual è il teorema che tu hai riuscito a dimostrare e Otter no? Così, per curiosità
http://eom.springer.de/d/d120070.htm Semplificato al caso $t=4$ per Otter: gli ho dato l'handicap
Mi domando se mai si riuscira' a scrivere un theorem prover piu' bravo di un essere umano: sarebbe fico
Ho bisogno di conferme su alcuni esercizi. Le seguenti derivazioni sono in LJ.
$B\vdash B$ $C \vdash C$
----------------------
$B,B\to C\vdash C$
----------------------
$A\vdash A$ $B,B\to C,\neg C \vdash$
----------------------
$A\vdash A$ $A,B,B\to C,A\to\neg C \vdash$
----------------------
$A,A,B,A\to(B\to C),A\to\neg C \vdash$
---------------------- contrazione
$A,B,A\to(B\to C),A\to\neg C \vdash$
----------------------
$A,A\to(B\to C),A\to\neg C \vdash \neg B$
----------------------
$A\to(B\toC),A\to\neg C \vdash A\to\neg B$
E' giusto? Poi, vale in LJ anche $A\vee (B\wedge C) \equiv (A\vee B) \wedge (A\vee C)$, vero?
Ora in LK, è giusta questa derivazione?
...
$A,B \vdash A\wedge B$ $C\vdash C$
$A,B,A\wedge B \to C, \vdash C$
$A,B,A\wedge B \to C,\neg C \vdash$
$A\wedge B \to C,\neg C \vdash \neg A, \neg B$
$A\wedge B \to C,\neg C \vdash \neg A \vee \neg B$
Poi, non riesco a trovare una derivazione in LK di $(A\to B) \wedge (\neg A \to B) \vdash B$, che non faccia uso della sostituzione $A\to B \equiv \neg A \vee B$.
$B\vdash B$ $C \vdash C$
----------------------
$B,B\to C\vdash C$
----------------------
$A\vdash A$ $B,B\to C,\neg C \vdash$
----------------------
$A\vdash A$ $A,B,B\to C,A\to\neg C \vdash$
----------------------
$A,A,B,A\to(B\to C),A\to\neg C \vdash$
---------------------- contrazione
$A,B,A\to(B\to C),A\to\neg C \vdash$
----------------------
$A,A\to(B\to C),A\to\neg C \vdash \neg B$
----------------------
$A\to(B\toC),A\to\neg C \vdash A\to\neg B$
E' giusto? Poi, vale in LJ anche $A\vee (B\wedge C) \equiv (A\vee B) \wedge (A\vee C)$, vero?
Ora in LK, è giusta questa derivazione?
...
$A,B \vdash A\wedge B$ $C\vdash C$
$A,B,A\wedge B \to C, \vdash C$
$A,B,A\wedge B \to C,\neg C \vdash$
$A\wedge B \to C,\neg C \vdash \neg A, \neg B$
$A\wedge B \to C,\neg C \vdash \neg A \vee \neg B$
Poi, non riesco a trovare una derivazione in LK di $(A\to B) \wedge (\neg A \to B) \vdash B$, che non faccia uso della sostituzione $A\to B \equiv \neg A \vee B$.
Qual è il teorema che tu hai riuscito a dimostrare e Otter no? Così, per curiosità .
Non abbiamo fatto il teorema di Godel, così come non abbiamo nemmeno fatto il teorema di compattezza
. Quel corollario l'ho trovato su Wiki, nell'articolo in inglese sui teoremi d'incompletezza.
.Non abbiamo fatto il teorema di Godel, così come non abbiamo nemmeno fatto il teorema di compattezza
. Quel corollario l'ho trovato su Wiki, nell'articolo in inglese sui teoremi d'incompletezza.
"TomSawyer":
Ti sei mai interessato agli automated theorem provers? Cioè hai approfondito qualche tecnica popolare per questi programmi?
Sì, ho letto i relativi capitoli del super classico "Artificial Intelligence" di Norvig, Russell. Una volta ho provato a far dimostrare un teorema non banale al famoso programma Otter. Risultato: lui non è riuscito a dimostrarlo, io sì.
"TomSawyer":
Ti sei mai interessato agli automated theorem provers? Cioè hai approfondito qualche tecnica popolare per questi programmi?
Comunque, ancora un po' di domande sporadiche (prima di tornare un po' a quelle iniziali del topic). Una riguarda il corollario del Secondo Teorema d'Incompletezza di Gödel che dice "Se una teoria $T_2$ dimostra la consistenza di un'altra teoria $T_1$, allora $T_1$ non può dimostrare la consistenza di $T_2$". Basta osservare che, soddisfacendo $T_1,T_2$ le condizioni di dimostrabilità di Hilbert-Bernays, se $T_1$ dimostrasse la consistenza di $T_2$, allora significherebbe che $T_1$ dimostra la propria consistenza, il che è impossibile?
Non saprei
Il problema non è rigorosamente formulato, forse tu sottintendi qualche definizione che io non so... Comunque: hai fatto il teorema di Godel?
E' cosa estremamente rara studiarlo all'uni! Io ad esempio l'ho studiato per conto mio. D'altra parte con il prof che hai
Ti sei mai interessato agli automated theorem provers? Cioè hai approfondito qualche tecnica popolare per questi programmi?
Comunque, ancora un po' di domande sporadiche (prima di tornare un po' a quelle iniziali del topic). Una riguarda il corollario del Secondo Teorema d'Incompletezza di Gödel che dice "Se una teoria $T_2$ dimostra la consistenza di un'altra teoria $T_1$, allora $T_1$ non può dimostrare la consistenza di $T_2$". Basta osservare che, soddisfacendo $T_1,T_2$ le condizioni di dimostrabilità di Hilbert-Bernays, se $T_1$ dimostrasse la consistenza di $T_2$, allora significherebbe che $T_1$ dimostra la propria consistenza, il che è impossibile?
Comunque, ancora un po' di domande sporadiche (prima di tornare un po' a quelle iniziali del topic). Una riguarda il corollario del Secondo Teorema d'Incompletezza di Gödel che dice "Se una teoria $T_2$ dimostra la consistenza di un'altra teoria $T_1$, allora $T_1$ non può dimostrare la consistenza di $T_2$". Basta osservare che, soddisfacendo $T_1,T_2$ le condizioni di dimostrabilità di Hilbert-Bernays, se $T_1$ dimostrasse la consistenza di $T_2$, allora significherebbe che $T_1$ dimostra la propria consistenza, il che è impossibile?
"TomSawyer":
Comunque, come si dimostra questa equivalenza?
E' un risultato non banale, tecnico, richiede gli ordinali. Un qualunque libro di teoria degli insiemi un minimo avanzato lo riporta.
Non lo so, non credo, dato che non la conosci . Comunque, come si dimostra questa equivalenza?
. Comunque, come si dimostra questa equivalenza?
"TomSawyer":
Conosci per caso la dimostrazione nella logica simbolica di questa equivalenza?
No, non la conosco. Perché, esiste?
Ho letto che AC è equivalente al seguente enunciato "Per due insiemi qualsiasi $S$ e $T$, si ha sempre o $|S|\le|T|$ o $|S|\ge|T|$". Conosci per caso la dimostrazione nella logica simbolica di questa equivalenza?
"TomSawyer":
Ah, fico, sono andato a leggere un po' di cose ed è veramente interessante. Quindi ogni formula può avere una sua formula equisoddisfacibile di rango $\le n+3$, con $n$ il numero di quantificatori universali. Conosci qualche applicazione pratica di queste proprietà?
Oh yes! Tutti i dimostratori automatici di teoremi lavorano su formule che hanno subito preliminarmente la "skolemizzazione" e sono state ridotte in CNF. Ci sono vari algoritmi, molto efficienti, che lavorano sulle CNF. Per la logica proposizionale c'è l'algoritmo di Davis-Putnam. Per le FOL ci sono le varie procedure di risoluzione e unificazione.
Ah, fico, sono andato a leggere un po' di cose ed è veramente interessante. Quindi ogni formula può avere una sua formula equisoddisfacibile di rango $\le n+3$, con $n$ il numero di quantificatori universali. Conosci qualche applicazione pratica di queste proprietà?
Accedi a tutti gli appunti
Tutor AI: studia meglio e in meno tempo