Universita di Bologna´sacerdot/linguaggi1011/lucidi/slides15.pdf · Dimostrazione: per induzione...

Deduzione naturale

Linguaggi

15: Deduzione naturale

Claudio Sacerdoti Coen<[email protected]>

Universita di Bologna

28/03/2011

Claudio Sacerdoti Coen

Deduzione naturale

Outline

1 Deduzione naturale


Deduzione naturale

Deduzione

Wikipedia: “. . . ”


Deduzione naturale

Deduzione naturale: sintassi

Definiamo ora la sintassi degli alberi (di prova) per la deduzionenaturale.

Note: in un albero di prova Γ Fla radice dell’albero e la conclusione Fle foglie dell’albero sono ipotesi scaricate [F ] o meno F

un’ipotesi non scaricata (o globale) F deve appartenere a Γun’ipotesi scaricata [F ] e un’ipotesi locale e deve essere“scaricata” da un qualche passo di inferenza

i nodi interni dell’albero debbono appartenere alla lista dipassi di inferenza che stiamo per elencare


Deduzione naturale

Deduzione naturale: passi di inferenza

Vi sono due tipi di passi di inferenza:1 Regole di introduzione di un connettivo:

ci dicono tutti i modi in cui concludere direttamente unaformula con in testa un determinato connettivocome concludo . . . ?

2 Regole di eliminazione di un connettivo:ci dicono tutti i modi in cui utilizzare direttamente un’ipotesicon in testa un determinato connettivocosa ricavo da . . . ?


Deduzione naturale


Usiamo la seguente sintassi per le regole di inferenza:

F1 . . .Fn

F(NOME REGOLA)

La formula F e la conclusione della regola.Le formule F1, . . . ,Fn sono le premesse della regola.

La premessa Fi verra indicata con[A]...

Fi

per indicare che e

possibile assumere localmente A per concludere Fi .

Una regola senza premesse (n = 0) si dice assioma.


Deduzione naturale

Deduzione naturale: alberi di deduzione

Gli alberi di deduzione vengono indicati componendoricorsivamente regole di inferenza. Esempio:

F1...FnH1

(regola1) . . . G1...GmHl

(regola2)

H(regola3)

Nell’esempio F1...FnH1

(regola1) e un sottoalbero dell’interoalbero di deduzione.

La struttura ricorsiva permette di definire funzioni per ricorsionestrutturale su alberi di deduzione e di effettuare prove perinduzione strutturale.


Deduzione naturale


Ogni passo di inferenza ammette sempre due letture:1 Bottom-up (dalle premesse alla conclusione):

date le premesse F1, . . . ,Fn, posso concludere F2 Top-down (dalla conclusione alle premesse):

per concludere F posso ridurmi a dimostrare F1, . . . ,Fn


Deduzione naturale

Deduzione naturale: correttezza e invertibilita

Definizione: una regola F1...FnF e corretta per la logica

classica/intuizionista quando F1, . . . ,Fn F (nella rispettivalogica).

Noi saremo interessati solamente a regole corrette.

Definizione: una regola F1...FnF e invertibile nella logica

classica/intuizionista quando per ogni i si ha F Fi (nellarispettiva logica).

L’invertibilita gioca un ruolo importante nella ricerca delle prove:se la regola e invertibile, puo essere sempre applicata nellaricerca top-down della prova.


Deduzione naturale

Deduzione naturale: ∧Regole di introduzione:

A BA ∧ B

(∧i )

Lettura bottom-up: se A e B allora A ∧ B.

Lettura top-down: per dimostrare A ∧ B debbo dimostrare sia Ache B.

Scrittura informale:. . . e quindi A. . . e quindi B[e quindi A ∧ B]

L’applicazione della regola viene spesso lasciata informalmenteimplicita.


Deduzione naturale

Deduzione naturale: ∧

Regole di introduzione:

A BA ∧ B

(∧i )

Correttezza classica: A,B A ∧ B in quanto, per ogni mondov , se [[A]]v = [[B]]v = 1 allora [[A ∧ B]]v = max{[[A]]v , [[B]]v} = 1.

Correttezza intuizionista: A,B A ∧ B in quando se a ∈ [[A]]v eb ∈ [[B]]v allora 〈a,b〉 ∈ [[A ∧ B]]v = [[A]]v × [[B]]v .

Invertibilita classica: se max{[[A]]v , [[B]]v} = 1 allora[[A]]v = [[B]]v = 1 e quindi A ∧ B A e A ∧ B B.

