Matematica Costruttiva. Seconda Lezione. Verità, …sacerdot/collegio/slides2.pdfLa logica...

La logica intuizionista

Matematica Costruttiva.

Seconda Lezione.

Verita, Esistenza, Conoscenza

Claudio Sacerdoti Coen<[email protected]>

Universita di Bologna

20/10/2010

Claudio Sacerdoti Coen


1 La logica intuizionista



Outline

1 La logica intuizionista



Assassini, innocenti, prove e arresti

Miss Scarlet e un’assassinaOgni assassino non e innocenteGiovanna Corsi non e innocenteArresti Miss Scarlet!L’ho vista commettere l’omicidio




So che c’e un’assassinoSia x l’assassinoOgni assassino non e innocentex non e innocenteSo che c’e un non innocenteSia x l’assassinoArresti x (??????)Ho visto un cadavere e non puo essersi pugnalato allaschiena da solo




So chi e l’assassinoSia x l’assassinoOgni assassino non e innocentex non e innocenteSo chi e il non innocenteSia x l’assassinoArresti x (!?)Ho visto Miss Scarlet commettere l’omicidio



Esempio matematico 1

Esistono (so che ci sono o so chi sono?) a,b irrazionali tali cheab e razionale.

Prova classica:√

2 e irrazionale. O√

2√

2e razionale oppure

no. Nel secondo caso (√

2√

2)√

2 =√

2(√

2·√

2)= 2 e razionale.

Costruzione: sia Q il quadrato di lato a.

Prova costruttiva:√

2log2 9

= 3 e log2 9 e irrazionale per ilteorema fondamentale dell’aritmetica.Costruzione: sia Q il quadrato di lato a.



Esempio matematico 2

Paradosso di Banach-Tarski sulla duplicabilita delle sfere.

Data una sfera S esistono 5 “pezzi” (insiemi disgiunti di punti)tali che S e l’unione di essi ed esistono traslazioni e rotazioniche applicate ai 5 pezzi fanno ottenere due sfere S1 e S2identiche a S.



Riduzione alla logica

“Miss Scarlet e l’assassina” = A(g)

“So che c’e un assassino” = ∃x .A(x)

“So chi e l’assassino” = Σx .A(x)




“Miss Scarlet e l’assassina” = A(g)“La procedura f mi dice chi e l’assassino di ogni vittima”

“So che c’e un assassino” = ∃x .A(x)“Per ogni vittima c’e un assassino”

“So chi e l’assassino” = Σx .A(x)“Per ogni vittima conosco l’assassino”




“Miss Scarlet e l’assassina” = A(g)“La procedura f mi dice chi e l’assassino di ogni vittima”f ∈ U → U, ∀x .A(f (x))

“So che c’e un assassino” = ∃x .A(x)“Per ogni vittima c’e un assassino”∀x .∃y .A(y)

“So chi e l’assassino” = Σx .A(x)“Per ogni vittima conosco l’assassino”∀x .Σy .A(y)




“Miss Scarlet e l’assassina” = A(g)“La procedura f mi dice chi e l’assassino di ogni vittima”f ∈ U → U, ∀x .A(f (x)) Cos’e una procedura?Funzione = procedura?

“So che c’e un assassino” = ∃x .A(x)“Per ogni vittima c’e un assassino”∀x .∃y .A(y) Dimostrabile, ma nessuna procedura

“So chi e l’assassino” = Σx .A(x)“Per ogni vittima conosco l’assassino”∀x .Σy .A(y) Esiste/ conosco la procedura?Posso concludere f ∈ U → U, ∀x .A(f (x))?



Matematica classica vs matematica costruttiva (1)

La matematica classica studia l’esistenza ∃Ma confonde ∃ con Σ (e funzione con procedura) con usoingiustificato di

assioma della sceltadefinizioni per casi (se . . . allora . . . altrimenti . . . )

Risultati “paradossali”: Banach-Tarski, esistenza di insieminon misurabili, etc.

La matematica costruttivaIn alcune varianti studia esplicitamente le procedure (la loroesistenza o la loro conoscenza)

Il risultato non sembra matematico

In altre studia la conoscenza Σ

Ma confonde Σ con ∃ e procedura con funzione



Logica Intuizionista del Prim’Ordine

Sintassi della logica intuizionista del prim’ordine:

