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
Ok, Tom, ottimo 
Credevo che nel corso fossi già arrivato al teorema di compattezza. In ogni caso ci arriverai.
L'idea è proprio quella che hai esposto. Se hai un insieme di formule $A$ che ha modelli finiti arbitrariamente grandi, consideri l'insieme di formule $Auu S$, dove $S$ è l'insieme che hai definito tu. Ogni sottinsieme finito di formule di $Auu S$ è soddisfacibile, grazie al fatto che $A$ ha modelli finiti arbitrariamente grandi. Per il teorema di compattezza, $AuuS$ ha dunque un modello, che deve necessariamente essere infinito, poiché l'insieme $S$ dice che il modello, per ogni $n\in NN$, ha almeno $n$ elementi.
Basta dunque prendere come $A$ l'insieme delle formule che dicono che il modello e' un campo finito di caratteristica $p$ e otteniamo la tesi (come hai detto tu)
Credevo che nel corso fossi già arrivato al teorema di compattezza. In ogni caso ci arriverai.L'idea è proprio quella che hai esposto. Se hai un insieme di formule $A$ che ha modelli finiti arbitrariamente grandi, consideri l'insieme di formule $Auu S$, dove $S$ è l'insieme che hai definito tu. Ogni sottinsieme finito di formule di $Auu S$ è soddisfacibile, grazie al fatto che $A$ ha modelli finiti arbitrariamente grandi. Per il teorema di compattezza, $AuuS$ ha dunque un modello, che deve necessariamente essere infinito, poiché l'insieme $S$ dice che il modello, per ogni $n\in NN$, ha almeno $n$ elementi.
Basta dunque prendere come $A$ l'insieme delle formule che dicono che il modello e' un campo finito di caratteristica $p$ e otteniamo la tesi (come hai detto tu)
Leggendo un po' sul teorema di compattezza, che non conoscevo nella logica simbolica, ho capito che, intuitivamente, si dovrebbe definire un insieme infinito $S$ di formule e osservare che ogni modello che soddisfa $S$ è per forza infinito; infine, dimostrare che ogni sottoinsieme di $S$ è soddisfatto da qualche modello. Dunque per il teorema di compattezza $S$ è soddisfatto da un modello infinito.
$S$ potrebbe essere, per esempio, semplicemente un insieme arbitrariamente grande di numeri tutti diversi tra di loro? Cioè una cosa del genere $S={s_j}$, con $j$ intero positivo e $s_j=\exists n_1 \exists n_2 ... \exists n_j (n_1 \ne n_2) \wedge (n_1 \ne n_3) \wedge ... \wedge (n_{j-1} \ne n_j)$.
Poi, credo che basti considerare l'insieme dei campi di caratteristica $p$, che ha modelli arbitrariamente grandi ($p^k$, con $k$ intero arbitrariamente grande); quindi esiste un campo infinito di caratteristica $p$.
$S$ potrebbe essere, per esempio, semplicemente un insieme arbitrariamente grande di numeri tutti diversi tra di loro? Cioè una cosa del genere $S={s_j}$, con $j$ intero positivo e $s_j=\exists n_1 \exists n_2 ... \exists n_j (n_1 \ne n_2) \wedge (n_1 \ne n_3) \wedge ... \wedge (n_{j-1} \ne n_j)$.
Poi, credo che basti considerare l'insieme dei campi di caratteristica $p$, che ha modelli arbitrariamente grandi ($p^k$, con $k$ intero arbitrariamente grande); quindi esiste un campo infinito di caratteristica $p$.
Usare il teorema di compattezza per dimostrare che se un insieme $S$ di formule ha modelli finiti arbitrariamente grandi (ovvero, per ogni $n\in NN$, $S$ ha un modello con almeno $n$ elementi) allora $S$ ha un modello infinito.
Trasferire poi il discorso ai campi di caratteristica $p$.
Trasferire poi il discorso ai campi di caratteristica $p$.
"fields":
Dimostrare che per ogni numero primo $p$ esiste un campo infinito di caratteristica $p$.
Suggerimento su come impostare l'inizio?
(...)
Uno dei tanti problemi interessanti che si puo' risolvere con le tecniche della Logica e' il seguente.
Dimostrare che per ogni numero primo $p$ esiste un campo infinito di caratteristica $p$.
Notevoli altre citazioni odierne del Mitico:
"Questa domanda, che sembra stupida, forse anche lo è."
"Non è che se io enuncio una proprietà, questa deve valere."
"Ci sono certi individui che farebbero bene ad andare a farsi una passeggiata. Hanno un'espressione che ti fa capire che non li smuovi, che non c'è niente da fare."
"Questa domanda, che sembra stupida, forse anche lo è."
"Non è che se io enuncio una proprietà, questa deve valere."
"Ci sono certi individui che farebbero bene ad andare a farsi una passeggiata. Hanno un'espressione che ti fa capire che non li smuovi, che non c'è niente da fare."
Sambin's quotes of the day:
"Perchè io voglio coinvolgervi."
[ad un alunno che proponeva una soluzione] "Dici di fare così? Bene. E' completamente sbagliato."
[ad un alunno che gli ha fatto notare che la soluzione del collega era plausibile] "Appunto. E io cosa ho detto?"
"A questi personaggi che scrivono le derivazioni al contrario chiedo: perchè non guidate a sinistra?"
Ok. Vado a fare un incidente.
Sambin ruleggia.
"Perchè io voglio coinvolgervi."
[ad un alunno che proponeva una soluzione] "Dici di fare così? Bene. E' completamente sbagliato."
[ad un alunno che gli ha fatto notare che la soluzione del collega era plausibile] "Appunto. E io cosa ho detto?"
"A questi personaggi che scrivono le derivazioni al contrario chiedo: perchè non guidate a sinistra?"
Ok. Vado a fare un incidente.
Sambin ruleggia.
Immaginavo che ne avessi sentito parlare. Le sue lezioni sono favolose, non me le perderei per niente al mondo. (Purtroppo spesso ci fa lezione una sua assistente.)
"TomSawyer":
Le dispense del mio professore (Giovanni Sambin; piuttosoto importante in Italia) sono fatte un po' strane e certe cose, tipo quelle che tu hai scritto, non sono mai dette esplicitamente. Appena ho altri dubbi, mi faccio vivo. Ma ora mi hai chiarito tutto. Grazie, nel frattempo.
Cavolo, conosco Sambin, e' uno dei maggiori logici italiani
"fields":
E' un peccato che il materiale di studio che hai letto non spieghi le cose come andrebbero spiegate.
Le dispense del mio professore (Giovanni Sambin; piuttosoto importante in Italia) sono fatte un po' strane e certe cose, tipo quelle che tu hai scritto, non sono mai dette esplicitamente. Appena ho altri dubbi, mi faccio vivo. Ma ora mi hai chiarito tutto. Grazie, nel frattempo.
"TomSawyer":
Quindi può anche darsi il caso che una variabile che occorre libera in $\Gamma$ soddisfi le condizioni per la nuova variabile che richiediamo per rendere falsa $A(z)$? Ma, chiaramente, non sapendo che sia questo il caso, dobbiamo richiedere una non libera.
Esatto. Prendi ad esempio la seguente errata applicazione della regola:
$y=0\vdash y=0$
-------------------------------
$y=0\vdash \forall x\ x=0$
Essa costituisce una derivazione di un sequente non valido. Infatti, il sequente in basso non e' valido: nel modello dei numeri naturali la premessa puo' essere resa vera e la conclusione falsa. Tuttavia il sequente in alto e' valido. Cio' e' appunto dovuto alla cattiva scelta della variabile $y$. In poche parole l'applicazione della regola non rispetta la semantica, e dunque produce effetti disastrosi. Noi vogliamo che solo i sequenti validi siano derivabili, ovvero quelli i cui le conclusioni sono conseguenza logica delle premesse.
"TomSawyer":
In cosa differirebbe la spiegazione di sopra con la semantica di LJ?
Differisce per il fatto che la semantica di LJ e' decisamente piu' complessa e meno intuitiva di quella di LK, e quindi ci vuole un po' piu' di lavoro per giustificare la regola.
Quindi può anche darsi il caso che una variabile che occorre libera in $\Gamma$ soddisfi le condizioni per la nuova variabile che richiediamo per rendere falsa $A(z)$? Ma, chiaramente, non sapendo che sia questo il caso, dobbiamo richiedere una non libera.
In cosa differirebbe la spiegazione di sopra con la semantica di LJ?
In cosa differirebbe la spiegazione di sopra con la semantica di LJ?
Be', fa piacere esserti stato utile E' un peccato che il materiale di studio che hai letto non spieghi le cose come andrebbero spiegate.
Ad esempio, prendi la prima domanda che hai fatto del post, riguardo alle regola:
$\Gamma \vdash A(z)$
---------------------------
$\Gamma \vdash \forall x A(x)$
con $z$ non libera in $\Gamma$.
Tale regola si puo' spiegare con la semantica.
Il sequente in basso significa, in LK, ma anche in LJ con la sua appropriata semantica, che non e' possibile rendere vero $\Gamma$ e nel contempo falsa $\forall x A(x)$. Rendere falsa $\forall x A(x)$ significa trovare un $z$ tale che $A(z)$ e' falsa. Ora questa variabile $z$ deve essere una nuova variabile, che non occorre libera in $\Gamma$. Infatti, se non richiedessimo che $z$ sia una nuova variabile, assumeremmo implicitamente che questo individuo $z$ che rende falsa $A(z)$ e' lo stesso individuo di cui si parla in $\Gamma$, il che non e' accettabile: noi non sappiamo chi e' $z$, sappiamo solo che rende falsa $A(z)$.
E' un peccato che il materiale di studio che hai letto non spieghi le cose come andrebbero spiegate.Ad esempio, prendi la prima domanda che hai fatto del post, riguardo alle regola:
$\Gamma \vdash A(z)$
---------------------------
$\Gamma \vdash \forall x A(x)$
con $z$ non libera in $\Gamma$.
Tale regola si puo' spiegare con la semantica.
Il sequente in basso significa, in LK, ma anche in LJ con la sua appropriata semantica, che non e' possibile rendere vero $\Gamma$ e nel contempo falsa $\forall x A(x)$. Rendere falsa $\forall x A(x)$ significa trovare un $z$ tale che $A(z)$ e' falsa. Ora questa variabile $z$ deve essere una nuova variabile, che non occorre libera in $\Gamma$. Infatti, se non richiedessimo che $z$ sia una nuova variabile, assumeremmo implicitamente che questo individuo $z$ che rende falsa $A(z)$ e' lo stesso individuo di cui si parla in $\Gamma$, il che non e' accettabile: noi non sappiamo chi e' $z$, sappiamo solo che rende falsa $A(z)$.
Chiarito tutti i dubbi grazie a te. Le spiegazioni che mi hai dato non le ho trovate da nessuna parte spiegate chiaramente.
Il significato inteso in LK di un sequente $\Gamma \vdash \Delta$ e': non e' possibile trovare un modello che renda vere le formule di $\Gamma$ e false quelle di $\Delta$; un tale sequente si dice valido.
Il teorema piu' importante e' allora il seguente: un sequente e' derivabile sse e' valido.
Dunque in effetti mostrare che un sequente non e' derivabile si riduce al trovare un modello che renda contemporaneamente vere tutte le formule di $\Gamma$ e false tutte le formule di $\Delta$. In poche parole, il tuo compito e' definire i predicati di base in modo che le proposizioni a sinistra vengano valutate nel vero e quella a destra nel falso. In effetti e' come andare a esplorare le tabelle di verita' di tutte le formule per cercare un controesempio.
Il teorema piu' importante e' allora il seguente: un sequente e' derivabile sse e' valido.
Dunque in effetti mostrare che un sequente non e' derivabile si riduce al trovare un modello che renda contemporaneamente vere tutte le formule di $\Gamma$ e false tutte le formule di $\Delta$. In poche parole, il tuo compito e' definire i predicati di base in modo che le proposizioni a sinistra vengano valutate nel vero e quella a destra nel falso. In effetti e' come andare a esplorare le tabelle di verita' di tutte le formule per cercare un controesempio.
Dunque si tratta, principalmente, di definire le proposizioni del sequente. Pensavo si dovesse usare un metodo più astruso. Inoltre, non sapevo che si potessero "assegnare" le verità e le falsità a tutte le proposizioni, ma pensavo che valesse solo per le proposizioni dell'antecedente.
Cioè, se ho ben capito, è come una tabella di verità di tutte le proposizioni del sequente, ed io scelgo una combinazione di verità o falsità (per ogni proposizione utile) per rendere falso il tutto?
Cioè, se ho ben capito, è come una tabella di verità di tutte le proposizioni del sequente, ed io scelgo una combinazione di verità o falsità (per ogni proposizione utile) per rendere falso il tutto?
Ah, ok, l'avevo sospettato.
Il sequente significa: (esiste $z$ tale che o $\not A(z)$ oppure $\forall x B(x)$) implica che per ogni $x$, se $A(x)$ allora $B(x)$.
Ho utilizzato il fatto che $A\rightarrow B$ equivale a $\not A \vee B$ per definizione.
Per verificare la premessa basta che prendi dunque un modello che renda vera $\not A(z)$ per qualche $z$. Per falsificare la conclusione deve esserci un $w$ tale che renda vere $A(w)$ e $\not B(w)$.
Dunque prendi un modello con due elementi: $z$ e $w$. Definisci falsa $A(z)$ e vera $A(w)$. Inoltre definisci falsa $B(w)$ e come vuoi $B(z)$.
Il sequente significa: (esiste $z$ tale che o $\not A(z)$ oppure $\forall x B(x)$) implica che per ogni $x$, se $A(x)$ allora $B(x)$.
Ho utilizzato il fatto che $A\rightarrow B$ equivale a $\not A \vee B$ per definizione.
Per verificare la premessa basta che prendi dunque un modello che renda vera $\not A(z)$ per qualche $z$. Per falsificare la conclusione deve esserci un $w$ tale che renda vere $A(w)$ e $\not B(w)$.
Dunque prendi un modello con due elementi: $z$ e $w$. Definisci falsa $A(z)$ e vera $A(w)$. Inoltre definisci falsa $B(w)$ e come vuoi $B(z)$.
Quel sequente significa "se esiste z tale che A(z) implica B(x) per ogni x, allora è vero che per ogni x A(x) implica B(x)" ? La mia difficoltà sta proprio nel definire quel modello..
Se una formula e' derivabile in LJ, e' derivabile in LK. Dunque ti basta trovare un controesempio in LK, ovvero definire un modello che ti verifica la premessa e falsifica la conclusione.
Un'atra questione:
Dire se $\exists z(A(z) \to \forall x B(x)) \vdash \forall x(A(x) \to B(x))$ e' derivabile in LJ. Se non lo e', fornire un controesempio...
Ho provato a derivarlo, ma non si puo' fare molto. E non saprei dare un controesempio.
Dire se $\exists z(A(z) \to \forall x B(x)) \vdash \forall x(A(x) \to B(x))$ e' derivabile in LJ. Se non lo e', fornire un controesempio...
Ho provato a derivarlo, ma non si puo' fare molto. E non saprei dare un controesempio.
Accedi a tutti gli appunti
Tutor AI: studia meglio e in meno tempo