Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s))...

76
Qualche esempio di tableaux pp. 29-30

Transcript of Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s))...

Page 1: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Qualche esempio di tableaux

pp. 29-30

Page 2: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Esercizio n. 2

• Si parte dalla formula

(x(U(x) M(x)) U(s)) M(s)

Page 3: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

• La si nega (cioè: si scrive la formula per intero tra due parentesi e davanti si pone la negazione):

¬((x(U(x) M(x)) U(s)) M(s))

Page 4: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

È in fnn(forma normale negativa)?

NO, perché

contiene il simbolo dell’implicazione e

Il simbolo di negazione non compare sempre “attaccato” ad un simbolo di predicato.

Page 5: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

ALLORA

Dobbiamo applicare le regole di riscrittura

(di p. 25, cui è utile aggiungere, per snellire i conti, anche quella relativa alla negazione dell’implicazione – che riportiamo qua per prima)

Page 6: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Regole di riscrittura

1) ¬(CD) ~~> (C ¬D)

2) (CD) ~~> (¬C D)

3) ¬¬C ~~> C

4) ¬(C D) ~~> (¬C ¬D)

5) ¬(C D) ~~> (¬C ¬D)

6) ¬xC ~~> x ¬C

7) ¬xC ~~> x ¬C

Page 7: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

La nostra formula

• è del tipo ¬(CD), dove

• “C” è x(U(x) M(x)) U(s)

e

• “D” è M(s)

Page 8: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Dunque applichiamo la regola 1)

• Ottenendo:

• C ¬D.

cioè

• (x(U(x) M(x)) U(s)) ¬M(s).

Page 9: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Ora applichiamo la regola 2)

DENTRO la formula precedente:(x(U(x) M(x)) U(s)) ¬M(s)aU(x) M(x)E otteniamo¬ C D

Cioè(x (¬U(x) M(x)) U(s)) ¬M(s).

Page 10: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

(x (¬U(x) M(x)) U(s)) ¬M(s)è in fnn

Dunque ora si può partire a costruire l’albero di refutazione (=il tableau)

applicando le regole di espansione di p. 28

Page 11: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

CB

CB

,,

,

CB

CB

,,

,

