Cos'e' un Sistema Formale ed un esempio:
il sistema formale per l'alfa-equivalenza

 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

• assiomi e
• regole di inferenza

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₁   ....   giudizio_n
___________________________
   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. I sistemi alla Hilbert sono inoltre caratterizzati dal fatto che le deduzioni sono sequenze di formula ben formate tali che ogni fbf nella sequenza e’ un assioma, una ipotesi (nel caso di deduzioni con ipotesi) oppure una conclusione di una regola di inferenza le cui premesse la precedono nella sequenza. Nei sistemi in deduzione naturale le deduzioni sono invece delle strutture ad albero in cui i nodi sono le regole (nella forma indicata sopra) e le foglie sono le ipotesi (se non sono ipotesi scaricate dall’applicazione di qualche regola).

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. Tale nozione di correttezza pero’ e’ sensata solo se si considerano deduzioni senza ipotesi. Infatti non tiene conto del fatto che sia possibile utilizzare ipotesi nelle nostre deduzioni. Una definizione di sistema formale corretto (rispetto ad una semantica), che tenga conto della possibile presenza di ipotesi nelle deduzioni, e che sia inoltre sensata per ogni possibile sistema formale, non puo’ essere fornita (infatti il martini non la fornisce). La definizione che ci potrebbe venire in mente in modo naturale potrebbe essere: se tutte le ipotesi in una deduzione sono valide, allora anche la conclusione e’ valida. Ma non e’ una definizione sufficientemente generale, come vedremo studiando i sistemi formali della Logica Proposizionale e della Logica dei Predicati, e le loro rispettive semantiche.

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.
Come detto prima per la nozione di correttezza, anche questa definizione dovrebbe tener conto della possibile presenza di ipotesi. Una definizione di completezza ragionevole ed utilizzabile per tutti i sistemi formali non e’ possibile fornirla.

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 alla Hilpert 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:

Il termine M e' alfa-equivalente al termine N

che rappresentiamo formalmente come

M =_alfa N

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:

Il termine M si riduce ad N con un passo di beta-riduzione

che rappresentiamo formalmente come

M →_β N

e la cui nozione di validita' corrisponde a "nel termine M c'e' un sottotermine della forma (\x.P)Q che viene sostituito con P[Q/x]".

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

• tutte le coppie di termini specificate dagli assiomi
• e chiusa rispetto alle regole.

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 "=_α".