Invertibilita intuizionista: se c ∈ [[A]]v × [[B]]v allora c = 〈a,b〉 perqualche a ∈ [[A]]v e b ∈ [[B]]v e quindi A ∧ B A e A ∧ B B.


Deduzione naturale

Deduzione naturale: ∧Regola di eliminazione:

A ∧ B

[A][B]...C

C(∧e)

Lettura bottom-up: se A∧B e se ipotizzando A e B concludo C, alloraC.

Lettura top-down: per dimostrare C data l’ipotesi A ∧ B e sufficientedimostrare C sotto le ipotesi A e B.

Scrittura informale:. . . A ∧ B

[supponiamo A e anche B]. . . e quindi C

[e quindi C]L’applicazione della regola viene sempre lasciata implicita.


Deduzione naturale


Regola di eliminazione:

A ∧ B

[A][B]...C

C(∧e)

Nota: un albero di derivazione che termini applicando la regola∧e ha due sotto-alberi immediati. Il primo dimostra A ∧ B. Ilsecondo dimostra C usando, fra le altre, le ipotesi A e B NONANCORA SCARICATE. E l’applicazione della regola chescarica le ipotesi dal sotto-albero.


Deduzione naturale

Deduzione naturale: ∧Regola di eliminazione:

A ∧ B

[A][B]...C

C(∧e)

Correttezza classica: dimostriamo A ∧ B,A⇒ B ⇒ C C.Basta costruire la tabella di verita.

Correttezza intuizionista: dimostriamo A ∧ B,A⇒ B ⇒ C C.Sia 〈a,b〉 ∈ [[A ∧ B]]v e sia f ∈ [[A⇒ B ⇒ C]]v . Alloraf (a) ∈ [[B ⇒ C]]v e f (a)(b) = f (a,b) ∈ [[C]]v .

La regola non e invertibile. Esempio: C = > e A,B = ⊥.La regola e intuizionisticamente (e quindi anche classicamente)invertibile se si assume A ∧ B: ovvio.


Deduzione naturale


Regole alternative di eliminazione:

A ∧ BA

(∧e1)

A ∧ BB

(∧e2)

Lettura bottom-up: se A ∧ B allora A (e B).Lettura top-down: per dimostrare A (o B) bastadimostrare A ∧ B.Scrittura informale:. . . e quindi A ∧ B[e quindi A]Le due regole vengono quasi sempre omesse.


Deduzione naturale


Regole alternative di eliminazione:

A ∧ BA

(∧e1)

A ∧ BB

(∧e2)

Correttezza classica e intuizionista: le due regole sono corrette.

Le due regole non sono invertibili: esempio A = > e B = bot .


Deduzione naturale

Deduzione naturale: ricerca delle prove

Le prove si possono cercare in vari modi:1 Bottom-up: partendo dalle ipotesi si applicano in avanti le

regole fino a trovare la conclusione.Pro: non si commettono mai erroriCons: e molto difficile vedere le prove cosı perche vi sonotroppe strade che non portanto alla conclusione cercata

2 Top-down: partendo dalla conclusione si applicano indietrole regole fino a ridursi a un sottoinsieme delle ipotesi.

Pro: piu facile trovare le dimostrazioni se si sta attenti a nonsbagliarsi (= ridursi a dimostrare qualcosa di non vero)Cons: e possibile sbagliarsi quando si applicano regole noninvertibili

3 Strategia mista: si alternano le due strategie, tipicamentepartendo con una top-down.


Deduzione naturale


Come evitare errori?1 Dopo l’applicazione top-down di una regola di inferenza

non invertibile, accertarsi che la conclusione sia ancoraconseguenza logica delle premesse.

Esempio: per dimostrare A ∧ B ` A si parte da A e lo siriduce a A ∧ C. Si ha A ∧ B 6 A ∧ C (anche se A ∧ B A).

2 Verificare di non essersi ridotti a dimostrare qualcosa chesi sta gia dimostrando con le stesse ipotesi (ragionamentocircolare).

Esempio: per dimostrare A ci si riduce a dimostrare A ∧ Bche dimostriamo riducendoci a dimostrare sia A che B.


Deduzione naturale


Esercizi (esempi alla lavagna):A ∧ B ` B ∧ AA ∧ (B ∧ C) ` (A ∧ B) ∧ C(A ∧ B) ∧ (C ∧ D) ` A ∧ D ∧ A

Cercare le dimostrazioni sia usando ∧e che usando ∧e1 e ∧e2 .L’ultimo esercizio evidenzia la difficolta della ricerca bottom-updelle prove.