Formule F ::= ⊥ | > | F + F | F ⇒ F | F ∧ F | Pn(t1, . . . , tn)| ∀x .F | Σx .F

Termini t ::= x | c | f n(t1, . . . , tn)

La negazione viene definita in funzione dell’implicazione:

¬F = F ⇒ ⊥

Precedenza degli operatori: ¬ > ∧ > + >⇒> ∀ = ΣEsempio: ∀x .Σy .P(x , y) ∧Q(x)⇒ Q(y)si legge ∀x .(Σy .((P(x , y) ∧Q(x))⇒ Q(y)))

P[t/x ] significa P dove sostituisco t al posto di x



Logica Intuizionista del Prim’Ordine

Lettura intesa:

⊥ falso, assurdo> vero, ovvieta, nulla da dimostrarePn(t1, . . . , tn) so che P vale per t1, . . . , tnF + G F o G, nel senso che so chi dei due e vera e percheF ∧G F e G, so che sono entrambe vere e percheF ⇒ G se so che F e vera e perche,

allora so anche G vera e perche∀x .P per ogni x so che P e vera e percheΣx .P so chi e un’x per il quale P e vera e perche



Semantica di Brouwer-Heyting-Kolmogorov

[[⊥]] = ∅ nessuna evidenza[[>]] = {?} una sola evidenza ?

[[Pn(t1, . . . , tn)]] = S[[Pn]]([[t1]],...,[[tn]]) insieme di evidenze (≈)[[F ∧G]] = [[F ]]× [[G]] coppie di evidenze[[F + G]] = [[F ]] + [[G]] = unione disgiunta delle evidenze{〈b,e〉| se b = 0 allora e ∈ [[F ]] altrimenti e ∈ [[G]]}

[[F ⇒ G]] ={p|p procedura che data f ∈ [[F ]] produce g(f ) ∈ [[G]]}

[[∀x .P]] = {p|p procedura che dato x produce p(x) ∈ [[P]]}[[Σx .P]] = {〈w ,p〉|p ∈ P[w/x ]} coppie di un testimone w eun’evidenza che P vale per w




Esempi:

f (p ∈ [[P]]) = 〈0,p〉 e un’evidenza per (dimostra) [[P ⇒ P + Q]]

f (g ∈ [[∀x .P(x)]]) = 〈33,g(33)〉e un’evidenza per [[(∀x .P(x))⇒ (Σx .P(x))]] ammesso che 33sia parte del dominio di interpretazione

vi e un’unica evidenza per ⊥ ⇒ P in quanto vi e una solafunzione dall’insieme vuoto ∅ = [[⊥]] a [[P]] (ex-falso)



Per confronto: semantica classica

La semantica della logica classica assegna a ogni proposizioneun valore di verita (nella seguente definizione ∅ per falso e {∅}per vero):

[[⊥]] = ∅[[>]] = {∅}[[Pn(t1, . . . , tn)]] ∈ {∅, {∅}} nessuna evidenza significativa[[F ∧G]] = [[F ]] ∩ [[G]]

[[F ∨G]] = [[F ]] ∪ [[G]] non si tiene traccia di cosa e vero[[F ⇒ G]] = [[F ]]c ∪ [[G]] nessuna procedura effettiva[[∀x .P]] =

⋂x{[[P]]} (≈) nessuna procedura effettiva

[[∃x .P]] =⋃

x{[[P]]} (≈) non si tiene traccia del testimoneIn particolare (terzo escluso): [[A ∨ ¬A]] = [[A]] ∪ [[A]]c ∪ ∅ = {∅}




Da ora in avanti identificheremo prove con evidenze eprocedure con procedure date in maniera esplicita, meccanicae terminanti in un tempo finito (≈ programmi).




NON VALIDITA DEL PRINCIPIO DEL TERZO ESCLUSO:Nel caso generale di una formula F non e ragionevoleassumere l’esistenza di alcuna evidenza per F + ¬F .

Esempio: sia F = (xn) = (yn). In un tempo finito non potro maiverificare ne l’uguaglianza, ne la diversita delle infinite coppie〈xi , yi〉 di elementi delle due successioni.

Esempio: sia x un oggetto a me inaccessibile e sia F = “x e dicolor rosso”. Sicuramente x e rosso oppure no, ma questo nonmi fornisce alcuna evidenza ne per F , ne per ¬F .




Definizione (decidibilita): F e decidibile se esiste una proceduraper F + ¬F .

