Una prueba de cálculo secuencial

Question

Consideremos el cálculo secuencial (con contextos multiplicativos) definido por las siguientes reglas (sin contracción ni debilitamiento). El cálculo secuencial se ha tomado de la página 23: http://users.ox.ac.uk/~cpgl0036/pdf/asudeh-giorgolo-perspectivas.pdf ):

$$ \frac{\qquad }{A \vdash A} \,{Id} $$

$$ \frac{\Gamma\vdash B \qquad B, \Delta\vdash C}{\Gamma, \Delta \vdash C} \,{Cut} $$

$$ \frac{\Delta\vdash A \qquad \Gamma, B\vdash C}{\Gamma, \Delta, A \rightarrow B \vdash C} \,{\rightarrow L} $$

$$ \frac{\Gamma, A \vdash B}{\Gamma \vdash A \rightarrow B} \,{\rightarrow R} $$

$$ \frac{\Gamma \vdash A}{\Gamma \vdash \bigcirc A} \,{\bigcirc R} $$

$$ \frac{\Gamma, A \vdash \bigcirc B \qquad }{\Gamma, \bigcirc A \vdash \bigcirc B} \,{\bigcirc L} $$

Puedo probar $\bigcirc (A \rightarrow B) \vdash \bigcirc A \rightarrow \bigcirc B$ en este cálculo, pero no a la inversa $\bigcirc A \rightarrow \bigcirc B \vdash \bigcirc (A \rightarrow B)$ . ¿Es demostrable lo contrario? No encuentro ninguna prueba.

Answer 1

La receta general para responder a estas preguntas se basa en una teorema de eliminación de cortes . Los autores afirman en la nota 28 que el $Cut$ es "admisible" para este cálculo, que es otra forma de decir que puede eliminarse.[*] Para decidir si $\bigcirc A \to \bigcirc B \vdash \bigcirc (A \to B)$ es demostrable, basta preguntarse: "¿Tiene una demostración sin cortes?".

Ahora, cualquier prueba sin cortes de $\bigcirc A \to \bigcirc B \vdash \bigcirc (A \to B)$ debe terminar necesariamente en ${\to}L$ o ${\bigcirc}R$ como en uno de los siguientes intentos de prueba: $$ \frac{\vdash \bigcirc A \qquad \bigcirc B \vdash \bigcirc (A \to B)}{\bigcirc A \to \bigcirc B \vdash \bigcirc (A \to B)} {\to}L \qquad \frac{\bigcirc A \to \bigcirc B \vdash A \to B}{\bigcirc A \to \bigcirc B \vdash \bigcirc (A \to B)} {\bigcirc}R $$ La primera posibilidad puede eliminarse inmediatamente porque no es posible demostrar $\vdash \bigcirc A$ para arbitraria $A$ (toma $A$ cualquier fórmula atómica). La segunda posibilidad puede eliminarse igualmente mediante un poco más de análisis de casos de pruebas sin corte: eventualmente tendríamos que demostrar $\bigcirc B \vdash B$ pero esto no es posible en el caso de $B$ .

Por lo tanto, $\bigcirc A \to \bigcirc B \vdash \bigcirc (A \to B)$ no es demostrable para $A$ y $B$ .

[*] técnicamente, una regla es admisible para un cálculo secuencial si, dadas las derivaciones de las premisas, podemos construir una derivación de la conclusión sin utilizar la propia regla. En particular, la regla $Cut$ es admisible si se dan derivaciones sin corte de $\Gamma \vdash B$ y $B, \Delta \vdash C$ siempre podemos construir una derivación sin cortes de $\Gamma,\Delta \vdash C$ .

---

Editar : Por supuesto, el razonamiento adicional que falta en este argumento es la prueba de la eliminación del corte que los autores afirman en la nota a pie de página. Eso se suele hacer caso por caso para un cálculo secuencial concreto, y es un buen ejercicio (puedes encontrar un ejemplo para otro cálculo secuencial en estos Notas de clase de Frank Pfenning ).