Deduzione naturale

Deduzione naturale: derivabilita

Definizione: un insieme di regole R e derivabile a partire da uninsieme di regole S quando per ogni regola in R le cuipremesse sono F1, . . . ,Fn e la cui conclusione e F si haF1, . . . ,Fn ` F usando solamente le regole in S.

Nota: e la stessa nozione chiamata in precedenza riducibilita.

Teorema: se R e derivabile a partire da S allora per ognidimostrazione ottenuta usando solo regole in R esiste unadimostrazione con le stesse premesse e conclusione che usasolo regole in S.Dimostrazione: per induzione strutturale sull’albero di derivazione.In tutti i casi, per ipotesi induttiva esistono alberi di derivazione perognuna delle premesse che usano solo regole in S. Per ipotesi esisteun albero di derivazione per la regola sotto esame che usa soloregole in S. Componendo gli alberi si ottiene la prova voluta.


Deduzione naturale

Deduzione naturale: derivabilita

Teorema: l’insieme {∧e1 ,∧e2} e derivabile a partire dall’insieme{∧e} e viceversa.Dimostrazione:

Prima parte: {∧e1 ,∧e2} e derivabile a partire da {∧e}.

A ∧ B [A]

A(∧e)

A ∧ B [B]

B(∧e)

Seconda parte: {∧e} e derivabile a partire da {∧e1 ,∧e2}.

A∧BA (∧e1) A∧B

B (∧e2)...C


Deduzione naturale

Deduzione naturale: ∨Regole di introduzione:

AA ∨ B

(∧i1)

BA ∨ B

(∧i2)

Lettura bottom-up: se A (B) vale, allora vale anche A ∨ B

Lettura top-down: per dimostrare A ∨ B e sufficiente dimostrareA (B)

Scrittura informale:. . . e quindi A[e quindi A ∨ B]

Il passo di deduzione viene spesso omesso.Claudio Sacerdoti Coen

Deduzione naturale

Deduzione naturale: ∨


AA ∨ B

(∧i1)

BA ∨ B

(∧i2)

Correttezza intuizionista (e quindi classica): A A ∨ B inquanto data a ∈ [[A]]v si ha 〈0,a〉 ∈ [[A ∨ B]]v

Le due regole non sono invertibili: per esempio quando A = ⊥e B = >


Deduzione naturale

Deduzione naturale: ∨Regole di eliminazione:

A ∨ B

[A]...C

[B]...C

C(∨e)

Lettura bottom-up: se vale A ∨ B e C vale sia quando vale A chequando vale B, allora necessariamente C vale.

Lettura top-down: per dimostrare qualunque cosa sapendo A ∨ B esufficiente procedere per casi, dimostrando la stessa cosaassumendo prima che A valga e poi che valga B

Scrittura informale:. . . e quindi A ∨ Bprocediamo per casi per dimostrare C

caso A: . . . e quindi Ccaso B: . . . e quindi C

[e quindi C]Claudio Sacerdoti Coen

Deduzione naturale

Deduzione naturale: ∨

Regole di eliminazione:

A ∨ B

[A]...C

[B]...C

C(∨e)

Correttezza intuizionista (e quindi classica): per ipotesi c ∈ [[A∨B]]v ef [x ] ∈ [[C]]v per x ∈ [[A]]v e g[y ] ∈ [[C]]v per y ∈ [[B]]v . Se c = 〈0,a〉dove a ∈ [[A]]v allora f [a/x ] ∈ [[C]]v . Se c = 〈1,b〉 dove b ∈ [[B]]v allorag[b/y ] ∈ [[C]]v .

Invertibilita: la regola non e invertibile (controesempio: C = > eA = B = ⊥. Tuttavia, quando A ∨ B e dimostrabile, allora la regola ebanalmente invertibile intuizionisticamente (e quindi ancheclassicamente). Infatti per ipotesi sia c ∈ [[C]]v e d ∈ [[A ∨ B]]v . Allorac ∈ [[C]]v anche senza usare nessun x ∈ [[A]]v o y ∈ [[B]]v .


Deduzione naturale


Esercizi (esempi alla lavagna):A ∧ B ` C ∨ AA ∨ B ` B ∨ AA ∨ (B ∨ C) ` (C ∨ B) ∨ A


Deduzione naturale

Deduzione naturale: ⊥

Regole di introduzione: NESSUNA.


⊥C

(⊥e)