Esempio: sia F (x) = “x e un numero pari”. Si ha F (x) edecidibile per ogni x . (Perche?)

Esempio: dati due numeri naturali, interi, razionali x , y , edecidibile se x = y . (Perche?)

Esempio: l’uguaglianza fra numeri reali NON e decidibile.(Perche?)

In logica classica (se confondiamo conoscenza e esistenza, +con ∨), tutto e decidibile.




NON VALIDITA DEL RAGIONAMENTO PER ASSURDO:Supponiamo di dover dimostrare P. Ragioniamo per assurdoassumendo un’evidenza generica ma fissata x per ¬P.Supponiamo di saper costruire un’evidenza q(x) per ⊥. Poichex e generica, otteniamo una procedura f (x) = q(x) che eun’evidenza per ¬¬P. In generale, non vi e alcun modo perottenere un’evidenza per P.

Similitudine: sapere che e impossibile che Paolo non sial’assassino non fornisce nessuna prova evidente percondannarlo oltre ogni ragionevole dubbio.

Esempio: ¬¬Σx .P(x) non ci dice per quale x valga P(x).



Negazione come assenza di informazione

Sia F una qualsiasi formula. [[F ]] puo avere una qualsiasicardinalita (0 se non dimostrabile, > 0 altrimenti)

Esempio: se F = Σx .P allora [[Σx .P]] contiene tutti quei w per iquali P vale.

[[¬F ]] = [[F ⇒ ⊥]] == {p|p procedura che data f ∈ [[F ]] produce g(f ) ∈ ∅ = [[G]]} =

=

