Elementi Di Logica

Transcript

Elementi di logica corsi di riconversione professionale Genova - 1995 appunti a uso interno: parte 4 Domingo Paola, liceo G. Bruno - Albenga, G.R.E.M.G. Dipartimento Matematica Genova Appunti sulla nozione di sistema formale e sui risultati metateorici relativi ai sistemi formali Sistema formale Un sistema formale S è una terna dove: L S è il linguaggio (formale), caratterizzato, a sua volta da: a) un insieme di simboli (alfabeto) b) un insieme di regole di buona formazione che consentono di generare un sottoinsieme di tutte le possibili sequenze (finite) di simboli di L S : l’insieme delle formule ben formate (f.b.f.) A S è un insieme di assiomi (di S), ossia un sottoinsieme di tutte le possibili f.b.f. di L S . R S è un insieme di regole inferenziali (o di derivazione) che consentono di ottenere f.b.f. a partire dagli assiomi di S. Ogni regola di inferenza può essere pensata come una funzione che associa a una n-upla di f.b.f. di L S una e una sola f.b.f. di L S . Linguaggio e metalinguaggio Quando si parla di un sistema formale e del relativo linguaggio, inevitabilmente si fa uso di un altro linguaggio. Per esempio, nella definizione sopra data di sistema formale abbiamo utilizzato la lingua italiana. Ricordiamo che in tal caso si dice che l’italiano è il metalinguaggio che serve per parlare di S. L S viene invece detto linguaggio oggetto. Nota che f.b.f. e assiomi di S sono espressi nel linguaggio oggetto L S .. Invece una regola inferenziale non è espressa nel linguaggio L S . Essa, come già accennato, esprime una relazione, anzi una dipendenza funzionale, fra un insieme di f.b.f. e un’altra f.b.f. di L S . Una regola inferenziale deve quindi essere espressa nel metalinguaggio. Sintassi e semantica Quando ci interessiamo allo studio di un sistema formale S limitandoci unicamente ad alcuni aspetti strutturali, quali, per esempio, la dimostrabilità di date formule di S, oppure il loro essere o meno ben formate, senza far riferimento ad alcun contenuto che possa dare alle formule stesse un significato, stiamo considerando il sistema S da un punto di vista puramente sintattico. Se, invece, ci occupiamo di attribuire un significato alle formule del sistema, o se precisiamo un insieme di oggetti di cui le formule devono parlare, allora stiamo considerando aspetti di carattere semantico. Sintassi e semantica sono due aspetti caratteristici di ogni linguaggio e, quindi, di ogni sistema formale. Essi possono essere studiati in una metateoria che abbia il sistema formale come oggetto di studio. Linguaggi del primo ordine Nello studio della logica dei predicati abbiamo introdotto variabili, predicati e quantificatori. Abbiamo anche visto che i quantificatori (universale ed esistenziale) si applicavano unicamente a variabili, a elementi di un insieme, ma mai a predicati o a insiemi. Un linguaggio caratterizzato dalla proprietà che solamente gli elementi di un insieme possono essere oggetto di quantificazione si dice del primo ordine. Per esempio la proprietà valida nell’insieme dei numeri naturali che afferma che Ogni sottoinsieme non vuoto di numeri naturali ammette minimo, presenta una quantificazione su insiemi. Tale proprietà non può quindi essere espressa, in questi termini, nel linguaggio dei predicati del primo ordine. Struttura Diciamo struttura una coppia in cui D è un insieme non vuoto detto dominio o supporto della struttura; R è un insieme di relazioni definite in D. Eventualmente è possibile definire anche un insieme F di funzioni definite in D e un sottoinsieme P di elementi i D che, per qualche motivo vengono considerati elementi privilegiati. In tal caso una struttura assuma la forma di una quadrupla del tipo < D, R, F, P >. Per esempio, la tripla individua la struttura avente per dominio l’insieme dei numeri interi, nel quale sono definite le operazioni di addizione e moltiplicazione e avente come elementi privilegiati l’identità additiva e moltiplicativa. Interpretazione o realizzazione di un sistema formale. Quando analizziamo una teoria dal punto di vista puramente sintattico, vuol dire che consideriamo, per il suo linguaggio, un alfabeto, un insieme di regole di formazione in base alle quali sia possibile distinguere le f. b.f. dalle altre stringhe, un insieme di assiomi e, infine, le regole di derivazione che consentono di ottenere, a partire dagli assiomi, altre f.b.f.. In tal caso non ci interessa fornire alcuna chiave di interpretazione per i segni dell' alfabeto del linguaggio, in particolare per le sue f.b.f. : gli uni e le altre non sono altro che puri segni tipografici. In conseguenza di tale fatto nemmeno alle proposizioni scelte come fondamento della teoria, ossia agli assiomi, è possibile attribuire un significato, ad esempio dire se sono veri o falsi. I linguaggi, però, sono costruiti per poter parlare di qualcosa: proprio per tale motivo è particolarmente importante interessarsi oltre che all' aspetto sintattico di un linguaggio, anche a quello semantico, ossia ai significati che è possibile attribuire alle sue f.b.f. . L' attribuzione di un significato ai segni di un linguaggio formale L , in particolare alle sue formule ben formate consente di utilizzare il linguaggio L per descrivere strutture, ossia insiemi di oggetti su cui sono definite relazioni e funzioni Un sistema formale , un esempio di suo modello e una breve digressione sul formalismo. Consideriamo il sistema formale L0 che ha: a) come alfabeto : { p N O E S A } b) come unico assioma : p c) come regole di produzione di formule ben formate: R1 : " una stringa di L0 è ben formata se e solo se inizia per p ma non con pA " R2 : " una sequenza ripetuta di E oppure di O oppure di N oppure di S può essere rimpiazzata, rispettivamente, con una sola E, oppure una sola O, oppure una sola N, oppure una sola S" R3 : " ogni volta che in una stringa compaiono le sequenze EO, oppure OE , oppure NS , oppure SN, esse possono essere soppresse" Ad esempio, sono f.b.f pNASO ; pSENNO ; pSANO ; pOSANO ; pESO ..... Nota che la stringa pSENNO potrebbe essere semplificata, in virtù della regola R 2 con la stringa pSENO Non sono f.b.f. ANNO ; ASSE ; NASO ; OSA pASO...... Una possibile realizzazione per L0 è costituita dal supporto I , insieme prodotto cartesiano Z x Z in cui è stato fissato un sistema di riferimento con origine in (0,0) e con due assi fra loro perpendicolari . Gli elementi di I sono quindi le coppie ordinate (m,n) in cui m e n sono numeri interi. Ad esempio, sono elementi di I : (-2, 5) ; (0,0); (-4;-6) ; (10, 80) e così via. Una rappresentazione grafica di I può essere la seguente: . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . /|\ | . . . . . . . 0,0 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . --> . . . . . . . Puoi anche pensare, se preferisci ad una scacchiera in cui siano state opportunamente numerate le caselle a partire da una casella origine indicata con (0,0) Alla costante p viene assegnato il significato (0,0) , ossia l' origine dell' insieme S (la casella di partenza della scacchiera infinita). Alle costanti N, O, E, S, A vengono rispettivamente assegnati i significati: N = "direzione Nord" O = " direzione Ovest" E = "direzione Est" S = "direzione Sud" A = " fai un passo avanti sul reticolato S (o sulla scacchiera infinita)" Ad ogni teorema di L0 viene associata una posizione sulla scacchiera e, quindi, un individuo del supporto I . Deriviamo, come esempio un teorema di L0 : partiamo dall' assioma p ; la R1 ci assicura che, purché non si utilizzi il segno alfabetico A, si ottiene una stringa ben formata giustapponendo a p un qualunque altro simbolo alfabetico. Deriviamo quindi pE. pE è già un teorema di L0. Partendo da pE vogliamo derivare un altro teorema. Per R1 siamo ora liberi di giustapporre a pE una qualunque sequenza di segni alfabetici. Scegliamo pEANO (in onore del grande matematico italiano del nostro secolo). pEANO è un teorema di L0. La sua interpretazione, nei termini di posizione sul reticolato Z x Z è immediata: partiamo dall' origine p, ossia dal punto (0,0) ; ci posizioniamo in direzione Est (E); compiamo un passo avanti sul reticolato, raggiungendo , per come è stato fissato l' orientamento, la posizione A, ossia il punto (1,0) . Ci rivolgiamo in direzione Nord (N); ci rivolgiamo in direzione Ovest (O) . . . . . . . . . . . . . 0,0 1,0 . . . . . . . . . Nota che sono possibili altre interpretazioni del sistema formale: ad esempio, lasciando inalterato il significato di N , O, E ,S , si potrebbe assegnare ad A il significato di " eseguire un' ora di volo nella direzione indicata dalla stringa che precede A e segue un' altra A". Si potrebbero inventare altre semantiche completamente diverse da quelle precedenti: è un lavoro che richiede senza dubbio molta fantasia e che sottolinea l' enorme potere espressivo implicito nei sistemi formali. Nel corso che hai fino ad ora seguito, il concetto di dimostrazione ha avuto un ruolo di grande importanza. Ci sembra importante, quindi, dedicare in questo capitolo un po’ di spazio ad alcune ulteriori riflessioni sulla nozione di dimostrazione e sulle sue interrelazioni con quella di verità.Prima, però, diamo qualche definizione. Interpretazione Si dice interpretazione di un sistema formale una struttura con una funzione g che associa: a) ad ogni costante e variabile individuale e ad ogni termine un individuo del supporto; b) ad ogni simbolo di funzione, una funzione definita nel dominio della struttura, ovviamente rispettando la condizione che simbolo per funzione e funzione associata abbiano lo stesso numero di argomenti; c) ad ogni simbolo di predicato o relazione, una relazione definita nel dominio della struttura; anche in tal caso è necessario rispettare la condizione di uguaglianza fra il numero degli argomenti del simbolo di predicato o di relazione e il numero degli argomenti della relazione associata; d) al simbolo “ = ” la relazione identica del dominio della struttura. Le variabili variano sugli individui del supporto, nel senso che possono assumere individui del supporto come loro valori. Modello di un sistema formale Quando sia stata data una interpretazione di un sistema formale, gli assiomi acquistano un significato, in quanto diventano asserzioni sul supporto stesso. Solo in tal caso possiamo parlare di verità o falsità di un assioma.Se accade che l' interpretazione assegnata rende veri tutti gli assiomi, si dice che il supporto fornisce un modello degli assiomi. Del resto, poiché gli assiomi stessi caratterizzano l' intero sistema teorico, si dice che il supporto costituisce, nelle condizioni sopra specificate, un modello del sistema formale o del relativo linguaggio. Soddisfacibilità Caratterizziamo la nozione di soddisfacibilità mediante qualche esempio. La formula x2 > 9 si dice soddisfacibile nella struttura dei numeri reali, in quanto è soddisfatta da qualche assegnazione per la sua variabile x. Per esempio, tutti i numeri reali maggiori di 3 o minori di -3 la soddisfano, mentre non la soddisfano i numeri reali appartenenti all’intervallo [-3,3].La formula x < 0 non è soddisfacibile in N in quanto non esistono interpretazioni che la soddisfano. E’ invece soddisfacibile, in N , la formula x > 5. Verità Data una struttura M una formula si dice vera in M se e solo se è soddisfatta da ogni possibile interpretazione (delle sue variabili libere). Notiamo che le formule chiuse sono sempre o vere o false in una struttura. Validità Una f.b.f. A di un linguaggio L si dice valida (o logicamente vera) quando è vera in ogni possibile struttura. Notiamo che una formula può essere vera in una data interpretazione, ma non vera in un’altra e, di conseguenza, non valida. Conseguenza diretta Una formula p ottenuta applicando la regola di inferenza R alle f.b.f. a1 , a2 ,..., an è detta conseguenza diretta di a1 , a2 ,..., an mediante R. Dimostrazione Una dimostrazione in un sistema formale S è una sequenza finita di f.b.f. di S, ciascuna delle quali è un assioma oppure è conseguenza diretta di f.b.f. (che la precedono) mediante una regola inferenziale R . Teorema Un teorema di S è la formula finale f che si ottiene in una dimostrazione. Per affermare che f è un teorema di S scriviamo S |--- f . Quando nella dimostrazione di f si fanno altre assunzioni (ipotesi), per esempio h1 , h2 ,...., hn , oltre agli assiomi di S , si scrive SU{ h 1 , h2 ,...., hn } |--- f. Conseguenza logica Dato un sistema formale S e il relativo linguaggio L, una f.b.f. A di L si dice conseguenza logica di (degli assiomi di ) S, quando ogni modello di S è anche modello di A. Verità e dimostrazione Se riflettiamo sulla struttura delle dimostrazioni possiamo giungere alle seguenti conclusioni: a) una dimostrazione non enuncia proprietà di proposizioni, bensì evidenzia una relazione tra differenti proposizioni; b) una dimostrazione è un ragionamento mediante il quale si giustificano, sotto debite condizioni, valutazioni sul valore di verità di proposizioni nel contesto della matematica. Nonostante siano spesso confuse fra loro, verità dimostrazione sono due nozioni ben distinte: la prima è una proprietà di cui una proposizione gode o non gode; ad esempio, la proposizione p  x  N : x+2 = 3 è vera, mentre la proposizione q  x  N : x+2 = 0 è falsa. La dimostrazione, invece, non è un requisito di cui una proposizione possa o meno godere: si può dire se una proposizione è o non è dimostrabile solo facendo riferimento ad altre proposizioni e a un ben determinato insieme di regole inferenziali. Ad esempio, la proposizione "la bisettrice dell' angolo al vertice di un triangolo isoscele è anche mediana ed altezza relativa alla base" è dimostrabile nel sistema assiomatico della geometria euclidea. Invece la proposizione " per un punto esterno a una retta data passa una e una sola parallela " non è dimostrabile nel sistema assiomatico formato, ad esempio, dai primi due assiomi presentati nel capitolo di geometria del primo volume. Ora che abbiamo chiarito il concetto di verità (in una determinata interpretazione), possiamo dire che un legame tra dimostrabilità e verità è offerto dalla seguente affermazione: se una proposizione è dimostrabile (in un dato sistema formale), allora è valida (ossia vera in ogni interpretazione di quel sistema) Se si potesse affermare anche l’implicazione inversa, allora dimostrabilità e validità di una proposizione sarebbero fortemente correlate. Vedremo, però, che così non è: non per tutti i sistemi interessanti della matematica tutte le proposizioni valide sono dimostrabili. Ti facciamo inoltre notare che il concetto di dimostrazione è tipicamente sintattico, mentre quelli di verità, soddisfacibilità e validità sono tipicamente semantici. Osservazione Un’idea per una definizione di "verità" Una definizione deve avere la forma di un' equivalenza logica, ossia deve essere del tipo "x se e solo se y" , dove x, primo membro dell' equivalenza, è detto definiendum, mentre il secondo membro y è detto definiens. Perché una definizione sia accettabile, il definiendum non deve comparire come termine del definiens; se ciò accade si ha un circolo vizioso, come nella definizione classica della probabilità. Se vogliamo definire il termine "vero" , dovremo fare in modo che tale termine compaia solo nel definiendum. Se ci riferiamo alla proposizione P " Il sole è una stella " , possiamo chiederci che cosa si intende dicendo che P è vera. La risposta che daremo può sembrarti banale, ma, in realtà, è molto profonda: "il sole è una stella" è vera se e solo se il sole è una stella. Come vedi la formulazione della nozione di verità in relazione alla proposizione p assume la forma di un' equivalenza logica, come avevamo richiesto. Potrebbe sembrarti che, però, il definiendum compaia nel definiens e che, quindi la definizione non sia accettabile. Se però rifletti attentamente dovresti accorgerti che la proposizione che compare come definiendum è "il sole è una stella" è vera ed ha come soggetto un ente linguistico: l' intera proposizione tra virgolette. Il soggetto del definiens (il sole), invece appartiene al mondo reale anche se viene denotato, e ciò è la fonte di confusione, con un ente linguistico (la parola composta delle quattro lettere s,o,l,e). In altri termini, si potrebbe riformulare la definizione di vero riferita alla proposizione p in questo modo: "la proposizione della lingua italiana costituita dalla successione dei simboli tipografici i , l , spazio, s, o ,l, e, spazio, è, spazio, u , n , a, spazio, s, t ,e , l, l , a è vera se e solo se il sole è una stella ". In tal modo sparisce ogni apparenza di circolo vizioso nella definizione di verità riferita alla proposizione P. Così come abbiamo fatto per la proposizione P potremmo fare per molte altre proposizioni e, in generale, sotto alcune condizioni più restrittive che qui non menzioniamo, generalizzare il concetto di verità riferito ad una proposizione P con la seguente definizione: " P " è vera se e solo se P. La trattazione del concetto di verità in questa formulazione è dovuta ad uno dei maggiori logici del nostro tempo: il polacco Alfred TarsKi. Una definizione di verità del tipo visto non può dirti nulla su come determinare il valore di verità di una proposizione. La definizione data non esplicita alcun criterio che consenta di individuare se una proposizione è vera o falsa. Solo un' indagine specifica basata su criteri stabiliti nell' ambito della disciplina in cui la proposizione è stata formulata potrà stabilire la verità o meno della proposizione stessa. Così un' indagine fisica sulla natura del sole potrà, in base ai criteri stabiliti dai fisici, assicurarci che il sole è una stella e, quindi, che la proposizione "il sole è una stella" è vera. Terminata questa prima carrellata su alcuni dei concetti che la logica matematica ha come oggetto di studio, passiamo ad esibire alcuni esempi di sistemi formali. 2. Un sistema formale per la logica proposizionale: il linguaggio L1 Per formalizzare la logica proposizionale e, più in generale, per trasformare un linguaggio logico L in un sistema formale S dovremo: a) definire le formule ben formate (f.b.f.) di L; b) scegliere fra le varie f.b.f. di L che traducono regole logiche, alcune formule che assumono il ruolo di assiomi di S; c) fissare fra le varie f.b.f di L che traducono regole logiche, alcune formule che assumono il ruolo di regole inferenziali di S; d) derivare dagli assiomi di S (f.b.f di L che traducono regole logiche) teoremi di S (altre f.b.f di L che traducono regole logiche) mediante regole di S (altre f.b.f di L che traducono regole logiche). Il vantaggio, di fronte all’apparente aumento di complessità, è quello di rendere gestibile l’insieme delle regole logiche, o meglio delle f.b.f. di L che esprimono regole logiche. Infatti si richiederà, necessariamente, che tutti i teoremi di S siano formule valide di L (validità o correttezza del sistema S) e, se possibile, che l’insieme dei teoremi di S esaurisca le formule valide di L (completezza o adeguatezza di S). Le due condizioni di validità e di completezza considerate insieme richiedono che i teoremi di S coincidano con le formule valide di L. Torneremo su questi aspetti in seguito. Vediamo di mettere in pratica le operazioni ora descritte per costruire il sistema formale della logica proposizionale, cui diamo il nome L1. L1 si forma sull' alfabeto: p ' ~ ( ) dove la lettera P , eventualmente seguita da apici, indica gli oggetti elementari del linguaggio, detti anche atomi o enunciati. Ad esempio p p ' p '' sono tre atomi differenti. A livello semantico, quando per gli atomi si fornisce un significato, ad esempio vero (V) o falso (F), si parla di p p ' p '' come di proposizioni. I segni ~ ,  sono simboli per connettivi logici. Le parentesi sono segni ausiliari utilizzati solamente per semplificare la scrittura delle stringhe di L1. Regole di formazione L1 è caratterizzato dalle seguenti regole di formazione di f.b.f.: 0. tutti gli atomi sono ben formati; (tale regola è detta anche regola di base ; per tale motivo l' abbiano contrassegnata con il numero 0) 1. se X è f.b.f. allora ~ X è f.b.f. 2. se X e Y sono f.b.f. , allora ( X  Y) è f.b.f. 6. nessun' altra stringa è f.b.f. di L1 (tale regola è detta regola di chiusura) Facciamo inoltre uso della convenzione di omettere, in una formula, le parentesi più esterne ogniqualvolta ciò non sia fonte di possibili di ambiguità. Nota che X e Y rappresentano una qualunque stringa di L1: sono quindi variabili metalinguistiche utilizzate per rappresentare formule qualsiasi (e quindi atomiche, ma anche composte) di L1. Assiomi di L1 Facciamo uso di variabili metalinguistiche anche per enunciare i seguenti assiomi della logica proposizionale. X  (Y  X) A2 : ( X (Y  Z))  ((X  Y )  (X  Z)) A3 : (~ X  ~Y)  (( ~ X  Y )  X ) A1 : Se passiamo dal piano sintattico di L1 a quello semantico, interpretando gli atomi come proposizioni vere o false, allora possiamo verificare, utilizzando il metodo delle tavole di verità, che gli assiomi sono schemi di tautologie, ossia schemi di proposizioni composte che hanno valore di verità V per ogni possibile valore di verità delle proposizioni componenti. Verifichiamo, ad esempio, che l' assioma A1 rappresenta, quali che siano le proposizioni di L1 rappresenbtate con X e Y, una tautologia. Costruiamo la tavola di verità sostituendo a Xe Y tutti i relativi valori di verità possibili: Y X Y X X (Y  X) ________________________________________________ V V V V V F F V F V V V F F V V Come puoi vedere, il valore di verità di A1 è V qualunque siano i valori di verità delle proposizioni X , Y, Y ----> X che lo compongono. Quindi A1 ( o meglio ciascuna proposizione costruita secondo lo schema A1) è una tautologia. Come abbiamo già accennato, poiché gli assiomi sono stati forniti utilizzando variabili metalinguistiche e non atomi di L1, sarebbe più corretto parlare, invece che di assiomi, di schemi di assiomi. Essi, cioè, sono validi per infinite formule di L1 e rappresentano, quindi, un' infinità di assiomi. Ad esempio, A1 garantisce che p  (p '  p) , oppure p '' ( p '  p '') , oppure (p  p ')  (p '' ( p  p ') sono tre degli infiniti assiomi di L1 rappresentati dallo schema A1. Puoi verificare quanto ora affermato stabilendo, per ciascuno dei tre esempi, una corrispondenza fra le variabili metalinguistiche utilizzate per enunciare lo schema di assiomi A1 e gli atomi di L1 utilizzati per enunciare i tre assiomi. La seguente tabella suggerisce quale sia la corrispondenza corretta: ___________________________________________________________________________ X Y p  (p '  p) p p' p '' ( p '  p '') p '' p' (p  p ') ( p '' ( p  p ') (p  p ' ) p '' ____________________________________________________________________________ _____________________________________________________________________ Osservazione . Non tutti i connettivi sono necessari! Come puoi notare, nella formulazione degli assiomi di L1 compaiono i soli connettivi ~ ,  Questo fatto, dato che le proposizioni di L1 sono generate a partire dagli assiomi, suggerisce che per esprimere proposizioni nel linguaggio L1 non siano necessari altri connettivi oltre a ~ ,  e che, quindi, i connettivi /\, \/ ,  siano utilizzati solo per semplificare le espressioni del linguaggio, un po' come quando si usa , nel linguaggio algebrico, la notazione (a+b)3 per evitare di scrivere (a+b)(a+b)(a+b). In effetti i connettivi /\ , \/ ,  possono essere definiti a partire da  , ~ nel seguente modo: X /\ Y sta per ~(X  ~ Y) sta per ~ X  X \/ Y X Y Y ~ (( X  Y )  sta per ~(Y  X)) Possiamo mostrare, assegnando un significato (V o F) agli atomi e utilizzando le tavole di verità, che si tratta di buone definizioni. Verifichiamo, ad esempio, che la tavola di verità di X /\ Y è identica a quella di ~(X  ~ Y) : X Y V V F F V F V F X /\ Y V F F F X V V F F Y V F V F ~ Y F V F V X  ~ F V V V ~(X  ~ Y) V F F F Y Poiché le due tavole di verità coincidono, le proposizioni X /\ Y e ~(X  ~ Y) hanno lo stesso valore di verità per ogni possibile valore di verità delle proposizioni che le compongono. Ciò giustifica la loro identificazione. Nota che l’identificazione viene effettuata nel metalinguaggio. A rigore, quindi, la proposizione p /\ q non può essere considerata f.b.f. di L1 (secondo le regole di buona formazione da noi scelte). Diremo, invece, che è ben formata la formula ~(p  ~ q) di L1 che corrisponde a p /\ q. ___________________________________________________________________________ Regole di inferenza Il sistema formale L1, è caratterizzato da una sola regola di inferenza detta regola di separazione o modus ponens (MP): Modus ponens X X Y MP : ------------------ Y La regola precedente assicura la possibilità, date le due formule X e X Y, di derivare la formula Y. Spesso si usa, per indicare L1, il termine calcolo delle proposizioni . Tale nome è particolarmente indicato: in un certo senso i teoremi di L1 vengono calcolati, a partire dagli assiomi, mediante operazioni logiche. Esempi di derivazioni in L1 Vogliamo fornire un esempio di derivazione in L1, per la precisione, vogliamo derivare la stringa di L1 p  p. Partendo dall' assioma A2 deriviamo la stringa: (1) (p  ((p  p)  p))  ((p  (p  p.)) (p  p.)) dove abbiamo sostituito X con p; Y con (p  p); Z con p. Dall' assioma A1 deriviamo la stringa: (2) p ((p  p)  p) dove, come nel caso precedente, abbiamo sostituito X con p; Y con (p  p); Z con p Se osservi attentamente la struttura formale di (1) e (2), dovresti accorgerti che la (2) figura come antecedente nella (1). E' quindi possibile applicare la regola MP. Da (1) /\ (2), per MP abbiamo: (3) (( p  (p  p))  (p  p)) Dall' assioma A1 possiamo derivare la stringa: (4) p (p  p) dove abbiamo sostituito X , Y , Z con p Da (3) /\ (4), per MP deriviamo: (5) (p  p) Abbiamo quindi dimostrato che (p  p) è un teorema del linguaggio L1. _____________________________________________________________________________ Osservazione. Generalizzazione di una derivazione. Tutte le considerazioni che abbiamo fatto per la f.b.f. p  p potrebbero essere ripetute per p ' p ' o anche per p '' p '' e, in generale, per ogni f.b.f. del tipo X X , ove X rappresenta una qualunque f.b.f. di L1. Il teorema prima dimostrato può, quindi, può essere generalizzato dicendo che se X è una qualunque f.b.f. di L1, vale il teorema X X. Avremmo anche potuto condurre la dimostrazione utilizzando la variabile metalinguistica X e derivando la formula X  X analogamente a come è stata derivata p  p . ________________________________________________________________________________ 3. Risultati metateorici su L1 Un sistema formale e, quindi, il relativo linguaggio, possono essi stessi essere oggetto di studio: anzi, se pensiamo che uno degli scopi della formalizzazione è quella di studiare limiti e potenzialità del linguaggio, è naturale convincersi che lo studio di un sistema formale sia attività naturalmente conseguente alla sua costruzione. Lo studio di un linguaggio andrà fatto in un metalinguaggio, in una metateoria che ha il sistema formale quale oggetto di studio. Ecco perché i teoremi relativi ai limiti e alle potenzialità di un sistema formale (che cosa il relativo linguaggio riesce a esprimere e che cosa non riesce a esprimere) vengono detti metateoremi. In questa sezione enunciamo alcuni risultati metateorici, ossia alcuni metateoremi, relativi a L1. Correttezza sintattica Un sistema formale si dice sintatticamente corretto quando le sue regole di inferenza fanno passare da f.b.f. a formule che sono ancora ben formate. E’ una proprietà, questa, che ogni sistema formale ben definito possiede, proprio in virtù della caratterizzazione della nozione di regola inferenziale. AncheL1, quindi, è sintatticamente corretto. Correttezza (semantica) o validità Un sistema formale si dice (semanticamente) corretto o valido quando le sue regole di inferenza fanno passare da formule valide a formule che sono ancora valide. Questa proprietà è posseduta da ogni sistema formale ben definito e, quindi, anche da L1. Possiamo quindi dire che un sistema formale, se ben definito, deve essere almeno sintatticamente corretto e valido. Vi sono però altre significative proprietà che non tutti i sistemi formali ben definiti possiedono. Vediamone alcune. Completezza sintattica Un sistema formale S, avente L come linguaggio, si dice sintatticamente completo quando, data una qualunque f.b.f. chiusa A esprimibile in L, o A o la sua negazione ~A, è un teorema di S (ossia è dimostrabile in S). Incompletezza sintattica Un sistema formale si dice sintatticamente incompleto quando non è sintatticamente completo, ossia quando esiste una f.b.f. chiusa A esprimibile nel linguaggio L del sistema tale che né A, né ~A sono teoremi. Completezza (semantica) o adeguatezza Un sistema formale si dice semanticamente completo o completo o adeguato, quando in esso è possibile dimostrare tutte le formule valide (ossia vere in ogni possibile intepretazione). In un sistema completo, quindi, tutte le formule valide sono teoremi. Il termine “completezza” utilizzato in questo caso non deve confondersi con quello di “completezza sintattica” precisato prima. Per tale motivo sarebbe forse preferibile utilizzare il termine “adeguatezza”, ma nei manuali di logica è ormai prevalente l’uso del termine completezza. Il sistema L1 è completo (adeguato). Infatti è possibile dimostrare che l’insieme dei teoremi di L1 coincide con l’insieme delle tautologie (ossia delle proposizioni logicamente valide) della logica delle proposizioni. Da quanto ora affermato discende che il sistema L1 è sintatticamente incompleto: infatti se prendiamo la proposizione p abbiamo che essa non è una tautologia. Quindi, nel sistema formale L1 né p , né ~p sono teoremi, per cui L1 non è sintatticamente completo. Incompletezza (semantica) o non adeguatezza Un sistema formale S si dice semanticamente incompleto o incompleto o non adeguato, quando non è completo, ossia se esiste una formula valida non dimostrabile in S. Decidibilità e indecidibilità Abbiamo visto che in un sistema completo (adeguato) è possibile dimostrare tutte le f.b.f. che sono valide. In altri termini, in un sistema completo (adeguato) è possibile dimostrare tutte le formule che sono conseguenza logica degli assiomi della teoria. Se, a partire dagli assiomi, tramite le regole inferenziali del sistema, generiamo tutte le possibili conseguenze degli assiomi, il tempo richiesto per dimostrare una data formula valida può essere più o meno lungo, ma se il sistema è completo è certo che, prima o poi, verrà esibita una dimostrazione della formula stessa (quanto sia lungo questo tempo è problema del quale ora non ci occupiamo). La completezza di un sistema formale non è però condizione sufficiente a garantire la possibilità di decidere, in un tempo finito, utilizzando esclusivamente le regole inferenziali del sistema, se una sua qualunque f.b.f. è valida o non valida. Infatti presa una qualunque f.b.f. A di un sistema S completo, se A è valida, allora A è un teorema di S e, quindi verrà prima o poi dimostrata in S semplicemente con un meccanismo che consenta di generare in successione, a partire dagli assiomi, tutti i possibili teoremi di S. Ma se A non è valida, ma è solo soddisfacibile, allora né A né ~ A sono teoremi di S. Il meccanismo che genera tutti e soli i teoremi di S non genererà mai né A , né ~A. Un sistema formale S si dice decidibile quando, data una qualunque f.b.f. di S , esiste una procedura meccanica (cioè eseguibile, in linea di principio, da una macchina) che consenta di determinare se la formula è o non è dimostrabile. Un sistema formale S si dice indecidibile quando non è decidibile, ossia quando non esiste una procedura meccanica che consenta di determinare se una qualunque f.b.f. di S è o non è dimostrabile. Il sistema L1 è decidibile: il metodo delle tavole di verità costituisce una procedura di decisione per una qualunque f.b.f. di L1. In generale un sottoinsieme A di numeri naturali si dice decidibile se esiste un procedimento meccanico (eseguibile in linea di principio da una macchina) che consenta di stabilire, per ogni numero naturale n se n appartiene o non appartiene ad A. Per esempio, gli insiemi dei numeri pari, dei numeri dispari, lo steso insieme dei numeri naturali sono decidibili. Invece l’insieme A definito dalla proposizione A è l’insieme dei numeri n tali che nello sviluppo decimale delle cifre di  compaiono almeno una volta esattamente n cifre consecutive tutte uguali a 9 Come facciamo a sapere se 1 appartiene ad A? Semplice: sviluppiamo  fino alla sesta cifra dopo la virgola e vediamo che in questo sviluppo compare una volta una cifra uguale a 9  = 3,141592.... quindi 1 appartiene ad A Come facciamo a sapere se 2 appartiene ad A?  =3.1415926535897932384626433832795028841971693993 quindi 2 appartiene ad A Come facciamo a sapere se 3 appartiene ad A ? Se siamo fortunati, ossia se effettivamente 3 appartiene ad A, allora, prima o poi, andando avanti nello sviluppo decimale di  troveremo una sequenza con tre 9 consecutivi ... Ma se 3 non appartiene ad A, non troveremo mai tale sequenza, ma non potremo mai affermare (visto che lo sviluppo decimale di  è illimitato non periodico) che tale sequenza non esiste ... L’insieme A non è quindi decidibile, visto che non è possibile decidere, dato un qualunque numero n se questo appartiene o non appartiene ad A. Coerenza o non contraddittorietà Un sistema formale S si dice coerente o non contraddittorio o, ancora, consistente, se in S non è dimostrabile nessuna formula del tipo A /\ ~A. Il sistema L1 è coerente. Incoerenza Un sistema formale S si dice incoerente o contraddittorio o inconsistente se non è coerente, ossia se in esso è possibile derivare una contraddizione, ossia una formula del tipo A /\ ~A. In un sistema formale incoerente è possibile dimostrare qualunque formula. Concludiamo questo paragrafo accennando a un’altra proprietà che in certi casi risulta interessante studiare in un sistema formale: l’eventuale dipendenza o indipendenza dei suoi assiomi. Indipendenza Abbiamo visto che in un sistema formale S sintatticamente incompleto esistono proposizioni che non sono dimostrabili né refutabili, ossia esiste almeno una f.b.f.chiusa A tale che né A , né ~A sono teoremi. In questo caso si dice anche che A e ~A sono indipendenti dagli assiomi di S. In generale una f.b.f. chiusa di S si dice indipendente dagli assiomi di S quando né A, né la sua negazione sono dimostrabili in S; altrimenti si dice dipendente. Una condizione che talvolta viene richiesta agli assiomi di S è che siano ridotti al minimo indispensabile, ossia che non vi sia un assioma A che possa essere dimostrato in S a partire dagli altri assiomi. Si esprime questa condizione dicendo che il sistema di assiomi di S deve essere indipendente (non deve essere dipendente). Le dimostrazioni di indipendenza di un assioma rispetto ai restanti assiomi del sistema sono a volte risultati di fondamentale importanza: esse consentono di determinare con precisione il significato dell’assioma per il sistema, ossia tutto ciò che il sistema non sarebbe più in grado di dire senza l’assunzione di quell’assioma. _______________________________________________________________________________ Osservazione Coerenza e indipendenza Abbiamo visto che affermare che un assioma A è indipendente da un sistema S di altri assiomi equivale a dire che in S è impossibile dimostrare sia A sia ~A. Tale considerazione ci fa comprendere che, se S è un sistema coerente, allora anche i sistemi S U {A} e S U {~A} sono coerenti. Quanto osservato dovrebbe farci apprezzare maggiormente il significato di una dimostrazione di indipendenza. Infatti dimostrare che l' assioma A è indipendente da un sistema di assiomi S ci consente di: a) non considerare l' assioma A e studiare tutte quelle proposizioni che il sistema S è in grado di giustificare sena ricorrere all' assioma A. Ad esempio, nel caso della geometria euclidea, la dimostrazione dell' indipendenza dell' assioma della parallela da quelli che lo precedono negli "Elementi" di Euclide, consente di scoprire quali proprietà geometriche non dipendono dall' unicità della parallela. Nel caso specifico si parla di geometria assoluta. b) Aggiungere al sistema S l' assioma A e considerare il sistema S U {A} . Riferendoci all' esempio dell' assioma della parallela, ciò porta ad evidenziare tutte quelle proprietà geometriche che non sono giustificabili nella geometria assoluta. c) Aggiungere al sistema S l' assioma ~A e considerare il sistema S U {~A}, ottenendo un sistema diverso da S U {A}, ma ugualmente accettabile dal punto di vista della coerenza . In riferimento all' esempio dell' assioma della parallela, in tal caso, si darebbe luogo alla geometria non euclidea che assume come assioma l' esistenza di più di una parallela per un punto esterno a una retta data. _____________________________________________________________________________ 4. Un sistema formale per la logica predicativa: il linguaggio L2 il linguaggio L2, ossia la logica dei predicati, è sotto certi aspetti un' estensione di L1 : un linguaggio rigoroso e preciso quanto L1, ma molto più adeguato a descrivere gli oggetti della matematica . Con L2 si passa all' analisi delle proposizioni in termini di soggetto e predicato. Alfabeto di L2 L2 si forma sull' alfabeto:   ( x ' a fn Pn ~ ----> ) , dove: x, x', x'',.... sono simboli per variabili individuali e consentono di rappresentare generici elementi dell' insieme i cui elementi sono oggetto di predicazione ; a, a' ,a''.... sono simboli per costanti individuali e rappresentano elementi ben determinati di un insieme; fn, fn', fn'' ... sono simboli per funzioni a n argomenti : Pn, Pn', Pn''... sono predicati a n argomenti, ossia simboli per relazioni ; ~ ---> sono simboli per i connettivi logici di L1;  ,  sono simboli per i quantificatori universale ed esistenziale; ( , ) sono segni ausiliari, utilizzati per rendere più comprensibile la scrittura delle formule. I simboli per variabili, costanti individuali, funzioni e relazioni costituiscono la parte descrittiva dell' alfabeto di L2: servono per parlare degli oggetti di un insieme e per descrivere relazioni tra essi. I simboli per connettivi logici e per i quantificatori costituiscono quello che viene detto alfabeto logico. Infine, le parentesi e la virgola costituiscono l' alfabeto ausiliario, ossia l' insieme di quei simboli accessori del linguaggio, utilizzati solo per semplificare la notazione. Regole di formazione di f.b.f. Così come abbiamo fatto per L1, anche per L2 assegniamo le regole che consentono di individuare tra tutte le possibili stringhe dell'alfabeto le formule ben formate. Nota che, in tal caso, la caratterizzazione delle f.b.f. avviene mediante la definizione dei termini del linguaggio. Per la precisione, le prime tre regole definiscono l' insieme dei termini, ossia di quelle stringhe di L2 cui si conferirà un significato, facendo loro corrispondere, a livello semantico, elementi di un insieme. Il significato dei connettivi /\ , \/ ,  può essere stabilito a livello metalinguistico nello stesso modo in cui è già stato stabilito nel metalinguaggio di L1. Regola 1. (regola di base) le variabili e le costanti individuali sono termini Regola 2. se fn è un simbolo di funzione a n argomenti e t, t ' , t '', .... sono n termini, allora f ( t, t', t'', ....) è un termine Regola 3. (regola di chiusura) non esistono altri termini di L2 Le regole seguenti definiscono l' insieme delle f.b.f. a partire dalla definizione ora data di termine e da quella di formula atomica, ossia di una stringa di L2 costituita da un predicato a n argomenti. In simboli, una formula atomica è una stringa del tipo P(x, x', x''.....). Regola 4. (regola di base) Le formule atomiche sono f.b.f. Regola 5. se Pn è un simbolo di predicato a n argomenti e t, t' , t '', .... sono n termini, allora P(t , t', t'' ...) è una f.b.f. Regola 6. se A e B sono f.b.f., allora ~A, (A B),  x A e  x A sono f.b.f. Regola 7. (regola di chiusura) Non esistono altri tipi di f.b.f. in L2 Le sette regole precedenti costituiscono la sintassi di L2 e consentono di poter generare, a partire dalle costanti e variabili individuali, le espressioni o formule ben formate del linguaggio. Assiomi di L2 Diamo gli assiomi che abbiamo scelto per caratterizzare L2 utilizzando, come al solito, variabili metalinguistiche: A1 : A ----> (B ----> A) A2 : (A ---> (B ----> C)) ----> ((A ----> B) -----> (A -----> C)) A3 : (~A -----> ~B) ----> (( ~A -----> B) -----> A) A4 :  x A(x) ----> A(a) A5 : A(a) ---->  x A(x) Come puoi notare i primi tre assiomi sono gli stessi che caratterizzano L1. Ad essi abbiamo aggiunto due assiomi riguardanti la quantificazione (universale ed esistenziale). A4 afferma che se un predicato si applica a ogni elemento x degli oggetti di un discorso, allora tale predicato si applica anche ad una particolare costante. A5 afferma che se un predicato si applica a una costante, allora esiste almeno un oggetto cui tale predicato si può applicare. Regole di inferenza. Il sistema assiomatico, da noi scelto per descrivere L2, è caratterizzato anche da tre regole di inferenza: Modus ponens A A ------> B MP : --------------------------- B Generalizzazione P(a) ----------- x P(x) Questa regola esprime il fatto che se una formula P vale per un generico oggetto, allora vale per ogni oggetto del discorso: è una regola che viene applicata quando, per esempio, si dimostra che dato un triangolo (su cui non si fanno ipotesi particolari), le tre mediane passano per uno stesso punto. Poiché il teorema vale per un triangolo generico, su cui non si sono fatte ipotesi particolari, possiamo concludere che la proposizione è valida per ogni triangolo del piano. 5. Risultati metateorici su L2 L2, come ogni sistema formale ben definito, è sintatticamente corretto e valido. Queste proprietà discendono, come già detto in precedenza, dalla nozione stessa di regola inferenziale. Nel 1930 il logico matematico Kurt Gödel dimostrò che il calcolo predicativo (al primo ordine) è semanticamente completo (adeguato). Ciò vuol dire, lo ricordiamo, che tutte le f.b.f. valide di L2 sono teoremi. Questo risultato fa comprendere come, a livello di logica proposizionale o predicativa del primo ordine, il concetto semantico di validità possa essere sostituito dal concetto sintattico di dimostrabilità. In altri termini, tutto ciò che è dimostrabile è vero in ogni possibile interpretazione e tutto ciò che è vero in ogni possibile interpretazione è dimostrabile. Se tutti i sistemi interessanti della matematica fossero completi, potremmo affermare che il concetto semantico di validità (verità in ogni possibile interpretazione) si cattura con il concetto sintattico di dimostrazione formale. Questo sarebbe un risultato innegabilmente sorprendente, dato che la sintassi di un linguaggio è per sua natura individuata da un numero ben definito di regole, mentre la semantica è notevolmente più ricca, potendo avere un sistema formale infinite interpretazioni. In effetti le cose non stanno in questi termini: nel 1931 Kurt Gödel dimostrò che ogni teoria formalizzata che sia capace di esprimere almeno l’aritmetica non è semanticamente completa. L’adeguatezza di un sistema formale è quindi per così dire un’eccezione nel mondo dei sistemi formali. Il fatto che L2 sia completo, però, ci assicura che la ricerca di un linguaggio atto ad esprimere regole logiche ha termine: L2 è sufficiente per catturare tutte le regole logicamente valide. Le dimostrazioni formali possono quindi essere condotte con gli strumenti che L2 ci mette a disposizione e non ha senso andare a cercare qualche linguaggio più potente, nel senso che un tale linguaggio non fornirà regole logicamente valide diverse da quelle che già L2 ci offre. E’ inoltre possibile dimostrare che L2 è coerente: ciò vuol dire, in un certo senso, che così come L1, anche L2 si fonda su basi sufficientemente sicure. In L2 non è possibile derivare alcuna contraddizione dagli assiomi. L2 non è, invece, sintatticamente completo. Infatti non è detto che data una sua qualunque f.b.f. chiusa A o A o ~A siano teoremi. Può infatti accadere che la formula A sia semplicemente soddisfacibile, ma non valida. Se A è soddisfacible senza essere valida (e abbiamo già visto che formule di tale tipo esistono in L2) allora, per il metateorema di completezza semantica, A non è teorema di L2; analogo discorso può essere fatto per ~A . Risulta quindi che né A né ~A sono teoremi; quindi L2 non è sintatticamente completo. Inoltre, nel 1936, il logico matematico Alonzo Church dimostrò che L2 non è decidibile. 6. Teorie matematiche formalizzate Prima di passare all’ultimo esempio di sistema formale soffermiamoci sull’attività di formalizzazione fino ad ora svolta. Con la formalizzazione della logica delle proposizioni e dei predicati (al primo ordine) siamo passati da teorie matematiche che utilizzavano, per dimostrare teoremi, alcune regole logiche non sempre ben precisate e definite una volta tutte, a teorie matematiche che utilizzano un sistema ben definito e precisato di assiomi e teoremi di una teoria logica formalizzata. La differenza fra le due situazioni può essere schematizzata nel modo seguente Teoria matematica Teoria matematica Sistema formale (Logica) Assiomi Assiomi Assiomi Teoremi Regole logiche Teoremi Teoremi M.P. Gen. Prima situazione Seconda situazione Questa seconda situazione può essere semplificata individuando un unico sistema formale che tenga conto sia della teoria matematica, sia del sistema formale logico che viene utilizzato per compiere dimostrazioni. In tal caso, nella cosiddetta teoria matematica formalizzata, avremo: a) un linguaggio L predicativo (al primo ordine) utile a descrivere la teoria matematica (sarà in tal caso importante scegliere simboli per costanti, per funzioni, per relazioni, limitandosi a quelli occorrenti. Per esempio se nella teoria si dovrà rappresentare unicamente la relazione “x è maggiore di y”, si introdurrà un unico simbolo predicativo a due posti ...); b) un insieme di assiomi logici (quelli scelti, per esempio, in L2, o altri che eventualmente riteniamo più adeguati); c) un insieme di regole inferenziali (per esempio Modus ponens e Generalizzazione); d) un insieme di assiomi relativi all’uguaglianza; e) un insieme di assiomi specifici della teoria matematica che si vuole descrivere. Ciò può essere schematizzato nel seguente modo Assiomi logici Assiomi specifici Teoremi M.P. Generaliz zazione La teoria così ottenuta verrà detta teoria formalizzata al primo ordine della teoria matematica che si vuole descrivere. In genere, quando si presenta una teoria matematica formalizzata si evita di precisare gli assiomi logici e le regole inferenziali utilizzate: si fa quindi a meno di esplicitare l’apparato logico della teoria. Esso è infatti sottinteso: si tratta, a meno di differenti indicazioni, di un sistema equivalente a L2. 7. Una teoria formalizzata per il calcolo delle probabilità Nel 1933 il matematico russo Kolmogorov scriveva: " La teoria delle probabilità può e deve essere derivata a partire da assiomi, esattamente come la geometria o l' algebra". Secondo tale punto di vista, la nozione di probabilità avrebbe dovuto essere data implicitamente, attraverso il sistema di assiomi scelto per descrivere il calcolo delle probabilità. Inoltre le derivazioni all' interno di tale sistema assiomatico avrebbero dovuto essere studiate indipendentemente dal significato intuitivo attribuito alle nozioni di evento casuale, probabilità di un evento e via dicendo. Infine, l' assiomatizzazione avrebbe consentito di costruire una teoria matematica suscettibile di differenti interpretazioni, ossia di diversi significati. Noi qui ci occupiamo di dare un sistema di assiomi per il calcolo delle probabilità. == Eventi e variabili casuali I concetti primitivi della teoria assiomatica delle probabilità che qui presentiamo sono quelli di evento casuale elementare e di variabile casuale. Tali concetti, in quanto primitivi, non possono essere definiti; Possiamo, però, fornirne qualche modello, esplicitando, in tal modo, alcuni dei possibili significati che è possibile attribuire loro. Per evento casuale elementare intendiamo tutti quei fenomeni su cui non possiamo dire a priori e con certezza se si verificheranno o meno. Ad esempio sono eventi casuali elementari: - l' uscita del numero 1 nel lancio di un dado con sei facce numerate da 1 a 6; - l' uscita del re di cuori nell' estrazione di una carta da un mazzo di carte da briscola. Utilizzando il linguaggio della logica delle proposizioni, possiamo dire che un evento casuale elementare è una proposizione e, come tale, è capace di assumere due possibili valori: V se si verifica; F se non si verifica . Utilizzando il linguaggio degli insiemi possiamo anche dire che un evento casuale elementare è un elemento dell' insieme {0,1}; per la precisione è 0 se non si verifica, 1 se si verifica. Un evento casuale non elementare o semplicemente evento casuale potrà essere interpretato, come un insieme di eventi elementari casuali. Ad esempio il lancio di un dado con sei facce numerate è un evento casuale, in quanto sono possibili sei eventi elementari (uno per ogni faccia numerata) . Sempre utilizzando il linguaggio degli insiemi, possiamo dire che una variabile casuale è una funzione definita su un insieme A di eventi elementari e che assume valori in un insieme B di numeri reali. Ad esempio la tabella: 1 2 3 4 5 6 p1 p2 p3 p4 p5 p6 rappresenta una funzione definita nell' insieme { 1, 2, 3, 4, 5, 6} e avente come codominio l' insieme di numeri reali {p1 , p2 , p3 , p4 , p5 , p6} . Se ipotizziamo che il codominio sia l' insieme {1/6} ossia se ipotizziamo che tutti i numeri reali p1,...., p6 siano uguali a 1/6, la variabile casuale considerata potrebbe rappresentare la distribuzione di probabilità dei possibili esisti del lancio di un dado cubico non truccato con facce numerate da 1 a 6. In genere si fa in modo di associare ad ogni evento elementare un numero; in tal caso una variabile casuale è una funzione definita in un insieme numerico A e avente valori in un insieme numerico B. Gli elementi del dominio vengono detti valori possibili della variabile casuale,gli elementi del codominio, vengono detti probabilità. In genere si distingue tra variabili casuali discrete e variabili casuali continue, a seconda che il dominio sia, rispettivamente, un insieme discreto o continuo. Nota che il concetto di probabilità è stato definito, ma solo nei termini di un concetto primitivo (quello di variabile casuale) che, come tale non può ammettere definizione esplicita. Assiomi del calcolo delle probabilità Sia E l' insieme di tutti gli eventi elementari casuali possibili; sia F una collezione di sottoinsiemi di E tale che a) E  F b) se a E, allora {a}F c) se A e B appartengono ad F , allora anche l'intersezione e l' unione di A e B appartengono a F d) se A appartiene a F, allora anche il complementare di A appartiene a F Sia data, infine, una funzione f che associ ad ogni elemento di F uno e un solo numero reale compreso fra 0 e 1. Sotto tali condizioni, il seguente sistema di assiomi, definisce implicitamente la nozione di probabilità di un evento che individuandola nella funzione f: A1. f(E) = 1 A2. f(  ) = 0 A3. se A  B =  allora f(A U B) = f(A) + f(B) essendo  l’insieme vuoto Regole di inferenza Le regole di inferenza possono essere ricondotte al Modus Ponens e alla regola di generalizzazione. E’ comunque possibile utilizzare sistemi più ricchi, come quello della deduzione naturale. Un esempio di dimostrazione Ricordiamo che si dice probabilità condizionale dell' evento A, dato l' evento B, la quantità: P(A/B) = P(A /\ B) / P(B) che equivale, nell' interpretazione insiemistica a : P(A/B) = P(AB) / P(B) Vogliamo dimostrare che dati due eventi casuali disgiunti E1 ed E2 , tali che la loro unione dia l' evento certo E (cui è associata probabilità uguale a 1) , la probabilità di un qualunque evento casuale A di F si calcola addizionando il prodotto della probabilità condizionale di A rispetto ad E1per la probabilità di E1 con il prodotto della probabilità condizionale di A rispetto a E2 per la probabilità di E2 . Vogliamo, cioè dimostrare che: ((E1  E2 =  ) /\ (E1 U E2 ) = E) ====> P(A) = P(A/E1) *P(E1) + P(A/E2)*P(E2) essendo E l' evento certo ed A un qualunque sottoinsieme di E . Essendo un generico sottoinsieme di E, A si può ottenere come unione dell' intersezione di A con E1 e di A con E2. In simboli: A = (A  E1) U (A  E2). Poiché E1 ed E2 sono disgiunti, anche (A E1) e (A  E2) sono disgiunti. Allora, per l' assioma A3, P((A  E1) U (A  E2)) = P(A) = P(A E1) + P(A E2). Per la definizione data di probabilità condizionale abbiamo che P(A  E1) = P(A/E1) * P(E1) e, analogamente, P(A  E2) = P(A/E2) * P(E2) Abbiamo, infine che : P(A) = P(A/E1) *P(E1) + P(A/E2)*P(E2) proposizione dimostrata a partire dalle ipotesi ((E1  E2 =  ) /\ (E1 U E2 ) = E) e dagli assiomi della teoria. 8. Utilizzazione del concetto di modello per la presentazione di risultati metateorici La nozione di modello di un sistema formale è particolarmente indicata per esprimere in modo più chiaro alcuni dei risultati metateorici di cui abbiamo parlato. Cerchiamo innanzitutto di dare un' idea del perché il fatto di possedere un qualunque modello assicuri la coerenza di un sistema formale S che sia corretto. Poniamoci nella seguente situazione: S è un sistema formale valido e S possiede un modello M . Supponiamo, per assurdo che S non sia coerente. Dire che S non è coerente equivale ad affermare che è possibile derivare in esso la f.b.f. (P/\~P), essendo P una qualunque f.b.f. di S. Poiché S è valido, ogni stringa in esso derivabile deve essere conseguenza logica degli assiomi. Allora la stringa (P /\~P) deve essere conseguenza logica degli assiomi di S; (P/\~P) dovrebbe quindi essere vera in ogni modello di S e, in particolare, in M. Ciò è però assurdo: infatti (P/\ ~P) è una contraddizione e, come tale, è falsa in qualunque modello. Quindi (P/\ ~P) non può essere conseguenza logica di un sistema corretto che ammetta un modello. In definitiva, se un sistema formale valido ha un modello, allora è coerente. Il concetto di modello è particolarmente utilizzato nelle dimostrazioni di indipendenza di una f.b.f. chiusa da un sistema di assiomi. Supponiamo di voler dimostrare l' indipendenza di P da un sistema di assiomi S. Dobbiamo far vedere che sia P sia ~P non sono conseguenza logica degli assiomi di S. L' idea è quella di trovare un modello di S che sia anche modello di P e, in seguito, determinare un altro modello di S che sia anche modello di ~P. Supponiamo di essere riusciti a trovare un modello di S che sia anche modello di P , ossia un insieme M tale che sia tutti gli assiomi di S, sia P risultano veri in M. L' esistenza di M garantisce che ~P non sia conseguenza logica degli assiomi di S . Infatti, se per assurdo ~P fosse conseguenza logica del sistema di assiomi S essa dovrebbe essere vera in ogni modello di S, anche in M, in cui è vera anche P. Avremmo quindi che anche (P/\~P) sarebbe vera in M, il che è assurdo, essendo (P/\ ~P) falsa in ogni modello. Analogamente, se riusciamo a determinare un insieme M1 che sia modello di tutti gli assiomi di S e anche di ~P , l' esistenza di M1 garantisce che P non è conseguenza logica del sistema di assiomi S. In definitiva, l' esistenza sia di M, sia di M1 garantisce l' indipendenza di P ( e di ~P) dal sistema di assiomi S, in quanto né P né ~P sono conseguenza logica del sistema di assiomi S . Ad esempio, è possibile dimostrare che la proposizione P: "per un punto passa una e una sola parallela a una retta data" è indipendente dal sistema di assiomi S della geometria euclidea che consta delle due proposizioni seguenti: Q : " due punti appartengono a una e una sola retta" R : " tre punti non allineati appartengono ad uno e un solo piano" Per far ciò è sufficiente esibire un modello M di S che sia anche modello di P e un altro modello M1 di S che sia anche modello di ~P Come puoi notare , prendendo M = {a,b,c}, ossia l' insieme dei tre punti di figura, in cui i punti sono i sottoinsiemi aventi un solo elemento , le rette i sottoinsiemi aventi due elementi e il piano è lo stesso insieme M , .a .b .c abbiamo un insieme che è modello sia di S che di ~P, in quanto in M sia Q, sia R, sia ~P sono vere (in M due rette sono sempre incidenti ). Prendendo M1 = {a,b,c,d} in cui i punti sono i sottoinsiemi di M1 aventi un solo elemento, le rette sono i sottoinsiemi aventi due elementi e il piano è l'insieme M1 stesso, .a .c .b .d abbiamo un insieme che è modello di S e di P, in quanto sia Q, sia R, sia P sono vere in M1. _____________________________________________________________________________ Il risultato che afferma che se un sistema formale valido ha un modello allora è coerente è uno dei più importanti risultati della logica dei predicati del primo ordine e ad esso si fa riferimento con il nome di teorema di validità. Nella logica dei predicati del primo ordine vale anche il risultato inverso. Possiamo quindi affermare che un qualunque sistema predicativo del primo ordine ha un modello se e solo se è coerente. 9. Ulteriori considerazioni sulla dimostrazione Abbiamo già fatto notare come in questo corso sia stato assegnato alla dimostrazione un ruolo di particolare importanza nelle attività matematiche. In questo capitolo abbiamo precisato la nozione di dimostrazione formale, anzi, possiamo dire di avere precisato, attraverso la definizione di dimostrazione formale, la nozione intuitiva di dimostrazione. La domanda che non possiamo fare a meno di porre, dopo i tanti risultati limitativi relativi ai sistemi formali, è se la definizione (rigorosa) di dimostrazione formale riesce a catturare a esprimere quella che è la nostra idea intuitiva di dimostrazione. In altri termini, quando eseguiamo una dimostrazione informale, siamo sicuri che a quella dimostrazione ha una corrispondente nel sistema formalizzato? Ha senso chiedersi se esiste un teorema che dimostra che per ogni dimostrazione non formale ne esiste una versione formalizzata? Posta in questi termini la domanda non ha senso, poiché pretenderebbe di stabilire un’equivalenza fra un concetto non ben definito come quello di dimostrazione non formale e quello di dimostrazione formale che è invece una nozione ben precisa e definita all’interno di una teoria. Quello che invece possiamo chiederci è se i matematici abbiano validi motivi per ritenere che il concetto di dimostrazione formale consegue l’obiettivo di definire rigorosamente quello che i matematici stessi pensano quando parlano di dimostrazioni. La risposta è affermativa, va sotto il nome di Tesi di Hilbert ed è espressa nel modo seguente: La nozione informale di dimostrazione è correttamente formalizzata dalla logica del primo ordine. Cenni alla deduzione naturale Se Hilbert si proponeva, con la sua Beweistheorie, l'analisi della nozione di dimostrabilità, Gerhard Gentzen, con il calcolo della deduzione naturale, spostava l'indagine sulla struttura delle dimostrazioni. Nelll'articolo del 1935 Untersuchungen uber das logische Schliessen (Ricerche sulla deduzione logica), Gentzen si propone di "fornire un sistema di formule che fosse il più vicino possibile all'effettivo ragionamento". In altri termini, Gentzen notò che "la formalizzazione della deduzione logica, in particolare come è stata sviluppata da Frege, Russell e Hilbert, si discosta alquanto dalle forme di deduzione usate nella pratica delle dimostrazioni matematiche" e si pone l'obiettivo di fornire un'analisi delle dimostrazioni e quindi un'individuazione delle regole inferenziali così come si presentano nella prassi matematica. Nel 1971, nell'articolo Ideas and Results in Proof Theory, Dag Prawitz propone un calcolo logico basato sulle idee di Gentzen, ma libero da alcune complicazioni tecniche e ancora più vicino al modo di dimostrare dei matematici. Il sistema formale di Prawitz, che qui proponiamo, anche se in forma non completa, consente di indagare la struttura delle dimostrazioni, in quanto si pone l’obiettivo di riprodurre direttamente le regole inferenziali utilizzate nelle dimostrazioni informali proprie della concreta pratica matematica. L’idea di fondo è che ogni dimostrazione possa essere analizzata in termini di inferenze fondamentali e che ciascuna di tali inferenze possa essere pensata come applicazione di regole che fissino il significato deduttivo di ogni operatore logico. Come abbiamo già detto, presentiamo una parte del calcolo della deduzione naturale di Prawitz, precisamente quella che fissa il significato deduttivo delle costanti logiche /\, \/, , ~,  , . Facciamo notare che ogni operatore logico interviene in due tipi di regole: una di introduzione dell’operatore e l'altra di eliminazione,che possono essere pensate come una inversa dell’altra. 0. Regola della premessa A ogni stadio di una derivazione si può aggiungere una nuova riga assumendo una formula qualsiasi, giustificata come premessa 1. Regola della /\ introduzione: se in una derivazione compaiono una formula A e una formula B, allora si può aggiungere alla derivazione una nuova riga in cui compare la formula A /\ B A,B ------- intro-/\ A /\ B 2. Regola della /\ eliminazione: se in una derivazione compare la formula A /\ B, allora si possono aggiungere alla derivazione sia una riga in cui compare A, sia una riga in cui comare B A /\ B ------A elimi-/\ A /\ B ---------B 3. Regola della \/ introduzione: se in una derivazione compare una formula A, allora si può aggiungere alla derivazione una nuova riga in cui compare la formula A \/ B A ------- intro-\/ A \/ B 4. Regola della \/ eliminazione: se in una derivazione compaiono una formula A \/ B e assumendo sia A sia B si ottiene sempre una stessa formula C, allora si può aggiungere alla derivazione una riga in cui compare la sola formula C [A] [B] A \/ B C C -------------------------- elimi-\/ C (le parentesi quadre ricordano che A e B sono assunzioni temporanee, che verranno scaricate nella derivazione, nel senso che la conclusione C non dipende né da A né da B. Riconoscerai in questa regola il corrispondente della dimostrazione per casi) 5. Regola della  eliminazione: se in una derivazione si è assunta una formula A e si è derivata una formula B, è possibile scarica l’assunzione A introducendo nella derivazione la formula A  B, che non dipende più dall’assunzione A [A] B ---------- intro-  A B 6. Regola della  eliminazione: se in una derivazione compaiono la formula A e la formula A  B, allora si può aggiungere alla derivazione una nuova riga in cui compare la formula B (riconoscerai in questa regola il corrispondente del Modus Ponens) A,A B --------------- elimi-  B 7. Regola del ~ introduzione Se in una derivazione è stata effettuata un’assunzione A e da questa si è ottenuta una contraddizione ( assurdo, indicato con il simbolo  ), allora è possibile scaricare l’assunzione A e aggiungere alla derivazione la formula ~ A [A]  ------ intro- ~ ~A 8. Regola del ~ eliminazione Se in una derivazione compaiono le formule A e ~A, allora è possibile aggiungere alla derivazione l’assurdo  A , ~A ---------- elimi- ~  9. Regola del  introduzione Se in una derivazione compare la formula P(a), allora è possibile aggiungere alla derivazione la formula  x P(x) (per ogni x P(x): riconoscerai in questa regola un corrispondente della formula di generalizzazione). Questa regola ha una restrizione: essa può essere applicata se il parametro a non compare nelle assunzioni da cui P(a) dipende. P(a) ----------- intro -   x P(x) 10. Regola di  eliminazione Se in una derivazione compare la formula  xP(x), allora, se t costante, si può aggiungere alla derivazione la formula P(t) . (In effetti le restrizioni su t possono essere rese meno forti)  xP(x) --------- elimi-  P(t) 11. Regola di  introduzione Se in una derivazione compare la formula P(t) , con t costante, si può aggiungere alla derivazione la formula xP(x) P(t) ----------- intro-  x P(x) 12. Regola di - eliminazione Se in una derivazione compare la formula  x P(x) e se dall’assunzione P(t) si ottiene la formula B, allora si può scaricare (con opportune restrizioni su t) l’assunzione P(t) e aggiungere alla derivazione B [P(t)] x P(x) B ---------------------- elim-  B Un utile esercizio potrebbe essere quello di rileggere, alla luce delle regole di questo calcolo logico, alcune dimostrazioni che si trovano in questo libro di testo e in altri. Potrebbe essere un buono spunto di riflessione (sulla) e di analisi (della) struttura logica delle dimostrazioni usualmente presentate nei manuali di matematica. E’ possibile dimostrare che il calcolo della deduzione naturale è un sistema formale valido e completo: ciò assicura che eseguire dimostrazioni all’interno del calcolo della deduzione naturale o all’interno del sistema L2 non pregiudica la possibilità di ottenere tutte le formule valide di una teoria formalizzata. Un po' di storia... Una cavalcata nella logica matematica da Boole a Godel Il 1847 la data in cui si può far risalire la nascita della logica matematica: è l' anno in cui viene pubblicata l' "Analisi matematica della logica" di George Boole. Con tale opera il logico inglese costruisce un sistema algebrico che rende conto della logica delle proposizioni . Quella di Boole è vera logica matematica non solo perché utilizza simboli e calcoli matematici, ma anche e soprattutto perché solleva questioni proprie delle discipline matematiche. La neonata disciplina acquista grande rilievo verso la fine del secolo scorso quando il logico Gottlob Frege annuncia l' ambizioso programma di ridurre " i numeri e le loro leggi alla sola logica". Frege parte dalla convinzione che solo i principi di tipo logico hanno una sicurezza fondazionale assoluta: riducendo l' aritmetica a soli principi di tipo logico si avrà la certezza che tale parte della matematica è fondata su basi sicure, che ne assicurano la validità. In seguito sarà possibile, proprio partendo dalla sistemazione dell' aritmetica, costruire l' intera matematica nota, ottenendo, così, un edificio dalle basi solide e sicure. Il punto debole nel programma di Frege è un principio detto principio di comprensione: esso afferma che se si può enunciare una proprietà di cui godono certi oggetti, si può pensare come logicamente esistente l' insieme di quegli oggetti. Ad esempio, se puoi enunciare la proprietà "avere i capelli biondi" puoi anche considerare l' insieme degli individui aventi capelli biondi. Il logico inglese Bertrand Russell, grande estimatore di Frege e del suo programma, comprese che il principio di comprensione portava inevitabilmente a contraddizioni. Proprio quando la grande opera di Frege, frutto di anni di pensiero e di lavoro, veniva data alle stampe, il giovane Russell inviò a Frege una lettera in cui dimostrava l' inconsistenza del programma fregeano. Il logico tedesco, con rara onestà intellettuale pubblicò nel suo volume la lettera di Russell aggiungendo questo breve commento: " A uno scrittore di scienza ben poco può giungere di più sgradito del fatto che, dopo completato un lavoro, venga scosso uno dei fondamenti della sua costruzione. Sono stato messo in questa situazione da una lettera del sig. Russell quando la stampa di questo volume stava per essere finita". Una forma della contraddizione individuata da Russell e che va sotto il nome di paradosso di Russell è la seguente: sia P(x) la proprietà per l' insieme X espressa dall' enunciato " l' insieme X non è elemento di sé stesso" Per il principio di comprensione possiamo pensare come logicamente esistente l' insieme W tale che : W = insieme di tutti gli insiemi che non sono elementi di sé stessi Notiamo che dalla definizione di W discende che, dato un qualunque insieme A, A app. W <--------> A non app. A Sostituiamo, nella formula precedente, A con W; otteniamo: W app. W <---------> W non app. W ossia, se si accetta il principio del terzo escluso, una contraddizione. Dopo aver determinato il fallimento del programma di Frege, lo stesso Russell si impegnò sulla stessa strada di ridurre l' intera matematica alla logica. Non accenniamo nemmeno agli accorgimenti tecnici che consentirono a Russell di superare la contraddizione da egli stesso evidenziata. Diciamo , invece, che la monumentale opera che Russell presentò , fra il 1910 e il 1913, insieme al matematico Alfred Whitehead non ebbe, fra i matematici, la fortuna sperata come soluzione al problema di determinare, per la disciplina matematica, fondamenta sicure. Il problema fu impostato in modo completamente differente dal matematico tedesco David Hilbert: se per Frege l' esistenza di un oggetto ne garantiva la non contraddittorietà, per Hilbert era la non contraddittorietà a garantire, eventualmente, l' esistenza. Per Hilbert fondare la matematica significa fondare le singole teorie in modo tale che siano non contraddittorie. Solo una dimostrazione di coerenza garantirà ad una teoria il diritto ad esistere nell' universo matematico . Da quanto detto risulta chiaro il perché Hilbert ponesse a fondamento del suo programma la dimostrazione di non contraddittorietà delle teorie matematiche e, in particolare , dell' aritmetica, in quanto già si sapeva che l' intero edificio della matematica poteva essere fondato sull' aritmetica. Il problema era quello di determinare le tecniche e le regole inferenziali utilizzabili per condurre una dimostrazione di coerenza dell' aritmetica. E' chiaro che la scelta di tali tecniche doveva risultare quanto mai delicata: dalla fiducia in tali tecniche sarebbe poi dipesa la fiducia nel risultato ottenuto. Si scelse un sottoinsieme dei metodi già utilizzati nell' aritmetica. Seguiamo la descrizione che ne dà Herbrand: "[...] si tratta sempre e solo con un numero finito e determinato di oggetti e funzioni; queste sono ben definite, permettendo la loro definizione il calcolo univoco dei loro valori; non si afferma mai l' esistenza di un oggetto senza indicare come costruirlo; non si considera mai l' insieme di tutti gli oggetti x di una totalità infinita; e quando si dice che un ragionamento ( o un teorema) vale per tutti questi x , questo significa che per ogni x particolare è possibile ripetere il ragionamento generale in questione, che deve quindi essere considerato solo come il prototipo di questi ragionamenti particolari". L' idea di Hilbert per dimostrare la non contraddittorietà di un sistema formale "ARI" per l' aritmetica è così schematizzabile : 1. si deve dimostrare che in "ARI" non è mai possibile derivare una formula del tipo (A /\ ~A) 2. dalla logica delle proposizioni è noto che ((A /\ ~A) ---> B) con B formula qualunque 3. da: ((A /\ ~A) ---> B) e (A /\ ~A) segue, per Modus Ponens (MP), B, con B formula qualunque. In simboli: ((A /\ ~A) ---> B) (A /\ ~A) -----------------------B Le tre precedenti considerazioni, quindi, assicurano che in un sistema non coerente è possibile dimostrare una qualunque formula. Allora per dimostrare che "ARI" è coerente basta dimostrare che in esso esiste almeno una formula non derivabile, ad esempio 0 = 1. Nonostante alcuni successi parziali il programma di Hilbert era destinato a fallire: nel 1931 il logico e matematico di origine austriaca Kurt Godel dimostra che non è possibile dimostrare la non contraddittorietà di un sistema formale che contenga almeno l' aritmetica con metodi finitisti (che corrispondono a quelli descritti sopra dalle parole di Herbrand). Il teorema di Godel non mette certo fine alle ricerche matematiche, ma apre un filone di nuove ricerche che porteranno un ' enorme ricchezza di risultati: ti basti pensare che è in questo periodo, conseguentemente ai risultati di Godel che si pongono le basi teoriche per lo sviluppo dell' informatica.