[Logica dei predicati] esercizi sugli assiomi di uguaglianza
Ciao a tutti, sto studiando logica dal libro "Logica: metodo breve" di Mundici.
Non sono sicuro su come ho svolto il primo esercizio del capitolo 15, per cui vi chiedo gentilmente di dare un'occhiata.
L'esercizio chiede di formalizzare queste frasi in clausole con uguaglianza:
a) Se Clementina è la nonna materna di Luisa, allora è anche la mamma di Filippo e di Marta.
b) Se un solo giocatore ha fatto tredici, allora almeno due giocatori hanno fatto dodici.
Cosa ne pensate?
Grazie in anticipo a chi risponderà.
[cut; motivo: risolto]
Non sono sicuro su come ho svolto il primo esercizio del capitolo 15, per cui vi chiedo gentilmente di dare un'occhiata.
L'esercizio chiede di formalizzare queste frasi in clausole con uguaglianza:
a) Se Clementina è la nonna materna di Luisa, allora è anche la mamma di Filippo e di Marta.
b) Se un solo giocatore ha fatto tredici, allora almeno due giocatori hanno fatto dodici.
Cosa ne pensate?
Grazie in anticipo a chi risponderà.
[cut; motivo: risolto]
Risposte
Aggiornamento: sono riuscito a trovare una refutazione per il secondo esercizio, per cui lo elimino.
Resto in attesa di qualcuno che dipani i miei dubbi sul primo.
Resto in attesa di qualcuno che dipani i miei dubbi sul primo.
Nel primo esercizio scriverei nonna = mamma di mamma dal momento che specifica che e' nonna materna.
Quindi mi verrebbe una cosa del genere (uso $a$ per la costante Marta):
\[
(c = m(m(l))) \to (c = m(f), c = m(a))
\]
che in clausole diventa
\[
\{c \ne m(m(l)), c=m(f)\} \{c \ne m(m(l)),c=m(f) \}
\]
Per la seconda parte credo di aver sbagliato qualcosa, dal momento che mi vengono molti quantificatori esistenziali e il processo di skolemizzazione sul libro che hai citato viene trattato dopo gli assiomi dell'uguaglianza. Comunque, prendendo "un solo" come "ne esiste uno ed e' unico" (piuttosto che "se ne esiste uno, allora e' unico" come piacerebbe a me, ma in questo modo otterremo pure una variabile libera), ottengo qualcosa del genere
\[
(\exists (x : Tx \wedge \forall y (Ty \to y = x))) \to (\exists z \exists w: (z \ne w,Dy,Dw)),
\]
che una volta portato in PNF va skolemizzato prima di poter essere scritto in clausole.
Quindi mi verrebbe una cosa del genere (uso $a$ per la costante Marta):
\[
(c = m(m(l))) \to (c = m(f), c = m(a))
\]
che in clausole diventa
\[
\{c \ne m(m(l)), c=m(f)\} \{c \ne m(m(l)),c=m(f) \}
\]
Per la seconda parte credo di aver sbagliato qualcosa, dal momento che mi vengono molti quantificatori esistenziali e il processo di skolemizzazione sul libro che hai citato viene trattato dopo gli assiomi dell'uguaglianza. Comunque, prendendo "un solo" come "ne esiste uno ed e' unico" (piuttosto che "se ne esiste uno, allora e' unico" come piacerebbe a me, ma in questo modo otterremo pure una variabile libera), ottengo qualcosa del genere
\[
(\exists (x : Tx \wedge \forall y (Ty \to y = x))) \to (\exists z \exists w: (z \ne w,Dy,Dw)),
\]
che una volta portato in PNF va skolemizzato prima di poter essere scritto in clausole.
Grazie per la risposta.
Per il punto a, anch'io inizialmente l'avevo scritta così, poi ho pensato che l'autore volesse una clausola unica.
Dunque non c'è nulla che vieti di formalizzare una "frase" in un insieme di clausole predicative?
Se è così, dimmi cosa ne pensi di questo ragionamento per il secondo esercizio:
\[
\exists x (Tx \wedge (Ty \to y = x)) \to ( (Dw \wedge Dz) \to w \neq z)
\]
che in clausole diventa (se non ho scritto castronerie):
\[
\{ \neg Tx, \neg Ty \neg Uw, \neg Uz, w \neq z \}, \{ \neg Tx, y \neq x, \neg Uw, \neg Uz, w \neq z \}
\]
Per il punto a, anch'io inizialmente l'avevo scritta così, poi ho pensato che l'autore volesse una clausola unica.
Dunque non c'è nulla che vieti di formalizzare una "frase" in un insieme di clausole predicative?
Se è così, dimmi cosa ne pensi di questo ragionamento per il secondo esercizio:
\[
\exists x (Tx \wedge (Ty \to y = x)) \to ( (Dw \wedge Dz) \to w \neq z)
\]
che in clausole diventa (se non ho scritto castronerie):
\[
\{ \neg Tx, \neg Ty \neg Uw, \neg Uz, w \neq z \}, \{ \neg Tx, y \neq x, \neg Uw, \neg Uz, w \neq z \}
\]
Da dove arriva la traduzione dal linguaggio naturale a quello che hai scritto? Non mi ritrovo con la seconda parte...
Credo che in generale, formalizzare in clausole, vuol dire tradurre dal linguaggio naturale a una CNF, pronta per poter essere refutata.
Credo che in generale, formalizzare in clausole, vuol dire tradurre dal linguaggio naturale a una CNF, pronta per poter essere refutata.
Ho modificato il precedente post.
L'idea (nella parte a destra dell'implicazione) è che se due qualsiasi w e z hanno fatto dodici, allora w e z non sono la stessa persona.
Non è una corretta traduzione?
Ottimo.
EDIT: visto che siamo in tema e non vorrei aprire un topic solo per una richiesta, mi potresti consigliare una buona risorsa per i tableaux nella logica del primo ordine? nel libro di Mundici non ci sono. Io come base ho studiato questo capitolo del fantastico libro di Smullyan.
L'idea (nella parte a destra dell'implicazione) è che se due qualsiasi w e z hanno fatto dodici, allora w e z non sono la stessa persona.
Non è una corretta traduzione?
"Pappappero":
Credo che in generale, formalizzare in clausole, vuol dire tradurre dal linguaggio naturale a una CNF, pronta per poter essere refutata.
Ottimo.
EDIT: visto che siamo in tema e non vorrei aprire un topic solo per una richiesta, mi potresti consigliare una buona risorsa per i tableaux nella logica del primo ordine? nel libro di Mundici non ci sono. Io come base ho studiato questo capitolo del fantastico libro di Smullyan.
Nella tua traduzione credo che le variabili vadano quantificate. Ci vuole un $\forall y$ nella parte sinistra prima che $y$ compaia e a destra penso che ci vogliano degli $\exists w$ ed $\exists z$.
A questo punto porterei tutto in PNF, skolemizzerei e a quel punto abbiamo le clausole che vogliamo.
Purtroppo non so niente del metodo dei tableaux.
A questo punto porterei tutto in PNF, skolemizzerei e a quel punto abbiamo le clausole che vogliamo.
Purtroppo non so niente del metodo dei tableaux.
D'accordo per il quantificatore universale a sinistra, ma può essere omesso, no?
A destra, alla fine credo che tu abbia ragione.
A questo punto sono ancora più curioso di capire se esiste un modo per formalizzare quella frase senza passare per PNF e skolemizzazione, come abbiamo considerato plausibile dato l'ordine dei capitoli del libro, oppure se è l'autore l'ha "erroneamente" posizionata lì.
Grazie della tua disponibilità.
A destra, alla fine credo che tu abbia ragione.
A questo punto sono ancora più curioso di capire se esiste un modo per formalizzare quella frase senza passare per PNF e skolemizzazione, come abbiamo considerato plausibile dato l'ordine dei capitoli del libro, oppure se è l'autore l'ha "erroneamente" posizionata lì.
Grazie della tua disponibilità.
Accedi a tutti gli appunti
Tutor AI: studia meglio e in meno tempo