¿El método de refutación intuicionista implicaría la permutación de premisas?

Question

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

Answer 1

$\Gamma=\varnothing$ no te ayudará. Usar la refutación de esta manera está completamente fuera de lugar en la lógica intuicionista, ya que $\Delta\vdash\bot$ se cumple intuitivamente si y sólo si se cumple clásicamente, debido al teorema de Glivenko. Por ejemplo, $\neg(p\lor\neg p)\vdash\bot$ pero no $\vdash p\lor\neg p$ .

En cuanto a la resolución: la regla de resolución es intuitivamente sólida, y junto con la regla de debilitamiento (que puede restringirse para que sea el último paso de la prueba) es clásicamente completa para inferencias $\Gamma\vdash C$ donde $\Gamma\cup\{C\}$ son conjuntos de cláusulas (disyunciones de variables y variables negadas) tales que $C$ no incluye simultáneamente una variable y su negación (es decir, no es un debilitamiento de la ley del medio excluido). De ello se deduce que, para inferencias de este tipo, la lógica clásica y la intuicionista coinciden, y la resolución con debilitamiento final es sólida y completa.

También existe otra forma de hacer de la resolución clásica un sistema de prueba intuicionista, a saber, identificar las cláusulas clásicas con fórmulas intuicionistas de la forma $p_1\land p_2\land\dots\land p_n\to q_1\lor q_2\lor\dots\lor q_m$ . Esta fórmula es equivalente al secuente $p_1,\dots,p_n\Rightarrow q_1,\dots,q_m$ sin símbolos lógicos, sólo variables. Mediante la eliminación de cortes, la regla de corte, el axioma de identidad y las reglas estructurales se completan para la derivación de un secuente de este tipo a partir de un conjunto de secuentes de este tipo. Esto, de nuevo, es una variante notacional de la resolución: el corte es la regla de resolución, el axioma de identidad corresponde a la cláusula $\{p,\neg p\}$ y en realidad no se necesita a menos que el endsequent contenga la misma variable en ambos lados, y tratando los cedents como conjuntos, la única regla estructural necesaria es el debilitamiento, que puede restringirse a ser la última regla de la prueba, y corresponde directamente al debilitamiento en la resolución. En particular, la lógica intuicionista y la clásica coinciden en inferencias de esta forma, como se ha indicado anteriormente.

En ambos casos, la resolución sólo cubre un pequeño fragmento de la lógica intuicionista; no existe un análogo de CNF para las fórmulas intuicionistas. Hay formas de ampliar la resolución con reglas que traten las fórmulas compuestas para convertirla en un sistema de prueba completo para toda la lógica intuicionista, incluso de primer orden. Instalación .

Answer 2

Citas : " ¬¬p,¬p⊢⊥ es intuitivamente válido, pero ¬¬p⊢p no lo es. Así que el método de refutación no es posible para la lógica intuicionista" Countably Infinite Jun 6 at 9:07

"Γ=∅" no te ayudará. Usar la refutación de esta manera está completamente fuera de lugar en lógica intuicionista, ya que Δ⊢⊥ se sostiene intuicionísticamente si y sólo si se sostiene clásicamente, debido al teorema de Glivenko. Por ejemplo, ¬(p∨¬p)⊢⊥, pero no ⊢p∨¬p". Emil Jeřábek

Incorrecto. Las derivaciones correctas en lógica intuicionista son las siguientes :

¬¬p,¬p⊢⊥ => ¬¬p ⊢ (¬p -> ⊥) es decir : ¬¬p,¬p⊢⊥ => ¬¬p ⊢ (p -> ⊥)-> ⊥ es decir ¬¬p ⊢ ¬¬p .

Lo mismo ocurre con el ejemplo de Jeřábek citado.

¬(p∨¬p) ⊢ ⊥ => ⊢ ¬(p∨¬p) -> ⊥ es decir

⊢ ¬ ¬(p∨¬p) que es intuitivamente correcto.

Le deseo lo mejor.

Jo.