Regole di espansione

))/(,

,

xcB

xB

xBxtB

xB

),/(,

,

Page 12: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

In quale ordine applicare le regole?

Quello in cui sono state presentate:

Congiunzione, disgiunzione, quantificatore esistenziale, quantificatore universale

Page 13: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

ATTENZIONE

• Quando si applicano le regole di riscrittura sé può (anzi, si deve) guardare dentro le parentesi (per scoprire qual è il connettivo principale e applicare le regola opportuna).

• INVECE, quando si applicano le regole di espansione E’ ASSOLUTAMENTE VIETATO GUARDARE DENTRO LE PARENTESI per applicare le regole ai connettivi principali che vi stanno dentro.

Page 14: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Esempi

x(P(x) Qx) è una formula del tipo:xB.

Cioè occorre applicare ad essa la regole di espansione per il quantificatore universale e NON quella per la disgiunzione (che non siamo autorizzati a ‘vedere’ in quanto è chiusa tra parentesi)

x(Px) Q(x) è una formula del tipo: xB.

Cioè occorre applicare ad essa la regole di espansione per il quantificatore esistenziale e NON quella per la congiunzione (che non siamo autorizzati a ‘vedere’ in quanto è chiusa tra parentesi)

Page 15: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Che cosa significano le singole regole di espansione?

• Nella riga più in alto viene espressa la situazione del tableau al momento in cui andiamo ad operare. La formula contenente il connettivo o il quantificatore su cui si vuole operare è isolata tramite una virgola dal resto dell’espressione, che viene simboleggiato con Γ.

Page 16: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Esempio

• Per esempio, se troviamo scritto

Γ, P QSignifica che noi adesso stiamo per lavorare

sulla formula P Q, che ci compare eventualmente assieme ad altre formule Γ, separata da esse da una virgola.

Page 17: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

• Nella seconda riga, in basso, è segnato il funzionamento della regola, cioè quello che noi andremo effettivamente a scrivere applicando quella regola.

Page 18: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

In particolare

• Se abbiamo:

Γ, P Q__________

• Γ, P , Q

Page 19: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

significherà

• che, se vogliamo lavorare su una congiunzione,

• Semplicemente alla riga successiva scriveremo tutto il resto dell’espressione (cioè Γ) e poi i due congiunti separati da una virgola.

Page 20: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

disgiunzione

• Se abbiamo

• Γ, P Q• ---------------

• Γ, P |Γ, Q

Page 21: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

significa

• che, se vogliamo lavorare su una disgiunzione,• alla riga successiva opereremo una biforcazione

della nostra diramazione e su un ramo scriveremo tutto il resto dell’espressione (senza la disgiunzione,cioè Γ) con uno dei disgiunti (P, separato da una virgola); sull’altro ramo scriveremo di nuovo tutto il resto dell’espressione (senza la disgiunzione,cioè Γ) e poi l’altro disgiunto (Q, separato da una virgola).

Page 22: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Quantificatore esistenziale

• Γ, xB

• ----------

• Γ, B(c/x)

Page 23: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

significa

• che, se vogliamo lavorare su un quantificatore esistenziale,

• alla riga successiva trascriveremo il resto dell’espressione (cioè Γ) e poi, separata da una virgola, l’esemplificazione del quantificatore, cioè non si scrive x, ma solo quanto viene dopo, sostituendo in esso la x con un simbolo di costante NUOVO

Page 24: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Per esempio

• Γ, x(P(x) Q(x))

• Diventa

• Γ, P(c) Q(c)

• Purché c non sia mai stata usata prima

Page 25: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Quantificatore universale

• Γ, xB

• ----------

• Γ, xB ,B(t/x)

Page 26: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

significa

• che, se vogliamo lavorare su un quantificatore universale,

• alla riga successiva trascriveremo tutta l’espressione (cioè sia Γ sia xB) e poi, separata da una virgola, IN AGGIUNTA, l’esemplificazione del quantificatore, cioè non si scrive (un’altra volta!) x, ma solo quanto viene dopo, sostituendo in esso la x con un simbolo di costante possibilmente VECCHIO.

Page 27: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Per esempio

• Γ, x(P(x) Q(x))

• diventa

• Γ, x(P(x) Q(x)), P(a) Q(a)

• Dove ‘a’ è una costante già presente nella dimostrazione (possibilmente, per ragioni di economicità, cioè per rendere più breve la dimostrazione).

Page 28: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Torniamo alla formula che stavamo considerando

Cioè a

(x (¬U(x) M(x)) U(s)) ¬M(s)

Page 29: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Applichiamo la regola per la congiunzione una prima volta

Su

(x (¬U(x) M(x)) U(s)) ¬M(s)

ottenendo:x (¬U(x) M(x)) U(s) , ¬M(s)

Page 30: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Una precisazione sulle parentesi

• Quando siamo passati da(x (¬U(x) M(x)) U(s)) ¬M(s)

ax (¬U(x) M(x)) U(s) , ¬M(s)

abbiamo tolto le parentesi qui segnate in verde, perché esse servivano solo a chiarire che l’espressione che contenevano formava un tutto unico (che si aggiungeva a ¬M(s) ) ed era una congiunzione di x (¬U(x) M(x)) e U(s).

Quando ¬M(s) compare preceduto da una virgola, non c’è più bisogno di precisare che è separato da ciò che sta prima di esso, che è un’unica formula (cioè x (¬U(x) M(x)) U(s) ) per suo conto.

Page 31: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

E una seconda

• Su

x (¬U(x) M(x)) U(s), ¬M(s)

• Ottenendo

x (¬U(x) M(x)), U(s), ¬M(s)

Page 32: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Applichiamo la regola per il quantificatore universale

E otteniamo:

x (¬U(x) M(x)), U(s), ¬M(s),

¬U(s) M(s).

Page 33: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Applichiamo la regola per la disgiunzione

• in x (¬U(x) M(x)), U(s), ¬M(s), ¬U(s) M(s).

e otteniamo la biforcazione:x (¬U(x) M(x)), U(s), ¬M(s), ¬U(s) e x (¬U(x) M(x)), U(s), ¬M(s), M(s)

Page 34: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

• In

x (¬U(x) M(x)), U(s), ¬M(s), ¬U(s)

notiamo la contraddizione in rosso e, dunque, chiudiamo il ramo.

In

x (¬U(x) M(x)), U(s), ¬M(s), M(s)

notiamo la contraddizione in rosso e, dunque, chiudiamo il ramo.

Page 35: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

ATTENZIONE

• C’è contraddizione solo quando si hanno due formule di cui una sia atomica e l’altra la sua negazione SEPARATE DA UNA VIRGOLA.

Page 36: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Per esempio

• C’è contraddizione se ho le due contraddittorie:

• P(x), ¬ P(x)

• Non c’è contraddizione se ho:

• P(x), ¬ P(x) Q(x)

perché ¬ P(x) appare dentro una congiunzione, non è tra due virgole.

Page 37: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Osserviamo

• Che entrambi i nodi finali dell’albero “chiudono”, cioè terminano con una contraddizione e, dunque, dichiariamo insoddisfacibile l’enunciato:

(x (¬U(x) M(x)) U(s)) ¬M(s)

che costituiva la fnn di

Page 38: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

¬(x(U(x) M(x)) U(s)) M(s))