Lettura bottom-up: dal falso segue qualunque cosa.

Lettura top-down: per dimostrare qualunque cosa possoridurmi a dimostrare un assurod.

Scrittura informale:. . . assurdoe quindi C


Deduzione naturale

Deduzione naturale: ⊥

Regole di introduzione: NESSUNA.


⊥C

(⊥e)

Correttezza classica: ovvia poiche in ogni mondo v si ha[[⊥]]v = 0 e quindi ⊥ C.

Correttezza intuizionista: dobbiamo fornire un programma in[[C]]v assumendo l’esistenza di un x ∈ [[⊥]]v . Poiche un tale xnon esiste, siamo in presenza di codice morto.

La regola non e invertibile: per esempio quando C = > si ha > ma 6 ⊥


Deduzione naturale

Deduzione naturale: >Regole di introduzione:

>(>i )

Regola di eliminazione (INUTILE):

> CC

(>e)

Lettura bottom-up: il > e vero.

Lettura top-down: per dimostrare > non debbo fare nulla.

Scrittura informale (sempre omessa)[> vale]


Deduzione naturale

Deduzione naturale: >Regole di introduzione:

>(>i )

Regola di eliminazione (INUTILE):

> CC

(>e)

Correttezza intuizionista (e quindi classica): ovvia (? ∈ [[>]]v ) ese c ∈ [[C]]v allora c ∈ [[C]]v .

Invertibilita intuizionista (e quindi classica): ovvia in quanto perla regola di introduzione non vi e nulla da dimostrare e perquella di eliminazione se c ∈ [[C]]v allora c ∈ [[C]]v e inoltre? ∈ [[>]]v .


Deduzione naturale

Deduzione naturale: ⇒Regole di introduzione:

[A]...B

A⇒ B(⇒i )

Lettura bottom-up: se ipotizzando A dimostro B allora A⇒ B.

Lettura top-down: per dimostrare A⇒ B basta assumere A edimostrare B.

Scrittura informale:supponiamo A. . . e quindi Bquindi A⇒ B


Deduzione naturale

Deduzione naturale: ⇒


[A]...B

A⇒ B(⇒i )

Correttezza intuizionista (e quindi anche classica): e unadirezione del teorema di deduzione semantica!

Invertibilita intuizionista (e quindi anche classica): e l’altradirezione del teorem di deduzione semantica!


Deduzione naturale



A⇒ B AB

(⇒e O MODUS PONENS)

Lettura bottom-up: se A e A⇒ B, allora necessariamente B.

Lettura top-down: per dimostrare B debbo trovare un A chevalga e tale per cui A⇒ B

Scrittura informale:da A e A⇒ B si ha B


Deduzione naturale



A⇒ B AB

(⇒e O MODUS PONENS)

Correttezza intuizionista (e quindi classica): dati a ∈ [[A]]v ef ∈ [[A⇒ B]]v si ha f (a)[[B]]v .

La regola non e invertibile per esempio quando B = > e A = ⊥.Rimane non invertibile anche sapendo che A⇒ B valga.

Nota: durante la ricerca top-down della prova la regola dimodus ponens e la piu difficile da applicare in quanto A non ein genere noto e, anche in presenza di una prova per A⇒ B, Apuo non essere dimostrabile.


Deduzione naturale


