3
$\begingroup$

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 ?

$\endgroup$
1
$\begingroup$

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):

Proof of formula corresponding to "derived rule"

$\endgroup$
  • $\begingroup$ Thanks ! But I still have a doubt about the "reading" of the "derived" rule. If it amount to : "if we have a proof of $B$ from axioms $\Gamma$ and $\lnot \lnot A$, we can also construct a proof of $B$ from $\Gamma$ and $A$ (without double negation)", it is not so clear to me how this fact "fits with" the BHK-Int. $\endgroup$ – Mauro ALLEGRANZA Apr 9 '14 at 9:58
  • $\begingroup$ This might be a bit difficult to grasp since the BKH interpretation does not talk about sequences. But lets attempt to transform the "derived" rule into a formula in a slightly sloppy manner: Then we obtain (ignoring $\Gamma$) $(\neg\neg A\rightarrow B)\rightarrow (A \rightarrow B)$, which makes perfect sense: If we have a transformation from the "unconstructive" $\neg\neg A$ to $B$, then it is even easier to construct a transformation from $A$ to $B$, now with more constructive information. The premise $\neg\neg A \rightarrow B$ is a strengthening of the conclusion. $\endgroup$ – rindPHI Apr 9 '14 at 10:14
  • $\begingroup$ Ok, maybe ... I understand your argument, also if (i) I'm not able to formally derive it from the rule : ignore $\Gamma$ and apply $\supset$-intro to the bottom sequent to have : $\lnot \lnot A \vdash B/\vdash A \supset B$; but what about the top sequent ? (ii) how I check that $(\lnot \lnot A→B)→(A→B)$ is intuitionistically valid ? Kripke's semantics ? $\endgroup$ – Mauro ALLEGRANZA Apr 9 '14 at 10:20
  • 1
    $\begingroup$ To (ii): You can show the intuitionistic validity easily by a proof in LJ. I added one to my answer. $\endgroup$ – rindPHI Apr 9 '14 at 10:55
  • $\begingroup$ To (i): The formula corresponds to the intended meaning of the sequent, but is actually something entirely different. I translated sequents into formulas (which is already sloppy) but then also the rule into a formula. Possibly there is no straightforward translation from the derived rule to the "corresponding" formula, it was rather an argument on the semantic side. $\endgroup$ – rindPHI Apr 9 '14 at 11:02
0
$\begingroup$

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!

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.