Se questo è insoddisfacibile, allora risulta essere logicamente valido

l’enunciato di partenza:

x (¬U(x) M(x)) U(s)) ¬M(s)

Page 39: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Nuovo esempio di tableau3)

Si parte da

(x(P(x)Q(x)) (xP(x) xQ(x))

Page 40: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Lo si nega

• Ottenendo:

¬((x(P(x)Q(x))) (xP(x) xQ(x))).

Page 41: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

È in fnn(forma normale negativa)?

NO, perché

contiene il simbolo dell’implicazione e

Il simbolo di negazione non compare sempre “attaccato” ad un simbolo di predicato.

Page 42: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

ALLORA

• Dobbiamo applicare le regole di riscrittura

Page 43: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

La nostra formula

È del tipo ¬(CD), dove

“C” è x(P(x)Q(x))

e

“D” è xP(x) xQ(x)

Page 44: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Dunque applichiamo la regola 1)

e otteniamo:

C ¬D

cioè

x(P(x)Q(x)) ¬ (xP(x) xQ(x))

Page 45: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Applichiamo la regola 5)

A

x(P(x)Q(x)) ¬ (xP(x) xQ(x))

sul secondo membro della formula (evidenziato in blu),

Ottenendo

x(P(x)Q(x)) (¬xP(x) ¬xQ(x)).

Page 46: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Applichiamo la regola 6)

A

x(P(x)Q(x)) (¬xP(x) ¬xQ(x)).

alle sottoformule evidenziate in blu

ottenendo:

x(P(x)Q(x)) (x¬P(x) x¬Q(x)).

Page 47: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

x(P(x)Q(x)) (x¬P(x) x¬Q(x))è in fnn

Dunque ora si può partire a costruire l’albero di refutazione (=il tableau)

applicando le regole di espansione di p. 28

Page 48: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

applichiamo la regola per la congiunzione

Su

x(P(x)Q(x)) (x¬P(x) x¬Q(x))

e otteniamox(P(x)Q(x)), x¬P(x) x¬Q(x)

Page 49: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Poi applichiamo la regola per la disgiunzione

a

x¬P(x) x¬Q(x)

Ottenendo la biforcazione:

1) x(P(x)Q(x)), x¬P(x)

2) x(P(x)Q(x)), x¬Q(x)

Page 50: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Cominciamo ad occuparci del ramo che contiene la 1)

Page 51: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

applichiamo ad essa la regola per l’esistenziale

Da

x(P(x)Q(x)), x¬P(x)

otteniamo

x(P(x)Q(x)), ¬P(a).

Page 52: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Applichiamo ora la regola per il quantificatore universale

• Da

x(P(x)Q(x)), ¬P(a).

Otteniamox(P(x)Q(x)), P(a) Q(a) , ¬P(a) .

Page 53: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Applichiamo ora la regola per la congiunzione

• Su

• P(a) Q(a)

• In x(P(x)Q(x)), P(a) Q(a) , ¬P(a) .

• Ottenendox(P(x)Q(x)), P(a) , Q(a) , ¬P(a)

Page 54: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Questo nodo

• Contiene una contraddizione (P(a) e ¬P(a)).

• Dunque chiude

Page 55: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Passiamo ad occuparci del ramo

che contiene la 2)

Page 56: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

applichiamo ad essa la regola per l’esistenziale

Da

x(P(x)Q(x)), x¬Q(x)

otteniamo

x(P(x)Q(x)), ¬Q(a).

Page 57: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Applichiamo ora la regola per il quantificatore universale

