Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

Dear All

In the classical refutation method, one searches for a proof of $\Gamma, \lnot A \vdash \bot$ instead of $\Gamma \vdash A$. The method works, i.e. is complete and correct, since it is for example easily seen that both sequents are interderivable (*).

In a Robinson resolution method based on the refutation method we also see to it that $\Gamma$ and $A$ are in skolemized conjunctive normal form and that we only make unification and a simple inference rule guided by some control strategies. This is actually the background why I am interested in the question.

Now there are a couple of proposals that give Robinson resolution refutation for intuitionistic logic. I want first understand the idea of refutation in intuitionistic logic. If the refutation method is applicable in intuitionistic logic, we would have interadmisibility of the following derivations:

$\Gamma, \lnot A \vdash \bot$

$\Gamma \vdash A$

We cannot show this via interderivability as in the classical case. The first direction would not work since it makes use of double negation elimination. But the second direction for example easily works in a Gentzen system (**).

I have the feeling the first direction could now be a result of a permutation lemma. In a Gentzen system when we have a derivation that ends in $\Gamma, \lnot A \vdash \bot$ we don't know whether the last rule application concerned $\lnot A$ or some formula among $\Gamma$.

If we can show that for any derivation, there is another accordingly permuted derivation, we would be done. Does such a permutation lemma hold for intuitionistic logic? Or can the refutation method be validated by other means, without refering to this permutation? Or is interadmissibility only guaranteed for some special clausal forms?

Best Regards

(*) Here are some derivations that show classical interderivability, I use $ \lnot A = A \rightarrow \bot$:

The first direction:

$${{\Gamma, \lnot A \vdash \bot \over \Gamma \vdash \lnot \lnot A}{(\rightarrow L)} \qquad {\over \lnot \lnot A \rightarrow A}{(DNE)} \over \Gamma \vdash A}{(MP)}$$

The second direction:

$${\Gamma \vdash A \qquad {\over \lnot A \vdash \lnot A}{(ID)} \over \Gamma, \lnot A \vdash \bot}{(MP)}$$

(**) The second direction can be shown in the intuitionistic case and when making use of a Gentzen system by directly applying the right implication introduction rule:

$${\Gamma \vdash A \qquad {\over \bot \vdash \bot}{(ID)} \over \Gamma, \lnot A \vdash \bot}{(\rightarrow R)}$$

share|improve this question
    
Oops I found somehow a counter example for the refutation method in intuitionistic logic. $\lnot \lnot p, \lnot p \vdash \bot$ is intuitionistically valid, but $\lnot \lnot p \vdash p$ is not. So refutation method is not possible for intuitionistic logic, but resolution method maybe. –  Countably Infinite Jun 6 '11 at 9:07
    
On the other hand, if we would restrict ourselves to $\Gamma = \oslash$, interadmissibility would hold I guess. Permutation would not anymore be needed. –  Countably Infinite Jun 6 '11 at 9:44
add comment

2 Answers 2

$\Gamma=\varnothing$ will not help you. Using refutation in this way is completely off the mark in intuitionistic logic, since $\Delta\vdash\bot$ holds intuitionistically if and only if it holds classically, due to Glivenko’s theorem. For example, $\neg(p\lor\neg p)\vdash\bot$, but not $\vdash p\lor\neg p$.

As for resolution: the resolution rule is intuitionistically sound, and together with the weakening rule (which can be restricted to be the last step in the proof) it is classically complete for inferrences $\Gamma\vdash C$ where $\Gamma\cup\{C\}$ are sets of clauses (disjunctions of variables and negated variables) such that $C$ does not simultaneously include a variable and its negation (i.e., it is not a weakening of the law of excluded middle). It follows that for inferrences of this kind, classical and intuitionistic logic coincide, and resolution with final weakening is sound and complete.

