Would intuitionistic refutation method imply permutation of premisses? - MathOverflow

Would intuitionistic refutation method imply permutation of premisses?

2011-06-06T07:58:02Z

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)}$$

Answer by Emil Jeřábek for Would intuitionistic refutation method imply permutation of premisses?

2011-06-06T10:26:52Z

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

Answer by Joseph Vidal-Rosset for Would intuitionistic refutation method imply permutation of premisses?

2011-12-29T12:12:21Z

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.