Regole per $\land, \lor, \rarr$:
Regole per $\neg \land, \neg \lor, \neg \rarr$:
Regola per $\neg \neg$:
Per semplificare la presentazione e le dimostrazioni, si considerano inizialmente linguaggi del primo ordine in cui non ci sono simboli di funzione:
Più avanti, si vedrà come modificare le regole del calcolo per ordine, $\Tau_{\text{CFO}}$, estende il calcolo a tableaux per la logica proposizionale, $\text{T} _{\text{CPL}}$, dal quale “eredita” le regole relative ai connettivi:
Regole per $\land, \lor, \rarr$:
Regole per $\neg \land, \neg \lor, \neg \rarr$:
Regola per $\neg \neg$:
Oltre a queste, $\text{T}_{\text{CFO}}$ introduce quattro nuove regole per i quantificatori:
La regola per il quantificatore universale,
afferma che, se la premessa contiene la formula $\forall x A$, allora la conclusione contiene ancora $\forall xA$, e, in più, contiene un’istanza di $A$ costruita su una qualunque costante $c$.
La regola per il quantificatore esistenziale,
sostituisce $\exist xA$ con un’istanza di $A$, $A[a/x]$, dove la costante $a$ (detta anche parametro) è una costante nuova, cioè non compare nell’alfabeto iniziale, nè nel tableau nel quale si sta applicando la regola.
Le regole per $\neg \forall$ e $\neg \exist$ sono duali a quelle appena introdotte:
Le regole per i quantificatori sono classificate in due famiglie:
$\gamma$-regole:
quelle in cui la costante $c$ introdotta nella conclusione è una qualuque costante già presente nell’alfabeto del tableau;
$\delta$-regole:
quelle in cui si introduce una costante $a$ nuova.
Come fatto per il caso proposizionale, l’obiettivo sarà mostrare che il calcolo a tableaux per la logica classica del primo ordine è corretto (valido) e completo.