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
Nella logica proposizionale è possibile formalizzare argomenti che coinvolgono quantificatori solo nei casi in cui l'insieme in cui si "quantifica" è finito, non imprecisato (così come succede nelle logiche di primo ordine). Cioè non puoi formalizzare frasi del tipo "ogni numero intero ha fattorizzazione canonica unica".
Una odmanda per voi stupida... ma per me molto importante:
c'è differenza in logica tra il linguaggio del primo ordine e la logica proposizionale???
Si si... potete spiegarmi qualcosa???
c'è differenza in logica tra il linguaggio del primo ordine e la logica proposizionale???
Si si... potete spiegarmi qualcosa???
"TomSawyer":
Generalmente, per trovare un contromodello, l'antecedente deve essere vero in tutti i nodi o basta che sia vero "in più nodi" rispetto al conseguente?
Tu in sostanza devi mostrare che la radice dell'albero forza l'antecedente e non forza il conseguente. Quindi per monotonia l'antecedente sarà vero in tutti i nodi.
ps: il contromodello con un solo nodo di prima è di fatto un contromodello anche per la logica proposizionale di LK. Ecco perché è così semplice..
Ah, si possono trovare contromodelli in cui alcune proposizioni possono non essere neanche definite. Così è semplicissmo, basta vedere che $x_0$ appartiene all'antecedente e non al conseguente.
Generalmente, per trovare un contromodello, l'antecedente deve essere vero in tutti i nodi o basta che sia vero "in più nodi" rispetto al conseguente?
Generalmente, per trovare un contromodello, l'antecedente deve essere vero in tutti i nodi o basta che sia vero "in più nodi" rispetto al conseguente?
Io avevo trovato il contromodello con un solo nodo $x_0$ con $V(A)={x_0}$ e $V(B)=V(C)=\emptyset$.
Il tuo non mi sembra che funzioni, sempre che io non abbia commesso errori di calcolo. Infatti $x_0 \notin V((A to B)to C)$
Il tuo non mi sembra che funzioni, sempre che io non abbia commesso errori di calcolo. Infatti $x_0 \notin V((A to B)to C)$
Sì, anch'io la intendo così. Tu intendi quindi $V(A)=V(B)={x_1,x_3}$, no? Anch'io intendevo così, mi ero dimenticato di aggiungere $x_3$.
"TomSawyer":
Un contromodello per $((A\to B)\to C) \to (A \wedge B) \vee C)$ può essere l'albero di prima, senza $x_4$, con $V(A)=V(B)={x_1}, V(C)={x_3,x_2}$?
Non so se va bene. Almeno, quando io ho studiato la semantica di Kripke, la funzione $V$ doveva essere definita in modo tale che se $y>=x$ e $x\in V(A)$, allora anche $y\in V(A)$.
EDIT: dimenticavo, il sequente sopra non è valido in LJ
Un contromodello per $((A\to B)\to C) \to (A \wedge B) \vee C)$ può essere l'albero di prima, senza $x_4$, con $V(A)=V(B)={x_1}, V(C)={x_3,x_2}$?
Sì, mi ero accorto di aver sbagliato con quelle derivazioni. Quindi in LJ non è valido questo sequente? In LK si può fare
...
$\forall x(Ax \vee Bx) \vdash Az, Bz$
$\forall x(Ax \vee Bx) \vdash \forall x Ax, \exists x Bx$
$\forall x(Ax \vee Bx) \vdash \forall x Ax \vee \exists x Bx$
...
$\forall x(Ax \vee Bx) \vdash Az, Bz$
$\forall x(Ax \vee Bx) \vdash \forall x Ax, \exists x Bx$
$\forall x(Ax \vee Bx) \vdash \forall x Ax \vee \exists x Bx$
"TomSawyer":
EDIT: capito.
Sei sicuro, Tom? Ti stavo proprio per scrivere che le derivazioni che hai rimosso non erano giuste... Non avevi applicato correttamente le regole sui quantificatori.
"TomSawyer":
EDIT: capito.
Per derivare $\forall x (Ax \vee Bx) \vdash \forall Ax \vee \exists x Bx$, arrivo ad avere ad un certo punto $Az \vdash \forall x Ax$, quindi un punto morto. Ma se non applico subito $\forall-L$ non posso scomporre, quindi sono bloccato.
Devi tener presente che conta l'ordine con cui applichi le regole sui quantificatori. Se inverti l'ordine ti funziona.
EDIT: capito.
Per derivare $\forall x (Ax \vee Bx) \vdash \forall Ax \vee \exists x Bx$, arrivo ad avere ad un certo punto $Az \vdash \forall x Ax$, quindi un punto morto. Ma se non applico subito $\forall-L$ non posso scomporre, quindi sono bloccato.
Per derivare $\forall x (Ax \vee Bx) \vdash \forall Ax \vee \exists x Bx$, arrivo ad avere ad un certo punto $Az \vdash \forall x Ax$, quindi un punto morto. Ma se non applico subito $\forall-L$ non posso scomporre, quindi sono bloccato.
Dovrebbe essere $V(P\to Q)={x_0,x_1,x_2,x_3,x_4}$ e $V(\not P\vee Q)={x_2,x_3,x_4}$. Ora la tua conclusione diventa giusta.
Devo dimostrare che, in un linguaggio proposizionale generato da $_|_$ e dalle proposizioni atomiche $P,Q$, il sequente $(P\to Q) \to (\neg P \vee Q)$ non è valido in LJ, usando il seguente albero
Con $V_{"Atm"}(P)={x_3}$ e $V_{"Atm"}(Q)={x_2,x_3}$. Intanto ho che $V(P \to Q)={x_2,x_3,x_4}$ e anche $V(\neg P \vee Q)={x_2,x_3,x_4}$. Quindi, anche $V((P\to Q) \to (\neg P \vee Q))={x_2,x_3,x_4}$. Quindi non vale per $x_0,x_1$. Giusto?
Con $V_{"Atm"}(P)={x_3}$ e $V_{"Atm"}(Q)={x_2,x_3}$. Intanto ho che $V(P \to Q)={x_2,x_3,x_4}$ e anche $V(\neg P \vee Q)={x_2,x_3,x_4}$. Quindi, anche $V((P\to Q) \to (\neg P \vee Q))={x_2,x_3,x_4}$. Quindi non vale per $x_0,x_1$. Giusto?
https://www.matematicamente.it/f/viewtop ... 502#146502 In quelle dispense trovi ciò che cerchi.
Si può dimostrare direttamente il teorema di compattezza senza ricorrere all'assioma della scelta usando il principio dell'ultrafiltro.
Si può dimostrare direttamente il teorema di compattezza senza ricorrere all'assioma della scelta usando il principio dell'ultrafiltro.
Grazie...
Non è che per caso mi sapete indicare (o inviare per e-mail) anche una dimostrazione in italiano???
Ma che voi sappiate, esiste una dimostrazione del "teorema di compattezza" senza usare nè l'assioma di scelta nè il teorema di completezza???
Non è che per caso mi sapete indicare (o inviare per e-mail) anche una dimostrazione in italiano???
Ma che voi sappiate, esiste una dimostrazione del "teorema di compattezza" senza usare nè l'assioma di scelta nè il teorema di completezza???
http://www.cas.mcmaster.ca/~wmfarmer/CA ... ctness.pdf
http://planetmath.org/encyclopedia/Proo ... Logic.html
http://planetmath.org/encyclopedia/Proo ... Logic.html
salve a tutti...
ho bisogno urgente della dimostrazione del TEOREMA DI COMPATTEZZA
(possibilmente senza l'uso dell'assioma di scelta)...
Ho cercato su internet ma non trovo nulla.
Mi sapete indicare un link o me la potete inviare per e-mail???
Fatemi sapere al più presto...
Tks!!!
ho bisogno urgente della dimostrazione del TEOREMA DI COMPATTEZZA
(possibilmente senza l'uso dell'assioma di scelta)...
Ho cercato su internet ma non trovo nulla.
Mi sapete indicare un link o me la potete inviare per e-mail???
Fatemi sapere al più presto...
Tks!!!
"TomSawyer":
Allora, è un albero binario con 3 nodi (mondi possibili), cioè da $x_0$ si ramifica in $x_1,x_2$. $V(A)={x_2}, V(B)={x_1}$.
Quindi abbiamo che $V(\neg A) \cap V(\neg B) \subseteq \emptyset$, che è vera, e inoltre abbiamo che $x_0 \notin V(A) \cup V(B)$.
Ok
Allora, è un albero binario con 3 nodi (mondi possibili), cioè da $x_0$ si ramifica in $x_1,x_2$. $V(A)={x_2}, V(B)={x_1}$.
Quindi abbiamo che $V(\neg A) \cap V(\neg B) \subseteq \emptyset$, che è vera, e inoltre abbiamo che $x_0 \notin V(A) \cup V(B)$.
Quindi abbiamo che $V(\neg A) \cap V(\neg B) \subseteq \emptyset$, che è vera, e inoltre abbiamo che $x_0 \notin V(A) \cup V(B)$.
Uhm... Per dirti se il tuo ragionamento è corretto dovresti dirmi come è fatto il tuo albero e definirmi $V(A),V(B)$, altrimenti non posso seguirti.
OT: quelli che tu chiami "nodi" io li chiamavo "mondi possibili", essendo la semantica di Kripke nata per la logica modale. La semantica di LJ nasce appunto da una interpretazione di LJ nella logica modale.
OT: quelli che tu chiami "nodi" io li chiamavo "mondi possibili", essendo la semantica di Kripke nata per la logica modale. La semantica di LJ nasce appunto da una interpretazione di LJ nella logica modale.
Accedi a tutti gli appunti
Tutor AI: studia meglio e in meno tempo