un calcolo assiomatico determina la deducibilità di una Σ-formula φ da un insieme Φ di Σ-formule mediante un sistema formale costituto da:

• assiomi: schemi di formule logicamente valide
• regole di inferenza: permettono di dedurre il conseguente di un'istanza della regola se ne sono stati già dedotti gli antecedenti

ad esempio, ecco un sistema HF di questo tipo per la logica predicativa ristretta agli operatori logici →, ¬, ∀ e trascurando l'eguaglianza:

assiomi HF:

• φ → (ψ → φ)
• (φ → (ψ → θ)) → ((φ → ψ) → (φ → θ))
• (¬φ → ¬ψ) → (ψ → φ)
• ∀xφ(x) → φ(t)                     [t liberamente sostituibile a x in φ(x)]
• (ψ → φ(x)) → (ψ → ∀xφ(x)) [x ∉ Free(ψ)]

regola di inferenza HF (modus ponens): se φ, φ → ψ allora ψ

una deduzione HF di φ da Φ è una sequenza finita di formule che sono istanze di assiomi HF, o di formule in Φ, o dedotte per modus ponens da formule precedenti

• Φ ⊢_HF φ designa l'esistenza di una tale sequenza
• si scrive ⊢_HF φ se si usano solo gli assiomi HF e la sua regola di inferenza, nel qual caso φ è un teorema HF

il teorema di deduzione (Herbrand, Tarski, 1930) generalizza alla logica predicativa un noto principio di logica proposizionale, relativamente alla deducibilità da una teoria Φ data:

• Φ, φ ⊢_HF ψ ⇒ Φ ⊢_HF φ→ψ

schema di dimostrazione: preliminarmente si dimostra il lemma ⊢_HF φ→φ

quindi, data per ipotesi una deduzione HF: Φ, φ ⊢_HF ψ, se ne costruisce la (φ→)-trasformata rimpiazzandovi ogni formula θ che vi occorre con la formula φ→θ

• la trasformata non è la deduzione HF voluta, ma aggiungendovi altri passi, giustificati dagli assiomi HF, si ottiene una deduzione HF di φ→ψ da Φ e φ→φ
• poiché φ→φ è un teorema HF, segue la tesi

i calcoli assiomatici, di parca eleganza, non sono di facile impiego

• si veda ad es. la deduzione del lemma impiegato nella dimostrazione del teorema di deduzione, Lemma 3.1 nel testo (Manca, 2001)

proprio il teorema di deduzione diede avvio alle ricerche di Gentzen sulla teoria della dimostrazione, verso formalizzazioni più prossime al ragionamento matematico

• i calcoli di deduzione naturale devono il loro nome a tale ispirazione

caratteristiche della deduzione naturale:

• il calcolo consta di due tipi di regole di inferenza per ciascun operatore logico:
  • eliminazione: l'operatore occorre nelle premesse, ma non nelle conclusioni
  • introduzione: l'operatore occorre nelle conclusioni, ma non nelle premesse
• una deduzione naturale è una sequenza di passi di tre tipi:
  • imposizione di ipotesi
  • eliminazione di un'ipotesi precedente, e blocco delle successive formule, per sua introduzione quale antecedente di una implicazione
  • deduzione per istanziazione di una regola di inferenza, le cui premesse sono state già dedotte e non bloccate

"/" separa le premesse dalle conclusioni (di solito si usa una linea orizzontale)

N.B. nelle regole E∃ e I∀, y non deve occorrere libera in ψ né in alcuna assunzione di φ(y), ovvero ipotesi (non eliminata) nella sua deduzione

L'ultima formula in una deduzione naturale è la sua tesi

φ₁,...,φ_n ⊢ ψ designa una deduzione naturale di tesi ψ e ipotesi (non eliminate) φ₁,...,φ_n

1. Deducibilità secondo Herbrand-Skolem
   un altro metodo deduttivo per la logica predicativa, che risale a Herbrand, è basato sul teorema di compattezza proposizionale e sulla equisoddisfacibilità tra una teoria predicativa e la sua espansione di Herbrand, si veda la sez. 3.2 del testo (Manca, 2001).
2. Calcolo dei sequenti di Gentzen
   analogamente ai calcoli di deduzione naturale, il calcolo dei sequenti è una forma strutturata e modulare di deduzione diretta, anziché refutativa; ciononostante, il testo (Manca, 2001) mostra, in sez. 3.4, come questo calcolo sia sostanzialmente una variante notazionale del calcolo dei tableau.
3. Tipologia dei calcoli logici
   La sez. 3.6 del testo (Manca, 2001) presenta una interessante tassonomia dei calcoli logici, che traccia le caratteristiche essenziali e il modus operandi di ciascun tipo di calcoli deduttivi considerato; si mettono inoltre in evidenza i diversi livelli in cui l'implicazione occorre nella logica predicativa.