Esercizi (esempi alla lavagna):` (A⇒ B)⇒ (B ⇒ C)⇒ A⇒ C` (A⇒ B ⇒ C ⇒ D)⇒ C ⇒ B ⇒ D ⇒ A` (A ∨ B)⇒ (A⇒ C ∧ D)⇒ (B ⇒ D)⇒ D ∧ (B ∨ C)


Deduzione naturale

Deduzione naturale: ¬Ricordiamoci che ¬A ≡ A⇒ ⊥ per ottenere le regole per il ¬come istanze delle regole per l’⇒.


[A]...⊥¬A

(¬i )

Lettura bottom-up: se ipotizzando A dimostro l’assurdo allora¬A.

Lettura top-down: per dimostrare ¬A basta assumere A edimostrare l’assurdo.

Scrittura informale:supponiamo A. . . assurdoe quindi ¬A


Deduzione naturale

Deduzione naturale: ¬Ricordiamoci che ¬A ≡ A⇒ ⊥ per ottenere le regole per il ¬come istanze delle regole per l’⇒.


¬A A⊥

(¬e)

Lettura bottom-up: e assurdo avere sia ¬A che A

Lettura top-down: per dimostrare l’assurdo basta dimostrarequalcosa e il suo contrario.

Scrittura informale:. . . e quindi ¬A. . . e quindi Aassurdo!


Deduzione naturale

Deduzione naturale: ¬

Correttezza intuizionista e classica: segue da quella delleregole per l’⇒.

Invertibilita intuizionista e classica per l’¬i : segue da quelladella regola dell’⇒i .

Invertibilita intuizionista e classica per l’¬e: ovvia in quanto⊥ A e ⊥ ¬A. La regola e comunque di difficile applicazionein quanto se non si sceglie l’A giusto, si e solo duplicato illavoro inutilmente.


Deduzione naturale

Deduzione naturale: ¬ATTENZIONE: non confondere la regola ¬i con la regola didimostrazione per assurdo (RAA) che dice qualcosa di diverso:

[A]...⊥¬A

(¬i)

[¬A]...⊥A

(RAA)

Infatti la regola ¬i istanziata con ¬A dice solo

¬A...⊥¬¬A

(¬i)

e ¬¬A ≡ A solamente classicamente ma nonintuizionisticamente.


Deduzione naturale

Deduzione naturale: ¬

Nota: la confusione fra ¬i e RAA e molto frequente presso imatematici e accentua in loro l’impressione che facendo logicaintuizionista (ove la RAA non vale) non si riesca a dimostrarequasi nulla.

In verita la ¬i vale intuizionisticamente e, anzi, sulleproposizioni negate (non informative) sappiamo che le duelogiche essenzialmente coincidono.


Deduzione naturale

Teorema di correttezza per la logicaclassica/intuizionista

Teorema di correttezza per la logica classica/intuizionista: seΓ ` F allora Γ F in logica classica/intuizionista.

Dimostrazione: per induzione strutturale sull’albero diderivazione Γ ` F .

Caso A: poiche A e una foglia non cancellata, si ha A ∈ Γ.Pertanto Γ A.

Caso [A]: impossibile in quanto un’ipotesi viene scaricatasolamente da una regola.


Deduzione naturale

Teorema di correttezza per la logicaclassica/intuizionista

Caso T1...TnF (r) dove T1, . . . ,Tn sono i sottoalberi immediati

dell’albero di deduzione:Sia Ti la derivazione Γi ` Fi . Si ha Γi = Γ ∪∆i dove ∆i el’insieme delle ipotesi cancellate in Ti dalla regola r . Per ipotesiinduttiva, Γi Fi per ogni i . Per correttezza locale della regola rsi ha ∆1 ⇒ F1, . . . ,∆n ⇒ Fn F . Quindi, per il teorema dideduzione semantica e per la transitivita della conseguenzasemantica, si ottiene Γ F .

NOTA: poiche l’unica assunzione sulle regole r e che sianolocalmente corrette, potremo in seguito aggiungere altre regolelocalmente corrette preservando la correttezza globale.


Deduzione naturale

Teorema di deduzione sintattica

Teorema di deduzione sintattica: A ` B sse ` A⇒ B.

Dimostrazione:

A...B

A⇒ B(⇒i)

A⇒ B AB

(⇒e)


Deduzione naturale

Teorema di completezza intuizionista

Teorema di completezza per la logica intuizionista: se Γ Fallora Γ ` F .

Cenni: dobbiamo fare riferimento a una semantica intuizionistafra quelle viste, ovvero la semantica di Kripke e quella diHeyting-Brower-Kolmogorov.

Nel primo caso la dimostrazione e alquanto complessa e non epossibile farla rientrare nel corso.

Nel secondo caso dobbiamo dimostrare che per ogniprogramma per [[C]]v scritto facendo riferimento a funzioni dilibreria per la semantica delle formule in Γ esiste una prova di Fche usa le ipotesi in Γ. In altre parole, A OGNI PROGRAMMACORRISPONDE UNA PROVA (E VICEVERSA PER ILTEOREMA DI CORRETTEZZA.


Deduzione naturale

Teorema di completezza intuizionista

Teorema di completezza per la logica intuizionista: se Γ Fallora Γ ` F .

Per ottenere questo risultato e necessario fissareesplicitamente il linguaggio di programmazione usato. Essocorrisponde a un linguaggio funzionale, higher-order, tipatosemplicemente e dotato di coppie, proiezioni per le coppie,booleani, if-then-else e niente altro.

Omettiamo la dimostrazione che, una volta fissato il linguaggioin maniera appropriata, e una semplice induzione strutturale sulprogramma dato in input.

