¿Qué significa "descargar supuestos o premisas"?

Question

Al construir pruebas utilizando deducción natural ¿qué significa decir que un supuesto o premisa es dado de alta ? ¿En qué circunstancias querría o necesitaría utilizar un mecanismo de este tipo?

La razón por la que hago esta pregunta es que muchos textos sobre lógica utilizan este término tal y como lo entiende el lector y no se toman la molestia de explicar adecuadamente el sentido técnico en el que lo están utilizando.

Answer 1

Apolo es correcto. Una forma un poco más técnica de decirlo es que la "descarga" es una aplicación de un teorema de la metalógica llamado teorema de la deducción:

$$ T,P \vdash Q \quad\text{iff}\quad T\vdash P \rightarrow Q $$

El símbolo del torniquete único " $\vdash$ "representa la relación de consecuencias sintácticas. El teorema de la deducción dice básicamente "Q es derivable de T y P si si P entonces Q es derivable sólo de T". Por supuesto, T puede ser una clase vacía de enunciados, en cuyo caso $P\rightarrow Q$ es tautológico.

Muchos sistemas de deducción natural introducen la prueba condicional como regla primitiva, pero hay sistemas más sencillos que son igual de potentes en los que se demuestra el teorema de la deducción y la prueba condicional es una regla derivada apoyada en el teorema de la deducción. El teorema de la deducción es importante porque muestra que no se necesita la prueba condicional como regla primitiva, y esto hace que la demostración de otros teoremas en metalógica sea mucho más sencilla. Básicamente, si tienes el menor número posible de reglas, tienes menos casos que comprobar. A efectos prácticos, sin embargo, es mucho más fácil enseñar y utilizar un sistema que introduce montones y montones de reglas primitivas que uno que utiliza el menor número posible de reglas.

Por cierto, los matemáticos utilizan pruebas condicionales todo el tiempo. Por ejemplo, en una demostración de Q por casos se obtienen los condicionales P1->Q, P2->Q, etc. suponiendo los antecedentes de cada caso, derivando Q de la suposición y "descargando" la suposición. Entonces se demuestra que la disyunción de los antecedentes es exhaustiva.

Answer 2

Tal y como yo lo entiendo, descargar una premisa o suposición es lo contrario de introducirla: la absorbes (por ejemplo) en el antecedente de una implicación --- esto significa que ya no es una suposición. Un ejemplo trivial:

P 1. Supongamos que P

__

P 2. De 1

__

P->P 3. Descarga 1

Así he concluido que P->P sin ninguna suposición (es decir |- P->P). Si no descargáramos la suposición, tendríamos P|-P

Answer 3

Nótese que los sistemas de deducción natural estándar también tienen una premisa introducida y luego descargada en la regla de negación-introducción.

Para los sistemas que realizan un seguimiento explícito de las subpruebas dentro de la prueba más amplia, un paso de "descarga" es simplemente el final de una subprueba, donde se llega a una conclusión que ya no depende de la suposición adicional utilizada al iniciar la subprueba.