3
$\begingroup$

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!

$\endgroup$
3
  • 1
    $\begingroup$ As you said, to say that $A$ is derivable independently from every context $\Gamma$ we have $\vdash A$. $\endgroup$ Jul 7, 2020 at 14:28
  • 2
    $\begingroup$ You can try with a contrived: $\Gamma \supseteq \emptyset \vdash A$, but I've never seen it... $\endgroup$ Jul 7, 2020 at 14:31
  • $\begingroup$ @MauroALLEGRANZA Thanks! I've never seen it either. It looks strange... $\endgroup$
    – Emini Jask
    Jul 7, 2020 at 14:57

1 Answer 1

6
$\begingroup$

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$".

$\endgroup$
2
  • $\begingroup$ Thanks! Yes, I agree, it's sufficient for the hypotheses of $A$ be a subset of those contained in $\Gamma$. But your suggestion didn't answer my question. I agree with you on the way to define the smallest context. But what I am wondering is that how we can signal the smallest context (in my question, it's an empty context) while using a larger one in front of the sequent. Do you have any idea about this? $\endgroup$
    – Emini Jask
    Jul 7, 2020 at 15:46
  • $\begingroup$ I don't know of any more compact notation than the one in my last sentence. $\endgroup$ Jul 7, 2020 at 15:47

This site is temporarily in read-only mode and not accepting new answers.

Not the answer you're looking for? Browse other questions tagged .