Alberi di gioco logica.
Devo dimostrare che dato un linguaggio del primo ordine, se \( \varphi = \varphi[x] \) è una formula di \(L\) e \( \psi \) una formula chiusa di \(L\). Allora vale
\[ ( \exists x \varphi \rightarrow \psi ) \equiv \forall x (\varphi \rightarrow \psi ) \]
per farlo devo usare gli alberi di gioco. Dunque poiché
\[ ( \exists x \varphi \rightarrow \psi ) \equiv ( \neg \exists x \varphi \vee \psi ) \equiv ( \forall x \neg \varphi \vee \psi ) \]
e
\[ \forall x ( \varphi \rightarrow \psi ) \equiv \forall x ( \neg \varphi \vee \psi ) \]
Dunque l'albero di \( ( \forall x \neg \varphi \vee \psi ) \) è
https://www.wolframalpha.com/input/?i=Graph%5B%7BV+%5C%5BDirectedEdge%5D+T%2C+V+%5C%5BDirectedEdge%5D+F%2C++++F+%5C%5BDirectedEdge%5D+D+%7D%5D
Chiamando con V il ruolo di verificatore, F il ruolo di falsificatore, con \(T \) l'albero di \( \psi \), e con \(D \) l'albero duale di \(\varphi[m/x] \) ho che il primo grafo è il seguente. Evidentemente non ho disegnato gli altri rami che da \(F\) partono e che il falsificatore potrebbe scegliere.
Mentre l'albero di \( \forall x ( \neg \varphi \vee \psi ) \) è
https://www.wolframalpha.com/input/?i=Graph%5B%7BF+%5C%5BDirectedEdge%5D+V%2C+V+%5C%5BDirectedEdge%5D+T%2C+V+%5C%5BDirectedEdge%5D+D%7D%5D
Con la stessa nomenclatura, con l'unica differenza che adesso \( D \) rappresenta l'albero duale di \( \varphi \).
Ora nel primo albero ad iniziare è il verificatore, nel secondo è il falsificatore. Ed è vero che se nel primo albero il verificatore ha una strategia vincente lo ha anche nel secondo. Ma il viceversa non mi sembra vero, se l'albero \(T \) non possiede una strategia vincente per \(V\) allora nel primo albero deve passare dal falsificatore e quest'ultimo potrebbe avere un ramo vincente da scegliere...
\[ ( \exists x \varphi \rightarrow \psi ) \equiv \forall x (\varphi \rightarrow \psi ) \]
per farlo devo usare gli alberi di gioco. Dunque poiché
\[ ( \exists x \varphi \rightarrow \psi ) \equiv ( \neg \exists x \varphi \vee \psi ) \equiv ( \forall x \neg \varphi \vee \psi ) \]
e
\[ \forall x ( \varphi \rightarrow \psi ) \equiv \forall x ( \neg \varphi \vee \psi ) \]
Dunque l'albero di \( ( \forall x \neg \varphi \vee \psi ) \) è
https://www.wolframalpha.com/input/?i=Graph%5B%7BV+%5C%5BDirectedEdge%5D+T%2C+V+%5C%5BDirectedEdge%5D+F%2C++++F+%5C%5BDirectedEdge%5D+D+%7D%5D
Chiamando con V il ruolo di verificatore, F il ruolo di falsificatore, con \(T \) l'albero di \( \psi \), e con \(D \) l'albero duale di \(\varphi[m/x] \) ho che il primo grafo è il seguente. Evidentemente non ho disegnato gli altri rami che da \(F\) partono e che il falsificatore potrebbe scegliere.
Mentre l'albero di \( \forall x ( \neg \varphi \vee \psi ) \) è
https://www.wolframalpha.com/input/?i=Graph%5B%7BF+%5C%5BDirectedEdge%5D+V%2C+V+%5C%5BDirectedEdge%5D+T%2C+V+%5C%5BDirectedEdge%5D+D%7D%5D
Con la stessa nomenclatura, con l'unica differenza che adesso \( D \) rappresenta l'albero duale di \( \varphi \).
Ora nel primo albero ad iniziare è il verificatore, nel secondo è il falsificatore. Ed è vero che se nel primo albero il verificatore ha una strategia vincente lo ha anche nel secondo. Ma il viceversa non mi sembra vero, se l'albero \(T \) non possiede una strategia vincente per \(V\) allora nel primo albero deve passare dal falsificatore e quest'ultimo potrebbe avere un ramo vincente da scegliere...
Risposte
@ 3m0o: Divertente questa rappresentazione con gli alberi, non l'avevo mai incontrata.
Mi sai dare un riferimento per capirne qualcosa in più?
Grazie.
Mi sai dare un riferimento per capirne qualcosa in più?
Grazie.
Non ho trovato nulla da nessuna parte nemmeno io, se non nelle note del corso di logica che sto seguendo. Quindi l'unica cosa che posso fare è scriverti ciò che è scritto nelle note di corso.
Consideriamo un gioco a informazione perfetta a due giocatori
Definizione 1 Albero di gioco:
Un albero di gioco è un albero di altezza finita etichettato con l'insieme \( \{1,2\} \), dove \(1\) e \(2\) sono i nomi per i nostri due giocatori. In simboli è una coppia \((T,j) \) dove \(T\) è un albero finito su un insieme \(A\) e \(j : T \rightarrow \{1,2\} \) è una funzione che associa ad ogni nodo del albero a ciascuno dei nostri due giocatori.
Un gioco a due giocatori a informazione perfetto associato a un albero di gioco \( (T,j)\) può essere descritto come segue. Poniamo un pedone su una radice di \(T\). Il gioco prosegue nel seguente modo. Consideriamo che il pedone si trova sul nodo \(N \in T \).
1) Se \(N \) è una foglia e
1.1) \(j(N) = 1 \) il giocatore 1 vince la partita,
1.2) \(j(N)=2 \) il giocatore 2 vince la partita.
2) Se \(N\) non è una foglia e
2.1) \(j(N) =1 \) il giocatore 1 sposta il pedone su un figlio del nodo \(N\) di sua scelta.
2.2) \( j(N) = 2 \) il giocatore 2 sposta il pedone su un figlio del nodo \(N\) di sua scelta.
Definizione 2 strategia:
Una strategia per il giocatore \(1\) nel gioco associato al albero di gioco \( (T,j) \) è un sottoinsieme di \( \sigma \) di \(T\) (un albero in effetti) tale che
1) la radice di \(T\) appartiene a \( \sigma \)
2) Per tutti i nodi \( N \) in \( \sigma \) che non sono una foglia
2.1) Se \( j(N) = 1 \) allora uno figlio di \( N\) e uno solo appartiene a \( \sigma \).
2.2) Se \( j(N) = 2 \) allora tutti i figli di \(N \) appartengono a \( \sigma \)
In modo analogo definiamo una strategia per il giocatore \(2\).
Definizione 3 strategia vincente:
Una strategia \( \sigma \) è una strategia vincente per il giocatore \(1\) se per tutte le foglie \( F \) di \( \sigma \) abbiamo \(j(F) =1 \). Analogamente per il giocatore \(2\).
Definizione 4 Albero duale:
Per tutti gli alberi di gioco \( T=(T,j) \) definiamo l'albero di gioco duale \(T^{\delta} = (T,j^{\delta} \) dove \( j^{\delta}(N)=1 \) se e solo se \(j(N) = 2 \).
Teorema Sia \( (T,j) \) un albero di gioco. Esiste una strategia vincente per uno dei due giocatori.
Dimostrazione: lunga
Definizione 5 Gioco della valutazione di una formula:
Sia \( L = \{ c_i, f_j^{n_j}, R_k^{n_k} \} \) un linguaggio e \( \mathcal{M} = \left< M, c_i^{\mathcal{M}}, (f_j^{n_j})^{\mathcal{M}}, (R_k^{n_k})^{\mathcal{M}} \right> \) una \(L\)-struttura e \( \varphi \) una formula chiusa su questo linguaggio i cui connettori appartengono a \( \{ \neg, \wedge, \vee \} \). Definiamo il gioco di valutazione della formula \( \varphi \) in \( M \) notato \( \mathbb{E}\mathbb{V}(\mathcal{M},\varphi) \). È un giocatore a due giocatori ad informazione perfetta, ai due giocatori attribuiamo il ruolo di verificatore \(V\) e falsificatore \(F\). Il primo giocatore comincia nel ruolo di Verificatore. Per ricorrenza definiamo l'insieme delle mosse possibili a partire dalle regole seguenti:
1) Se \( \varphi \) è una formula atomica il gioco finisce.
2) Se \( \varphi = \exists x \psi \) è il turno di \(V\) che sceglie un elemento \( a \in M \), il gioco continua con \( \psi[a/x] \).
3) Se \( \varphi = \forall x \psi \) è il turno di \(F\)che sceglie un elemento \( a \in M \), il gioco continua con \( \psi[a/x] \).
4) Se \( \varphi = \varphi_1 \vee \varphi_2 \) è il turno di \(V\) che sceglie \( \varphi_1\) oppure \( \varphi_2 \), il gioco continua con la formula scelta da \(V\).
5) Se \( \varphi = \varphi_1 \wedge \varphi_2 \) è il turno di \(F\) che sceglie \( \varphi_1\) oppure \( \varphi_2 \), il gioco continua con la formula scelta da \(F\).
6) Se \( \varphi= \neg \psi \), scambiamo i ruoli di \(V\) e \(F\), il gioco continua con \( \psi \).
L'obbiettivo di questo gioco è finire su una formula atomica \( R(t_1,\ldots,t_n ) \) con \( \mathcal{M} \models R(t_1,\ldots,t_n) \) avente il ruolo di Verificatore oppure tale che \( \mathcal{M} \not\models R(t_1,\ldots,t_n) \) avendo il ruolo di Falsificatore.
NB: Consdierare le formule solo con connettori \( \{ \neg, \vee, \wedge \} \) non è restrittivo.
Definizione 5 Albero del gioco di valutazione:
Ci fissiamo in un linguaggio \(L\), \( \varphi[x_0,\ldots,x_n] \) una formula su questo linguaggio i cui connettivi sono in \( \{ \neg, \vee, \wedge \} \) e le variabili libere sono tra \( x_0, \ldots, x_n \) e \( \mathcal{M}_{x_0 \rightarrow a_0, \ldots, x_n \rightarrow a_n} \) una \(L\)-struttura con interpretazioni in \( \left| \mathcal{M} \right| \) di variabili \( x_0, \ldots, x_n \). Definiamo l'albero del gioco \( T(\varphi[x_0,\ldots,x_n], \mathcal{M}_{x_0 \rightarrow a_0, \ldots, x_n \rightarrow a_n}) \) o per alleggerire la notazione \( T(\varphi, \mathcal{M} ) \) associato alla formula \( \varphi[x_0,\ldots, x_n ] \) nella struttura \( \mathcal{M}_{x_0 \rightarrow a_0, \ldots, x_n \rightarrow a_n} \) per induzione sull'altezza di \( \varphi \) come segue:
1) Se \( \varphi \) è una formula atomica
1.1 ) Se \( \mathcal{M}_{x_0 \rightarrow a_0, \ldots, x_n \rightarrow a_n} \models \varphi \) allora \( T(\varphi, \mathcal{M}) = V \)
1.2) Se \( \mathcal{M}_{x_0 \rightarrow a_0, \ldots, x_n \rightarrow a_n} \not\models \varphi \) allora \( T(\varphi, \mathcal{M}) = F \)
2) Se \( \varphi = \varphi_1 \vee \varphi_2 \) allora \[ T(\varphi,\mathcal{M} ) = T(\varphi_1, \mathcal{M}) \leftarrow V \rightarrow T(\varphi_2, \mathcal{M} ) \] (il nodo è V e i figli sono i due alberi di \( \varphi_1 \) e \( \varphi_2 \) ho provato a usare xymatrix ma mi dice "unparseable or potentially dangerous latex formula")
3) Se \( \varphi = \varphi_1 \wedge \varphi_2 \) allora \[ T(\varphi,\mathcal{M} ) = T(\varphi_1, \mathcal{M}) \leftarrow F \rightarrow T(\varphi_2, \mathcal{M} ) \]
4) Se \( \varphi = \exists x \psi \) allora per ogni \(m \in M \) \[ T(\varphi,\mathcal{M} ) = V \rightarrow T(\psi, \mathcal{M}_{x \rightarrow m} ) \]
5) Se \( \varphi = \forall x \psi \) allora per ogni \(m \in M \) \[ T(\varphi,\mathcal{M} ) = F \rightarrow T(\psi, \mathcal{M}_{x \rightarrow m} ) \]
6) Se \( \varphi = \neg \psi \) allora
\[ T(\varphi,\mathcal{M}) = ( T(\psi, \mathcal{M} )^{\delta} \]
dove \( T^{ \delta} \) è l'albero duale. I giocatori 1 e 2 sono chiamati V e F.
Definizione 6 Valutazione di una formula:
Sia \( \varphi \) una formula e \( \mathcal{M } \) una \(L\)-struttura come in precedenza. Diciamo che \( \varphi \) è soddisfatta in \( \mathcal{M} \) e lo notiamo \( \mathcal{M} \models \varphi \) se e solo se nel gioco \( \mathbb{E}\mathbb{V}(\mathcal{M},\varphi) \) il giocatore che comincia nel ruolo di verificatore possiede una strategia vincente. In modo equivalente \( \mathcal{M} \models \varphi \) se e solo se il verificatore possiede una strategia vincente nel albero \( T(\varphi,\mathcal{M} \). In caso contrario \( \mathcal{M} \not\models \varphi \).
Teorema Le due definizioni di valutazione di una formula sono equivalenti.
La dimostrazione è lunga, noiosa e facile. Consiste nel dimostrare che
\[ \mathcal{M} \models \varphi \Leftrightarrow \text{ il verificatore possiede una strategia vincente} \]
\[ \mathcal{M} \not\models \varphi \Leftrightarrow \text{ il falsificatore possiede una strategia vincente} \]
e si fa per induzione sull'altezza della formula \( \varphi \).
Consideriamo un gioco a informazione perfetta a due giocatori
Definizione 1 Albero di gioco:
Un albero di gioco è un albero di altezza finita etichettato con l'insieme \( \{1,2\} \), dove \(1\) e \(2\) sono i nomi per i nostri due giocatori. In simboli è una coppia \((T,j) \) dove \(T\) è un albero finito su un insieme \(A\) e \(j : T \rightarrow \{1,2\} \) è una funzione che associa ad ogni nodo del albero a ciascuno dei nostri due giocatori.
Un gioco a due giocatori a informazione perfetto associato a un albero di gioco \( (T,j)\) può essere descritto come segue. Poniamo un pedone su una radice di \(T\). Il gioco prosegue nel seguente modo. Consideriamo che il pedone si trova sul nodo \(N \in T \).
1) Se \(N \) è una foglia e
1.1) \(j(N) = 1 \) il giocatore 1 vince la partita,
1.2) \(j(N)=2 \) il giocatore 2 vince la partita.
2) Se \(N\) non è una foglia e
2.1) \(j(N) =1 \) il giocatore 1 sposta il pedone su un figlio del nodo \(N\) di sua scelta.
2.2) \( j(N) = 2 \) il giocatore 2 sposta il pedone su un figlio del nodo \(N\) di sua scelta.
Definizione 2 strategia:
Una strategia per il giocatore \(1\) nel gioco associato al albero di gioco \( (T,j) \) è un sottoinsieme di \( \sigma \) di \(T\) (un albero in effetti) tale che
1) la radice di \(T\) appartiene a \( \sigma \)
2) Per tutti i nodi \( N \) in \( \sigma \) che non sono una foglia
2.1) Se \( j(N) = 1 \) allora uno figlio di \( N\) e uno solo appartiene a \( \sigma \).
2.2) Se \( j(N) = 2 \) allora tutti i figli di \(N \) appartengono a \( \sigma \)
In modo analogo definiamo una strategia per il giocatore \(2\).
Definizione 3 strategia vincente:
Una strategia \( \sigma \) è una strategia vincente per il giocatore \(1\) se per tutte le foglie \( F \) di \( \sigma \) abbiamo \(j(F) =1 \). Analogamente per il giocatore \(2\).
Definizione 4 Albero duale:
Per tutti gli alberi di gioco \( T=(T,j) \) definiamo l'albero di gioco duale \(T^{\delta} = (T,j^{\delta} \) dove \( j^{\delta}(N)=1 \) se e solo se \(j(N) = 2 \).
Teorema Sia \( (T,j) \) un albero di gioco. Esiste una strategia vincente per uno dei due giocatori.
Dimostrazione: lunga
Definizione 5 Gioco della valutazione di una formula:
Sia \( L = \{ c_i, f_j^{n_j}, R_k^{n_k} \} \) un linguaggio e \( \mathcal{M} = \left< M, c_i^{\mathcal{M}}, (f_j^{n_j})^{\mathcal{M}}, (R_k^{n_k})^{\mathcal{M}} \right> \) una \(L\)-struttura e \( \varphi \) una formula chiusa su questo linguaggio i cui connettori appartengono a \( \{ \neg, \wedge, \vee \} \). Definiamo il gioco di valutazione della formula \( \varphi \) in \( M \) notato \( \mathbb{E}\mathbb{V}(\mathcal{M},\varphi) \). È un giocatore a due giocatori ad informazione perfetta, ai due giocatori attribuiamo il ruolo di verificatore \(V\) e falsificatore \(F\). Il primo giocatore comincia nel ruolo di Verificatore. Per ricorrenza definiamo l'insieme delle mosse possibili a partire dalle regole seguenti:
1) Se \( \varphi \) è una formula atomica il gioco finisce.
2) Se \( \varphi = \exists x \psi \) è il turno di \(V\) che sceglie un elemento \( a \in M \), il gioco continua con \( \psi[a/x] \).
3) Se \( \varphi = \forall x \psi \) è il turno di \(F\)che sceglie un elemento \( a \in M \), il gioco continua con \( \psi[a/x] \).
4) Se \( \varphi = \varphi_1 \vee \varphi_2 \) è il turno di \(V\) che sceglie \( \varphi_1\) oppure \( \varphi_2 \), il gioco continua con la formula scelta da \(V\).
5) Se \( \varphi = \varphi_1 \wedge \varphi_2 \) è il turno di \(F\) che sceglie \( \varphi_1\) oppure \( \varphi_2 \), il gioco continua con la formula scelta da \(F\).
6) Se \( \varphi= \neg \psi \), scambiamo i ruoli di \(V\) e \(F\), il gioco continua con \( \psi \).
L'obbiettivo di questo gioco è finire su una formula atomica \( R(t_1,\ldots,t_n ) \) con \( \mathcal{M} \models R(t_1,\ldots,t_n) \) avente il ruolo di Verificatore oppure tale che \( \mathcal{M} \not\models R(t_1,\ldots,t_n) \) avendo il ruolo di Falsificatore.
NB: Consdierare le formule solo con connettori \( \{ \neg, \vee, \wedge \} \) non è restrittivo.
Definizione 5 Albero del gioco di valutazione:
Ci fissiamo in un linguaggio \(L\), \( \varphi[x_0,\ldots,x_n] \) una formula su questo linguaggio i cui connettivi sono in \( \{ \neg, \vee, \wedge \} \) e le variabili libere sono tra \( x_0, \ldots, x_n \) e \( \mathcal{M}_{x_0 \rightarrow a_0, \ldots, x_n \rightarrow a_n} \) una \(L\)-struttura con interpretazioni in \( \left| \mathcal{M} \right| \) di variabili \( x_0, \ldots, x_n \). Definiamo l'albero del gioco \( T(\varphi[x_0,\ldots,x_n], \mathcal{M}_{x_0 \rightarrow a_0, \ldots, x_n \rightarrow a_n}) \) o per alleggerire la notazione \( T(\varphi, \mathcal{M} ) \) associato alla formula \( \varphi[x_0,\ldots, x_n ] \) nella struttura \( \mathcal{M}_{x_0 \rightarrow a_0, \ldots, x_n \rightarrow a_n} \) per induzione sull'altezza di \( \varphi \) come segue:
1) Se \( \varphi \) è una formula atomica
1.1 ) Se \( \mathcal{M}_{x_0 \rightarrow a_0, \ldots, x_n \rightarrow a_n} \models \varphi \) allora \( T(\varphi, \mathcal{M}) = V \)
1.2) Se \( \mathcal{M}_{x_0 \rightarrow a_0, \ldots, x_n \rightarrow a_n} \not\models \varphi \) allora \( T(\varphi, \mathcal{M}) = F \)
2) Se \( \varphi = \varphi_1 \vee \varphi_2 \) allora \[ T(\varphi,\mathcal{M} ) = T(\varphi_1, \mathcal{M}) \leftarrow V \rightarrow T(\varphi_2, \mathcal{M} ) \] (il nodo è V e i figli sono i due alberi di \( \varphi_1 \) e \( \varphi_2 \) ho provato a usare xymatrix ma mi dice "unparseable or potentially dangerous latex formula")
3) Se \( \varphi = \varphi_1 \wedge \varphi_2 \) allora \[ T(\varphi,\mathcal{M} ) = T(\varphi_1, \mathcal{M}) \leftarrow F \rightarrow T(\varphi_2, \mathcal{M} ) \]
4) Se \( \varphi = \exists x \psi \) allora per ogni \(m \in M \) \[ T(\varphi,\mathcal{M} ) = V \rightarrow T(\psi, \mathcal{M}_{x \rightarrow m} ) \]
5) Se \( \varphi = \forall x \psi \) allora per ogni \(m \in M \) \[ T(\varphi,\mathcal{M} ) = F \rightarrow T(\psi, \mathcal{M}_{x \rightarrow m} ) \]
6) Se \( \varphi = \neg \psi \) allora
\[ T(\varphi,\mathcal{M}) = ( T(\psi, \mathcal{M} )^{\delta} \]
dove \( T^{ \delta} \) è l'albero duale. I giocatori 1 e 2 sono chiamati V e F.
Definizione 6 Valutazione di una formula:
Sia \( \varphi \) una formula e \( \mathcal{M } \) una \(L\)-struttura come in precedenza. Diciamo che \( \varphi \) è soddisfatta in \( \mathcal{M} \) e lo notiamo \( \mathcal{M} \models \varphi \) se e solo se nel gioco \( \mathbb{E}\mathbb{V}(\mathcal{M},\varphi) \) il giocatore che comincia nel ruolo di verificatore possiede una strategia vincente. In modo equivalente \( \mathcal{M} \models \varphi \) se e solo se il verificatore possiede una strategia vincente nel albero \( T(\varphi,\mathcal{M} \). In caso contrario \( \mathcal{M} \not\models \varphi \).
Teorema Le due definizioni di valutazione di una formula sono equivalenti.
La dimostrazione è lunga, noiosa e facile. Consiste nel dimostrare che
\[ \mathcal{M} \models \varphi \Leftrightarrow \text{ il verificatore possiede una strategia vincente} \]
\[ \mathcal{M} \not\models \varphi \Leftrightarrow \text{ il falsificatore possiede una strategia vincente} \]
e si fa per induzione sull'altezza della formula \( \varphi \).
Comunque penso di essere riuscito a risolvere il mio problema iniziale
Credo che il mio errore fosse che ritenevo la strategia dipendente dal valore \(a\) scelto dal falsificatore, ovvero che a dipendenza del valore che sceglieva il verificatore doveva scegliere il ramo di destra o di sinistra, ma credo che non sia così.
Supponiamo che nell'albero del gioco \( \mathbb{E}\mathbb{V}(\mathcal{M}, \forall x \neg \varphi \vee \psi ) \) il verificatore possiede una strategia vincente \( \sigma \).
In \( T(\forall x \neg \varphi \vee \psi, \mathcal{M}) \) incomincia il verificatore, se la strategia vincente è entrare nell'albero \( T(\psi,\mathcal{M}) \) ci va e possiede una strategia vincente \( \tau \) la segue e vince. Nel albero del gioco \( \mathbb{E}\mathbb{V}(\mathcal{M}, \forall x (\neg \varphi \vee \psi) ) \) abbiamo che inizia il falsificatore e per qualunque \(a \in \left| \mathcal{M} \right| \) scelto va dal verificatore. Ora il verificatore entra in \( T( \psi,\mathcal{M}_{x \rightarrow a} ) \) poi segue \( \tau \) e vince.
Se \( \sigma \) è passare al falsificatore allora per qualunque \(a \in \left| \mathcal{M} \right| \) scelto dal falsificatore va nell'albero \( T( \varphi,\mathcal{M}_{x \rightarrow a} )^{\delta} \) e il verificatore vince con una strategia. Nell'altro albero abbiamo che per qualunque \(a \in \left| \mathcal{M} \right| \) scelto dal falsificatore il turno passa al verificatore che entra in \( T( \varphi,\mathcal{M}_{x \rightarrow a} )^{\delta} \) e vince.
Supponiamo ora che nell'albero \( \mathbb{E}\mathbb{V}(\mathcal{M}, \forall x (\neg \varphi \vee \psi) ) \) il verificatore abbia una strategia vincente \( \sigma \). Poiché inizia il falsificatore, scegliere qualunque \( a \in \left| \mathcal{M} \right| \) ma per qualunque \(a \) il falsificatore sceglie abbiamo che il verificatore possiede una strategia vincente.
Supponiamo che sia scegliere \( T(\psi, \mathcal{M}_{x \rightarrow a}) \), allora vuol dire che il verificatore possiede una strategia vincente \( \tau \) in \( T(\psi, \mathcal{M}) \) per arbitrarietà di \(a \) scelto dal falsificatore. Quindi nel albero del gioco \( \mathbb{E}\mathbb{V}(\mathcal{M}, \forall x \neg \varphi \vee \psi) ) \) abbiamo che il verificatore entra in \( T(\psi,\mathcal{M}) \) e vince.
Supponiamo che \( \sigma \) sia scegliere di entrare in \( T(\varphi, \mathcal{M}_{x \rightarrow a})^{\delta} \), allora nel albero del gioco \( \mathbb{E}\mathbb{V}(\mathcal{M}, \forall x \neg \varphi \vee \psi) ) \) abbiamo che il verificatore va dal falsificatore ma per qualunque \( a \in \left| \mathcal{M} \right| \) entrando in \( T(\varphi, \mathcal{M}_{x \rightarrow a})^{\delta} \) il verificatore vince.
Questo dimostra che \( \mathcal{M} \models ( ( \forall x \neg \varphi \vee \psi) \leftrightarrow \forall x (\neg \varphi \vee \psi)) \) e per arbitrarietà della \( L\)-struttura considerata abbiamo che \( ( \forall x \neg \varphi \vee \psi) \equiv \forall x (\neg \varphi \vee \psi) \)
Credo che il mio errore fosse che ritenevo la strategia dipendente dal valore \(a\) scelto dal falsificatore, ovvero che a dipendenza del valore che sceglieva il verificatore doveva scegliere il ramo di destra o di sinistra, ma credo che non sia così.
Supponiamo che nell'albero del gioco \( \mathbb{E}\mathbb{V}(\mathcal{M}, \forall x \neg \varphi \vee \psi ) \) il verificatore possiede una strategia vincente \( \sigma \).
In \( T(\forall x \neg \varphi \vee \psi, \mathcal{M}) \) incomincia il verificatore, se la strategia vincente è entrare nell'albero \( T(\psi,\mathcal{M}) \) ci va e possiede una strategia vincente \( \tau \) la segue e vince. Nel albero del gioco \( \mathbb{E}\mathbb{V}(\mathcal{M}, \forall x (\neg \varphi \vee \psi) ) \) abbiamo che inizia il falsificatore e per qualunque \(a \in \left| \mathcal{M} \right| \) scelto va dal verificatore. Ora il verificatore entra in \( T( \psi,\mathcal{M}_{x \rightarrow a} ) \) poi segue \( \tau \) e vince.
Se \( \sigma \) è passare al falsificatore allora per qualunque \(a \in \left| \mathcal{M} \right| \) scelto dal falsificatore va nell'albero \( T( \varphi,\mathcal{M}_{x \rightarrow a} )^{\delta} \) e il verificatore vince con una strategia. Nell'altro albero abbiamo che per qualunque \(a \in \left| \mathcal{M} \right| \) scelto dal falsificatore il turno passa al verificatore che entra in \( T( \varphi,\mathcal{M}_{x \rightarrow a} )^{\delta} \) e vince.
Supponiamo ora che nell'albero \( \mathbb{E}\mathbb{V}(\mathcal{M}, \forall x (\neg \varphi \vee \psi) ) \) il verificatore abbia una strategia vincente \( \sigma \). Poiché inizia il falsificatore, scegliere qualunque \( a \in \left| \mathcal{M} \right| \) ma per qualunque \(a \) il falsificatore sceglie abbiamo che il verificatore possiede una strategia vincente.
Supponiamo che sia scegliere \( T(\psi, \mathcal{M}_{x \rightarrow a}) \), allora vuol dire che il verificatore possiede una strategia vincente \( \tau \) in \( T(\psi, \mathcal{M}) \) per arbitrarietà di \(a \) scelto dal falsificatore. Quindi nel albero del gioco \( \mathbb{E}\mathbb{V}(\mathcal{M}, \forall x \neg \varphi \vee \psi) ) \) abbiamo che il verificatore entra in \( T(\psi,\mathcal{M}) \) e vince.
Supponiamo che \( \sigma \) sia scegliere di entrare in \( T(\varphi, \mathcal{M}_{x \rightarrow a})^{\delta} \), allora nel albero del gioco \( \mathbb{E}\mathbb{V}(\mathcal{M}, \forall x \neg \varphi \vee \psi) ) \) abbiamo che il verificatore va dal falsificatore ma per qualunque \( a \in \left| \mathcal{M} \right| \) entrando in \( T(\varphi, \mathcal{M}_{x \rightarrow a})^{\delta} \) il verificatore vince.
Questo dimostra che \( \mathcal{M} \models ( ( \forall x \neg \varphi \vee \psi) \leftrightarrow \forall x (\neg \varphi \vee \psi)) \) e per arbitrarietà della \( L\)-struttura considerata abbiamo che \( ( \forall x \neg \varphi \vee \psi) \equiv \forall x (\neg \varphi \vee \psi) \)
Grazie, 3m0o, leggerò con attenzione appena possibile.
Scusa se ti ho costretto a ricopiare pagine di appunti, ma non sapevo: credevo avessi un riferimento bibliografico pronto all'uso.
Scusa se ti ho costretto a ricopiare pagine di appunti, ma non sapevo: credevo avessi un riferimento bibliografico pronto all'uso.
Accedi a tutti gli appunti
Tutor AI: studia meglio e in meno tempo