• Da

x(P(x)Q(x)), ¬Q(a).

Otteniamox(P(x)Q(x)), P(a) Q(a) , ¬Q(a) .

Page 58: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Applichiamo ora la regola per la congiunzione

• Su

• P(a) Q(a)

• In x(P(x)Q(x)), P(a) Q(a) , ¬Q(a) .

• Ottenendox(P(x)Q(x)), P(a) , Q(a) , ¬Q(a).

Page 59: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Anche questo nodo

• Contiene una contraddizione (P(a) e ¬P(a)).

• Dunque chiude

Page 60: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Osserviamo

• Che entrambi i nodi finali dell’albero “chiudono”, cioè terminano con una contraddizione e, dunque, dichiariamo insoddisfacibile l’enunciato:

x(P(x)Q(x)) (x¬P(x) x¬Q(x))che costituiva la fnn di:

Page 61: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

¬((x(P(x)Q(x))) (xP(x) xQ(x))).

• Se questo è insoddisfacibile, allora

Risulta logicamente valido l’enunciato:

(x(P(x)Q(x))) (xP(x) xQ(x)).

Page 62: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Esempio 4

• Si parte dalla formula x(yP(y) P(x)).

Page 63: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

• La si nega ottenendo:

¬(x(yP(y) P(x)))

Che si può semplicemente scrivere come

¬x(yP(y) P(x))

Perché non esiste un’altra possibilità di lettura.

Page 64: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

È in fnn(forma normale negativa)?

NO, perché

contiene il simbolo dell’implicazione e

Il simbolo di negazione non compare sempre “attaccato” ad un simbolo di predicato.

Page 65: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

La nostra formula

È del tipo

¬xC,

Dove

C

è

yP(y) P(x))

Page 66: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Applichiamo dunque la regola di riscrittura 7)

• DA• ¬x(yP(y) P(x))

• OTTENIAMOx¬(yP(y) P(x))

Page 67: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Applichiamo la regola di riscrittura 1

• Alla sottoformula

¬(yP(y) P(x))

Inx¬(yP(y) P(x)) ,

dove

• C sarà yP(y) e D sarà P(x)

ottenendo:

Page 68: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

x(C ¬D)

cioè

x(yP(y) ¬P(x))

Page 69: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Questa è in fnn

Dunque ora si può partire a costruire l’albero di refutazione

applicando le regole di espansione

Page 70: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Applichiamo la regola di espansione del

quantificatore universale

• Ax(yP(y) ¬P(x))

• Ottenendox(yP(y) ¬P(x)), yP(y) ¬P(c).

Page 71: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Applichiamo la regola di espansione della congiunzione

inx(yP(y) ¬P(x)), yP(y) ¬P(c).

ottenendo:x(yP(y) ¬P(x)), yP(y), ¬P(c).

Page 72: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Ora applichiamo la regola di espansione del

quantificatore esistenziale

• Inx(yP(y) ¬P(x)), yP(y), ¬P(c).

• Ottenendox(yP(y) ¬P(x)), P(a), ¬P(c).

Page 73: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Riapplichiamo la regola di espansione del

quantificatore universale

in

x(yP(y) ¬P(x)), P(a), ¬P(c).

Ottenendo

x(yP(y) ¬P(x)), yP(y) ¬P(a), P(a), ¬P(c).

[la prima volta avevamo esemplificato il quantificatore universale con la costante “c”; ora l’abbiamo esemplificato con la costante “a” che era stata introdotta nel frattempo]

Page 74: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Applichiamo la regola della congiunzione

• In

x(yP(y) ¬P(x)), yP(y) ¬P(a), P(a), ¬P(c)

Ottenendo

x(yP(y) ¬P(x)), yP(y) , ¬P(a), P(a), ¬P(c)

Qui abbiamo la contraddizione P(a) e ¬ P(a),

Dunque il nodo chiude.

Page 75: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

Dunque

dichiariamo insoddisfacibile l’enunciato:

x(yP(y) ¬P(x))

che costituiva la fnn di

¬x(yP(y) P(x))

Page 76: Qualche esempio di tableaux pp. 29-30. Esercizio n. 2 Si parte dalla formula ( x(U(x) M(x)) U(s)) M(s)

• Se questo è insoddisfacibile, allora

risulta logicamente valido l’enunciato iniziale:

x(yP(y) P(x))