Logica, discorso e conoscenza Primo modulo: Logica e ...martini/CS/logicaCollSup456.pdf · Logica,...

92
Logica, discorso e conoscenza Primo modulo: Logica e verit` a (matematica) ovvero Logica, deduzione, verit` a Lezioni 4, 5 e 6 Simone Martini Dipartimento di Scienze dell’Informazione Alma mater studiorum – Universit` a di Bologna [email protected] Collegio Superiore Ottobre–novembre, 2006 1 / 92

Transcript of Logica, discorso e conoscenza Primo modulo: Logica e ...martini/CS/logicaCollSup456.pdf · Logica,...

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

[email protected]

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