Teorema di deduzione

Template:S Nella logica matematica, il teorema di deduzione afferma che se una formula F è deducibile da un'altra formula E allora l'implicazione E → F è dimostrabile (ovvero è "deducibile" dall'insieme vuoto) e, viceversa, che se l'implicazione E → F è dimostrabile, allora la formula F è deducibile da E. In simboli, $E⊢F$ se e solo se $⊢E\to F.$. Più in generale, esso afferma che, se da un insieme di formule Γ è dimostrabile E → F, allora F è deducibile dall'insieme di premesse [Γ + (E)].

Il teorema di deduzione può essere generalizzato ad una sequenza numerabile di formule tali che da

$E_1,E_2,...,E_{n-1},E_n⊢F$, si inferisce $E_1,E_2,...,E_{n-1}⊢E_n\to F$, e così via fino a

$⊢E_1\to (...(E_{n-1}\to (E_n\to F))...)$.

Il teorema di deduzione è un meta-teorema: è usato per dedurre dimostrazioni in una certa teoria sebbene non sia un teorema della stessa teoria.

Voci correlate

• Dimostrazione condizionale
• Logica proposizionale

Collegamenti esterni

• Introduction to Mathematical Logic di Vilnis Detlovs e Karlis Podnieks. In particolare v. Section 1.5