El desempeño de los supuestos

Question

Cuando la construcción de las pruebas mediante deducción natural ¿qué significa decir que una hipótesis o premisa es dado de alta? En qué circunstancias deseo, o la necesidad, el uso de un mecanismo de este tipo?

La razón por la que estoy haciendo esta pregunta es que muchos de texto en la lógica de uso de este término como entendido por el lector y no se toman el tiempo de explicar adecuadamente el sentido técnico en que se están utilizando.

Answer 1

Como yo lo entiendo, para el desempeño de una premisa o supuesto es el opuesto de la introducción: se absorben (por ejemplo) en el antecedente de una implicación --- esto significa que no es más que una suposición. Un ejemplo trivial:

P 1. Suponga Que P

__

P 2. A partir del 1 de

__

P->P 3. Descarga 1

Por lo tanto he llegado a la conclusión de que la P->P sin ningún tipo de supuestos (iow |- P->P). Si no descarga la asunción, tendríamos P|-P

Answer 2

En el espíritu de Kenny observación, tenga en cuenta también que podemos formular la lógica clásica el uso de un Peircian regla de inferencia (equivalente a la usual de la teoría en la presencia de ex falso quodlibet) en el que claramente se modifica el inferencial propiedades de la implicación:

${{{A \rightarrow B} \atop \vdots} \atop A } \over A$

pero de un modo extraño: es una introducción de la regla? Pero no hay ninguna estructura lógica en la conclusión. Es una eliminación de la regla? Pero la implicación por encima de la regla aparece entre los supuestos para la subderivation, no la conclusión. Parece ser algo así como una implicación de la eliminación la eliminación de la regla, una especie de estructura de doble negativo de la introducción de la regla, donde usted puede introducir la estructura lógica mediante la descarga en los supuestos.

Todas las reglas para sumar clásica-la fuerza de la inferencia a la habitual, bien educado intuitionistic deducción natural involucrar a las reglas de inferencia que son excéntricas, de alguna manera u otra. Parigot lambda-mu cálculo muestra cómo el estructural fundamental a la cola de la (a través de un clásico de Curry-Howard correspondencia) deducción natural puede ser modificado para hacerlo un buen ajuste para la lógica clásica como el secuente cálculo.

En el capítulo 3 de mi DPhil tesis doctoral (Stewart, 2000), doy lo que yo creo que es un éxito de la reconstrucción de Prawitz del principio de la inversión para el lambda-mu-base de deducción natural, y mostrar cómo esto proporciona la base para algo que podríamos llamar "clásico constructivismo", donde el principio del medio excluido admitido como tener constructivo contenido por ser un principio que proporciona una constructivo, dialéctica de la mediación entre las pruebas y refutaciones.

Ref. Stewart (2000) En las fórmulas-como-tipos de correspondencia para la lógica clásica.

Answer 3

Apolo es correcta. Un poco más técnico manera de decirlo es que la "descarga" es una aplicación de un teorema de metalogic llamado el teorema de la deducción:

T,P|-Q iff T|-P->Q

El único torniquete del símbolo "|-" representa el sintáctica consecuencias de la relación. El teorema de la deducción básicamente dice "Q es derivable de T y P iff si P entonces Q es derivable de T solos". T puede, por supuesto, ser una clase vacía de declaraciones, en cuyo caso P->Q es tautologous.

Muchos de los sistemas de deducción natural introducir condicional de la prueba como regla primitiva, pero hay sistemas más simples que son igual de poderosos, en el que la deducción del teorema se prueba y la prueba condicional es un derivado de la regla apoyada por el teorema de la deducción. El teorema de la deducción es importante porque muestra que no necesita condicional de la prueba como regla primitiva, y esto hace que la prueba de otros teoremas en metalogic un todo mucho más sencillo. Básicamente, si usted tiene tan pocas reglas como sea posible, esto le da menos casos de verificación. Para fines prácticos, sin embargo, es mucho más fácil de enseñar y utilizar un sistema que presenta un montón y un montón de primitivas reglas en oposición a uno que utiliza como pocas reglas como sea posible.

Los matemáticos utilizan condicional a prueba todo el tiempo, por el camino. Por ejemplo, en una prueba de Q de los casos se obtienen los condicionales P1->P, P2->Q, etc. para cada caso, suponiendo que los antecedentes, derivados de Q a partir de la suposición, a continuación, "descarga" de la suposición. A continuación, se muestran en la separación de los antecedentes es exhaustiva.

Answer 4

Tenga en cuenta que el estándar de los sistemas de deducción natural también tiene una premisa introducido y luego dados de alta en la negación-introducción de la regla.

Para sistemas en los que explícitamente pista sub-pruebas dentro de la gran prueba, una "descarga" paso es sólo el final de un subproof, donde se llega a una conclusión que ya no depende de la suposición adicional utilizado en el inicio de la subproof.