Adjuntar una premisa en una lógica de primer orden de deducción natural intuicionista

Question

Supongamos que tenemos una prueba para el secuente $P\vdash A$ cómo derivar una prueba para el secuente $P,B\vdash A$ ?

Obtengo una prueba de este tipo con reglas de introducción y eliminación de conjunciones. De $P\vdash A$ y $B\vdash B$ obtenemos $P,B\vdash A\wedge B$ introduciendo la conjunción, por lo que derivamos $P,B\vdash A$ eliminando la conjunción.

¿Esta es la forma correcta?

Answer 1

Diferentes formalizaciones de la deducción natural manejan esto de diferentes maneras. Las dos opciones principales son:

1. Tener explícito "estructural" reglas de inferencia como el debilitando regla $$ \frac{P, Q \vdash B}{P, A, Q \vdash B} $$

2. Incorporar las reglas estructurales en el axioma de la "suposición" de manera que se lea $$ \frac{}{P, A, Q \vdash A} $$ que permite llevar las suposiciones no utilizadas hasta las hojas del árbol de pruebas e ignorarlas allí.

Tu descripción "lógica intuicionista de deducción natural de primer orden" no es lo suficientemente precisa como para decir cuál de las soluciones ha sido elegida por el autor de la formalización con la que estás trabajando, pero si tu regla de intrucción de conjunción es $$ \frac{P\vdash A \qquad Q\vdash B}{P,Q \vdash A\land B} \quad\text{rather than}\quad \frac{P\vdash A \qquad P\vdash B}{P \vdash A\land B} $$ entonces parece probable que esté utilizando reglas estructurales, por lo que debe buscar algo como la regla de debilitamiento anterior en su material de origen.