Double Negation is sequent calculus systems LK and LJ

Question

In sequent calculus LK (see Gaisi Takeuti, Proof Theory (2nd ed - 1987)) we have a "standard" derivation of Double Negation in the form $\rightarrow \lnot \lnot A \supset A$.

We have to start from an Axiom :

$$\frac{A \rightarrow A}{\rightarrow \lnot A, A}$$ by $\lnot$-right;

then :

$$\frac{\rightarrow \lnot A, A}{\lnot \lnot A \rightarrow A}$$ by $\lnot$-left;

finally :

$$\frac{\lnot \lnot A \rightarrow A}{\rightarrow \lnot \lnot A \supset A}$$ by $\supset$-right.

The proof is not intuitionistically admissible, due to the violation (in the first step) of the restriction [see Takeuti, page 28] that : "a sequent in LJ is of the form $\Gamma \rightarrow \Delta$, where $\Delta$ consists of at most one formula".

In a previous post we have a proof (assuming it is correct) of the "derived rule" :

$$\frac {\Gamma, \lnot \lnot A \vdash \Delta } {\Gamma, A \vdash \Delta }$$

that looks like a form of Double Negation.

If we impose the restriction that $\Delta$ must consists of at most one formula, we have (assuming that the proof is correct) that the rule is admissible in LJ.

What is the "meaning" of this derived rule compared to the previous formulation ?

Answer 1

The (classically valid) sentence $ {\vdash \neg\neg A \rightarrow A} $ means that we can drop a double negation before arbitrary formulas. In intuitionistic systems, this only holds for special classes of formulas, like propositional formulas. In many systems, an extended axiom of this type (called "Markov principle") for formulas of the form $\exists x A_0(x) $, where $A_0(x)$ is quantifier-free and has only $x$ free, is admitted.

The "derived rule"

$$ {\Gamma,\neg\neg A\vdash B \over \Gamma,A\vdash B} $$

does not allow to drop double negation. It merely says that if we have a proof of $B$ from axioms $\Gamma$ and $\neg\neg A$, we can also construct a proof of $B$ from $\Gamma$ and $A$ (without double negation). This is a fundamentally different thing. The post referred by you supplies such a construction.

Finally a word on the invalidity of $ {\vdash \neg\neg A \rightarrow A} $ in intuitionistic logic: $\neg\neg A$ is basically a shortcut for $((A \rightarrow \bot)\rightarrow\bot)$. According to the Brouwer-Heyting-Kolmogorov-Interpretation, which aims to define the intuitive meaning of an intuitionistic proof, the proof of an implication is a function converting a proof of the premise into a proof of the conclusion. However, assuming that we have a proof of $((A \rightarrow \bot)\rightarrow\bot)$, this gives us absolutely none constructively usable information (we have a construction transforming a proof of the construction transforming a proof of $A$ to a proof of $\bot$ to a proof of $\bot$, see what I mean...). So we would have to proof $A$ basically "from scratch". Now, just let $A$ be the special halting problem $\exists n\in\mathbb{N}T(e,e,n)$, $T$ is the Kleene-T-predicate, then a proof of $A$ would solve the special halting problem which is not possible since the undecidability of this problem has been shown by Turing.

/edit: As a reaction to the comments to this answer, here another addition: Let us interpret the "derived rule" as a formula $ (\neg\neg A\rightarrow B) \rightarrow (A\rightarrow B) $ (assuming, for simplicity, that $\Gamma$ is empty). Obviously, the formula reflects the intuitive meaning of the rule. We can show the validity of this formula by a derivation in LJ (the existence of which, due to soundness, implies validity):

Answer 2

Here is a way to look at this: if something follows from assumption --A, then it should follow from the intuitionistically stronger assumption A. The "deductive direction" on the assumption side is the opposite of the succedent side, sort of upwards!