NOTA: la logica determina il linguaggio di programmazione eviceversa. Entrambi sono comunque estremamente naturali enoti a priori.


Deduzione naturale

Normalizzazione di prove

I linguaggi di programmazione sono caratterizzati dalle regoledi calcolo (o computazione).

La nozione corrispondente sulle prove e quella disemplificazione di una prova.

La semplificazione e essenzialmente resa possibile dal fattoche i connettivi di eliminazione sono ottenuti a partire da quellidi introduzione e viceversa.

Un’introduzione seguita immediatamente da un conclusioneporta a una prova sempre semplificabile. Esistono altre regoledi semplificazione.

Semplificazioni ripetute portano a una forma normale che eanche canonica.


Deduzione naturale


Esempio:

[A]...B

A⇒ B(⇒i)

...A

B(⇒e)

si semplifica in...A...B

mantenendo le stesse ipotesi e conclusioni. Semanticamente el’applicazione di funzione che si riduce a istanziare gliargomenti.


Deduzione naturale


Esempio:

...A

...B

A ∧ B(∧i)

A(∧e1)

si semplifica in...A

mantenendo le stesse ipotesi e conclusioni. Semanticamente ela prima proiezione applicata a una coppia che ritorna il primoelemento della coppia.


Deduzione naturale


Esempio:

...A

A ∨ B(∨i1)

[A]...C

[B]...C

C(∨e)

si semplifica in...A...C

mantenendo le stesse ipotesi e conclusioni. Semanticamente e≈ la regola di riduzione dell’if-then-else nel caso true.


Deduzione naturale


Il corso (obbligatorio) di “Fondamenti Logici dell’Informatica” delprimo anno della Laurea Magistrale in Informatica einteramente dedicato allo studio di questa corrispondenza fra:

Programmi e prove in logica intuizionistaCalcolo di un programma e semplificazione di proveTipi e formuleLinguaggi di programmazione e logiche intuizioniste. . .


Deduzione naturale

Deduzione naturale per la logica classica

Le regole viste fino ad ora NON sono complete per la logicaclassica (in quanto lo sono per la logica intuizionista).

Esempio: 6` A ∨ ¬A (principio del terzo escluso)Esempio: 6` ¬¬A⇒ A (base del ragionamento per assurdo)

Provare a dimostrare le formule qua sopra per convincersidell’impossibilita di costruire una derivazione.


Deduzione naturale

Deduzione naturale per la logica classica: RAA

Per essere completi rispetto alla semantica classica, bastaintrodurre la regola di Riduzione ad Assurdo (RAA):

[¬A]...⊥A

(RAA)

Note:La regola non e ne di introduzione, ne di eliminazione di unconnettivo.Non avendo una regola duale (introduzione/eliminazione),un teorema classico (= dimostrato con la RAA) non sisemplifica/normalizza. Meglio evitarla se possibile.La regola e invertibile (in quanto A ¬A⇒ ⊥) e sempreapplicabile (MALE!)


Deduzione naturale

Deduzione naturale per la logica classica: RAA

Un uso frequente della RAA e il seguente schema

[¬A]...A [¬A]

⊥ (¬e)

A(RAA)

Ovvero, per trovare una prova di A ci si riduce a cercare ancorauna prova di A, ma dopo aver assunto ¬A.

Esercizio: dimostrare ` (¬A⇒ A)⇒ A.


Deduzione naturale

Deduzione naturale per la logica classica: EM

Il principio del terzo escluso (EM) e dimostrabile a partire dallaRAA:

Esercizio: ` A ∨ ¬A

In generale le dimostrazioni classiche effettuate con il soloausilio della RAA possono essere laboriose e/o anti-intuitive.

Tuttavia il principio del terzo escluso combinato conl’eliminazione dell’or fornisce uno schema di prova moltopotente (analisi per casi su una variabile).

...A ∨ ¬A

[A]...C

[¬A]...C

C(∨e)


Deduzione naturale

Deduzione naturale per la logica classica: EM

Metodo generalizzato:Sia F una formula da dimostrarsi. Ripetendo per ognuna dellevariabili in Var(F ) = {A1, . . . ,An} l’analisi per casi (come per ilcalcolo della forma normale di Shannon) ci si riduce adimostrare F sotto a n ipotesi aggiuntive [F1], . . . , [Fn] tali cheper ogni i si ha Fi ∈ {Ai ,¬Ai}.