{∅ se [[F ]] = ∅{∅} altrimenti

Quindi ¬F non puo possedere evidenze utili!In matematica costruttiva si cerca di evitare tutte le sentenzenegative in quanto non informative.



Doppia negazione come distruzione dell’informazione

La doppia negazione distrugge il contenuto informativo:

[[¬¬F ]] =

{∅ se [[F ]] = ∅{∅} se [[F ]] 6= ∅

E quindi evidente come da una doppia negazione(dimostrazione per assurdo) non sia possibile ricavareconoscenza (nel senso delle evidenze).

La conoscenza priva di evidenza corrisponde alla logicaclassica.



Logica classica nella logica intuizionista

Una formula ¬F per un qualche F si dice classica.

Definiamo:F ∨G := ¬¬(F + G) disgiunzione debole∃x .P := ¬¬Σx .P esistenziale debole

Nota:F ∨G puo essere dimostrabile (avere un’evidenza) senza chenemmeno una fra F e G sia dimostrabile.Analogamente ∃x .P puo essere dimostrabile anche quandoP[w/x ] non e dimostrabile per alcun w .




Teorema (terzo escluso): F ∨ ¬F .Dimostrazione: dobbiamo dimostrare ¬¬(F + ¬F ) ovvero((F + F ⇒ ⊥)⇒ ⊥)⇒ ⊥;assumendo ¬(F + ¬F ) (H), dobbiamo dimostrare ⊥;per (H) e sufficiente dimostrare (F + ¬F );dimostriamo che vale ¬F ;assumendo F (K), dobbiamo dimostrae ⊥; per (H) e sufficientedimostrare (F + ¬F );il che e dimostrabile usando l’ipotesi (K)




Teorema (dimostrazione per assurdo): sia F una formulaclassica. ¬¬F ⇒ F . Dimostrazione:sia F = ¬G;dobbiamo dimostrare ¬¬¬G⇒ ¬G;assumendo ¬¬¬G (H) e G (K), resta da dimostrare ⊥per (H), e sufficiente dimostrare ¬¬G;assumendo ¬G (I), resta da dimostrare ⊥per (I), e sufficiente dimostrare G;il che e dimostrabile usando l’ipotesi (K)




Teorema: siano F e G formule classiche.¬¬(F ∧G)⇒ ¬F ∧ ¬G(il prodotto cartesiano di insiemi vuoti o singoletti e ancoravuoto o singoletto; la congiunzione preserva l’assenza diinformazione)

Teorema: ¬¬⊥ ⇒ ⊥, ¬¬> ⇒ >(ove non vi e informazione non la si puo distruggere)

. . .

Conclusione: non serve introdurre una versione classica deglialtri connettivi poiche il comportamento su formule classiche egia classico.




La logica classica e un frammento della logica intuizionista che,pertanto, risulta piu espressivo.

Lavorando nel frammento classico si rinuncia al contenutoinformativo delle dimostrazioni e il ragionamento diventa noneffettivo.

In particolare, dimostrare ∃x .P non implica la conoscenza di unw per cui valga P, mentre questo avviene per Σx .P.

Analogamente, dimostrare P ∨Q non implica alcunaconoscenza di quale caso si verifiche, mentre questo avvieneper P + Q.



Note

In logica classica i connettivi Σ e + non sono definibili (se nonattraverso un deep embedding della logica).

La presentazione tradizionale della logica intuizionista omette iconnettivi ∃ e ∨ e chiama i connettivi Σ e + come ∃ e ∨.

Le due letture restano comunque distinte:per il classico tutti i connettivi parlano di esistenza e veritain un senso platonicoper l’intuizionista tutti i connettivi parlano di conoscenza o,in alternativa, di esistenza come risultato di unacostruzione umana



Problemi aperti

Cos’e una procedura?Quali oggetti matematici “esistono” costruttivamente?Cos’e costruttivamente valido? (vero o dimostrabile)Cos’e una dimostrazione costruttiva?C’e una “logica costruttiva”?Come posso spiegare costruttivamente la logica classica?E la matematica classica?Cosa posso sapere del contenuto computazionale?Quando e valido/accettabile l’assioma della scelta?E le definizioni per casi?C’e contenuto computazionale fuori dalla matematicacostruttiva?



Il problema centrale: le procedure

Una procedura y = f (x) permette a un esecutore di restituireun y ottenuto a partire da un x dato.

Quali “oggetti” possono essere dati? Come? (dipendedall’esecutore)Quali “oggetti” possono essere restituiti? Come? (dipendedall’esecutore)Quali “operazioni” consentono all’esecutore di ottenere ilrisultato?Esiste una nozione di tempo all’interno del quale operal’esecutore (diventando cosı soggetto creativo?)



Il problema centrale: gli oggetti

finiti (finitisti, ultrafinitisti)infiniti (e infinitesimi) potenziali (matematicapre-Cantoriana) e infiniti (e infinitesimi) attuali al piu concardinalita del continuo

assolutamente predeterminatolawlike (ottenuti grazie a una procedura deterministica epre-determinata)

Paradiso di Cantor (platonismo, internalismo, . . . ): e lecitoconsiderare tutti gli infiniti attuali ottenuti da qualunque“procedura” il piu liberale possibile (a meno di incoerenze)

lawless, possibly constrained (choice sequence)Richiede nozione di tempo e di soggetto creatore(intuizionismo)?

infiniti con cardinalita maggiore di quella del continuoParadiso di Cantor (p.e. cardinali inaccessibili)



Il problema centrale: considerare gli oggetti

Un “oggetto” puo essere considerato/percepito/letto:in un tempo finito (o istantaneo) e nella sua interezza

se e finitose e assolutamente predeterminato e ammette unadescrizione finitase e lawlike e la procedura ammette una descrizione finita(matematica ricorsiva, scuola Russa)?mai se e lawless (intuizionismo)se e lawlike e si suppongono capacita “sovrumane”(superiori a quelle di una macchina di Turing di tipo II):logica classica?

progressivamente (tramite approssimazioni successive)se la cardinalita e quella del continuo e la sequenzadetermina approssimazioni successivesenza differenze fra sequenze lawlike e lawless (Bishop!)



Il problema centrale: restituire un oggetto

produzione di un oggetto finito o un oggetto lawlike nellasua interezza

se l’oggetto di partenza e finito e la procedura e calcolabileda una macchina di Turing di tipo Ise l’oggetto di partenza e una successione lawlike, e sisuppongono capacita “sovrumane”

produzione di un oggetto enumerabile con cardinalita alpiu del continuo

se l’oggetto di partenza ha cardinalita al piu del continuo ela procedura e calcolabile da una macchina di Turing di tipoII (senza distinzione fra lawlike e lawless)l’oggetto prodotto e lawlike e si supponono capacita“sovrumane”

produzione di un oggetto piu che continuosolo in maniera non costruttiva (paradiso di Cantor)


Matematica Costruttiva. Seconda Lezione. Verità, …sacerdot/collegio/slides2.pdfLa logica...

Documents

Transcript of Matematica Costruttiva. Seconda Lezione. Verità, …sacerdot/collegio/slides2.pdfLa logica...