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
Sì, esiste. Si possono eliminare i quantificatori esistenziali attraverso le cosiddette "funzioni di Skolem". Sicché puoi trasformare la tua formula in una del tipo $\forall x_1...forall x_n CNF$, dove CNF e' senza quantificatori e in forma normale congiuntiva. Le due formule sono equisoddisfacibili: una ha un modello sse anche l'altra ha un modello.
Sì, ho cambiato leggermente. Comunque, ok, come dicevo. Basta fare un po' di associazioni tra i termini, dopo aver sviluppato le implicazioni. Caaapito.
E nel caso di formule con quantificatori, non esiste qualche proprietà interessante?
E nel caso di formule con quantificatori, non esiste qualche proprietà interessante?
Solo che è cambiata la formula rispetto a quella che ho trasformato... 
Comunque si tratta di applicare semplicemente le leggi "algebriche" per trasformare la formula.
Comunque si tratta di applicare semplicemente le leggi "algebriche" per trasformare la formula.
Voilà, i passaggi di trasformazione.
$A\wedge (\not B\vee ((C\vee B)\rightarrow D))$
$A\wedge (\not B\vee (\not(C\vee B)\vee D))$
$A\wedge (\not B\vee ((\not C\wedge\not B)\vee D))$
$A\wedge (\not B\vee ((\not C\vee D)\wedge (\not B\vee D)))$
$A\wedge (\not B\vee\not C\vee D)\wedge (\not B\vee D)$
$A\wedge (\not B\vee ((C\vee B)\rightarrow D))$
$A\wedge (\not B\vee (\not(C\vee B)\vee D))$
$A\wedge (\not B\vee ((\not C\wedge\not B)\vee D))$
$A\wedge (\not B\vee ((\not C\vee D)\wedge (\not B\vee D)))$
$A\wedge (\not B\vee\not C\vee D)\wedge (\not B\vee D)$
Un esempio per capire bene. Sia $P$ la formula senza quantificatori $A \wedge (B \rightarrow (C \vee (B \rightarrow \neg D))$. Allora $rk(P)=4$. Quale sarebbe la formula equivalente, $P'$, di $rk(P')\le3$? Basta tenere conto che $A\rightarrow B \equiv \neg A \vee B$ e sviluppare etc?
"TomSawyer":
Ma allora non signficherebbe che ogni formula senza quantificatori in LK ha rango $\le3$? Io pensavo che dovesse essere resa equivalente ad una di rango $\le3$, ma non che si trattasse proprio della stessa formula.
No. Ogni formula $A$ senza quantificatori di LK è sì equivalente ad una formula $B$ di rango $<=3$, ma spesso $B$ e' diversa da $A$ (come tu stesso dici nella seconda frase)
"TomSawyer":
E per quanto riguarda le formule con quantificatori? Devo vedere se possono essere eliminati, poi anche quelle rientrerebbero in questa categoria?
Il teorema non vale per le formule senza quantificatori. Certo se i quantificatori sono eliminabili ci si riconduce al caso precedente.
Non avevo visto. Ma allora non signficherebbe che ogni formula senza quantificatori in LK ha rango $\le3$? Io pensavo che dovesse essere resa equivalente ad una di rango $\le3$, ma non che si trattasse proprio della stessa formula.
E per quanto riguarda le formule con quantificatori? Devo vedere se possono essere eliminati, poi anche quelle rientrerebbero in questa categoria?
E per quanto riguarda le formule con quantificatori? Devo vedere se possono essere eliminati, poi anche quelle rientrerebbero in questa categoria?
"fields":
[quote="fields"]Cos'è il rango di una formula?
Immagino che sarà il numero massimo di connettivi proposizionali "annidati" nella formula. Considerando che ogni formula senza quantificatori è equivalente ad una in forma normale congiuntiva, la tesi è immediata.[/quote]
Il rango di una formula proposizionale è l'altezza del suo albero di parsing.
Induttivamente, io ho questa definizione.
atomi: $rk(p)=0$
$\neg$: $rk(\neg A)=rk(A)+1$
connettivi: $rk(A & B)= \max{rk(A),rk(B)}+1$, con $&$ uno dei connettivi.
Stavo pensando a che proprietà possano far equivalere una formula di $rk(A)>3$ una di rango $\le3$, ma non vedo soluzioni.
Induttivamente, io ho questa definizione.
atomi: $rk(p)=0$
$\neg$: $rk(\neg A)=rk(A)+1$
connettivi: $rk(A & B)= \max{rk(A),rk(B)}+1$, con $&$ uno dei connettivi.
Stavo pensando a che proprietà possano far equivalere una formula di $rk(A)>3$ una di rango $\le3$, ma non vedo soluzioni.
"fields":
Cos'è il rango di una formula?
Immagino che sarà il numero massimo di connettivi proposizionali "annidati" nella formula. Considerando che ogni formula senza quantificatori è equivalente ad una in forma normale congiuntiva, la tesi è immediata.
Cos'è il rango di una formula?
Per sapere di preciso cosa intendesse il professore, devo aspettare lunedì.
Un altro, allora. In LK ogni formula senza quantificatori equivale ad una di rango $\le3$.
Un altro, allora. In LK ogni formula senza quantificatori equivale ad una di rango $\le3$.
Uhm... Non c'è l'equivalenza, a meno che tu non intenda qualcosa di diverso dal consueto...
Di solito si dice che per ogni formula $A$ c'è una formula in forma normale congiuntiva $B$ tale che $A$ ha un modello sse $B$ ha un modello. Tra l'altro $B$ e' in forma normale congiuntiva quando si omettono i suoi quantificatori universali.
Di solito si dice che per ogni formula $A$ c'è una formula in forma normale congiuntiva $B$ tale che $A$ ha un modello sse $B$ ha un modello. Tra l'altro $B$ e' in forma normale congiuntiva quando si omettono i suoi quantificatori universali.
Rieccomi con un problema. Dimostrare che in LK ogni formula equivale ad una sotto forma di una congiunzione di disgiunzioni di $P$ e $\neg P$. Il professore ha accennato una dimostrazione, ma poi ha detto che e' troppo difficile e l'ha lasciato stare.
Allora, come segnatura prendiamo semplicemente un simbolo per funzione $f$. L'enunciato
$(\forall x\forall y f(x)=f(y)\rightarrow x=y) \wedge \exists x \forall y f(y)\ne x$
afferma che $f$ e' una funzione iniettiva e non suriettiva. Dunque il modello che soddisfa l'enunciato (che ovviamente esiste) deve essere infinito.
$(\forall x\forall y f(x)=f(y)\rightarrow x=y) \wedge \exists x \forall y f(y)\ne x$
afferma che $f$ e' una funzione iniettiva e non suriettiva. Dunque il modello che soddisfa l'enunciato (che ovviamente esiste) deve essere infinito.
Ciao vl4d!
Tornando al quesito di fields, cioè quello di fornire una proposizione di un qualche linguaggio che ha un modello infinito, ma non modelli arbitrariamente grandi, stavo pensando di usare il solito insieme $S$, unito a qualche altro insieme, ma, purtroppo, non saprei fornirne uno preciso, anche se di sicuro non è difficile.
Tornando al quesito di fields, cioè quello di fornire una proposizione di un qualche linguaggio che ha un modello infinito, ma non modelli arbitrariamente grandi, stavo pensando di usare il solito insieme $S$, unito a qualche altro insieme, ma, purtroppo, non saprei fornirne uno preciso, anche se di sicuro non è difficile.
non finito, ok,
per "inferiormente" intendevo (impropriamente) fino ad "(al piu') infinito enumerabile"
per "inferiormente" intendevo (impropriamente) fino ad "(al piu') infinito enumerabile"
Esiste sia il cosiddetto teorema di Lowenheim-Skolem Ascendente sia quello Discendente.
Quello citato da TomSawyer, con la mia precisazione, è quello Ascendente.
Quello di vl4d è quello Discendente. Tuttavia il teorema di vl4d vale solo per linguaggi di cardinalità numerabile.
In ogni caso, esiste un enunciato che ha un modello infinito ma non modelli finiti, dunque di certo per "arbitrariamente" non si intende "inferiormente"
Quello citato da TomSawyer, con la mia precisazione, è quello Ascendente.
Quello di vl4d è quello Discendente. Tuttavia il teorema di vl4d vale solo per linguaggi di cardinalità numerabile.
In ogni caso, esiste un enunciato che ha un modello infinito ma non modelli finiti, dunque di certo per "arbitrariamente" non si intende "inferiormente"
"TomSawyer":
Io ho trovato questa affermazione su Wikipedia:
"Also, it follows from the [compactness]theorem that any theory that has an infinite model has models of arbitrary large cardinality (this is the Upward Löwenheim–Skolem theorem)."
Come devo interpretarla, allora?
Uhm, come teorema di Lowenheim-Skolem io conosco:
Se una teoria ha un modello, allora ha un modello di card. enumerabile.
Tra l'altro la dim. e' costruttiva, il modello enumerabile e' definito con la costruzione che
si usa anche per provare la completezza della logica al prim'ordine.
Dunque deduco che per "arbitrary large cardinality" si intenda "arbitrariamente" sia "inferiormente"
che "superiormente" (??)...
Il teorema di wiki che hai citato dice che se un insieme di enunciati ha un modello infinito di cardinalità $C$, allora ha modelli infiniti di qualsiasi cardinalità maggiore o uguale a $C$.
Accedi a tutti gli appunti
Tutor AI: studia meglio e in meno tempo