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
No, si deve semplicemente fornire una procedura per stabilire se $\sigma$ è vera o falsa in $A$. Dal momento che i quantificatori variano su un insieme finito di elementi, una formula del tipo $\forall x \alpha$ equivale ad una congiunzione finita $\alpha(a_1)\wedge...\wedge \alpha(a_n)$, dove $a_1,...,a_n$ sono gli elementi di $A$. Per i predicati k-ari inoltre puoi decidere in un tempo finito se $P(a_1,...,a_k)$ è vera o falsa, perché le relazioni su insiemi finiti sono sempre decidibili. Stessa cosa per trovare la denotazione di un termine $t$: le funzioni su insiemi finiti sono sempre computabili.
Consideriamo un linguaggio con un numero finito di parametri. Dimostrare che, data una struttura finita $A$ e una proposizione $\sigma$, si può effettivamente decidere se $\models_A \sigma$ o no. Si dovrebbe fare appello al teorema di validità, per decidere solo se $\vdash_A \sigma$ e al fatto che le deduzioni da $\emptyset$ siano un insime decidibile?
Fico l'algoritmo, ingegnoso. Avrei dovuto capire che le congiunzioni suggerivano l'approccio del dividere ogni $\alpha$ in una congiunzione finita. Grazie di nuovo..
Ok, allora ti espongo io la soluzione, perche' i concetti sono delicati (l'algoritmo che hai proposto non termina se $a\notin T$, dunque non va).
Abbiamo un algoritmo $A$ che enumera i $\sigma_i$. In poche parole possiamo immaginare che $A$ dia in output sullo schermo prima $\sigma_0$ poi $\sigma_1$ poi $\sigma_2$ e via all'infinito...
Sia allora $\alpha\in S$. Se la analizziamo sintatticamente, vediamo che $\alpha=\tau_0\wedge\tau_1\wedge...\wedge\tau_n$. Chiediamo allora ad $A$ di darci le proposizioni $\sigma_0,\sigma_1,...\sigma_n$. A questo punto controlliamo se $\sigma_0=\tau_0$, $\sigma_1=\tau_1$,...,$\sigma_n=\tau_n$. Se si', allora $\alpha\in X$, se no, $\alpha\notin X$. Quindi $X$ e' decidibile.
EDIT: l'ultimo passaggio che avevo scritto era inutile.
Abbiamo un algoritmo $A$ che enumera i $\sigma_i$. In poche parole possiamo immaginare che $A$ dia in output sullo schermo prima $\sigma_0$ poi $\sigma_1$ poi $\sigma_2$ e via all'infinito...
Sia allora $\alpha\in S$. Se la analizziamo sintatticamente, vediamo che $\alpha=\tau_0\wedge\tau_1\wedge...\wedge\tau_n$. Chiediamo allora ad $A$ di darci le proposizioni $\sigma_0,\sigma_1,...\sigma_n$. A questo punto controlliamo se $\sigma_0=\tau_0$, $\sigma_1=\tau_1$,...,$\sigma_n=\tau_n$. Se si', allora $\alpha\in X$, se no, $\alpha\notin X$. Quindi $X$ e' decidibile.
EDIT: l'ultimo passaggio che avevo scritto era inutile.
Infatti, il mio dubbio era sull'insieme di appartenenza degli enunciati $a$. Cioè io pensavo che $S=T$. In ogni caso, non saprei proprio come affrontare il problema, esperienza zero con questo tipo di esercizi. Direi che, dato che $X$ e $T$ hanno gli stessi modelli, possiamo controllare se $a \in T$. Essendo $T$ effettivamente numerabili, se $a \in T$, allora eventualmente lo troviamo.
"TomSawyer":
Quindi per essere decidibile, devo verificare che per qualsiasi $\sigma_i$ si può dire o che $\sigma_i \in {\sigma_0,\sigma_0 \wedge \sigma_1,...}$ o che $\sigma_i \notin {\sigma_0,\sigma_0 \wedge \sigma_1,...}$?
No, no, cosi' confondi la notazione...
Un insieme $X\sube S$, dove $S$ e' un insieme, e' decidibile se esiste un algoritmo che, dato in input un $a\in S$, dopo un numero finito di operazioni risponde "si'", se $a\in X$ e "no", se $a\notin X$.
Nel nostro caso $S$ e' l'insieme di tutti i possibili enunciati del linguaggio, e $X={\sigma_0,\sigma_0\wedge\sigma_1,\sigma_0\wedge\sigma_1\wedge\sigma_2, ...} $. Quindi tu devi saper dire, con un algoritmo, data una proposizione $a\in S$, se $a\in X$ o no, chiaramente sfruttando il fatto che $T={\sigma_0,\sigma_1,\sigma_2,...}$ e' effettivamente enumerabile.
Quindi per essere decidibile, devo verificare che per qualsiasi $\sigma_i$ si può dire o che $\sigma_i \in {\sigma_0,\sigma_0 \wedge \sigma_1,...}$ o che $\sigma_i \notin {\sigma_0,\sigma_0 \wedge \sigma_1,...}$? Non saprei come fare 
.
.
"TomSawyer":
Ma le varie $\sigma$ non sono tutte le proposizioni vere nella teoria? Tu dici che sono gli assiomi, o sbaglio?
I $\sigma_i$ sono le proposizioni della teoria, mentre ${\sigma_0,\sigma_0\wedge\sigma_1,\sigma_0\wedge\sigma_1\wedge\sigma_2, ...} $ e' l'insieme degli assiomi.
ps: nel mio post precedente c'era un typo: avevo scritto $\sigma_1\wedge \sigma_2$ invece che $\sigma_0\wedge\sigma_1$.
Ma le varie $\sigma$ non sono tutte le proposizioni vere nella teoria? Tu dici che sono gli assiomi, o sbaglio?
"TomSawyer":
Una domanda, prima: nella teoria ${\sigma_0,\sigma_1,...}$, non si potrebbe controllare per ogni $\sigma_i$ se è della forma $\alpha_n\to...\to \alpha_0$, per poi inserire $\alpha_n$ nella lista degli assiomi
Certo che puoi. Però non seguo il tuo ragionamento... L'elenco degli assiomi lo hai già dato, no? (${\sigma_0,\sigma_0\wedge \sigma_1,...}$). Ora devi solo mostrare che e' decidibile.
Una domanda, prima: nella teoria ${\sigma_0,\sigma_1,...}$, non si potrebbe controllare per ogni $\sigma_i$ se è della forma $\alpha_n\to...\to \alpha_0$, per poi inserire $\alpha_n$ nella lista degli assiomi, che così dovrebbe essere decidibile?
"TomSawyer":
Come si può dimostrare che si può applicare l'eliminazione dei quantificatori solo su una formula del tipo $\exists x (\alpha_1 \wedge ... \wedge \alpha_n)$, con le $\alpha$ atomiche o negazioni di atomiche?
Si dimostra per induzione, in modo perfettamente uguale a questo, dove mi sono appunto ricondotto alle formule del tipo $\exists x (\alpha_1\wedge...\wedge \alpha_n)$.
"TomSawyer":
Una teoria efficientemente numerabile (in un linguaggio ragionevole) è assiomatizzabile, perché, se elenchiamo le sue proposizioni così ${\sigma_0, \sigma_0 \wedge \sigma_1, ...}$, prendendo ogni congiunzione possiamo stabilire se qualche $\sigma_i$ non è deducibile dalle altre
Dovresti spiegare meglio: "prendendo ogni congiunzione possiamo stabilire se qualche $\sigma_i$ non è deducibile dalle altre", non mi è chiaro...
Sì, praticamente dice che due classi $EC_{\Delta}$ disgiunte possono essere separate da una classe $EC$.
Come si può dimostrare che si può applicare l'eliminazione dei quantificatori solo su una formula del tipo $\exists x (\alpha_1 \wedge ... \wedge \alpha_n)$, con le $\alpha$ atomiche o negazioni di atomiche?
Una teoria efficientemente numerabile (in un linguaggio ragionevole) è assiomatizzabile, perché, se elenchiamo le sue proposizioni così ${\sigma_0, \sigma_0 \wedge \sigma_1, ...}$, prendendo ogni congiunzione possiamo stabilire se qualche $\sigma_i$ non è deducibile dalle altre, stabilendolo poi come assioma. Va bene come procedura?
Come si può dimostrare che si può applicare l'eliminazione dei quantificatori solo su una formula del tipo $\exists x (\alpha_1 \wedge ... \wedge \alpha_n)$, con le $\alpha$ atomiche o negazioni di atomiche?
Una teoria efficientemente numerabile (in un linguaggio ragionevole) è assiomatizzabile, perché, se elenchiamo le sue proposizioni così ${\sigma_0, \sigma_0 \wedge \sigma_1, ...}$, prendendo ogni congiunzione possiamo stabilire se qualche $\sigma_i$ non è deducibile dalle altre, stabilendolo poi come assioma. Va bene come procedura?
Sia $M$ un modello. Se $M\models F_2$, poiché $F_1 uu F_2$ è non soddisfacibile, $M$ non rende vere tutte le formule di $F_1$, e dunque $M\models \not \wedge F_1$.
Interessante il risultato in sè di questo esercizio, comunque.
Interessante il risultato in sè di questo esercizio, comunque.
Per il primo, non ho capito perché $Mod F_2 \sube Mod \not \wedge F_1$. Gli altri due erano proprio facilini, devo farci la mano con la teoria dei modelli, che mi sembra quella più interessante, per quel poco che ho studiato finora.
"TomSawyer":
[quote="fields"][quote="TomSawyer"]Allora, siano $\Sigma_1$ e $\Sigma_2$ due insiemi di formule tali che non siano mai soddisfacibili dallo stesso modello. Dimostrare che esiste una proposizione $\tau$ tale che $"Mod" \Sigma_1 \subseteq "Mod" \tau$ e $"Mod" \Sigma_2 \subseteq "Mod" \neg \tau$. Per come l'ho dimostrato io, l'unica $\tau$ e' $_|_$. Giusto?
No, in quanto avresti $Mod \Sigma_1\sube Mod _|_=\emptyset$ e quindi $\Sigma_1$ non soddisfacibile: non e' detto che questo accada. Basta che prendi $\Sigma_1={A}$ e $\Sigma_2={\not A}$ con $A$ e $\not A$ non valide.[/quote]
Quindi qui tratti il caso in cui il sottoinsieme di proposizioni non soddisfacibile di $\Sigma_1 \cup \Sigma_2$ è un'unione di un sottoinsieme di $\Sigma_1$ e uno di $\Sigma_2$. Poi, non ho capito perché si può prendere a volontà $A$ e $\neg A$ non valide.
[/quote]
Quella cosa di $A$ e $\not A$ era ancora il controesempio alla tua affermazione.
L'esercizio invece si fa così. Poiche' $\Sigma_1uu\Sigma_2$ e' non soddisfacibile, esistono, per il teorema di compattezza, $F_1\sube \Sigma_1$ e $F_2\sube \Sigma_2$ tali che $F_1$ e $F_2$ sono finiti e $F_1 uu F_2$ e' non soddisfacibile. Indichiamo con $\wedge F_1$ la congiunzione delle formule di $F_1$. Chiaramente $Mod \Sigma_2\sube Mod F_2 \sube Mod \not \wedge F_1$ e $Mod \Sigma_1\sube Mod F_1= Mod \wedge F_1$, che e' la tesi.
"TomSawyer":
Un altro: sia $σ$ vera in tutti i modelli infiniti di una teoria $T$. Dimostrare che esiste un numero finito $k$ tale che $σ$ e' vera in tutti i modelli $\mathcal{A}$ di $T$ tali che $card(|\mathcal{A}|)≥k$.
Per assurdo sia falsa la tesi. Allora $Tuu{\not \sigma}$ ha modelli finiti arbitrariamente grandi, e dunque un modello infinito: impossible.
"TomSawyer":
Infine, una conferma per questo. Siano $T_1,T_2$ sono due teorie nello stesso linguaggio tali che $T_1 \subseteq T_2$, con $T_1$ completa e $T_2$ soddisfacibili. Mostrare che $T_1=T_2$.
Se $A$ è un modello di $T_2$, allora lo è anche di $T_1$, dunque $"Mod" T_2 \subseteq "Mod" T_1$. Per ogni $\sigma$ abbiamo che o $\sigma \in T_1$ o $\neg \sigma \in T_1$, quindi se $\sigma \in T_1$, allora anche $\sigma \in T_2$ e lo stesso per $\neg\sigma$. Data l'arbitrarietà di $\sigma$ segue che le due teorie sono uguali.
Be', quello che dici e' corretto, pero' per concludere dovresti spiegare un po' meglio, perche' cosi' non basta. Questi esercizi vanno fatti alla perfezione, essendo brevi.
Devi dimostrare che $T_2\sube T_1$. Sia dunque $\sigma\in T_2$. Supponiamo per assurdo $\not sigma\in T_1$. Poiche' $T_1\sube T_2$, abbiamo che anche $not \sigma\in T_2$, e dunque $T_2$ e' non soddisfacibile, assurdo. Dunque $\not sigma\notin T_1$, e per la completezza di $T_1$, vale che $\sigma\in T_1$, che e' quanto volevamo mostrare.
"fields":
[quote="TomSawyer"]Allora, siano $\Sigma_1$ e $\Sigma_2$ due insiemi di formule tali che non siano mai soddisfacibili dallo stesso modello. Dimostrare che esiste una proposizione $\tau$ tale che $"Mod" \Sigma_1 \subseteq "Mod" \tau$ e $"Mod" \Sigma_2 \subseteq "Mod" \neg \tau$. Per come l'ho dimostrato io, l'unica $\tau$ e' $_|_$. Giusto?
No, in quanto avresti $Mod \Sigma_1\sube Mod _|_=\emptyset$ e quindi $\Sigma_1$ non soddisfacibile: non e' detto che questo accada. Basta che prendi $\Sigma_1={A}$ e $\Sigma_2={\not A}$ con $A$ e $\not A$ non valide.[/quote]
Quindi qui tratti il caso in cui il sottoinsieme di proposizioni non soddisfacibile di $\Sigma_1 \cup \Sigma_2$ è un'unione di un sottoinsieme di $\Sigma_1$ e uno di $\Sigma_2$. Poi, non ho capito perché si può prendere a volontà $A$ e $\neg A$ non valide.
Per il secondo mancava quell'ipotesi, sì..
Infine, una conferma per questo. Siano $T_1,T_2$ sono due teorie nello stesso linguaggio tali che $T_1 \subseteq T_2$, con $T_1$ completa e $T_2$ soddisfacibili. Mostrare che $T_1=T_2$.
Se $A$ è un modello di $T_2$, allora lo è anche di $T_1$, dunque $"Mod" T_2 \subseteq "Mod" T_1$. Per ogni $\sigma$ abbiamo che o $\sigma \in T_1$ o $\neg \sigma \in T_1$, quindi se $\sigma \in T_1$, allora anche $\sigma \in T_2$ e lo stesso per $\neg\sigma$. Data l'arbitrarietà di $\sigma$ segue che le due teorie sono uguali.
"TomSawyer":
Allora, siano $\Sigma_1$ e $\Sigma_2$ due insiemi di formule tali che non siano mai soddisfacibili dallo stesso modello. Dimostrare che esiste una proposizione $\tau$ tale che $"Mod" \Sigma_1 \subseteq "Mod" \tau$ e $"Mod" \Sigma_2 \subseteq "Mod" \neg \tau$. Per come l'ho dimostrato io, l'unica $\tau$ e' $_|_$. Giusto?
No, in quanto avresti $Mod \Sigma_1\sube Mod _|_=\emptyset$ e quindi $\Sigma_1$ non soddisfacibile: non e' detto che questo accada. Basta che prendi $\Sigma_1={A}$ e $\Sigma_2={\not A}$ con $A$ e $\not A$ non valide.
Per il secondo manca un'ipotesi. Forse e' così:
"TomSawyer":
Un altro: sia $\sigma$ vera in tutti i modelli infiniti di una teoria $T$. Dimostrare che esiste un numero finito $k$ tale che $\sigma$ e' vera in tutti i modelli $\mathcal{A}$ di T tali che $card(|\mathcal{A}|) \ge k$.
Allora, siano $\Sigma_1$ e $\Sigma_2$ due insiemi di formule tali che non siano mai soddisfacibili dallo stesso modello. Dimostrare che esiste una proposizione $\tau$ tale che $"Mod" \Sigma_1 \subseteq "Mod" \tau$ e $"Mod" \Sigma_2 \subseteq "Mod" \neg \tau$. Per come l'ho dimostrato io, l'unica $\tau$ e' $_|_$. Giusto?
Un altro: sia $\sigma$ vera in tutti i modelli infiniti di una teoria $T$. Dimostrare che esiste un numero finito $k$ tale che $\sigma$ e' vera in tutti i modelli $\mathcal{A}$ tali che $card(|\mathcal{A}|) \ge k$.
Un altro: sia $\sigma$ vera in tutti i modelli infiniti di una teoria $T$. Dimostrare che esiste un numero finito $k$ tale che $\sigma$ e' vera in tutti i modelli $\mathcal{A}$ tali che $card(|\mathcal{A}|) \ge k$.
Ah ecco! Mi sembrava infatti strano che mi chiedessi i dettagli del teorema di completezza . Avevo pensato che volessi sapere l'idea che c'era dietro...
Da sinistra a destra. Sia $\Gamma$ consistente e per assurdo non soddisfacibile. Allora, banalmente, $\Gamma \models\phi$ e $\Gamma\models \not\phi$ e dunque $\Gamma\vdash\phi$ e $\Gamma \vdash\not \phi$ e quindi $Gamma$ e' non consistente: assurdo.
Da destra a sinistra. Supponiamo $\Gamma\models \phi$. Cio' vuol dire che $\Gamma uu {\not\phi}$ e' non soddisfacibile, e dunque non consistente. Ma sappiamo (Enderton, pag 119, corollario 24E) che $\Gamma uu {\not\phi}$ non consistente implica che $\Gamma\vdash\phi$, che e' la tesi.
. Avevo pensato che volessi sapere l'idea che c'era dietro..."TomSawyer":
Come si dimostra l'equivalenza tra $\Gamma \models \phi \implies \Gamma \vdash \phi$ e $"insieme consistente " \implies " soddisfacibile"$?
Da sinistra a destra. Sia $\Gamma$ consistente e per assurdo non soddisfacibile. Allora, banalmente, $\Gamma \models\phi$ e $\Gamma\models \not\phi$ e dunque $\Gamma\vdash\phi$ e $\Gamma \vdash\not \phi$ e quindi $Gamma$ e' non consistente: assurdo.
Da destra a sinistra. Supponiamo $\Gamma\models \phi$. Cio' vuol dire che $\Gamma uu {\not\phi}$ e' non soddisfacibile, e dunque non consistente. Ma sappiamo (Enderton, pag 119, corollario 24E) che $\Gamma uu {\not\phi}$ non consistente implica che $\Gamma\vdash\phi$, che e' la tesi.
Accedi a tutti gli appunti
Tutor AI: studia meglio e in meno tempo