Deduzione naturale - Dipartimento di Informatica

Deduzione naturale
Linguaggi
15: Deduzione naturale
Claudio Sacerdoti Coen
<[email protected]>
Universitá di Bologna
28/03/2011
Claudio Sacerdoti Coen
Deduzione naturale
Outline
1
Deduzione naturale
Claudio Sacerdoti Coen
Deduzione naturale
Deduzione
Wikipedia: “. . . ”
Claudio Sacerdoti Coen
Deduzione naturale
Deduzione naturale: sintassi
Definiamo ora la sintassi degli alberi (di prova) per la deduzione
naturale.
Note: in un albero di prova Γ F
la radice dell’albero è la conclusione F
le foglie dell’albero sono ipotesi scaricate [F ] o meno F
un’ipotesi non scaricata (o globale) F deve appartenere a Γ
un’ipotesi scaricata [F ] è un’ipotesi locale e deve essere
“scaricata” da un qualche passo di inferenza
i nodi interni dell’albero debbono appartenere alla lista di
passi di inferenza che stiamo per elencare
Claudio Sacerdoti Coen
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 una
formula con in testa un determinato connettivo
come concludo . . . ?
2
Regole di eliminazione di un connettivo:
ci dicono tutti i modi in cui utilizzare direttamente un’ipotesi
con in testa un determinato connettivo
cosa ricavo da . . . ?
Claudio Sacerdoti Coen
Deduzione naturale
Deduzione naturale: passi di inferenza
Usiamo la seguente sintassi per le regole di inferenza:
F1 . . . Fn
F
(NOME REGOLA)
La formula F è la conclusione della regola.
Le formule F1 , . . . , Fn sono le premesse della regola.
[A]
La premessa Fi verrà indicata con ... per indicare che è
Fi
possibile assumere localmente A per concludere Fi .
Una regola senza premesse (n = 0) si dice assioma.
Claudio Sacerdoti Coen
Deduzione naturale
Deduzione naturale: alberi di deduzione
Gli alberi di deduzione vengono indicati componendo
ricorsivamente regole di inferenza. Esempio:
F1 ...Fn
H1
(regola1)
...
G1 ...Gm
Hl
H
(regola2)
(regola3)
n
Nell’esempio F1H...F
(regola1) è un sottoalbero dell’intero
1
albero di deduzione.
La struttura ricorsiva permette di definire funzioni per ricorsione
strutturale su alberi di deduzione e di effettuare prove per
induzione strutturale.
Claudio Sacerdoti Coen
Deduzione naturale
Deduzione naturale: passi di inferenza
Ogni passo di inferenza ammette sempre due letture:
1
Bottom-up (dalle premesse alla conclusione):
date le premesse F1 , . . . , Fn , posso concludere F
2
Top-down (dalla conclusione alle premesse):
per concludere F posso ridurmi a dimostrare F1 , . . . , Fn
Claudio Sacerdoti Coen
Deduzione naturale
Deduzione naturale: correttezza e invertibilità
n
Definizione: una regola F1 ...F
è corretta per la logica
F
classica/intuizionista quando F1 , . . . , Fn F (nella rispettiva
logica).
Noi saremo interessati solamente a regole corrette.
n
Definizione: una regola F1 ...F
è invertibile nella logica
F
classica/intuizionista quando per ogni i si ha F Fi (nella
rispettiva logica).
L’invertibilità gioca un ruolo importante nella ricerca delle prove:
se la regola è invertibile, può essere sempre applicata nella
ricerca top-down della prova.
Claudio Sacerdoti Coen
Deduzione naturale
Deduzione naturale: ∧
Regole di introduzione:
A B
A∧B
(∧i )
Lettura bottom-up: se A e B allora A ∧ B.
Lettura top-down: per dimostrare A ∧ B debbo dimostrare sia A
che B.
Scrittura informale:
. . . e quindi A
. . . e quindi B
[e quindi A ∧ B]
L’applicazione della regola viene spesso lasciata informalmente
implicita.
Claudio Sacerdoti Coen
Deduzione naturale
Deduzione naturale: ∧
Regole di introduzione:
A B
A∧B
(∧i )
Correttezza classica: A, B A ∧ B in quanto, per ogni mondo
v , 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 e
b ∈ [[B]]v allora ha, bi ∈ [[A ∧ B]]v = [[A]]v × [[B]]v .
Invertibilità classica: se max{[[A]]v , [[B]]v } = 1 allora
[[A]]v = [[B]]v = 1 e quindi A ∧ B A e A ∧ B B.
Invertibilità intuizionista: se c ∈ [[A]]v × [[B]]v allora c = ha, bi per
qualche a ∈ [[A]]v e b ∈ [[B]]v e quindi A ∧ B A e A ∧ B B.
Claudio Sacerdoti Coen
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, allora
C.
Lettura top-down: per dimostrare C data l’ipotesi A ∧ B è sufficiente
dimostrare 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.
Claudio Sacerdoti Coen
Deduzione naturale
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. Il
secondo dimostra C usando, fra le altre, le ipotesi A e B NON
ANCORA SCARICATE. È l’applicazione della regola che
scarica le ipotesi dal sotto-albero.
Claudio Sacerdoti Coen
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 verità.
Correttezza intuizionista: dimostriamo A ∧ B, A ⇒ B ⇒ C C.
Sia ha, bi ∈ [[A ∧ B]]v e sia f ∈ [[A ⇒ B ⇒ C]]v . Allora
f (a) ∈ [[B ⇒ C]]v e f (a)(b) = f (a, b) ∈ [[C]]v .
La regola non è invertibile. Esempio: C = > e A, B = ⊥.
La regola è intuizionisticamente (e quindi anche classicamente)
invertibile se si assume A ∧ B: ovvio.
Claudio Sacerdoti Coen
Deduzione naturale
Deduzione naturale: ∧
Regole alternative di eliminazione:
A∧B
A
A∧B
B
Lettura bottom-up: se A ∧ B allora A (e B).
Lettura top-down: per dimostrare A (o B) basta
dimostrare A ∧ B.
Scrittura informale:
. . . e quindi A ∧ B
[e quindi A]
Le due regole vengono quasi sempre omesse.
Claudio Sacerdoti Coen
(∧e1 )
(∧e2 )
Deduzione naturale
Deduzione naturale: ∧
Regole alternative di eliminazione:
A∧B
A
A∧B
B
(∧e1 )
(∧e2 )
Correttezza classica e intuizionista: le due regole sono corrette.
Le due regole non sono invertibili: esempio A = > e B = bot.
Claudio Sacerdoti Coen
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 errori
Cons: è molto difficile vedere le prove cosı̀ perchè vi sono
troppe strade che non portanto alla conclusione cercata
2
Top-down: partendo dalla conclusione si applicano indietro
le regole fino a ridursi a un sottoinsieme delle ipotesi.
Pro: più facile trovare le dimostrazioni se si sta attenti a non
sbagliarsi (= ridursi a dimostrare qualcosa di non vero)
Cons: è possibile sbagliarsi quando si applicano regole non
invertibili
3
Strategia mista: si alternano le due strategie, tipicamente
partendo con una top-down.
Claudio Sacerdoti Coen
Deduzione naturale
Deduzione naturale: ricerca delle prove
Come evitare errori?
1
Dopo l’applicazione top-down di una regola di inferenza
non invertibile, accertarsi che la conclusione sia ancora
conseguenza logica delle premesse.
Esempio: per dimostrare A ∧ B ` A si parte da A e lo si
riduce a A ∧ C. Si ha A ∧ B 6 A ∧ C (anche se A ∧ B A).
2
Verificare di non essersi ridotti a dimostrare qualcosa che
si sta già dimostrando con le stesse ipotesi (ragionamento
circolare).
Esempio: per dimostrare A ci si riduce a dimostrare A ∧ B
che dimostriamo riducendoci a dimostrare sia A che B.
Claudio Sacerdoti Coen
Deduzione naturale
Deduzione naturale: ricerca delle prove
Esercizi (esempi alla lavagna):
A∧B `B∧A
A ∧ (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 difficoltà della ricerca bottom-up
delle prove.
Claudio Sacerdoti Coen
Deduzione naturale
Deduzione naturale: derivabilità
Definizione: un insieme di regole R è derivabile a partire da un
insieme di regole S quando per ogni regola in R le cui
premesse sono F1 , . . . , Fn e la cui conclusione è F si ha
F1 , . . . , Fn ` F usando solamente le regole in S.
Nota: è la stessa nozione chiamata in precedenza riducibilità.
Teorema: se R è derivabile a partire da S allora per ogni
dimostrazione ottenuta usando solo regole in R esiste una
dimostrazione con le stesse premesse e conclusione che usa
solo regole in S.
Dimostrazione: per induzione strutturale sull’albero di derivazione.
In tutti i casi, per ipotesi induttiva esistono alberi di derivazione per
ognuna delle premesse che usano solo regole in S. Per ipotesi esiste
un albero di derivazione per la regola sotto esame che usa solo
regole in S. Componendo gli alberi si ottiene la prova voluta.
Claudio Sacerdoti Coen
Deduzione naturale
Deduzione naturale: derivabilità
Teorema: l’insieme {∧e1 , ∧e2 } è derivabile a partire dall’insieme
{∧e } e viceversa.
Dimostrazione:
Prima parte: {∧e1 , ∧e2 } è derivabile a partire da {∧e }.
A ∧ B [A]
(∧e )
A
A ∧ B [B]
(∧e )
B
Seconda parte: {∧e } è derivabile a partire da {∧e1 , ∧e2 }.
A∧B
A (∧e1 )
Claudio Sacerdoti Coen
..
.
C
A∧B
B (∧e2 )
Deduzione naturale
Deduzione naturale: ∨
Regole di introduzione:
A
A∨B
B
A∨B
(∧i1 )
(∧i2 )
Lettura bottom-up: se A (B) vale, allora vale anche A ∨ B
Lettura top-down: per dimostrare A ∨ B è sufficiente dimostrare
A (B)
Scrittura informale:
. . . e quindi A
[e quindi A ∨ B]
Claudio Sacerdoti Coen
Deduzione naturale
Deduzione naturale: ∨
Regole di introduzione:
A
A∨B
B
A∨B
(∧i1 )
(∧i2 )
Correttezza intuizionista (e quindi classica): A A ∨ B in
quanto data a ∈ [[A]]v si ha h0, ai ∈ [[A ∨ B]]v
Le due regole non sono invertibili: per esempio quando A = ⊥
eB=>
Claudio Sacerdoti Coen
Deduzione naturale
Deduzione naturale: ∨
Regole di eliminazione:
A∨B
[A]
..
.
[B]
..
.
C
C
C
(∨e )
Lettura bottom-up: se vale A ∨ B e C vale sia quando vale A che
quando vale B, allora necessariamente C vale.
Lettura top-down: per dimostrare qualunque cosa sapendo A ∨ B è
sufficiente procedere per casi, dimostrando la stessa cosa
assumendo prima che A valga e poi che valga B
Scrittura informale:
. . . e quindi A ∨ B
procediamo per casi per dimostrare C
caso A: . . . e quindi C
caso B: . . . e quindi C
[e quindi C]
Claudio Sacerdoti Coen
Deduzione naturale
Deduzione naturale: ∨
Regole di eliminazione:
A∨B
[A]
..
.
[B]
..
.
C
C
C
(∨e )
Correttezza intuizionista (e quindi classica): per ipotesi c ∈ [[A ∨ B]]v e
f [x] ∈ [[C]]v per x ∈ [[A]]v e g[y] ∈ [[C]]v per y ∈ [[B]]v . Se c = h0, ai
dove a ∈ [[A]]v allora f [a/x] ∈ [[C]]v . Se c = h1, bi dove b ∈ [[B]]v allora
g[b/y ] ∈ [[C]]v .
Invertibilità: la regola non è invertibile (controesempio: C = > e
A = B = ⊥. Tuttavia, quando A ∨ B è dimostrabile, allora la regola è
banalmente invertibile intuizionisticamente (e quindi anche
classicamente). Infatti per ipotesi sia c ∈ [[C]]v e d ∈ [[A ∨ B]]v . Allora
c ∈ [[C]]v anche senza usare nessun x ∈ [[A]]v o y ∈ [[B]]v .
Claudio Sacerdoti Coen
Deduzione naturale
Deduzione naturale: ricerca delle prove
Esercizi (esempi alla lavagna):
A∧B `C∨A
A∨B `B∨A
A ∨ (B ∨ C) ` (C ∨ B) ∨ A
Claudio Sacerdoti Coen
Deduzione naturale
Deduzione naturale: ⊥
Regole di introduzione: NESSUNA.
Regole di eliminazione:
⊥
C
Lettura bottom-up: dal falso segue qualunque cosa.
Lettura top-down: per dimostrare qualunque cosa posso
ridurmi a dimostrare un assurod.
Scrittura informale:
. . . assurdo
e quindi C
Claudio Sacerdoti Coen
(⊥e )
Deduzione naturale
Deduzione naturale: ⊥
Regole di introduzione: NESSUNA.
Regole di eliminazione:
⊥
C
(⊥e )
Correttezza classica: ovvia poichè 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 . Poichè un tale x
non esiste, siamo in presenza di codice morto.
La regola non è invertibile: per esempio quando C = > si ha
> ma 6 ⊥
Claudio Sacerdoti Coen
Deduzione naturale
Deduzione naturale: >
Regole di introduzione:
>
(>i )
Regola di eliminazione (INUTILE):
> C
C
Lettura bottom-up: il > è vero.
Lettura top-down: per dimostrare > non debbo fare nulla.
Scrittura informale (sempre omessa)
[> vale]
Claudio Sacerdoti Coen
(>e )
Deduzione naturale
Deduzione naturale: >
Regole di introduzione:
>
(>i )
Regola di eliminazione (INUTILE):
> C
C
(>e )
Correttezza intuizionista (e quindi classica): ovvia (? ∈ [[>]]v ) e
se c ∈ [[C]]v allora c ∈ [[C]]v .
Invertibilità intuizionista (e quindi classica): ovvia in quanto per
la regola di introduzione non vi è nulla da dimostrare e per
quella di eliminazione se c ∈ [[C]]v allora c ∈ [[C]]v e inoltre
? ∈ [[>]]v .
Claudio Sacerdoti Coen
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 e
dimostrare B.
Scrittura informale:
supponiamo A
. . . e quindi B
quindi A ⇒ B
Claudio Sacerdoti Coen
Deduzione naturale
Deduzione naturale: ⇒
Regole di introduzione:
[A]
..
.
B
A⇒B
Correttezza intuizionista (e quindi anche classica): è una
direzione del teorema di deduzione semantica!
Invertibilità intuizionista (e quindi anche classica): è l’altra
direzione del teorem di deduzione semantica!
Claudio Sacerdoti Coen
(⇒i )
Deduzione naturale
Deduzione naturale: ⇒
Regole di eliminazione:
A⇒B A
B
(⇒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 che
valga e tale per cui A ⇒ B
Scrittura informale:
da A e A ⇒ B si ha B
Claudio Sacerdoti Coen
Deduzione naturale
Deduzione naturale: ⇒
Regole di eliminazione:
A⇒B A
B
(⇒e O MODUS PONENS)
Correttezza intuizionista (e quindi classica): dati a ∈ [[A]]v e
f ∈ [[A ⇒ B]]v si ha f (a)[[B]]v .
La regola non è 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 di
modus ponens è la più difficile da applicare in quanto A non è
in genere noto e, anche in presenza di una prova per A ⇒ B, A
può non essere dimostrabile.
Claudio Sacerdoti Coen
Deduzione naturale
Deduzione naturale: ricerca delle prove
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)
Claudio Sacerdoti Coen
Deduzione naturale
Deduzione naturale: ¬
Ricordiamoci che ¬A ≡ A ⇒ ⊥ per ottenere le regole per il ¬
come istanze delle regole per l’⇒.
Regole di introduzione:
[A]
..
.
⊥
¬A
(¬i )
Lettura bottom-up: se ipotizzando A dimostro l’assurdo allora
¬A.
Lettura top-down: per dimostrare ¬A basta assumere A e
dimostrare l’assurdo.
Claudio Sacerdoti Coen
Deduzione naturale
Deduzione naturale: ¬
Ricordiamoci che ¬A ≡ A ⇒ ⊥ per ottenere le regole per il ¬
come istanze delle regole per l’⇒.
Regole di eliminazione:
¬A A
⊥
(¬e )
Lettura bottom-up: è assurdo avere sia ¬A che A
Lettura top-down: per dimostrare l’assurdo basta dimostrare
qualcosa e il suo contrario.
Scrittura informale:
. . . e quindi ¬A
. . . e quindi A
assurdo!
Claudio Sacerdoti Coen
Deduzione naturale
Deduzione naturale: ¬
Correttezza intuizionista e classica: segue da quella delle
regole per l’⇒.
Invertibilità intuizionista e classica per l’¬i : segue da quella
della regola dell’⇒i .
Invertibilità intuizionista e classica per l’¬e : ovvia in quanto
⊥ A e ⊥ ¬A. La regola è comunque di difficile applicazione
in quanto se non si sceglie l’A giusto, si è solo duplicato il
lavoro inutilmente.
Claudio Sacerdoti Coen
Deduzione naturale
Deduzione naturale: ¬
ATTENZIONE: non confondere la regola ¬i con la regola di
dimostrazione per assurdo (RAA) che dice qualcosa di diverso:
[¬A]
..
.
[A]
..
.
⊥
¬A
(¬i )
⊥
A
(RAA)
Infatti la regola ¬i istanziata con ¬A dice solo
¬A
..
.
⊥
(¬i )
¬¬A
e ¬¬A ≡ A solamente classicamente ma non
intuizionisticamente.
Claudio Sacerdoti Coen
Deduzione naturale
Deduzione naturale: ¬
Nota: la confusione fra ¬i e RAA è molto frequente presso i
matematici e accentua in loro l’impressione che facendo logica
intuizionista (ove la RAA non vale) non si riesca a dimostrare
quasi nulla.
In verità la ¬i vale intuizionisticamente e, anzi, sulle
proposizioni negate (non informative) sappiamo che le due
logiche essenzialmente coincidono.
Claudio Sacerdoti Coen
Deduzione naturale
Teorema di correttezza per la logica
classica/intuizionista
Teorema di correttezza per la logica classica/intuizionista: se
Γ ` F allora Γ F in logica classica/intuizionista.
Dimostrazione: per induzione strutturale sull’albero di
derivazione Γ ` F .
Caso A: poichè A è una foglia non cancellata, si ha A ∈ Γ.
Pertanto Γ A.
Caso [A]: impossibile in quanto un’ipotesi viene scaricata
solamente da una regola.
Claudio Sacerdoti Coen
Deduzione naturale
Teorema di correttezza per la logica
classica/intuizionista
n
(r ) dove T1 , . . . , Tn sono i sottoalberi immediati
Caso T1 ...T
F
dell’albero di deduzione:
Sia Ti la derivazione Γi ` Fi . Si ha Γi = Γ ∪ ∆i dove ∆i è
l’insieme delle ipotesi cancellate in Ti dalla regola r . Per ipotesi
induttiva, Γi Fi per ogni i. Per correttezza locale della regola r
si ha ∆1 ⇒ F1 , . . . , ∆n ⇒ Fn F . Quindi, per il teorema di
deduzione semantica e per la transitività della conseguenza
semantica, si ottiene Γ F .
NOTA: poichè l’unica assunzione sulle regole r è che siano
localmente corrette, potremo in seguito aggiungere altre regole
localmente corrette preservando la correttezza globale.
Claudio Sacerdoti Coen
Deduzione naturale
Teorema di deduzione sintattica
Teorema di deduzione sintattica: A ` B sse ` A ⇒ B.
Dimostrazione:
A
..
.
B
(⇒i )
A⇒B
Claudio Sacerdoti Coen
A⇒B A
(⇒e )
B
Deduzione naturale
Teorema di completezza intuizionista
Teorema di completezza per la logica intuizionista: se Γ F
allora Γ ` F .
Cenni: dobbiamo fare riferimento a una semantica intuizionista
fra quelle viste, ovvero la semantica di Kripke e quella di
Heyting-Brower-Kolmogorov.
Nel primo caso la dimostrazione è alquanto complessa e non è
possibile farla rientrare nel corso.
Nel secondo caso dobbiamo dimostrare che per ogni
programma per [[C]]v scritto facendo riferimento a funzioni di
libreria per la semantica delle formule in Γ esiste una prova di F
che usa le ipotesi in Γ. In altre parole, A OGNI PROGRAMMA
CORRISPONDE UNA PROVA (E VICEVERSA PER IL
TEOREMA DI CORRETTEZZA.
Claudio Sacerdoti Coen
Deduzione naturale
Teorema di completezza intuizionista
Teorema di completezza per la logica intuizionista: se Γ F
allora Γ ` F .
Per ottenere questo risultato è necessario fissare
esplicitamente il linguaggio di programmazione usato. Esso
corrisponde a un linguaggio funzionale, higher-order, tipato
semplicemente e dotato di coppie, proiezioni per le coppie,
booleani, if-then-else e niente altro.
Omettiamo la dimostrazione che, una volta fissato il linguaggio
in maniera appropriata, è una semplice induzione strutturale sul
programma dato in input.
NOTA: la logica determina il linguaggio di programmazione e
viceversa. Entrambi sono comunque estremamente naturali e
noti a priori.
Claudio Sacerdoti Coen
Deduzione naturale
Normalizzazione di prove
I linguaggi di programmazione sono caratterizzati dalle regole
di calcolo (o computazione).
La nozione corrispondente sulle prove è quella di
semplificazione di una prova.
La semplificazione è essenzialmente resa possibile dal fatto
che i connettivi di eliminazione sono ottenuti a partire da quelli
di introduzione e viceversa.
Un’introduzione seguita immediatamente da un conclusione
porta a una prova sempre semplificabile. Esistono altre regole
di semplificazione.
Semplificazioni ripetute portano a una forma normale che è
anche canonica.
Claudio Sacerdoti Coen
Deduzione naturale
Normalizzazione di prove
Esempio:
[A]
..
.
B
A⇒B
(⇒i )
B
..
.
A
(⇒e )
si semplifica in
..
.
A
..
.
B
mantenendo le stesse ipotesi e conclusioni. Semanticamente è
l’applicazione di funzione che si riduce a istanziare gli
argomenti.
Claudio Sacerdoti Coen
Deduzione naturale
Normalizzazione di prove
Esempio:
..
..
.
.
A
B
A∧B
A
(∧i )
(∧e1 )
si semplifica in
..
.
A
mantenendo le stesse ipotesi e conclusioni. Semanticamente è
la prima proiezione applicata a una coppia che ritorna il primo
elemento della coppia.
Claudio Sacerdoti Coen
Deduzione naturale
Normalizzazione di prove
Esempio:
..
.
A
A∨B
(∨i1 )
[A]
..
.
[B]
..
.
C
C
C
(∨e )
si semplifica in
..
.
A
..
.
C
mantenendo le stesse ipotesi e conclusioni. Semanticamente è
≈ la regola di riduzione dell’if-then-else nel caso true.
Claudio Sacerdoti Coen
Deduzione naturale
Normalizzazione di prove
Il corso (obbligatorio) di “Fondamenti Logici dell’Informatica” del
primo anno della Laurea Magistrale in Informatica è
interamente dedicato allo studio di questa corrispondenza fra:
Programmi e prove in logica intuizionista
Calcolo di un programma e semplificazione di prove
Tipi e formule
Linguaggi di programmazione e logiche intuizioniste
...
Claudio Sacerdoti Coen
Deduzione naturale
Deduzione naturale per la logica classica
Le regole viste fino ad ora NON sono complete per la logica
classica (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 convincersi
dell’impossibilità di costruire una derivazione.
Claudio Sacerdoti Coen
Deduzione naturale
Deduzione naturale per la logica classica: RAA
Per essere completi rispetto alla semantica classica, basta
introdurre la regola di Riduzione ad Assurdo (RAA):
[¬A]
..
.
⊥
A
(RAA)
Note:
La regola non è ne di introduzione, ne di eliminazione di un
connettivo.
Non avendo una regola duale (introduzione/eliminazione),
un teorema classico (= dimostrato con la RAA) non si
semplifica/normalizza. Meglio evitarla se possibile.
La regola è invertibile (in quanto A ¬A ⇒ ⊥) e sempre
applicabile (MALE!)
Claudio Sacerdoti Coen
Deduzione naturale
Deduzione naturale per la logica classica: RAA
Un uso frequente della RAA è il seguente schema
[¬A]
..
.
A
[¬A]
⊥
(¬e )
A
(RAA)
Ovvero, per trovare una prova di A ci si riduce a cercare ancora
una prova di A, ma dopo aver assunto ¬A.
Esercizio: dimostrare ` (¬A ⇒ A) ⇒ A.
Claudio Sacerdoti Coen
Deduzione naturale
Deduzione naturale per la logica classica: EM
Il principio del terzo escluso (EM) è dimostrabile a partire dalla
RAA:
Esercizio: ` A ∨ ¬A
In generale le dimostrazioni classiche effettuate con il solo
ausilio della RAA possono essere laboriose e/o anti-intuitive.
Tuttavia il principio del terzo escluso combinato con
l’eliminazione dell’or fornisce uno schema di prova molto
potente (analisi per casi su una variabile).
..
.
A ∨ ¬A
[A]
..
.
C
C
Claudio Sacerdoti Coen
[¬A]
..
.
C
(∨e )
Deduzione naturale
Deduzione naturale per la logica classica: EM
Metodo generalizzato:
Sia F una formula da dimostrarsi. Ripetendo per ognuna delle
variabili in Var (F ) = {A1 , . . . , An } l’analisi per casi (come per il
calcolo della forma normale di Shannon) ci si riduce a
dimostrare F sotto a n ipotesi aggiuntive [F1 ], . . . , [Fn ] tali che
per ogni i si ha Fi ∈ {Ai , ¬Ai }.
Esempio: dimostrare A ∧ B, B ⇒ C ` A ∨ C usando il metodo
generalizzato su A e su B.
Nota: usando il metodo generalizzato in genere NON si trovano
le dimostrazioni più semplici/naturali.
Tuttavia il metodo può essere usato meccanicamente per
decidere se ` F (vedi teorema di completezza nei prossimi
lucidi). L’albero di deduzione ottenuto è ancora una volta
esponenziale nel numero delle variabili.
Claudio Sacerdoti Coen
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 proposizionale
classica allora Γ ` F (potendo usare anche la RAA).
Nota: il teorema si dice di completezza debole per via della
limitazione a contesti Γ finiti. Per i teoremi di deduzione
sintattia/semantica, il teorema di completezza debole si può
riformulare come: se F allora ` F .
Corollario (teorema di COMPLETEZZA FORTE per la logica
classica): per ogni Γ, F , se Γ F allora Γ ` F .
Dimostrazione del corollario: sia Γ F . Per il teorema di
compattezza esiste ∆ ⊂ Γ, ∆ finito tale che ∆ F . Per il
teorema di completezza debole si ha ∆ ` F e quindi Γ ` F .
Claudio Sacerdoti Coen
Deduzione naturale
Teorema di completezza per la logica classica
Osservazioni:
Dal teorema di completezza debole e da quello di
compattezza deduciamo il teorema di completezza forte.
Poichè la prova di quello di compattezza non è costruttiva
(= la meta-logica è classica), NON OTTENIAMO ALCUN
ALGORITMO CHE DATO Γ E F RESTITUISCA UN
ALBERO DI PROVA Γ ` F .
Viceversa, forniremo ora una prova costruttiva del teorema
di completezza debole (= la meta-logica è intuizionista),
OTTENENDO UN ALGORITMO CHE DATO Γ FINITO E F
RESTITUISCE UN ALBERO DI PROVA Γ ` F .
La complessità dell’algoritmo sarà, ancora una volta,
esponenziale nel numero di atomi che occorrono nelle
formule.
Claudio Sacerdoti Coen
Deduzione naturale
Teorema di completezza per la logica classica
Dimostrazione del teorema di completezza debole per la logica
classica.
Dimostriamo il teorema nella sua forma equivalente se F
allora ` F .
La prima fase della dimostrazione consiste nell’applicare il
metodo generalizzato (slide 55) per ridursi, tramite il principio di
EM (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 è in relazione come segue con l’i-esima riga vi della tabella
di verità 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.
Poichè per ipotesi F si ha che, per ogni i, vi F .
Dobbiamo dimostrare ∆i ` F per ogni i.
Claudio Sacerdoti Coen
Deduzione naturale
Teorema di completezza per la logica classica
Lemma: per ogni F , per ogni i e per ogni vi e ∆i definiti come
sopra, si ha
1
se vi F allora ∆i ` F
2
se vi 6 F allora ∆i ` ¬F
Nota: la dimostrazione del lemma è 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
Claudio Sacerdoti Coen
Deduzione naturale
Teorema di completezza per la logica classica
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
2
(∧i )
Caso vi 6 F1 ∧ F2 o, equivalentemente [[F1 ∧ F2 ]]v = 0 e
quindi vi è un Fh con h ∈ {1, 2} t.c. [[Fh ]]v = 0.
Claudio Sacerdoti Coen
Deduzione naturale
Teorema di completezza per la logica classica
Per ipotesi induttiva ∆i ` ¬Fh e quindi
..
.
¬Fh
[F1 ∧ F2 ]
(∧eh )
Fh
(¬e )
⊥
¬(F1 ∧ F2 )
Claudio Sacerdoti Coen
(¬i )
Deduzione naturale
Teorema di completezza per la logica classica
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 = max{[[F1 ]]v , [[F2 ]]v } = 1 e quindi vi è un
h ∈ {1, 2} t.c. [[Fh ]]v = 1 e, per ipotesi induttiva, ∆i ` Fh :
..
.
Fh
(∨ih )
F1 ∨ F2
2
Caso vi 6 F1 ∨ F2 o, equivalentemente [[F1 ∨ F2 ]]v = 0 e
quindi [[F1 ]]v = [[F2 ]]v = 0.
Claudio Sacerdoti Coen
Deduzione naturale
Teorema di completezza per la logica classica
Per ipotesi induttiva ∆i ` ¬F1 e ∆i ` ¬F2 e quindi
[F1 ∨ F2 ]
..
.
¬F1
[F1 ]
..
.
¬F2
⊥
⊥
¬(F1 ∨ F2 )
Claudio Sacerdoti Coen
[F2 ]
⊥
(¬e )
(¬i )
Deduzione naturale
Teorema di completezza per la logica classica
Caso ¬F :
Per ipotesi induttiva si ha
1
se vi F allora ∆i ` F
2
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
Claudio Sacerdoti Coen
(¬i )
Deduzione naturale
Teorema di completezza per la logica classica
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
2
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.
Caso vi 6 F1 ⇒ F2 o, equivalentemente [[F1 ⇒ F2 ]]v = 0 e
quindi [[F1 ]]v = 1 e [[F2 ]]v = 0 e, per ipotesi induttiva,
∆i ` F1 e ∆i ` ¬F2 . Vedi slide dopo la prossima.
Claudio Sacerdoti Coen
Deduzione naturale
Teorema di completezza per la logica classica
Casi ∆i ` ¬F1 e ∆i ` F2 , dobbiamo dimostrare ∆i ` F1 ⇒ F2 :
..
.
¬F1
[F1 ]
⊥
(¬e )
F2
F1 ⇒ F2
(⊥e )
Claudio Sacerdoti Coen
(⇒i )
..
.
F2
F1 ⇒ F2
(⇒i )
Deduzione naturale
Teorema di completezza per la logica classica
Caso ∆i ` F1 e ∆i ` ¬F2 , dobbiamo dimostrare
∆i ` ¬(F1 ⇒ F2 ):
..
.
¬F2
..
.
F1
[F1 ⇒ F2 ]
(⇒e )
F2
(¬e )
⊥
¬(F1 ⇒ F2 )
Qed.
Claudio Sacerdoti Coen
(¬i )
Deduzione naturale
Correttezza, completezza, compattezza.
Abbiamo già visto: completezza debole ∧ compattezza ⇒
completezza forte.
Vale anche:
Teorema: completezza forte ∧ correttezza ⇒ compattezza.
Dimostrazione: siano Γ ed F tale che Γ F . Per il teorema di
completezza forte si ha Γ ` F , ovvero esiste un albero di
derivazione la cui radice è F e le cui foglie sono un insieme
finito ∆ ⊆ Γ. Per correttezza si ha ∆ F . Qed.
Osservazione: il precedente teorema ci dice che ogni prova
costruttiva del teorema di completezza forte ci darebbe una
prova costruttiva (un algoritmo) per il teorema di compattezza.
Non esistono prove del genere perchè si dimostra la non
esistenza degli algoritmi relativi.
Claudio Sacerdoti Coen