5 votos

¿Por qué la regla de introducción a la izquierda en Cálculo secuencial es equivalente a la regla de eliminación en la Deducción natural?

He estado leyendo Florian Steinberger la tesis de Doctorado en armonía en el secuente cálculo, cuando afirma que la izquierda-introducción de la regla es funcionalmente equivalente a la eliminación de la regla.

Su argumento se adjunta en la parte inferior, pero hay dos cosas que no entiendo:

  1. ¿Por qué es $C$ ser comprobable de $\Gamma, A\land B$ a fortiori? $\{\Gamma, A\land B\}$ no es realmente un conjunto más fuerte de los locales de $\{\Gamma, A\}$, ya que este último puede ser fortalecido para el primero por la izquierda-$\land$ regla, pero el primero no puede volver a la última. En otras palabras, parecería que el anterior puede resultar inferior a la segunda. Entonces, ¿por qué a fortiori/por una razón más fuerte?

  2. ¿Por qué es la extensión hacia arriba (al final de la cita) una justificación de los dos, siendo funcionalmente equivalente? Yo no entender lo que él está tratando de hacer con la última deducción natural ($\land$ eliminación).


enter image description here enter image description here enter image description here

9voto

Taroccoesbrocco Puntos 427
  1. Se puede decir que la hipótesis de $\Gamma, A \land B$ es más fuerte que el de $\Gamma, A$ porque en $\Gamma, A \land B$ tiene más hipótesis que en $\Gamma, A$. Pero la declaración de $\Gamma, A \land B \vdash C$ (es decir, $C$ es derivable a partir de la hipótesis de $\Gamma, A \land B$) es más débil (en el sentido de menos generales o menos informativo) de la declaración de $\Gamma, A \vdash C$ (es decir, $C$ es derivable a partir de la hipótesis de $\Gamma, A$). La última afirmación significa que en realidad la hipótesis de $B$ no es necesario derivar $C$ de $\Gamma, A$. Por lo tanto, si usted puede derivarse $C$ de $\Gamma, A$, entonces a fortiori puede derivar $C$ de $\Gamma, A$ más otra hipótesis ($B$) que en realidad no es necesario.

  2. Técnicamente, el problema es demostrar que cualquier derivación en el secuente cálculo puede ser traducido a una deducción en deducción natural, con la misma conclusión y la misma hipótesis. Esta traducción se define por inducción sobre el tamaño de la derivación en el secuente el cálculo que se ha traducido. Consideremos el caso de la siguiente derivación en el secuente cálculo (cuya última regla es una introducción a la izquierda de la conjunción): \begin{align}\tag{1} \dfrac{\quad \Pi \\ \Gamma, A \vdash C}{\Gamma, A \land B \vdash C} \land_{L_1} \end{align} Por hipótesis de inducción aplicada a la derivación $\Pi$ (cuya conclusión es $\Gamma, A \vdash C$), existe una deducción en deducción natural \begin{align} \Gamma, A \\ \vdots \Pi_0 \\ \!\!\!\!\!\!\!\!\!C \end{align} Pero si le añadimos una eliminación de la regla de la conjunción por encima de $A$, obtenemos la siguiente derivación en deducción natural \begin{align} \Gamma,& \dfrac{A \land B}{A}\land_{E_1} \\ &\vdots \Pi_0 \\ &C \end{align} que es la traducción de la derivación $(1)$ en la deducción natural, con la misma conclusión e hipótesis. En este sentido, la introducción de la regla de la conjunción en $(1)$ corresponde a un alza de la extensión de la deducción en deducción natural, comenzando con la eliminación de la regla de la conjunción.


EDIT: Contexto y Preliminares para las Dos Preguntas.

Supongo que el contexto de lo que Streinberger escribí es para mostrar la equivalencia (o "coextensivenes") de deducción natural y sequent cálculo: cada prueba en el sistema anterior se puede traducir en una prueba en la última formalismo, con la misma hipótesis y la conclusión, y viceversa. En particular, el pasaje citado es acerca de la traducción de un secuente cálculo de la derivación en una deducción natural derivación. Para ser precisos en la declaración que quieres demostrar, usted tiene que tomar en cuenta una diferencia entre el secuente cálculo y deducción natural: la inferencia de reglas de deducción natural tienen un efecto en las fórmulas, mientras que las reglas de inferencia en el secuente de cálculo tienen un efecto sobre sequents, que son pares de la forma $\Gamma \vdash A$ donde $A$ es una fórmula y $\Gamma$ es una secuencia o conjunto múltiple de fórmulas. Por ejemplo, mira la diferencia entre la izquierda de la regla de la conjunción en el secuente cálculo ($\land_{L_1}$) y la eliminación de la regla de la conjunción en la deducción natural ($\land_{E_1}$, ver arriba).

Así, una deducción en deducción natural que tiene la forma de \begin{align}\tag{2} \Gamma \\ \vdots \\ A \end{align} donde $\Gamma$ es el conjunto de no cumplidas hipótesis (aproximadamente, la parte superior de las fórmulas en la derivación), y $A$ es la conclusión (la parte de abajo de la derivación).

Una derivación en el secuente cálculo tiene la forma \begin{align}\tag{3} &\vdots \\ \Gamma &\vdash A \end{align} donde el secuente en la parte inferior de la derivación contiene tanto la hipótesis de $\Gamma$ y el real de la conclusión de $A$.

Por lo tanto, en el pasaje citado, Streinberger pretende demostrar que cada sequent cálculo de la derivación de la forma $(3)$ puede ser traducido a una deducción natural derivación de la forma $(2)$ (en el pasaje citado no considera la viceversa, supongo que lidia con ello en algún otro lugar). La idea de la prueba es definir una regla por regla de traducción, es decir, para mostrar que cada regla de inferencia en el secuente cálculo se puede traducir en una o más reglas de inferencia en la deducción natural. Esta traducción es bastante fácil de definir por las normas de derecho en el secuente cálculo, ya que su comportamiento es análogo a la introducción de las reglas de la deducción natural. La traducción de la izquierda de las reglas en el secuente cálculo es el más delicado, ya que en la deducción natural al parecer no hay reglas similares. Como se muestra por Steinbergerer en el caso de la conjunción (ver arriba), la idea es que la izquierda reglas en el secuente cálculo modificar la parte de hipótesis en un secuente, por lo que pueden ser simulados en la deducción natural por la eliminación de las reglas.

i-Ciencias.com

I-Ciencias es una comunidad de estudiantes y amantes de la ciencia en la que puedes resolver tus problemas y dudas.
Puedes consultar las preguntas de otros usuarios, hacer tus propias preguntas o resolver las de los demás.

Powered by:

X