Contexts in Natural Deduction

Question

This is my first post. I have a basic question about the use of context in natural deduction. If $A$ is true in an empty context, written as

$\vdash A$

then, by monotonicity, in any context $\Gamma$, $A$ is true as well, written as

$\Gamma\vdash A.$

However, the interpretation of $\Gamma\vdash A$ is usually that $A$ is true under the assumptions in $\Gamma$.

My question is, if there is any way to signal that $A$ is true and independent from any assumption in $\Gamma$ in the sequent $\Gamma\vdash A$? In other words, how is it possible to keep the interpretation of $\vdash A$ while adding a context $\Gamma$ (by monotonicity) in front of the sequent? Thanks!

Answer 1

The interpretation of Γ⊢ is usually that is true under the assumptions in Γ.

Not quite: It is "under at most the assumptions in $\Gamma$". The definition of $\vdash$ reads

$\Gamma \vdash A$ iff there is a derivation $\mathcal{D}$ with end formula $A$ and $\text{Hyp}(\mathcal{D}) \subseteq \Gamma$ (where $\text{Hyp}(\mathcal{D})$ is the set of open assumptions of the derivation).

Note the $\subseteq$ rather than $=$: It is nowhere required that all or even any of the assumptions in $\Gamma$ actually be used in the derivation of $A$. The possibility that there are formulas in $\Gamma$ on which $A$ is not dependent, or conversely, the ability to add arbitrary premises to the left-hand side of the turnstile, is already built into the definition of derivability.

To express that an empty context suffices, write just that: $\vdash A$.

And to express that all premises in a given context are necessary for the derivation and can not be reduced further, write that: "$\Gamma \vdash A$, and there exists no $\Delta \subsetneq \Gamma$ such that $\Delta \vdash A$".