Esempio: dimostrare A ∧ B,B ⇒ C ` A ∨ C usando il metodogeneralizzato su A e su B.

Nota: usando il metodo generalizzato in genere NON si trovanole dimostrazioni piu semplici/naturali.Tuttavia il metodo puo essere usato meccanicamente perdecidere se ` F (vedi teorema di completezza nei prossimilucidi). L’albero di deduzione ottenuto e ancora una voltaesponenziale nel numero delle variabili.


Deduzione naturale

Teorema di completezza per la logica classica

Teorema di COMPLETEZZA DEBOLE per la logica classica:per ogni Γ,F , con Γ finito, se Γ F in logica proposizionaleclassica allora Γ ` F (potendo usare anche la RAA).

Nota: il teorema si dice di completezza debole per via dellalimitazione a contesti Γ finiti. Per i teoremi di deduzionesintattia/semantica, il teorema di completezza debole si puoriformulare come: se F allora ` F .

Corollario (teorema di COMPLETEZZA FORTE per la logicaclassica): per ogni Γ,F , se Γ F allora Γ ` F .Dimostrazione del corollario: sia Γ F . Per il teorema dicompattezza esiste ∆ ⊂ Γ, ∆ finito tale che ∆ F . Per ilteorema di completezza debole si ha ∆ ` F e quindi Γ ` F .


Deduzione naturale


Osservazioni:Dal teorema di completezza debole e da quello dicompattezza deduciamo il teorema di completezza forte.Poiche la prova di quello di compattezza non e costruttiva(= la meta-logica e classica), NON OTTENIAMO ALCUNALGORITMO CHE DATO Γ E F RESTITUISCA UNALBERO DI PROVA Γ ` F .Viceversa, forniremo ora una prova costruttiva del teoremadi completezza debole (= la meta-logica e intuizionista),OTTENENDO UN ALGORITMO CHE DATO Γ FINITO E FRESTITUISCE UN ALBERO DI PROVA Γ ` F .La complessita dell’algoritmo sara, ancora una volta,esponenziale nel numero di atomi che occorrono nelleformule.


Deduzione naturale


Dimostrazione del teorema di completezza debole per la logicaclassica.

Dimostriamo il teorema nella sua forma equivalente se Fallora ` F .

La prima fase della dimostrazione consiste nell’applicare ilmetodo generalizzato (slide 55) per ridursi, tramite il principio diEM (e quindi tramite la RAA), a costruire 2n alberi di prova∆i ` F ove n = |Var(F )| = |{A1, . . . ,An}| e l’i-esimo contesto∆i e in relazione come segue con l’i-esima riga vi della tabelladi verita per F : ∆i = A∗1, . . . ,A

∗n dove per ogni j si ha A∗j = Aj

se vi(Aj) = 1 e A∗j = ¬Aj se vi(Aj) = 0.

Poiche per ipotesi F si ha che, per ogni i , vi F .Dobbiamo dimostrare ∆i ` F per ogni i .


Deduzione naturale


Lemma: per ogni F , per ogni i e per ogni vi e ∆i definiti comesopra, si ha

1 se vi F allora ∆i ` F2 se vi 6 F allora ∆i ` ¬F

Nota: la dimostrazione del lemma e costruttiva.

Dimostrazione: per induzione strutturale su F .

Caso Aj :1 se vi Aj allora vi(Aj) = 1 e quindi Aj ∈ ∆i e ∆i ` Aj

2 se vi 6 Aj allora vi(Aj) = 0 e quindi ¬Aj ∈ ∆i e ∆i ` ¬Aj


Deduzione naturale


Caso F1 ∧ F2:Per ipotesi induttiva, per ogni h ∈ {1,2} si ha

1 se vi Fh allora ∆i ` Fh

2 se vi 6 Fh allora ∆i ` ¬Fh

Procediamo per casi su vi F1 ∧ F2 o vi 6 F1 ∧ F2.1 Caso vi F1 ∧ F2 o, equivalentemente

[[F1 ∧ F2]]v = min{[[F1]]v , [[F2]]v} = 1 e quindi[[F1]]v = [[F2]]v = 1 e, per ipotesi induttiva, ∆i ` F1 e∆i ` F2:

...F1

...F2

F1 ∧ F2(∧i)

2 Caso vi 6 F1 ∧ F2 o, equivalentemente [[F1 ∧ F2]]v = 0 equindi vi e un Fh con h ∈ {1,2} t.c. [[Fh]]v = 0.


Deduzione naturale


