In generale, in matematica, un calcolo è un meccanismo puramente sintattico che consente di dedurre proprietà degli oggetti su cui opera.
Nell’ambito della logica, i calcoli sono sistemi formali, meccanismi sintattici, di prova che vengono utilizzati per stabilire una qualche proprietà semantica (validità / soddisfacibilità / insoddisfacibilità) delle formule di una logica.
I calcoli a tableaux permettono di stabilire se una formula (o un insieme di formule) è o meno insoddisfacibile (e con un “trucco”, se è o meno valida). Essi operano su insiemi di formule, tramite delle regole che consentono di “destrutturare” le formule nell’insieme. In particolare, il calcolo a tableaux per la logica proposizionale classica è costituito da regole per destrutturare i seguenti tipi di formule:
Due esempi di regole sono:
quella per destrutturare le formule del tipo $A\land B$:
$$ \cfrac{\Gamma, A\land B}{\Gamma, A, B}\small{\land} $$
quella per destrutturare le formule $\neg(A\land B)$:
$$ \cfrac{\Gamma, \neg(A\land B)}{\Gamma, \neg A | \Gamma, \neg B}\small{\neg \land} $$
Innanzitutto, le regole si leggono dall’alto verso il basso: a partire dall’insieme di formule scritto sopra la linea orizzontale, applicando la regola di ottiene l’insieme (o gli insiemi, come nel caso della regola 2) scritto sotto la linea.
Come già detto, le regole operano su insiemi,; per comodità, come abbreviazione si utilizza la virgola per indicare l’unione insiemistica. Ad esempio, nella 1, $\Gamma, A\land B$ va inteso come $\Gamma \cup \{A\land B\}$.
L’insieme di formule che sta sopra la linea prende il nome di premessa, e la formula evidenziata nella premessa (ad esempio $A\land B$ nella 1, e $\neg (A\land B)$ nella 2) è chiamata formula principale della regola (di fatto, è quella su cui agisce la regola, mentre $\Gamma$ rappresenta tutte le eventuali altre formule nella premessa, sulle quali la regola non opera).
Una regola può avere una o più conclusioni, cioè insiemi sotto la linea orizzontale. Ad esempio, la 1 ha una sola conclusione, mentre la 2 ne ha due, $\Gamma, \neg A$ e $\Gamma, \neg B$, separate dalla barra verticale $|$. Si riporta $\Gamma$ nella conclusioni per indicare che tutte le formule della premessa, tranne quella principale, rimangono inalterate.
Le formule evidenziate nelle conclusioni, costruite a partire dalle sottoformule della formula principale, vengono chiamate ridotti della formula principale:
Infine, ogni regola ha un nome, scritto a destra della linea orizzontale: ad esempio, il nome della 1 è $\land$. Comunque, il nome può essere omesso, perchè è sempre deducibile dalla premessa e dalle conclusioni quale sia la regola che è stata applicata.