Queridos todos
En el método clásico de refutación, se busca una prueba de $\Gamma, \lnot A \vdash \bot$ en lugar de $\Gamma \vdash A$ . El método funciona, es decir, es completo y correcto, ya que, por ejemplo, se ve fácilmente que ambas secuencias son interderivables (*).
En un método de resolución de Robinson basado en el método de refutación también nos aseguramos de que $\Gamma$ y $A$ están en forma normal conjuntiva skolemizada y que sólo hacemos unificación y una regla de inferencia simple guiada por algunas estrategias de control. Este es en realidad el trasfondo por el que me interesa la cuestión.
Ahora hay un par de propuestas que dan la refutación de la resolución de Robinson para la lógica intuicionista. Primero quiero entender la idea de refutación en lógica intuicionista. Si el método de refutación es aplicable en lógica intuicionista, tendríamos interadmisibilidad de las siguientes derivaciones:
$\Gamma, \lnot A \vdash \bot$
$\Gamma \vdash A$
No podemos demostrarlo mediante la interderivabilidad como en el caso clásico. La primera dirección no funcionaría ya que hace uso de la eliminación de la doble negación. Pero la segunda dirección, por ejemplo, funciona fácilmente en un sistema de Gentzen (**).
Tengo la sensación de que la primera dirección podría ser ahora el resultado de un lema de permutación. En un sistema de Gentzen cuando tenemos una derivación que termina en $\Gamma, \lnot A \vdash \bot$ no sabemos si la última aplicación de la norma se refería a $\lnot A$ o alguna fórmula entre $\Gamma$ .
Si podemos demostrar que para cualquier derivación existe otra derivación con la permutación correspondiente, habremos terminado. ¿Existe tal lema de permutación para la lógica intuicionista? ¿O se puede validar el método de refutación por otros medios, sin hacer referencia a esta permutación? ¿O la interadmisibilidad sólo está garantizada para algunas formas de cláusula especiales?
Saludos cordiales
(*) Aquí hay algunas derivaciones que muestran la interderivabilidad clásica, yo uso $ \lnot A = A \rightarrow \bot$ :
La primera dirección:
$${{\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)}$$
La segunda dirección:
$${\Gamma \vdash A \qquad {\over \lnot A \vdash \lnot A}{(ID)} \over \Gamma, \lnot A \vdash \bot}{(MP)}$$
(**) La segunda dirección puede demostrarse en el caso intuicionista y al hacer uso de un sistema de Gentzen aplicando directamente la regla de introducción de la implicación correcta:
$${\Gamma \vdash A \qquad {\over \bot \vdash \bot}{(ID)} \over \Gamma, \lnot A \vdash \bot}{(\rightarrow R)}$$