Sistemi deduttivi

I metodi che permettono di stabilire se una formula ha una certa proprietà (tipicamente, se è una tautologia, o se è soddisfacibile) senza fare riferimento alla semantica prendono il nome di sistemi deduttivi (o calcoli logici, o sistemi di prova). In questo ambito si parla di:

• dimostrazioni: gli oggetti che certificano una proprietà semantica (ad esempio la verià) di una formula;
• teoremi: le formule di cui le dimostrazioni asseriscono la verità (o, in generale, la proprietà semantica considerata).

Ad esempio, il calcolo a tableaux $\Tau_{CPL}$ è un sistema deduttivo in cui:

• le dimostrazioni sono i tableaux chiusi di formule negate $\neg H$;

• i teoremi sono le formule $H$ per cui esiste una dimostrazione, ricordando che

  

In letteratura, esistono varie tipologie di sistemi deduttivi (calcoli a tableaux, calcoli alla Hilbert, cacoli a sequenti, deduzione naturale, risoluzione, ecc...), che hanno caratteristiche e applicazioni diverse (studio delle proprietà della logica, dimostrazione automatica, dimostrzione semi-automatica).

Calcoli alla Hilbert

Tra i vari sistemi deduttivi, i calcoli alla Hilbert, detti anche sistemi assiomatici, hanno un ruolo particolarmente importante, per due ragioni:

• sono uno dei sistemi deduttivi più facilmente applicabili a logiche diverse;
• sono la formalizzazione del processo di ragionamento - introdotto da Euclide nel III seconlo a.C., con i suoi trattati di geometria (Elementi) - che parte da un insieme di formule assunte intuitivamente come verità (assiomi o postulati) e, da queste, dimostra i teoremi utilizzando un insieme molto limitato di meccanismi di ragionamento.

Il caso della geometria euclidea

I postulatidegli Elementi di Euclide sono i seguenti (che egli assume veri sulla base dell’osservazione del mondo reale):

1. Tra due punti qualsiasi è possibile tracciare una e una sola retta
2. Si può prolungare un segmento oltre i due punti indefinitivamente
3. Dato un punto e una lunghezza, è possibile descrivere un cerchio.
4. Tutti gli angoli retti sono congruenti tra loro.
5. Per un punto esterno a una retta data passa una e una sola retta parallela a questa.

A partire da questi postulati, utilizzando un insieme limitato di schemi di ragionamento (principi logici) “evidentemente corretti”, Euclide sviluppa le dimostrazioni dei teoremi che costituiscono il “cuore” della geometria piana, a partire dalla quale si sviluppa poi la geometria solida.