There is also another way of making classical resolution an intuitionistic proof system, namely to identify classical clauses with intuitionistic formulas of the form $p_1\land p_2\land\dots\land p_n\to q_1\lor q_2\lor\dots\lor q_m$. This formula is equivalent to the sequent $p_1,\dots,p_n\Rightarrow q_1,\dots,q_m$ with no logical symbols, just variables. By cut elimination, the cut rule, the identity axiom, and structural rules are complete for derivation of one such sequent from a set of other such sequents. This, again, is a notational variant of resolution: cut is the resolution rule, the identity axiom corresponds to the clause $\{p,\neg p\}$ and it is not actually needed unless the endsequent contains the same variable on both sides, and treating cedents as sets, the only structural rule needed is weakening, which may be restricted to be the last rule in the proof, and corresponds directly to weakening in resolution. In particular, intuitionistic and classical logic coincide on inferrences of this form, as above.

In both cases, resolution covers only a small fragment of intuitionistic logic; there is no analogue of CNF for intuitionistic formulas. There are ways of extending resolution with rules dealing with compound formulas to make it a complete proof system for full intuitionistic logic, even first-order, see e.g. Fitting.

share|improve this answer
    
You sure $\Delta \vdash \bot$ intuitionisticall iff $\Delta \vdash \bot$ classically for arbitrary $\Delta$? Is that what you are saying in the beginning? –  Countably Infinite Jun 6 '11 at 11:16
    
Yes, that is correct, for propositional logic. –  Sridhar Ramesh Jun 6 '11 at 11:21
    
Is there something known about the non-propositional case? Any relationship between intuitionistic consistency and classical consistency? Do we need to invoke some complex translation, or can there something simpler be said? –  Countably Infinite Jun 7 '11 at 23:01
1  
The Fitting reference was a bit random, do not take it too seriously. Nevertheless, it is older than Mints, it appeared in: Methodologies for Intelligent Systems, Proceedings of the 2nd International Symposium (Ras, Zemankova, eds.), Elsevier, 1987, 400–407. –  Emil Jeřábek Jun 8 '11 at 11:02
1  
As for the first-order case, Glivenko’s theorem no longer holds in this case, one has to use a slightly more complicated negative translation (often known as Gödel–Gentzen translation; there are several variants). The effect is that classically inconsistent formulas may be intuitionistically consistent, for example $\neg\forall x\,(P(x)\lor\neg P(x))\nvdash\bot$. Nevertheless, the equivalence of classical and intuitionistic consistency holds (1) for formulas without $\forall$, and (2) for all formulas in the extension of intuitionistic logic with the double negation shift axiom. –  Emil Jeřábek Jun 8 '11 at 11:06
show 1 more comment

Quotations : " ¬¬p,¬p⊢⊥ is intuitionistically valid, but ¬¬p⊢p is not. So refutation method is not possible for intuitionistic logic" Countably Infinite Jun 6 at 9:07

"Γ=∅ will not help you. Using refutation in this way is completely off the mark in intuitionistic logic, since Δ⊢⊥ holds intuitionistically if and only if it holds classically, due to Glivenko’s theorem. For example, ¬(p∨¬p)⊢⊥, but not ⊢p∨¬p." Emil Jeřábek

Wrong. The correct derivations in intuitionistic logic are the following ones :

¬¬p,¬p⊢⊥ => ¬¬p ⊢ (¬p -> ⊥) i.e. : ¬¬p,¬p⊢⊥ => ¬¬p ⊢ (p -> ⊥)-> ⊥ i.e. ¬¬p ⊢ ¬¬p .

Same thing for Jeřábek's example given in the quotation.

¬(p∨¬p) ⊢ ⊥ => ⊢ ¬(p∨¬p) -> ⊥ i.e.

⊢ ¬ ¬(p∨¬p) which is intuitionistically correct.

All the best.

Jo.

share|improve this answer
3  
So, are you confirming or refuting the two claims? (It looks like you're confirming them, but the word 'wrong' seems to suggest otherwise.) –  François G. Dorais Dec 29 '11 at 14:03
3  
I second Francois's comment. The two quotations say that certain things cannot be deduced intuitionistically. Joseph Vidal-Rosset shows that some other things can be deduced intuitionistically. My reaction is: So what? –  Andreas Blass Dec 29 '11 at 15:12
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.