|
Cos'e' un Sistema Formale ed un esempio: Sistemi Formali Per quanto riguarda l'aspetto sintattico, una volta fornita una definizione di giudizio (formula ben formata) a partire da un insieme di simboli, un sistema formale e' un'insieme di
che ci permettono di derivare giudizi tramite una opportuna definizione di derivazione (prova). Gli assiomi solitamente hanno la seguente forma: giudizio mentre una regola di inferenza ha solitamente la seguente forma: ___________________________ giudizio dove i giudizi sopra la linea sono le premesse della regola e il giudizio sotto la linea e' la conclusione della regola. Come indicato nel testo di Martini, il concetto di regola di inferenza si puo' formalizzare come relazione tra formule ben formate. Sistemi formali in cui le regole di inferenza sono essenzialmente relazioni tra formule ben formate si chiamano sistemi formali alla Hilbert. Ci sono sistemi formali invece in cui le regole non possono essere formalizzate come relazioni tra giudizi, per esempio i sistemi logici di Deduzione Naturale. La semantica di un sistema formale consiste nel fornire una definizione di validita' per i giudizi del sistema formale. Un sistema formale si dice corretto rispetto ad una semantica (cioe' rispetto ad una nozione di validita' per i suoi giudizi) quando i suoi assiomi sono tutti validi e quando le regole sono tali da garantire che se le premesse sono giudizi validi allora la conclusione sara' anch'essa valida. Quando cioe' tutti i teoremi che si riescono a derivare nel sistema formale sono validi. Un sistema formale si dice completo rispetto una semantica (cioe' rispetto ad una nozione di validita' per i suoi giudizi) quando tutti i giudizi validi sono derivabili nel sistema formale. (Queste definizioni di correttezza e completezza in realta' vanno completate meglio per tenere conto anche della possibile presenza di ipotesi, come vedremo studiando la logica proposizionale e quella del primo ordine). Il minimo che si deve richiedere ad un sistema formale e' che sia corretto rispetto a qualche nozione di validita'. Se e' anche completo, meglio. Ma questa proprieta' non e' goduta da tutti i sistemi formali. La logica proposizionale e' corretta e completa, per esempio, ma l'aritmetica non lo e' (anche se in un senso non propriamente identico a quello introdotto ora). Un sistema formale si dice consistente quando esiste almeno un giudizio che non e' derivabile. Quindi, se sappiamo che un sistema formale permette di derivare tutti e soli i giudizi validi (e' cioe' corretto e completo), allora per dimostrare che e' consistente basta far vedere che esiste un giudizio che non e' valido (che equivale a dire che non e' vero che tutti i giudizi sono validi). E' ovvio che la proprieta' di consistenza e' importantissima per un sistema formale. Un sistema formale non consistente non servirebbe a nulla. Un esempio di sistema formale e' CL nel testo del Martini (in cui pero' non viene specificata una semantica), oppure il seguente (che pero' va studiato dopo aver iniziato la parte relativa al lambda-calcolo) Esempio di sistema formale Prendiamo il considerazione la seguente forma di giudizio: che rappresentiamo formalmente come Per tali giudizi forniamo la seguente definizione di validita: M =α N e' valido se e solo se M si ottiene da N (o viceversa) attraverso una rinomina di variabili legate. Il sistema formale per l'alfa conversione e' quindi dato da queste definizioni di giudizio e di validita' e dagli assiomi e regole di inferenza descritte nella Table 1 a pag. 14 delle note [PS] sul Lambda-calcolo. (In tale tabella viene utilizzato il simbolo '=' anziche' '=α'). Gli assiomi sono (refl) e (alfa), mentre tutte le altre sono regole di inferenza. In realta' possiamo considerare anche gli assiomi come regole di inferenza: regole senza premesse, e quindi con conclusione sempre valida. Il sistema formale per l'alfa equivalenza ci garantisce che, se partiamo da assiomi ed utilizziamo regole di inferenza arriveremo sempre a giudizi validi. Inoltre, qualsiasi giudizio valido sara' sempre ottenibile partendo dagli assiomi ed utilizzando regole di inferenza. Si vede subito che il sistema formale per l'alfa-quivalenza e' consistente: basta mostrare un giudizio non valido, per esempio, banalmente x =α y Un altro esempio di sistema formale e' quello che formalizza la nozione di passo singolo di beta-riduzione, rappresentato dalle regole a pag.17 di [PS]. In questo caso i giudizi sono: che rappresentiamo formalmente come Anche il sistema formale della beta-riduzione e' consistente. Nota: Per quanto riguarda l'alpha-equivalenza o la beta-riduzione, possiamo ovviamente vedere (come fatto in [PS]) "=α" e "→β" come due relazioni tra Lambda-termini definite rispettivamente dalle regole della Table 1 di pag. 14 in [PS], e dalle regole di pag.17. La relazione "=α" e' infatti la piu' piccola relazione che contiene
Per chiusura rispetto alle regole si intende che se se le coppie di termini corrispondenti alle premesse di una regola appartengono alla relazione "=α" allora anche la coppia corrispondente alla conclusione della regola deve appartenere alla relazione "=α". |