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
Ah, non intendevo il teorema di completezza vero e proprio, ma l'equivalenza tra quelle due affermazioni. I dettagli del teorema di completezza ci sono sull'Enderton, infatti, e sono parecchio lunghi, e la dimostrazione di quell'equivalenza viene data come esercizio.
"TomSawyer":
Come si dimostra l'equivalenza tra $\Gamma \models \phi \implies \Gamma \vdash \phi$ e $"insieme consistente " \implies " soddisfacibile"$? Intuitivamente è abbastanza ovvio, ma i dettagli quali sono?
I dettagli sono parecchio lunghi. Ad ogni modo, i passi sono concettualmente due:
1) Si estende $\Gamma$ ad un insieme massimale consistente, ovvero un insieme che non può essere allargato senza distruggerne la consistenza.
2) Si dimostra che gli insiemi massimali consistenti sono soddisfacibili.
Per quanto riguarda il punto 1) è interessante il fatto che un insieme massimale consistente corrisponde sostanzialmente al duale di un ideale primo proprio di un anello booleano e $\Gamma$ viene esteso come un ideale proprio viene esteso ad un ideale primo proprio in un anello commutativo.
La 2) invece utilizza una tecnica importantissima, che coinvolge i cosiddetti universi di Herbrand.
Comunque, non direi che il teorema di completezza è "ovvio"
, è un teorema profondo e dimostrato con tecniche non banali 
Concettualmente ci sono. E' che non riuscivo a capire come si scrive la formula per una struttura generica con un simbolo predicativo generico; basta "far capire" che le $v_i$ soddisfano la relazione e le $v_j$ no.
Come si dimostra l'equivalenza tra $\Gamma \models \phi \implies \Gamma \vdash \phi$ e $"insieme consistente " \implies " soddisfacibile"$? Intuitivamente è abbastanza ovvio, ma i dettagli quali sono?
Come si dimostra l'equivalenza tra $\Gamma \models \phi \implies \Gamma \vdash \phi$ e $"insieme consistente " \implies " soddisfacibile"$? Intuitivamente è abbastanza ovvio, ma i dettagli quali sono?
Un esempio 
Come $A$ prendiamo i naturali ${1,2,3}$ con la relazione $<$, che indichiamo con la lettera P.
$\exists v_1 \exists v_2 \exists v_3 (v_1!=v_2\wedge v_1!=v_3\wedge v_2!=v_3 \wedge(\forall x\ x=v_1\vee x=v_2\vee x=v_3) \wedge P(v_1,v_2)\wedge P(v_1,v_3)\wedge P(v_2,v_3)\wedge \not P(v_2,v_1)\wedge \not P(v_3,v_1)\wedge \not P(v_3,v_2)\wedge\not P(v_1,v_1)\wedge\not P(v_2,v_2)\wedge\not P(v_3,v_3))$
dove naturalmente $v_i$ corrisponde al numero $i$.
Come $A$ prendiamo i naturali ${1,2,3}$ con la relazione $<$, che indichiamo con la lettera P.$\exists v_1 \exists v_2 \exists v_3 (v_1!=v_2\wedge v_1!=v_3\wedge v_2!=v_3 \wedge(\forall x\ x=v_1\vee x=v_2\vee x=v_3) \wedge P(v_1,v_2)\wedge P(v_1,v_3)\wedge P(v_2,v_3)\wedge \not P(v_2,v_1)\wedge \not P(v_3,v_1)\wedge \not P(v_3,v_2)\wedge\not P(v_1,v_1)\wedge\not P(v_2,v_2)\wedge\not P(v_3,v_3))$
dove naturalmente $v_i$ corrisponde al numero $i$.
"fields":
Allora, un pezzo della formula deve dire ci sono esattamente $n$ elementi $v_1,...,v_n$. Poi dirà $P(v_(i1),v_(i2))\wedge P(v_(i3),v_(i4))\wedge....\not P(v_(j1),v_(j2))\wedge....$, in modo da specificare completamente la relazione $P$.
E non devo descrivere all'interno della stessa formula che le $v_i$ sono tutte le variabili che soddisfano $P$ e viceversa per le $v_j$ o basta solo quello che hai scritto?
"fields":
Per assurdo e con metodi semantici. Per mostrare che $\not\not A$ e' derivabile in LJ, per il teorema di completezza, basta dimostrare che $\not\not A$ e' valida. Quindi supponiamo che per assurdo esista un modello di Kripke che rende falsa $\not\not A$. Is it possible?
No
, ma devo pensare perché "no".
"TomSawyer":
Quindi basta una cosa del genere $v_1 \ne ... \v_n \wedge \forall v_i \forall v_j ((v_i,v_j) \in P \to P(v_i,v_j) \wedge...)$, e lo stesso anche per le coppie $(v_i,v_j) \notin P$?
Il simbolo dell'appartenenza non lo puoi mettere nella formula. Io ho usato quel simbolo perché, come sai, una relazione binaria è un insieme di coppie ordinate.
Allora, un pezzo della formula deve dire ci sono esattamente $n$ elementi $v_1,...,v_n$. Poi dirà $P(v_(i1),v_(i2))\wedge P(v_(i3),v_(i4))\wedge....\not P(v_(j1),v_(j2))\wedge....$, in modo da specificare completamente la relazione $P$.
"TomSawyer":[/quote]
Mi accorgo ora di questo tuo esercizio. Come lo dimostri, per induzione?
[quote="fields"]
Esercizio: sia $A$ un formula proposizionale derivabile in LK. Dimostrare che $not not A$ è derivabile in LJ
Per assurdo e con metodi semantici. Per mostrare che $\not\not A$ e' derivabile in LJ, per il teorema di completezza, basta dimostrare che $\not\not A$ e' valida. Quindi supponiamo che per assurdo esista un modello di Kripke che rende falsa $\not\not A$. Is it possible?
Quindi basta una cosa del genere $v_1 \ne ... \v_n \wedge \forall v_i \forall v_j ((v_i,v_j) \in P \to P(v_i,v_j) \wedge...)$, e lo stesso anche per le coppie $(v_i,v_j) \notin P$?
Mi accorgo ora di questo tuo esercizio. Come lo dimostri, per induzione?
Mi accorgo ora di questo tuo esercizio. Come lo dimostri, per induzione?
"fields":
Esercizio: sia $A$ un formula proposizionale derivabile in LK. Dimostrare che $not not A$ è derivabile in LJ
Sì, $\theta$ dovra' dire che $v_1,...,v_n$ sono tutti fra loro distinti e inoltre, per ogni $i,j$, $\theta$ conterrà $P(v_i,v_j)$ se $(v_i,v_j)\in P$, mentre invece conterra' $\not P(v_i,v_j)$ se $(v_i,v_j)\notin P$. In questo modo la formula descrive esattamente come e' fatta $A$.
Già, molto utili. Enderton dà non pochi suggerimenti, ed è ottimo, ma a volte mi dispiace anche .
Si consideri un linguaggio con parametri $\forall$ e un simbolo predicativo binario $P$. Mostrare che se la struttura $A$ è finita e $A \equiv B$, allora $A \cong B$. Supponiamo che $|A|=n$. Se si descrive una proposizione della forma $\exists v_1 ... \exists v_n \theta$, tale che sia vera in $A$ e tale che ogni suo modello sia isomorfo ad $A$, allora, essendo che $A$ e $B$ soddisfano le stesse proposizioni, si avrà $A \cong B$. $\theta$ dovrebbe contenere tutte le coppie $(v_i,v_k) \in P$ o di che forma è?
.Si consideri un linguaggio con parametri $\forall$ e un simbolo predicativo binario $P$. Mostrare che se la struttura $A$ è finita e $A \equiv B$, allora $A \cong B$. Supponiamo che $|A|=n$. Se si descrive una proposizione della forma $\exists v_1 ... \exists v_n \theta$, tale che sia vera in $A$ e tale che ogni suo modello sia isomorfo ad $A$, allora, essendo che $A$ e $B$ soddisfano le stesse proposizioni, si avrà $A \cong B$. $\theta$ dovrebbe contenere tutte le coppie $(v_i,v_k) \in P$ o di che forma è?
"TomSawyer":
Sì, mi sono dimenticato anche $[a,\infty)$ e $(\infty,a]$. Quell'affermazione è dall'Enderton, ma non la dimostra.
Non la dimostra forse perché non è un risultato elementare.
"TomSawyer":
Sempre da lì. Dimostrare che la relazione di addizione, $ {(m,n,p)|m+n=p}$, non è definibile in $(NN,*)$. Considero l'automorfismo $h(*)$ di $(NN,*)$ che scambia due primi di $NN$. Chiaramente la moltiplicazione è preservata, dato che $m*n=p \iff h(m)h(n)=h(p)$. L'addizione non può essere definita, semplicemente perché esistono $(m,n,p) \in NN^3$ che rendono falsa $m+n=p \iff h(m)+h(n)=h(p)$. Giusto?
Ok, bella dimostrazione, devo dire. Viva gli automorfismi
Sì, mi sono dimenticato anche $[a,\infty)$ e $(\infty,a]$. Quell'affermazione è dall'Enderton, ma non la dimostra.
Sempre da lì. Dimostrare che la relazione di addizione, $ {(m,n,p)|m+n=p}$, non è definibile in $(NN,*)$. Considero l'automorfismo $h(*)$ di $(NN,*)$ che scambia due primi di $NN$. Chiaramente la moltiplicazione è preservata, dato che $m*n=p \iff h(m)h(n)=h(p)$. L'addizione non può essere definita, semplicemente perché esistono $(m,n,p) \in NN^3$ che rendono falsa $m+n=p \iff h(m)+h(n)=h(p)$. Giusto?
Sempre da lì. Dimostrare che la relazione di addizione, $ {(m,n,p)|m+n=p}$, non è definibile in $(NN,*)$. Considero l'automorfismo $h(*)$ di $(NN,*)$ che scambia due primi di $NN$. Chiaramente la moltiplicazione è preservata, dato che $m*n=p \iff h(m)h(n)=h(p)$. L'addizione non può essere definita, semplicemente perché esistono $(m,n,p) \in NN^3$ che rendono falsa $m+n=p \iff h(m)+h(n)=h(p)$. Giusto?
"TomSawyer":
Consideriamo il campo reale $\mathcal{R}$, con i parametri usuali $\forall, *, +$. Dimostrare che ogni unione finita di intervalli, i cui estremi sono algebrici, è definibile in $\mathcal{R}$.
Basterebbe scrivere la formula per definire la relazione d'ordine $<$, quella per definire un algebrico, poi gli intervalli e infine una bella congiunzione finita di intervalli?
Ok.
"TomSawyer":
Dopo, come si dimostra che questi sono gli unici insiemi definibili in $\mathcal{R}$?
Be', anche i reali non negativi sono definibili, però non sono unione finita di intervalli i cui estremi sono algebrici. Mi sa che fra gli intervalli devi includere anche quelli del tipo $[a,oo)$ e $(oo,a]$ con $a$ algebrico
Per la dimostrazione, molto dipende da dove hai preso il problema e da che teoremi hai a disposizione.
Ah, ok. Quindi supponiamo di avere $\models_A \tau$. Supponiamo per assurdo che $\Sigma \models \neg \tau$; allora ogni modello di $\Sigma$ dovrebbe rendere vera $\neg \tau$, contraddizione. Quindi la premessa (hilbertiana ) ci dice che $\Sigma \models \tau$.
Consideriamo il campo reale $\mathcal{R}$, con i parametri usuali $\forall, *, +$. Dimostrare che ogni unione finita di intervalli, i cui estremi sono algebrici, è definibile in $\mathcal{R}$.
Basterebbe scrivere la formula per definire la relazione d'ordine $<$, quella per definire un algebrico, poi gli intervalli e infine una bella congiunzione finita di intervalli?
Dopo, come si dimostra che questi sono gli unici insiemi definibili in $\mathcal{R}$?
) ci dice che $\Sigma \models \tau$. Consideriamo il campo reale $\mathcal{R}$, con i parametri usuali $\forall, *, +$. Dimostrare che ogni unione finita di intervalli, i cui estremi sono algebrici, è definibile in $\mathcal{R}$.
Basterebbe scrivere la formula per definire la relazione d'ordine $<$, quella per definire un algebrico, poi gli intervalli e infine una bella congiunzione finita di intervalli?
Dopo, come si dimostra che questi sono gli unici insiemi definibili in $\mathcal{R}$?
"TomSawyer":
Come si dimostra che $"Mod" \Sigma$, cioè la classe di tutti i modelli dell'insieme di proposizioni $\Sigma$, è una classe propria (i.e., troppo grande per essere un insieme)? Nel caso in cui $\Sigma \ne \emptyset$, naturalmente.
Bisogna assumere che $\Sigma$ abbia almeno un modello. Detto questo, non so come la cosa si mostra rigorosamente, in questo momento non ricordo alcune definizioni. Però c'entra di sicuro il fatto che se $\Sigma$ ha un modello, allora ha un modello per ogni cardinalità sufficientemente grande. E siccome la collezione dei cardinali è una classe propria, si dovrebbe derivare che anche $Mod\Sigma$ lo è.
"TomSawyer":
Sia di nuovo $\Sigma$ un insieme di proposizioni, con la proprietà che per ogni proposizione $\tau$ si ha o $\Sigma \models \tau$ o $\Sigma \models \neg \tau$. Si supponga che $A$ sia un modello di $\Sigma$. Dimostrare che per ogni proposizione $\tau$, si ha $\models_A \tau$ sse $\Sigma \models \tau$. Allora, se $\Sigma \models \tau$, allora lo stesso vale anche per ogni modello di $\Sigma$. Per l'altro verso, non ho capito se $A$ sia fissata o meno.
Sì, $A$ è fissato. Devi dimostrare che se il modello $A$ soddisfa $\tau$, allora $\Sigma\models\tau$.
Come si dimostra che $"Mod" \Sigma$, cioè la classe di tutti i modelli dell'insieme di proposizioni $\Sigma$, è una classe propria (i.e., troppo grande per essere un insieme)? Nel caso in cui $\Sigma \ne \emptyset$, naturalmente.
Sia di nuovo $\Sigma$ un insieme di proposizioni, con la proprietà che per ogni proposizione $\tau$ si ha o $\Sigma \models \tau$ o $\Sigma \models \neg \tau$. Si supponga che $A$ sia un modello di $\Sigma$. Dimostrare che per ogni proposizione $\tau$, si ha $\models_A \tau$ sse $\Sigma \models \tau$. Allora, se $\Sigma \models \tau$, allora lo stesso vale anche per ogni modello di $\Sigma$. Per l'altro verso, non ho capito se $A$ sia fissata o meno.
Sia di nuovo $\Sigma$ un insieme di proposizioni, con la proprietà che per ogni proposizione $\tau$ si ha o $\Sigma \models \tau$ o $\Sigma \models \neg \tau$. Si supponga che $A$ sia un modello di $\Sigma$. Dimostrare che per ogni proposizione $\tau$, si ha $\models_A \tau$ sse $\Sigma \models \tau$. Allora, se $\Sigma \models \tau$, allora lo stesso vale anche per ogni modello di $\Sigma$. Per l'altro verso, non ho capito se $A$ sia fissata o meno.
"TomSawyer":
Dall'Enderton: Si supponga che ogni sottoinsieme finito di $\Sigma$ abbia un modello. Dimostrare che vale la stessa cosa per almeno uno degli insiemi $\Sigma; \alpha$ e $\Sigma;\neg \alpha$.
Supponiamo per assurdo il contrario; allora $\Sigma_1;\alpha$ e $\Sigma_2;\neg \alpha$ non hanno modelli, per qualche sottoinsiemi finiti $\Sigma_1 \sube \Sigma$ e $\Sigma_2 \sube \Sigma$. Poiché $\Sigma_1 \cup \Sigma_2$ ha un modello, i sottoinsiemi non soddisfacibili di $\Sigma_1;\alpha$ e $\Sigma_2;\neg \alpha$ devono essere necessariamente $\alpha$ e $\neg \alpha$; ma significherebbe che nessuna delle due non ha un modello, assurdo. Ma mi sembra troppo semplice la parte finale
Infatti, l'ultima parte non va. Non c'è ragione perché $\alpha$ non abbia un modello.
Dovevi concludere così. Il modello di $\Sigma_1 uu \Sigma_2$ rende vera $\alpha$ o $not \alpha$, e dunque o $\Sigma_1 uu \Sigma_2; \alpha$ ha un modello oppure $\Sigma_1 uu \Sigma_2; not \alpha$ ha un modello, assurdo
Dall'Enderton: Si supponga che ogni sottoinsieme finito di $\Sigma$ abbia un modello. Dimostrare che vale la stessa cosa per almeno uno degli insiemi $\Sigma; \alpha$ e $\Sigma;\neg \alpha$.
Supponiamo per assurdo il contrario; allora $\Sigma_1;\alpha$ e $\Sigma_2;\neg \alpha$ non hanno modelli, per qualche sottoinsiemi finiti $\Sigma_1 \sube \Sigma$ e $\Sigma_2 \sube \Sigma$. Poiché $\Sigma_1 \cup \Sigma_2$ ha un modello, i sottoinsiemi non soddisfacibili di $\Sigma_1;\alpha$ e $\Sigma_2;\neg \alpha$ devono essere necessariamente $\alpha$ e $\neg \alpha$; ma significherebbe che nessuna delle due non ha un modello, assurdo. Ma mi sembra troppo semplice la parte finale.
Supponiamo per assurdo il contrario; allora $\Sigma_1;\alpha$ e $\Sigma_2;\neg \alpha$ non hanno modelli, per qualche sottoinsiemi finiti $\Sigma_1 \sube \Sigma$ e $\Sigma_2 \sube \Sigma$. Poiché $\Sigma_1 \cup \Sigma_2$ ha un modello, i sottoinsiemi non soddisfacibili di $\Sigma_1;\alpha$ e $\Sigma_2;\neg \alpha$ devono essere necessariamente $\alpha$ e $\neg \alpha$; ma significherebbe che nessuna delle due non ha un modello, assurdo. Ma mi sembra troppo semplice la parte finale
.
"TomSawyer":
Intuitivamente, direi che un modello minimale di un sistema di assiomi è un modello che soddisfa quegli assiomi e nient'altro.
La tua definizione non mi convince (o meglio, non mi è chiara). Cercando un po' in rete, ho trovato una roba di questo tipo. $M$ è un modello minimale dell'aritmetica se ogni sottomodello di $M$ non è un modello dell'aritmetica. Può essere? Quindi $NN$ sarebbe un modello minimale.
Se le cose stanno così, la tua dim è giusta. Cioè, l'idea è quella, chiaramente.
"jacopo":
[quote="TomSawyer"]Non ho ben capito cosa vuoi dire per "passare per la derivazione". Il contromodello di questo sequente è particolarmente semplice, ed è quello che differenzia LJ da LK.
Ti faccio un esempio su un'altra derivazione:
$not A -> not B |-- B -> A$
Se il sequente è derivabile in LJ, lo è per ogni A e per ogni B. Ponendo $B= not not A$ si ottiene
$not A -> not not not A |-- not not A -> A$
che non è derivabile in LJ.
Comunque mi sembra più semplice trovare un contromodello di Kripke
.[/quote]Ho capito cosa intendi. Questo modo di "dimostrare" la non-validità di un sequente va bene finché non si studiano i teoremi di validità e completezza in LJ, dato che questi teoremi ti offrono il procedimento formale per dimostrare ciò.
"fields":
[quote="TomSawyer"]modello numerabile di Peano e modello minimale di Peano sono la stessa cosa, vero?
Non so, non ho mai sentito la nozione di modello minimale dell'aritmetica. Mi servirebbe la definizione...[/quote]
Intuitivamente, direi che un modello minimale di un sistema di assiomi è un modello che soddisfa quegli assiomi e nient'altro.
Comunque, va bene quella dimostrazione?
$|-- not not (not not B ->B)$
Ah, ecco!
Esercizio: sia $A$ un formula proposizionale derivabile in LK. Dimostrare che $not not A$ è derivabile in LJ
Accedi a tutti gli appunti
Tutor AI: studia meglio e in meno tempo