Deduction theorem for Natural Deduction

187 Views Asked by At

I am learning the basics of Natural Deduction and I meet a problem about the role of context.

In Natural Deduction, if we have $\vdash A\rightarrow B$, we also have $A\vdash B$; if we have $A\vdash B$, we obtain $\vdash A\rightarrow B$.

My question is: if we have $\Gamma\vdash A$ where $\Gamma$ denotes a context, do we have $\vdash\Gamma\rightarrow A$; and if we have $\vdash\Gamma\rightarrow A$, do we have $\Gamma\vdash A$? I ask this because I didn't see any occurrence of contexts written as $\Gamma,\Delta$ after $\vdash$, is it wrong to write in that way?

Thank you in advance!

1

There are 1 best solutions below

8
On BEST ANSWER

Yes, we do, in a way, have the generalization $\Gamma \vdash A\ \Longleftrightarrow\ \vdash "\Gamma \to A"$, and yes, it is wrong to write it that way, because $\Gamma$ is not a formula, and only formulas may occur as the antecedent to an object-language implication $\to$.

The solution is that when importing the set of premises into the conclusion, the premises become conjoined: The generalized deduction theorem says that

$$\Gamma \vdash A \ \Longleftrightarrow \ \vdash (\gamma_1 \land \ldots \land \gamma_n) \to A$$

(where $\gamma_i \in \Gamma$).

For more convenient notation, one may introduce a symbol for generalized conjunction:

$$\bigwedge \Gamma = \gamma_1 \land \ldots \land \gamma_n$$

and thus write

$$\Gamma \vdash A \ \Longleftrightarrow \ \vdash \bigwedge \Gamma \to A.$$

However, as user21820 correctly points out, this is only applicable if the set $\Gamma$ is finite, since there is no such thing as infinitely conjoined formulas.