Derivazione logica

La derivazione è un processo logico che spiega come una proposizione (o formula) può essere ottenuta da un insieme iniziale di affermazioni vere, chiamate assiomi o ipotesi, attraverso l'applicazione di precise regole di inferenza.

Una derivazione è composta da tre elementi principali:

Assiomi e ipotesi
Un insieme di assiomi o ipotesi che si assumono vere a priori. Ad esempio, in geometria euclidea, si parte dagli assiomi di Euclide; nella logica proposizionale, si può partire da una formula come $ P \to Q $ (se $ P $, allora $ Q $).
Regole di inferenza
Sono i passi logici permessi per derivare nuove affermazioni. Ogni regola deve garantire che, se le premesse sono vere, anche la conclusione lo sarà. Esempi di regole comuni includono.
Conclusione
La proposizione finale è la formula che si vuole dimostrare. Questa formula è giustificata dalla catena di inferenze costruite a partire dagli assiomi. E' anche detta proposizione derivata.

Una forma proposizionale $ A $ è detta derivabile se esiste una derivazione finita $ X =\{A_1, A_2,..., A_n \} $ che la dimostra a partire da un insieme di assiomi (e/o ipotesi) attraverso l'applicazione di regole di inferenza.

Si indica con $ X \vdash A $ dove $ X $ è l'insieme delle ipotesi.

Un esempio pratico

Supponiamo di voler derivare la formula $ Q $ a partire dai seguenti assiomi:

$ P $ (ipotesi 1)
$ P \to Q $ (ipotesi 2)

In questo caso $ P $ e $ P \to Q $ sono considerati veri per ipotesi.

Applico il modus ponens come regola di inferenza e concludo che $ Q $ è vero.

La sequenza $ P, P \to Q, Q $ costituisce la derivazione e $ Q $ è il risultato finale o proposizione derivata.

Quindi, la proposizione derivata è l'ultimo elemento del processo di derivazione.

In questo esempio la forma proposizionale $ Q $ è derivabile dall'insieme di ipotesi $ X = \{P, P \to Q\} $, poiché esiste una sequenza logica (derivazione) che conduce a $ Q $ usando $ P $ e $ P \to Q $ come assiomi e applicando il Modus Ponens. Si scrive:

$$ X \vdash Q \quad \text{oppure} \quad P, P \to Q \vdash Q $$

Nota. Una derivazione può essere lineare, seguendo una sequenza unica di passi, o ramificata, quando più linee di inferenza Si può immaginare come un albero logico in cui gli assiomi e le ipotesi sono le radici, le applicazioni sono i rami e lc conclusioni sono la chioma.

E così via.