Introduzione alla Deduzione Naturale

 

Il sistema formale per il calcolo proposizionale descritto in [SM] e' un sistema assiomatico (tali sistemi sono anche detti alla Hilbert) in quanto contiene un certo numero di assiomi ed un ristretto numero di regole di inferenza (nel nostro caso una sola regola: il modus ponens). Inoltre la nozione di prova e' formalizzata come sequenza di formule ben formate (con certe caratteristiche, vedi [SM])

Ovviamente non e' indispensabile rappresentare prove come sequenze di fbf. Potremmo utilizzare anche una notazione ad albero (la comune struttura dati utilizzata in informatica, tenendo conto che in questo caso gli alberi si considerano rappresentati con la radice in basso, mentre solitamente gli alberi si rappresentano con la radice in alto).
Cerchiamo di capire con un esempio questo differente modo di presentare le derivazioni.

Prendiamo la soluzione dell'esercizio 22 della sezione Logica degli esercizi, cioe'

1.   α → (¬β → α)                 Ak
2.   α                             ipotesi
3.   ¬β → α                       MP(1,2)
4.   ¬α → (¬β → ¬α)               Ak
5.   ¬α                           ipotesi
6.   ¬β → ¬α                      MP(4,5)
7.   (¬β → ¬α) → ((¬β → α) → β)   A¬
8.   (¬β → α) → β                 MP(6,7)
9.   β                            MP(3,8)

Se la rappresentiamo come albero diventa

            
                                    _______________
                            ¬α      ¬α → (¬β → ¬α)
        ____________       ------------------------   __________________________
  α     α → (¬β → α)            ¬β → ¬α               (¬β → ¬α) → ((¬β → α) → β)
---------------------        ---------------------------------------------------
      ¬β → α                                 (¬β → α) → β)
    ----------------------------------------------------------
                                        β

Notare come, passando dalla notazione in sequenza alla notazione ad albero, una riga in cui viene applicata una regola

k: δ   R(i,j)

diventi

    fbf in i      fbf in j
---------------------------- (R)
            δ 

(Per maggiore chiarezza conviene talvolta inserire, a destra della linea di separazione, il nome della regola.)

Inoltre gli assiomi

k:  δ  Ax

diventano foglie della forma

--------- (Ax)
    δ 

Mentre le ipotesi

k: δ  Ipotesi 

diventano semplicemente foglie della forma

  δ

E' molto facile passare, al contrario, da una rappresentazione ad albero ad una sequenziale. In questo caso possiamo notare che ci sono molte sequenze corrispondenti allo stesso albero.


Esistono molti sistemi formali per la logica proposizionale equivalenti a quello alla Hilbert utilizzato in [SM]. Uno di questi e' il sistema formale della logica proposizionale in deduzione naturale (che studieremo in [AA] e [AU].
In questo sistema formale l'insieme degli assiomi e' vuoto. Ci sono solo regole di inferenza.
Rispetto ai sistemi assiomatici la nozione di derivazione e' esclusivamente quella ad albero. QUesto fatto dipende dalla caratteristica di avere regole di inferenza in cui vengono scaricate delle ipotesi. Tale meccanismo di scaricamento non risulterebbe rappresentabile in modo sufficientemente chiaro in una rappresenzazione sequenziale.
Nel sistema formale della logica proposizionale in deduzione naturale abbiamo cosi' che Γ ⊢ P (cioe' "la formula P e' derivabile dall'insieme di ipotesi Γ") quando e' possibile costruire un albero di derivazione di P da ipotesi in Γ cosi' come descritto a pag.2 di [AU].

Il sistema assiomatico descritto in [SM] e la deduzione naturale sono equivalenti dal punto di vista della derivabilita'. Cioe' dato un insieme Γ di ipotesi, l'insieme delle conseguenze di Γ e' lo stesso sia nel sistema assiomatico in [SM] che nella deduzione naturale (l'insieme delle conseguenze e' definito nella Definizione 2.7 di [SM]).

Il sistema di deduzione naturale per la logica proposizionale descritto a pag.1 di [AU], contrariamente al calcolo proposizionale in [SM], possiede regole di inferenza anche per i connettivi logici congiunzione e disgiunzione.
In realta' potremmo (come per il sistema in [SM]) definire la congiunzione e la disgiunzione in termini di implicazione e negazione (e far vedere che regole di inferenza per congiunzione e disgiunzione sono derivabili).
Da notare che se vogliamo considerare in [AU] solo i connettivi implicazione e negazione, le regole da prendere in considerazione siano tutte quello che riguardano appunto l'implicazione, la negazione, insieme a quelle che riguardano il simbolo ⊥. Tale simbolo e' utilizzato in deduzione naturale per rappresentare l'assurdo (si potrebbe utilizzare al suo posto, volendo, una proposizione contraddittoria).

Sostituzioni
(da leggere quando si studia la deduzione naturale per la logica dei predicati)

Nel λ-calcolo le nozioni di variabile libera e legata dipendono dall'operatore di lambda-astrazione, che lega nel corpo della funzione la variabile che viene utilizzata come argomento della stessa.
Nello stesso modo, nella logica dei predicati, le variabili quantificate universalmente o esistenzialmente sono da considerare legate all'interno della fbf a cui si riferisce il quantificatore. Anche per le fbf della logica dei predicati si puo' quindi parlare di variabili libere e variabili legate. Analogamente, come per il lambda-calcolo, possiamo parlare di fbf α convertibili, cioe' identiche a meno di rinomina di variabili legate.
L'operazione di sostituzione (di una variabile individuale con un termine) e' utilizzata anche in logica dei predicati (per esempio in alcune regole di deduzione naturale per i quantificatori universale ed esistemziale (vedi [AU])).
Non abbiamo bisogno di definire l'operatore di sostituzione per la logica, poiche' la sua definizione e' simile a quella che abbiamo definito per il λ-calcolo. (se interessati, una definizione esplicita si trova in [SM])