Per ipotesi induttiva ∆i ` ¬Fh e quindi

...¬Fh

[F1 ∧ F2]Fh

(∧eh)

⊥ (¬e)

¬(F1 ∧ F2)(¬i)


Deduzione naturale


Caso F1 ∨ F2:Per ipotesi induttiva, per ogni h ∈ {1,2} si ha



Procediamo per casi su vi F1 ∨ F2 o vi 6 F1 ∨ F2.1 Caso vi F1 ∨ F2 o, equivalentemente

[[F1 ∨ F2]]v = max{[[F1]]v , [[F2]]v} = 1 e quindi vi e unh ∈ {1,2} t.c. [[Fh]]v = 1 e, per ipotesi induttiva, ∆i ` Fh:

...Fh

F1 ∨ F2(∨ih )

2 Caso vi 6 F1 ∨ F2 o, equivalentemente [[F1 ∨ F2]]v = 0 equindi [[F1]]v = [[F2]]v = 0.


Deduzione naturale


Per ipotesi induttiva ∆i ` ¬F1 e ∆i ` ¬F2 e quindi

[F1 ∨ F2]

...¬F1 [F1]⊥

...¬F2 [F2]⊥

⊥ (¬e)

¬(F1 ∨ F2)(¬i)


Deduzione naturale


Caso ¬F :Per ipotesi induttiva si ha

1 se vi F allora ∆i ` F2 se vi 6 F allora ∆i ` ¬F

Procediamo per casi su vi ¬F o vi 6 ¬F .1 Caso vi ¬F o, equivalentemente [[¬F ]]v = 1 e quindi

[[F ]]v = 0 e, per ipotesi induttiva, ∆i ` ¬F .2 Caso vi 6 ¬F o, equivalentemente [[¬F ]]v = 0 e quindi

[[F ]]v = 1 e, per ipotesi induttiva, ∆i ` F :

[¬F ]

...F

⊥ (¬e)

¬¬F(¬i)


Deduzione naturale


Caso F1 ⇒ F2:Per ipotesi induttiva, per ogni h ∈ {1,2} si ha



Procediamo per casi su vi F1 ⇒ F2 o vi 6 F1 ⇒ F2.1 Caso vi F1 ⇒ F2 o, equivalentemente

[[F1 ⇒ F2]]v = max{1− [[F1]]v , [[F2]]v} = 1 e quindi o[[F1]]v = 0 e, per ipotesi induttiva, ∆i ` ¬F1, oppure[[F2]]v = 1 e, per ipotesi induttiva, ∆i ` F2.Vedi slide successiva per ambedue i casi.

2 Caso vi 6 F1 ⇒ F2 o, equivalentemente [[F1 ⇒ F2]]v = 0 equindi [[F1]]v = 1 e [[F2]]v = 0 e, per ipotesi induttiva,∆i ` F1 e ∆i ` ¬F2. Vedi slide dopo la prossima.


Deduzione naturale


Casi ∆i ` ¬F1 e ∆i ` F2, dobbiamo dimostrare ∆i ` F1 ⇒ F2:

...¬F1 [F1]⊥ (¬e)

F2(⊥e)

F1 ⇒ F2(⇒i)

...F2

F1 ⇒ F2(⇒i)


Deduzione naturale


Caso ∆i ` F1 e ∆i ` ¬F2, dobbiamo dimostrare∆i ` ¬(F1 ⇒ F2):

...¬F2

[F1 ⇒ F2]

...F1

F2(⇒e)

⊥ (¬e)

¬(F1 ⇒ F2)(¬i)

Qed.


Deduzione naturale

Correttezza, completezza, compattezza.

Abbiamo gia visto: completezza debole ∧ compattezza⇒completezza forte.

Vale anche:

Teorema: completezza forte ∧ correttezza⇒ compattezza.Dimostrazione: siano Γ ed F tale che Γ F . Per il teorema dicompletezza forte si ha Γ ` F , ovvero esiste un albero diderivazione la cui radice e F e le cui foglie sono un insiemefinito ∆ ⊆ Γ. Per correttezza si ha ∆ F . Qed.

Osservazione: il precedente teorema ci dice che ogni provacostruttiva del teorema di completezza forte ci darebbe unaprova costruttiva (un algoritmo) per il teorema di compattezza.Non esistono prove del genere perche si dimostra la nonesistenza degli algoritmi relativi.


Universita di Bologna´sacerdot/linguaggi1011/lucidi/slides15.pdf · Dimostrazione: per induzione...

Documents

Transcript of Universita di Bologna´sacerdot/linguaggi1011/lucidi/slides15.pdf · Dimostrazione: per induzione...