Logica, discorso e conoscenza
Primo modulo:
Logica e verita (matematica)ovvero Logica, deduzione, verita
Lezioni 4, 5 e 6
Simone Martini
Dipartimento di Scienze dellInformazioneAlma mater studiorum Universita di Bologna
Collegio Superiore
Ottobrenovembre, 2006
1 / 92
Outline
1 Quarta lezione: dimostrazioni
Sistemi formali per la derivabilita
2 Quinta lezione: laritmetica di Peano
Un sistema di assiomi; proprieta
3 Sesta lezione: i teoremi limitativi
I teoremi di Godel e Church
4 Temi desame
2 / 92
Dimostrazioni come oggetti formali
Un linguaggio L
Un insieme di formule su L, gli assiomi
Un insieme di regole di inferenza
Un insieme di (meta-)regole (sintattiche, combinatorie,
effettive) che spiegano come le regole di inferenza permettono
di dedurre nuove formule a partire da formula gia dedotte
Un teorema e una formula dedotta dagli assiomi con una serie
(finita) di applicazioni delle regole di inferenza
Nessun riferimento ad una specifica semantica o modello
inteso
3 / 92
Sistemi formaliPluralita di tipi di sistemi formali:
alla Hilbert (assiomi e regole)
il piu antico; comodo per parlare dei modelli di una teoria
deduzione naturale (Gentzen, 1934)
studio delle dimostrazioni come oggetti formali
sequenti (Gentzen, 1934)
studio delle dimostrazioni, dimostrazioni di consistenza
tableaux (Beth, 1955)
ricerca di dimostrazioni
risoluzione (Robinson, 1963)
ricerca di dimostrazioni
reti di dimostrazione (Girard, 1987)
dimostrazioni in logica lineare
ecc.
4 / 92
Esempio: logica positiva dellimplicazionealla Hilbert
(Schemi di) assioma1 A (B A) assioma K2 (A (B C )) ((A B) (A C )) assioma S
Regola di inferenza
P Q PQ
modus ponens
Meta-regole1 Ogni istanza di un assioma e un assioma2 Una derivazione e una sequenza di formule P0,P1, . . . ,Pn
dove ogni Pi e:F un assioma, oppureF e ottenuta mediante modus ponens da Pj e Pk , con j , k < i
5 / 92
Una derivazione
Vogliamo dimostrare A A(1) (A ((A A) A)) ((A (A A)) (A A))
assioma S(2) A ((A A) A)
assioma K(3) (A (A A)) (A A) MP, da (1) e (2)(4) A (A A)
assioma K(5) A A MP, da (3) e (4)
6 / 92
Logica classica proposizionale, alla Hilbert
1 A (B A)2 (A (B C )) ((A B) (A C ))3 B C B4 B C C5 B (C B C )6 B B C7 C B C8 (B D) ((C D) (B C D))9 (B C ) ((B C ) B)10 B (B C )11 A A
12 Regola: modus ponens
7 / 92
Logica classica dei predicati, alla Hilbert
1 Gli assiomi proposizionali
2 (8xP(x)) P(t)3 P(t) 9xP(x)4 8x(Q P(x)) (Q 8xP(x))5 8x(P(x) Q) (9xP(x) Q)6 Regole di inferenza
I modus ponensI
P(x)
8xP(x)generalizzazione
Condizione aggiuntiva: In 4 e 5, Q non deve contenere x (libera)
8 / 92
Altri sistemi logici
Diverso ruolo reciproco di assiomi e regole
Diversa nozione di dimostrazione (e.g., no successione di
formule, ma oggetto grafico bidimensionale)
Un certo sistema formale S da luogo ad una propria nozione
di derivazione `S
Equivalenza
Tutti i sistemi formali per la logica del primordine sono equivalenti
rispetto ai teoremi
cioe, dati due sistemi formali S e S 0, si ha
`S A sse `S 0 A
9 / 92
La deduzione naturale:calcolo minimale per e
Assiomi: nessuno
Regole:
A BA B
IA B
AE1
A BB
E2
[A]....B
A B I A B AB E
10 / 92
Deduzione naturale:un esempio di dimostrazione
` A B B A[A B]
A
[A B]
BA B B A
11 / 92
Dimostrazioni
`S A
la formula A e un teorema allinterno del sistema formale S
Possiamo usare anche assiomi propri
Sia uninsieme di formule (assiomi propri)
Una dimostrazione da (o in ) e una dimostrazione in
cui possono comparire (oltre ad assiomi o a formule
precedentemente derivate) anche (istanze del-) le formule di
`S A
la formula A e un teorema allinterno del sistema formale S, con
assiomi propri
12 / 92
Teoremi in specifiche teorie
I sistemi formali con assiomi propri permettono di indagare classi di
strutture matematiche (di modelli)
Grp ` P
Ord ` P
PA ` P
13 / 92
Consistenza
Un certo sistema logico S e consistente se 6`S A A
In virtu dellequivalenza dei sistemi logici rispetto ai teoremi,
possiamo considerare la consistenza come una proprieta delle
formule (e non dei sistemi formali)
Un insieme di formule e consistente
sse
6` A A
Se inconsistente, dimostra qualsiasi cosa:
per ogni B si ha ` B
14 / 92
Consistenza, 2
Nozione sintattica molto importante
Sistemi formali quali il calcolo dei sequenti sono stati
introdotti per dare dimostrazioni di consistenza
I sistemi formali che abbiamo visto sono tutti, per se,
consistenti
Importante: Consistenza di assiomi propri,
quali Ord, Grp, PA ?
15 / 92
Sintassi e semantica: correttezza
Teorema di correttezza (o validita, soundness):
` A = |= A
In particolare, se ` A, allora A e una legge logica
16 / 92
Consistenza, 3
Lesistenza di un modello per implica, per correttezza, la
consistenza di
(la semantica e platonicamente consistente)
Ma la costruzione di un modello coinvolge strumenti
semanticamente complessi (p.e., infinito)
Come dare dimostrazioni di consistenza sintattiche e
semplici?
Questo problema per laritmetica PA (quale fondamento
dellintera matematica) e il cuore del progetto hilbertiano
In effetti, Gentzen con i sequenti dimostra la consistenza di
PA, ma in modo non soddisfacente secondo Hilbert (e
necessariamente cos, dapres Godel)
17 / 92
La nozione di dimostrazione e decidibile
Nella definizione di sistema formale dicemmo
E presente un insieme di (meta-)regole (sintattiche, combinatorie,
effettive) che spiegano come le regole di inferenza permettono di
dedurre nuove formule a partire da formula gia dedotte
Deve essere sempre possibile, ispezionando una sequenza di
formule, decidere se si tratta di una dimostrazione nel senso
tecnico di questa parola
Cioe, la nozione di essere una dimostrazione nel sistema S e
decidibile
Proprieta intrinseca di un sistema formale: se non vale, non
abbiamo un sistema formale
18 / 92
La nozione di teorema e decidibile?
Una formula A e un teorema sse esiste una dimostrazione per
A
A differenza della nozione di dimostrazione, nella definizione
di sistema formale nulla impone che i teoremi siano decidibili
La nozione di sistema formale ci dice pero che, se gli assiomi
sono enumerabili, allora anche i teoremi sono enumerabili
meccanicamente:
parti dagli assiomi ed applica le regole in tutti i modi possibili
E semidecidibile se una formula e un teorema di una teoria
con assiomi enumerabili
Lo Entscheidungsproblem alla radice della logica (e
dellinformatica) moderna
19 / 92
Sintassi e semantica: completezza
Teorema di completezza:
|= A = ` A
In particolare, se A e una legge logica, allora ` A.
20 / 92
Lo Entscheidungsproblem proposizionale edecidibile
Esiste un mezzo automatico per decidere se una formula
proposizionale e una legge logica (tautologia):
le tabelle di verita
In virtu del teorema di completezza, questo e un procedimento
di decisione anche per la nozione di teorema proposizionale
Nel caso predicativo (puro) tale metodo non si puo applicare
21 / 92
Intermezzo: Una questione di cardinalita
Sia L un linguaggio del primordine e A uninterpretazione
per L, con dominio D
Una formula P(x) su L con una sola variabile libera x viene
interpretata come [[P(x)]]A 2 {V ,F }
Ovvero (solo x e libera):
[[P(x)]]A : D {V ,F }Quante sono le possibili funzioni D {V ,F }?E quante sono le possibili formule P(x) su L?
22 / 92
Quante sono le formule?
Lalfabeto di L e numerabile (cioe della cardinalita di N)Le formule sono certo non di piu di tutte le stringhe su tale
alfabeto
. . .
Le formule sono al piu di cardinalita numerabile anchesse
23 / 92
Quante sono le funzioni?
Largomento diagonale di Cantor
Un ragionamento per assurdo mostra che le funzioni
D {V ,F } non possono essere numerabiliEssendo certo di cardinalita infinita, esse sono di cardinalita
strettamente maggiore di NCi sono (molte) piu funzioni che formule!
Ci sono (molte) piu proprieta semantiche di quelle descrivibili
dal nostro linguaggio!
24 / 92
Largomento diagonale di Cantor
Supponiamo D numerabile e anzi che D = NSupponiamo che le funzioni N {V ,F } siano numerabili:{fi }i2N
Ogni funzione e una sequenza infinita (dove fi (n) 2 {V ,F })
fi : fi (0), fi (1), fi (2), fi (3), , fi (n),
Disponiamo i loro valori in una tabella infinita
f0 f0(0) f0(1) f0(2) . . . f0(i) . . .
f1 f1(0) f1(1) f1(2) . . . f1(i) . . .
f2 f2(0) f2(1) f2(2) . . . f2(i) . . ....
fi fi (0) fi (1) fi (2) . . . fi (i) . . ....
25 / 92
Largomento diagonale di Cantor, 2
Disponiamo i loro valori in una tabella infinita
f0 f0(0) f0(1) f0(2) . . . f0(i) . . .
f1 f1(0) f1(1) f1(2) . . . f1(i) . . .
f2 f2(0) f2(1) f2(2) . . . f2(i) . . ....
fi fi (0) fi (1) fi (2) . . . fi (i) . . ....
Definiamo la funzione g(n) = fn(n)
Puo la funzione gn : N {V ,F } comparire tra le {fi }i2N?No! Differisce da ciascuna di essa sulla diagonale
26 / 92
Questioni di cardinalita
There are more things in heaven and earth, Horatio,
Than are dreamt of in your philosophy.[W. Shakespeare, Hamlet, Act 1, Scene 5]
Ci son dunque (molte) piu proprieta vere su N di quante lanostra logica potra mai nominare
Restringiamo la nostra attenzione alle proprieta che possiamo
descrivere col linguaggio (le sole alla nostra portata)
Siamo in grado di dimostrare tutte le formule vere in N?Occorre in primo luogo unassiomatizzazione (delle proprieta
salienti) di N
27 / 92
Il teorema di Lowenheim-Skolem
Sia L un linguaggio del primordine
Sia un insieme di formule su L
Se ha un modello di cardinalita infinita, ha un modello di ogni
cardinalita infinita.
Corollario: Ogni teoria con modelli infiniti ha un modello
numerabile
Esempio: La teoria formale dei numeri reali
28 / 92
Aritmetica formale
Una teoria che formalizzi e descriva le proprieta vere in NIn un certo senso, che caratterizzi N. Che vuol dire?
I Che ha N come unico modello?I Che prova tutte e sole le proprieta vere in N?I Che sia in grado di distinguere N da altri eventuali modelli?
Hermann Grassmann, 1861. Lehrbuch der Arithmetik
Richard Dedekind, 1888. Was sind und was sollen die Zahlen?
Giuseppe Peano, 1889. Arithmetices principia, nova methodo
exposita
29 / 92
Gli assiomi di Peano
Da Arithmetices principia, con piccole modifiche notazionali. In
rosso le modifiche allassiomatica
1 2 N
a 2 N succ(a) 2 Na, b 2 N [a = b succ(a) = succ(b)]a 2 N succ(a) 6= 1a, b 2 N a + succ(b) = succ(a + b)a 2 N a + 1 = succ(a)a, b 2 N a succ(b) = a b + aa 2 N a 1 = ase k e una classe
[1 2 k (x 2 k succ(x) 2 k)] N k30 / 92
Il ruolo dellinduzione
se k e una classe
[1 2 k (x 2 k succ(x) 2 k)] N kLassioma di induzione e la vera potenza dellaritmetica
Senza di esso si potrebbero dimostrare solo enunciati puntuali,
come
(3 + 5) + 1 = 3 + (5 + 1)
senza poter dimostrare il caso generale (certo vero in N):
8a8b8c [(a + b) + c = a + (b + c)]
E una proprieta di chiusura:
Dice che (linterpretazione di) N e il piu piccolo insieme che
contiene 1 ed e chiuso rispetto al successore succ
31 / 92
Gli assiomi al primordine: PA
LPA: costanti: 0
LPA: funzioni: succ1
8a8b [succ(a) = succ(b) a = b]8a [succ(a) 6= 0]
8a8b [a + succ(b) = succ(a + b)]
8a [a + 0 = a]
8a8b [a succ(b) = a b + a]
8a [a 0 = 0]
Sia P una formula con la sola x libera
P(0) 8x [P(x) P(succ(x))] 8x P(x)
32 / 92
Commenti
Gli assiomi
8a [succ(a) 6= 0] 8a8b [succ(a) = succ(b) a = b]assicurano che il dominio (di ogni modello) e infinito
La definizione ricorsiva di somma e prodotto non da problemi
Lo schema di induzione
P(0) 8x [P(x) P(succ(x))] 8x P(x)sostituisce alla quantificazione sulle classi
se k e una classe [1 2 k (x 2 k succ(x) 2 k)] N k(cioe sulla semantica dei predicati) la variabilita sulle formule
Differenza di cardinalita sostanziale!
33 / 92
Modelli di PA
Non e difficile vedere che N |= PAMa: la costruzione di N e piu complessa della teoria PAInvero: N |= PA implica la consistenza di PAPer Lowenheim-Skolem esistono modelli in tutte le cardinalita
infinite
Dunque PA e ben lungi dal caratterizzare (almeno in
termini di modelli) N
34 / 92
Il teorema di compattezza
Modelli numerabili diversi da N?Si ottengono da un importante teorema della logica del primo
ordine
Teorema di compattezza
Se tutti i sottoinsiemi finiti di un insieme di formule hanno un
modello, allora anche lintero insieme ha un modello
35 / 92
Modelli non standard
Se tutti i sottoinsiemi finiti di un insieme di formule hanno un
modello, allora anche lintero insieme ha un modello
Aggiungiamo a LPA una nuova costante c , ottenendo LPA.
Su questo linguaggio, consideriamo le (infinite) formule
Pn c 6= n
PA = PA [ {Pn}n0
Ogni sottoinsieme finito di PA ha un ovvio modello
(Esercizio: quale?)
Dunque PA ha un modello; e un modello numerabile per LS
Chiamiamo modello non standard di PA ogni modello
numerabile di PA
36 / 92
Conseguenze del teorema di correttezza
Correttezza: PA ` Q = PA |= QDunque, tutti i teoremi di PA son veri anche nei modelli non
standard
Il che impone una struttura complessa in tali modelli
37 / 92
Qualche cenno alla struttura di unmodello non standard
0 1 n d 1 d d + 1 2d 1 2d 2d + 1
38 / 92
Livelli di descrizione
Fissiamo un linguaggio, un sistema formale e un modello.
Esempi canonici: LPA, PA, N oppure N non standard.Sia P(n) una proprieta sul modello (P : N {V ,F }).
P e definibile, se esiste una formula P(n) tale che
P(n) vero sse P(n) vero
P e rappresentabile (in modo forte), se esiste una formulaP(n) tale che
I per ogni n, se P(n) e vero, allora PA ` P(n)I per ogni n, se P(n) e falso, allora PA ` P(n)
Per cardinalita, esistono infinite proprieta non rappresentabili.
Non ci preoccuperanno molto (ma vedremo esempi per N e N).
39 / 92
Overspill
Se una proprieta vale per infiniti standard, allora vale anche per
qualche non standard
Corollario
Per un qualsiasi N , non esiste alcuna formula S(x) (nel
linguaggio LPA) tale che
S(n) vera sse n e standard
Non possiamo definire (separare) la parte standard di un modello
per mezzo del linguaggio LPA
40 / 92
Alcuni personaggi in commedia
Le formule (esprimibili in LPA) vere in NI costituiscono la teoria di N: Th(N)
Le formule (esprimibili in LPA) vere in tutti i modelliI {P | PA |= P}
Le formule (esprimibili in LPA) dimostrabili nella teoriaformale
I {P | PA ` P}
{P | PA ` P} = {P | PA |= P} Th(N)
(al primordine)
41 / 92
Laritmetica del secondordine
La teoria formale del secondo ordine PA2 sostituisce lo schema
dinduzione
P(0) 8x [P(x) P(succ(x))] 8x P(x)con lassioma di induzione
8P [P(0) 8x [P(x) P(succ(x))] 8x P(x)]
42 / 92
PA2 e categorica
PA2 ha un solo modello (che e ovviamente N)Sia M |= PA2E facile vedere che M deve contenere una copia di N.Sia essa St M
Definiamo su M la proprieta P(n) = V sse n 2 St
Certo 0 2 St, dunque vale P(0)
Supposto n 2 St, sia ha anche n + 1 2 St, ovvero
8n[P(n) P(succ(n))]Ma allora, per linduzione al secondo ordine, per ogni n 2M,
vale P(n), cioe n 2 St
Dunque M = St
43 / 92
Esercizio
Perche lo stesso ragionamento non si puo condurre per
laritmetica del primordine PA ?
Suggerimento: su quale proprieta deve essere applicata
linduzione ?
E qual e la differenza sostanziale tra linduzione in PA e quella
in PA2?
44 / 92
Al secondordine dunque. . .
Primo ordine:
{P | PA ` P} = {P | PA |= P} Th(N)
Secondo ordine:
{P | PA2 ` P} {P | PA2 |= P} = Th2(N)
Godel: entrambe le inclusioni sono proprie.
45 / 92
Incompletezza
Una teoria T e incompleta se esiste una formula G tale che ne
T ` G, ne T ` G
Se T e incompleta e consistente
Dunque ha modelli
Fissato uno di tali modelli, la formula indipendente G e
vera o falsa, in quel modello
Per completezza, vi saranno modelli in cui G e vera ed altri in
cui G e falsa
46 / 92
Vari risultati di incompletezza
Sia T una teoria con assiomi decidibili, che includa abbastanza
aritmetica.
Se T e vera (cioe N e un modello), e incompletaSe T e consistente, e incompleta
E possibile costruire una formula G nel linguaggio LPA, tale
che, se T e vera, G testimonia lincompletezza di T .
E possibile costruire una formula G nel linguaggio LPA, tale
che, se T e (-)consistente, G testimonia lincompletezza di
T .
Lultimo enunciato e propriamente il primo teorema di Godel
47 / 92
Una prima idea (molto rozza)
Sostituire il paradosso del mentitoreI Questa frase e falsa
(che non e un paradosso in PA, perche non formalizzabile)
con una formula della formaI Questa formula non e dimostrabile
Se la formula fosse dimostrabile, PA non sarebbe corretta
Se non e dimostrabile non ce paradosso, ma. . .
Se e vera in N, e una formula vera e non dimostrabile
48 / 92
Aritmetizzazione, 1
Aritemetizzazione = far corrispondere numeri e relazioni
aritmetiche ai concetti sintattici (linguaggio e derivazioni di PA).
Per il momento: tali relazioni sono semantiche (in N).Esempi:
Ad ogni termine t un numero ptq
Ad ogni formula A un numero pAq
Ad ogni successione di formule A1, . . . , An un numero
pA1, . . . , Anq
Informalmente:
p q : Sintassi N49 / 92
Funzioni effettive
I dettagli di p q non sono rilevanti
Importante:I p q deve essere davvero calcolabile in termini di + e
Scopo:I trasformare la p q semantica in termini e formule di LPA.
Col senno di poi:I p q e una funzione effettiva
Ovvero: (primitiva) ricorsiva, calcolabile secondo Turing,
calcolabile da un programma di calcolatore ecc.
Godel non aveva tale concetto e lo introduce!
50 / 92
Aritmetizzazione, 2
Un predicato effettivo Term(n) con valore 1 (vero) sse n e lacodifica di un termine
I Term(psucc(0)q) = 1I Term(p0 = 0q) = 0
Un predicato effettivo Fbf (n) con valore 1 (vero) sse n e lacodifica di una formula
I Fbf (psucc(0)q) = 0I Fbf (p0 = 0q) = 1
Un predicato effettivo Dimo(n) con valore 1 (vero) sse n e la
codifica di una successione di formule
Un predicato effettivo Dim(n,m) sse n codifica una
dimostrazione della formula (il cui codice e) m
51 / 92
Predicati decidibili
Tutti i predicati visti sinora ammettono un procedimento
(semantico) di decisione
Cioe un programma che in tempo finito risponde SI o NO
52 / 92
Mappa del teorema, 1
Codificare le operazioni sintattiche come relazioni
(semantiche) aritmetiche X
Riflettere tali operazioni semantiche nella sintassi. . .
53 / 92
Lemma di rappresentazione
Se P(n,m) e un predicato decidibile, esiste una formula P(x , y)
che rappresenta (in modo forte) P. Cioe:
per ogni n e m, se P(n,m) e vero, allora PA ` P(n,m)
per ogni n e m, se P(n,m) e falso, allora PA ` P(n,m)
Espressione (semantica) vs rappresentazione (sintattica)
54 / 92
Sul lemma di rappresentazione
Proprieta sintattiche corrispondono a dimostrabilita di
opportune formule
Il lemma vale per teorie molto piu deboli di PA. P.e.,Aritmetica di Robinson (Q):
I 8a8b [succ(a) = succ(b) a = b]I 8a [succ(a) 6= 0]I 8a8b [a + succ(b) = succ(a + b)]I 8a [a + 0 = a]I 8a8b [a succ(b) = a b + a]I 8a [a 0 = 0]I 8a[a 6= 0 9b(a = succ(b))]
55 / 92
Mappa del teorema, 2
Codificare le operazioni sintattiche come relazioni
(semantiche) aritmetiche X
Riflettere (rappresentare) tali operazioni semantiche nella
sintassi X
Autoriferimento. . .
56 / 92
Lemma di diagonalizzazione
Sia (x) una formula con la sola x libera. Allora e possibile
costruire una formula (senza variabili) tale che
PA ` (pq)Insomma:
e (nel sistema formale) la stessa cosa della formula (x)
applicata a (il numero di Godel di) se stessa
57 / 92
Sul lemma di diagonalizzazione
La dimostrazione usa prima le tecniche di aritmetizzazione,
poi il lemma di rappresentazione
Dunque la diagonalizzazione vale laddove vale la
rappresentazione
58 / 92
Mappa del teorema, 3
Codificare le operazioni sintattiche come relazioni
(semantiche) aritmetiche X
Riflettere (rappresentare) tali operazioni semantiche nella
sintassi X
Autoriferimento X
La formula godeliana. . .
59 / 92
Definiamo la formula Teor(x) 9y [Dim(y , x)]
Per diagonalizzazione costruiamo
G Teor(pGq)
60 / 92
Primo teorema di Godelversione semantica
Se PA ha assiomi veri (ovvero: se N e un modello di PA), alloraPA 6` G e anche PA 6` G.
61 / 92
G e vera
Segue subito che:
Se PA ha assiomi veri (ovvero: se N e un modello di PA), alloraN |= G.
Teor(x) 9y [Dim(y , x)]G Teor(pGq)Sappiamo che PA 6` G
Dunque, per ogni n, Dim(n, pGq) e falso
Per il lemma di rappresentazione, PA ` Dim(n, pGq)
Per correttezza, N |= Dim(n, pGq), per ogni nChe e lo stesso che N |= 9xDim(x , pGq)Ovvero N |= Teor(pGq)
62 / 92
Sulla versione semantica
Abbiamo una formula G
Che e vera nel modello standard NMa ne PA ` G , ne PA ` G
Il teorema e sufficiente se siamo convinti della consistenza di
PA
Ma e inutile se vogliamo indagare la consistenza
Osserva: il teorema vale anche per Q!
63 / 92
Incompletezza e Incompletabilita
Sia PA = PA + G
Ora PA ` G
Ma lesistenza di G dipende dal solo lemma di
rappresentazione
Possiamo rifare tutto, in riferimento a PA
Otterremo G indipendente in PA
E cos via. . .
Incompletabilita di PA (a dire il vero: di Q)
64 / 92
Primo teorema di Godelversione semantica
Sia T unestensione di Q i cui assiomi siano decidibili e veri in N.E possibile costruire una formula GT (nel linguaggio LPA) per cui
T 6` GT e anche T 6` GT .
65 / 92
Incompletabilita
Se vogliamo teorie con assiomi decidibili
e corrette (cioe i cui assiomi sono veri in N)non possiamo avere teorie complete
66 / 92
Primo teorema di Godel (-Rosser)versione sintattica
Sia T unestensione consistente di Q con assiomi decidibili.
E possibile costruire una formula GT (nel linguaggio LPA) per cui
T 6` GT e anche T 6` GT .
67 / 92
Anche PA2. . .
Teorema (Godel-Rosser)
Sia T unestensione consistente di Q con assiomi decidibili.
E possibile costruire una formula GT (nel linguaggio LPA) per cui
T 6` GT e anche T 6` GT .
PA2 e unestensione di Q con assiomi decidibili.
Se PA2 e consistente, e incompleta (e incompletabile)
Certo, PA2 dimostra cose che PA non dimostra:I PA2 ` GPA
PA2 6` GPA2
68 / 92
PA2 non gode del thm di completezza
PA2 6` GPA2
PA2 |= GPA2per gli stessi motivi per cui N |= GPADunque:
PA2 |= P 6= PA2 ` PAl primordine:
{P | PA ` P} = {P | PA |= P} Th(N)
Al secondordine:
{P | PA2 ` P} {P | PA2 |= P} = Th(N)
69 / 92
Verso gli altri teoremi limitativi
Gli ingredienti fondamentali del teorema di Godel:
Lemma di rappresentazione
Tutte le funzioni effettivamente calcolabili sono rappresentabili
in modo forte in Q
Lemma di diagonalizzazione
Segue da rappresentazione, se la sintassi e effettivamente
calcolabile
permettono di stabilire anche:
1 Teorema di Church
2 Teorema di Tarski
70 / 92
Il teorema di Church
Sia T unestensione consistente di Q con assiomi decidibili.
La nozione di essere un teorema di T non e decidibile.
Il teorema segue da questo lemma
Sia T unestensione consistente di Q con assiomi decidibili.
La nozione di essere un teorema di T (cioe il predicato Teor(n))
non e rappresentabile in modo forte in T .
che mostra le relazioni con le altre nozioni viste sino a qui.
71 / 92
Conseguenze per il calcolo puro
La nozione di essere un teorema del calcolo dei predicati puro
(cioe senza assiomi) non e decidibile.
Dim.: Il teorema di Church si applica allaritmetica di Robinson Q.
Q ha un numero finito di assiomi (a differenza di PA).
Allora Q ` P sse ` Q P.
72 / 92
Che fine ha fatto il mentitore?
Godel riposa sulla riflessione del metalinguaggio nel linguaggio
Allora forse questa frase e falsa e una proposizione
Certo il lemma di diagonalizzazione permette di dire
questa frase...
E possibile riflettere in LPA la metateoria semantica (cioe la
nozione di vero/falso)?
73 / 92
Un predicato di verita
Definiamo il predicato True(n) vero sse
n e il numero di Godel di una formula (in LPA) vera in N
Esiste una formula T (x) (in LPA) che definisca True?
Cioe per la quale valga:
True(n) vero in N sse T (n) vera in N
74 / 92
Il teorema di Tarski
Non esiste nel linguaggio LPA alcuna formula che definisca True.
75 / 92
Livelli di descrizione
Sia P(n) una qualche proprieta su N.P e definibile, se esiste una formula P(n) tale che
P(n) vero sse P(n) vero
P e rappresentabile, se esiste una formula P(n) tale cheI per ogni n, se P(n) e vero, allora PA ` P(n)I per ogni n, se P(n) e falso, allora PA ` P(n)
76 / 92
Livelli di descrizione, 2
Esistono proprieta non definibili: True(n)
Esistono proprieta definibili, ma non rappresentabili: Teor(n)
Teor(n) 9xDim(x , y)Esistono proprieta rappresentabili: ogni proprieta decidibile
77 / 92
Livelli di descrizione, 3
Lemma (rappresentazione):
Decidibile = Rappresentabile (in modo forte)
78 / 92
Verso il secondo teorema di Godel
(Mezzo) enunciato del primo teorema
Se PA e consistente, allora PA 6` G
Puo essere espresso nel linguaggio di PA
Sia Con Teor(pA Aq)E scriviamo
Con Teor(pGq)
79 / 92
Il secondo teorema di Godel
Non solo lenunciato del primo teorema e esprimibile. E addirittura
dimostrabile allinterno di PA:
Teorema
PA ` Con Teor(pGq)Ma allora:
Teorema (II teorema di Godel)
Se PA e consistente, allora PA 6` Con.
perche altrimenti avremmo PA ` Teor(pGq), ovvero (percostruzione di G ), PA ` G , che contraddice il primo teorema.
80 / 92
Vale per teorie piu semplici?
Il secondo teorema non vale per Q
Qualche forma di induzione e necessaria
Occorre lassioma dinduzione almeno per formule della forma
9xA, con A senza quantificatori. (1-formule)
81 / 92
PA e incompleta solo in casi patologici?
Le formule G e Con sono un caso patologico
Forse PA decide tutti i casi di genuino interesse matematico
No!I una variante del teorema di Ramsey finito,
Paris & Harrington, 1977I teorema di Goodstein
Kirby & Paris, 1980I molti altri. . .
82 / 92
Verso il teorema di Goodstein, 1
1 Rappresentazione pura di n in base kI Rappresenta n come somma di potenze di k
Esempio: 266 = 28 + 23 + 21
266 = 35 + 32 + 32 + 31 + 30 + 30
I Riscrivi gli esponenti di k come somma di potenze di k
266 = 223
+ 221+20 + 22
0
I E cos via
266 = 22(22
0+20)
+ 2220+20 + 22
0
266 = 3330+30+30 + 33
0+30 + 330
+ 30 + 30
83 / 92
Verso il teorema di Goodstein, 2
2 Bump: Bk(n)
Prendi la rappresentazione pura di n in base k e cambia k in
k + 1; sottrai 1
B2(266) = 33(3
30+30)+ 33
30+30 + 330 1 3.990838 1039
B2(19) = 7625597484990
3 Sequenza di Goodstein:
G (n) = n,B2(n),B3(B2(n)),B4(B3(B2(n))), . . .
Esempi:
G (3) = 3, 3, 3, 2, 1, 0
G (4) = 4, 26, 41, 60, 83, 109, 139, 173, 211, 253, 299, 348, . . .
G (6) = 6, 29, 257, 3125, 46655, 98039, 187243, . . .
84 / 92
Il teorema di Goodstein
Teorema (Goodstein)
Per ogni n, G (n) termina su zero.
Teorema (Kirby & Paris, 1982)
Lenunciato del teorema di Goodstein e formalizzabile in PA, ma
non e dimostrabile in PA.
Siccome PA e corretta, neppure la negazione del teorema e
dimostrabile in PA.
85 / 92
Vero e non dimostrabile
La validita del teorema di Goodstein non e un atto di fede
Abbiamo dimostrazioni perfette, ma. . .
esse utilizzano strumenti/concetti non esprimibili in PA
Thm di Goodstein: ordinali
Variante del Thm di Ramsey finito: lemma di Konig
86 / 92
Lemma di Konig
Un albero infinito che ad ogni nodo interno ha un numero finito di
figli, ha un cammino infinito.
Questo riferimento allinfinito non puo essere formalizzato in PA.
87 / 92
Principio di buon ordinamento
Un insieme non vuoto di numeri naturali possiede un elemento piu
piccolo di tutti gli altri.
Questo riferimento alla struttura ordinata (geometrica) non puo
essere formalizzato in PA.
Invero: tale principio implica linduzione al secondo ordine.
88 / 92
Le dimostrazioni in PA sonoaritmetiche?
[Una formula e dimostrabile in PA se] its truth or falsity [is]
perceived directly on the basis of [...] the fundamental nature and
structure of the natural numbers.[D. Isaacson, Some consideration on arithmetical truth and the -rule]
E una posizione difendibile/ragionevole?
89 / 92
Commenti
Scarto tra principi di costruzione e principi di
dimostrazione [Bailly&Longo]
Principi di costruzioneI Intuizione spazio-temporale della successione naturale
Principi di dimostrazione
I Induzione formale al I ordine
Gli enunciati indipendenti (e.g., Goodman) usano proprieta
(e.g., buon ordinamento) evidenti allintuizione
spazio-temporale, ma non colti dallinduzione.
Il formalismo e una visione limitata dellaccesso alla verita
(aritmetica)
90 / 92
Commenti, 2
Il formalismo ha dato vita alla (e sopravvive nella) informatica
Ma la bonta del prodotto (le macchine calcolatrici) non
giustifica il formalismo come filosofia della matematica. . .
91 / 92
Temi desame1 Il paradosso del mentitore: soluzioni moderne (non semplice)
(Etchemendy)
2 Il programma di Hilbert per la fondazione della matematica
3 I teoremi di completezza e compattezza per la logica dei predicati
4 Un sistema formale per la logica dei predicati: deduzione naturale
5 Un sistema formale per la logica dei predicati: calcolo dei sequenti
6 Un sistema formale per la logica dei predicati: risoluzione
7 Un sistema formale per la logica dei predicati: tableaux
8 La nozione di decidibilita (ovvero: rudimenti di calcolabilita)
9 Il teorema di Goodstein (richiede nozioni elementari di aritmetica ordinale)
10 Il lemma di diagonalizzazione (richiede rudimenti di calcolabilita)
11 Il lemma di rappresentazione (ovvero: aritmetizzazione della sintassi; per
chi ama le codifiche combinatorie)
12 La discussione filosofica sul teorema di Godel (p.e. Minds, machines
and Godel di Lukas ecc.)
13 Il teorema di Godel nella versione originale (-completezza).
92 / 92
Quarta lezione: dimostrazioniSistemi formali per la derivabilit
Quinta lezione: l'aritmetica di PeanoUn sistema di assiomi; propriet
Sesta lezione: i teoremi limitativiI teoremi di Gdel e Church
Temi d'esame