2 added 73 characters in body

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

1

# Would intuitionistic refutation method imply permutation of premisses?

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?

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