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
Capito tutto, grazie mille. Le regole sono le stesse che posso usare anch'io, tranne il taglio.
"TomSawyer":
Quando nella dimostrazione di $\not(\forall x \in D)\not A(x) \vdash (\exists x \in D)A(x)$ arrivo ad avere $\not \forall x \not A(x) \vdash A(z)$, posso trasformala direttamente in $\not\not A(z) \vdash A(z)$? Che vale, appunto, solo in LK.
No, devi applicare soltanto e rigorosamente le regole permesse, non utilizzare altro. Io farei cosi':
$ A(y)\vdash A(y)$
$\vdash \not A(y), A(y)$
$\vdash \not A(y), \exists x A(x)$
$\vdash \forall x \not A(x), \exists x A(x)$
$\not \forall x \not A(x) \vdash \exists x A(x)$
prova valida solo in LK, dal momento che a destra ad un certo punto compaiono due formule.
"TomSawyer":
Cioè le dimostrazioni in LJ e LK sono diverse, in questo caso? I passaggi non sono semplicemente
$\forall x \not A(x) \vdash \not A(z)$
$\not A(z) \vdash \not A(z)$
per le $\forall$-riflessione e $\exists$-riflessione in tutte e due le logiche?
Uhm, provo a darti la mia versione, poi se vedi che le regole non coincidono, può essere la differenza fra sistemi.
$ A(z) \vdash A(z)$
$ \not A(z), A(z) \vdash $
$\forall x \not A(x) , A(z) \vdash $
$\forall x \not A(x), \exists x A(x) \vdash $
$\forall x \not A(x) \vdash \not \exists x A(x)$
prova valida in LK e LJ.
PS: le regole che ho usato sono http://en.wikipedia.org/wiki/Sequent_calculus
Quando nella dimostrazione di $\not(\forall x \in D)\not A(x) \vdash (\exists x \in D)A(x)$ arrivo ad avere $\not \forall x \not A(x) \vdash A(z)$, posso trasformala direttamente in $\not\not A(z) \vdash A(z)$? Che vale, appunto, solo in LK.
Si' (l'idea e' quella, poi dipende dai dettagli del sistema)[/quote]
Cioè le dimostrazioni in LJ e LK sono diverse, in questo caso? I passaggi non sono semplicemente
$\forall x \not A(x) \vdash \not A(z)$
$\not A(z) \vdash \not A(z)$
per le $\forall$-riflessione e $\exists$-riflessione in tutte e due le logiche?
"fields":
[quote="TomSawyer"]
Per la prima che ho scritto nel post precedente, basta applicare la $\exists$-riflessione e la $\forall$-riflessione per concludere banalmente che $\not A(x) \vdash \not A(x)$?
Si' (l'idea e' quella, poi dipende dai dettagli del sistema)[/quote]
Cioè le dimostrazioni in LJ e LK sono diverse, in questo caso? I passaggi non sono semplicemente
$\forall x \not A(x) \vdash \not A(z)$
$\not A(z) \vdash \not A(z)$
per le $\forall$-riflessione e $\exists$-riflessione in tutte e due le logiche?
"TomSawyer":
Mi mancava questa relazione $\not \forall x \not A(x) \equiv \exists xA(x)$.
Nella dispensa del professore c'è scritto:
"si possono dimostrare le seguenti
$(\exists x \in D)A(x)\vdash \not (\forall x \in D)A(x)$ e
$\not(\forall x \in D)A(x) \vdash (\exists x \in D)A(x)$. Con l'ultima dimostrabile solo in LK."
E' certamente un errore di stampa. Forse, riferendosi alla relazione $\not \forall x \not A(x) \equiv \exists xA(x)$, voleva dire che
"si possono dimostrare le seguenti
$(\exists x \in D)A(x)\vdash \not (\forall x \in D)\not A(x)$ e
$\not(\forall x \in D)\not A(x) \vdash (\exists x \in D)A(x)$. Con l'ultima dimostrabile solo in LK."
il che e' vero.
"TomSawyer":
Per la prima che ho scritto nel post precedente, basta applicare la $\exists$-riflessione e la $\forall$-riflessione per concludere banalmente che $\not A(x) \vdash \not A(x)$?
Si' (l'idea e' quella, poi dipende dai dettagli del sistema)
Mi mancava questa relazione $\not \forall x \not A(x) \equiv \exists xA(x)$.
Nella dispensa del professore c'è scritto:
"si possono dimostrare le seguenti
$(\exists x \in D)A(x)\vdash \not (\forall x \in D)A(x)$ e
$\not(\forall x \in D)A(x) \vdash (\exists x \in D)A(x)$. Con l'ultima dimostrabile solo in LK."
Per la prima che ho scritto nel post precedente, basta applicare la $\exists$-riflessione e la $\forall$-riflessione per concludere banalmente che $\not A(x) \vdash \not A(x)$?
Nella dispensa del professore c'è scritto:
"si possono dimostrare le seguenti
$(\exists x \in D)A(x)\vdash \not (\forall x \in D)A(x)$ e
$\not(\forall x \in D)A(x) \vdash (\exists x \in D)A(x)$. Con l'ultima dimostrabile solo in LK."
Per la prima che ho scritto nel post precedente, basta applicare la $\exists$-riflessione e la $\forall$-riflessione per concludere banalmente che $\not A(x) \vdash \not A(x)$?
In LK, $\not\forall x \not A(x)$ equivale a $\exists x A(x)$ (ovvero il quantificatore esistenziale si simula con quello universale), proprio per il principio del terzo escluso. Ragioniamo infatti classicamente. Se $\not\forall x \not A(x)$, vuol dire che per qualche $y$, $\not A(y)$ non vale. A questo punto uno utilizza il principio del terzo escluso: $A(y) \vee \not A(y)$. Dunque conclude $A(y)$.
Ma nella logica LJ, il fatto che $\not A(y)$ non vale non implica $A(y)$, perche' non si da' il terzo escluso. Puoi vederla cosi': LJ e' la logica, non del vero, ma del dimostrabile. In LK, $A$ significa $A$ e' vera, in LJ significa $A$ e' dimostrabile. Ora $A\vee not A$ in LJ signicherebbe $A$ e' dimostrabile o $\not A$ e' dimostrabile, mentre cio' non e' sempre vero.
Nota che dal terzo escluso si deduce anche che $\not \not A \vdash A$ in LK, ma non in LJ. Ovvero, in LJ non vale la legge della doppia negazione.
PS: Non e' vero che $\not\forall x A(x) \vdash \exists x A(x)$, hai sbagliato a scrivere
Ma nella logica LJ, il fatto che $\not A(y)$ non vale non implica $A(y)$, perche' non si da' il terzo escluso. Puoi vederla cosi': LJ e' la logica, non del vero, ma del dimostrabile. In LK, $A$ significa $A$ e' vera, in LJ significa $A$ e' dimostrabile. Ora $A\vee not A$ in LJ signicherebbe $A$ e' dimostrabile o $\not A$ e' dimostrabile, mentre cio' non e' sempre vero.
Nota che dal terzo escluso si deduce anche che $\not \not A \vdash A$ in LK, ma non in LJ. Ovvero, in LJ non vale la legge della doppia negazione.
PS: Non e' vero che $\not\forall x A(x) \vdash \exists x A(x)$, hai sbagliato a scrivere
Ok, dubbio chiarito, grazie.
Ora mi piacerebbe capire esattamente i legami che sussistono tra $\forall$ e $\exists$ in LK. Ho letto che essi sono equivalenti in LK, dato che si ammette il principio del terzo escluso. Non ho ben capito come si collegano concettualmente questi fatti.
Poi, alcune questioni tecniche su cui ho dei dubbi:
$\forall x \not A(x) \vdash \not\exists x A(x)$ come si può dimostrare in LJ?
E $\not \forall x A(x) \vdash \exists x A(x)$ perché vale solo in LK? Inoltre, cosa significa, precisamente?
EDIT: corretto le formule
Ora mi piacerebbe capire esattamente i legami che sussistono tra $\forall$ e $\exists$ in LK. Ho letto che essi sono equivalenti in LK, dato che si ammette il principio del terzo escluso. Non ho ben capito come si collegano concettualmente questi fatti.
Poi, alcune questioni tecniche su cui ho dei dubbi:
$\forall x \not A(x) \vdash \not\exists x A(x)$ come si può dimostrare in LJ?
E $\not \forall x A(x) \vdash \exists x A(x)$ perché vale solo in LK? Inoltre, cosa significa, precisamente?
EDIT: corretto le formule
La questione è puramente tecnica, e difficile da spiegare se non si ha sottomano la stessa versione del calcolo dei sequenti (ce ne sono parecchie).
L'idea è comunque la stessa che sta dietro a tutti i sistemi di deduzione logica. $\Gamma$ rappresenta le premesse del ragionamento. Se $z$ e' libera da qualche parte in $\Gamma$ significa che tu stai indicando con $z$ un particolare individuo del dominio, e stai dicendo qualcosa su $z$. E' chiaro che non puoi generalizzare a tutti gli individui del dominio cio' che dici su $z$. Se invece $z$ non occorre libera in $\Gamma$, significa che tu hai ottenuto in qualche modo $A(z)$ come caso particolare, ma del tutto generico, di qualche quantificazione universale, e quindi puoi dedurre che $A(z)$ vale per tutti gli individui del dominio.
Un esempio concreto. Supponiamo di sapere che $\forall n A(n) \wedge B(n)$. Allora noi diciamo: sia $z$ tale che $A(z)\wedge B(z)$ ($z$ vuole essere un individuo generico). Poi diciamo: allora $A(z)$. Poiche' inoltre $z$ non occorre libero nelle nostre premesse, possiamo concludere $\forall z A(z)$. Giusto?
Se invece avessimo come premessa $z=0$, non potremmo certo concludere $\forall z\ z=0$, perche' quel $z$ e' un particolare individuo concreto di cui stiamo parlando, e non possiamo generalizzare. In altri termini $z=0$ non e' stata ottenuta attraverso qualche quantificazione universale precedente.
L'idea è comunque la stessa che sta dietro a tutti i sistemi di deduzione logica. $\Gamma$ rappresenta le premesse del ragionamento. Se $z$ e' libera da qualche parte in $\Gamma$ significa che tu stai indicando con $z$ un particolare individuo del dominio, e stai dicendo qualcosa su $z$. E' chiaro che non puoi generalizzare a tutti gli individui del dominio cio' che dici su $z$. Se invece $z$ non occorre libera in $\Gamma$, significa che tu hai ottenuto in qualche modo $A(z)$ come caso particolare, ma del tutto generico, di qualche quantificazione universale, e quindi puoi dedurre che $A(z)$ vale per tutti gli individui del dominio.
Un esempio concreto. Supponiamo di sapere che $\forall n A(n) \wedge B(n)$. Allora noi diciamo: sia $z$ tale che $A(z)\wedge B(z)$ ($z$ vuole essere un individuo generico). Poi diciamo: allora $A(z)$. Poiche' inoltre $z$ non occorre libero nelle nostre premesse, possiamo concludere $\forall z A(z)$. Giusto?
Se invece avessimo come premessa $z=0$, non potremmo certo concludere $\forall z\ z=0$, perche' quel $z$ e' un particolare individuo concreto di cui stiamo parlando, e non possiamo generalizzare. In altri termini $z=0$ non e' stata ottenuta attraverso qualche quantificazione universale precedente.
Accedi a tutti gli appunti
Tutor AI: studia meglio e in meno tempo