Deducción natural, Prueba $\vdash$ $P\Rightarrow(Q\Rightarrow P)$

Question

Así que tengo una pregunta con respecto a la deducción natural, ¿estamos permitido "copiar" nuestra suposición anterior dentro de una nueva suposición. Utilizaré un ejemplo para ilustrarlo.

$\vdash$ $P\Rightarrow(Q\Rightarrow P)$

Así que aquí están mis pasos.

1.) $P$ Supuesto

2.) $Q$ Supuesto

3.) $P$ Copia (1)

4.) $Q \Rightarrow P$ Implicación Introducción

5.) $P \Rightarrow (Q \Rightarrow P)$ Implicación Introducción

¿Es correcta mi prueba o falta algo?

Answer 1

Para que quede claro por qué su solución es correcta, aquí está en estilo Fitch: $\def\imp{\Rightarrow}$

Solución

Si $P$ : [(1)]

  Si $Q$ :

    $P$ . [(2); copia de (1)]

  $Q \imp P$ . [(3); introducción de la implicación a partir de (2)]

$P \imp ( Q \imp P )$ . [introducción de la implicación a partir de (3)]

Notas

Intuitivamente es obviamente correcto porque cualquier cosa que se pueda afirmar en el exterior de cualquier supuesto es sigue siendo cierto por dentro la suposición. Eso le permite copiar el supuesto exterior bajo el supuesto interior como usted lo hizo. El resto es sólo la introducción de la implicación como lo hizo, que no es más que el colapso de la estructura de la suposición en una sola línea.

Answer 2

Sí, su prueba es correcta (modulo $P$ se añade utilizando una regla diferente a la de $Q$ ).

En la deducción natural tienes normas estructurales llamados contracción, debilitamiento e intercambio. $$ \frac{S,P,P,T \vdash Q}{S,P,T \vdash Q}\ \text{contraction} \quad \frac{S,T \vdash Q}{S, P, T \vdash Q}\ \text{weakening} \quad \frac{S,P,Q,T \vdash R}{S,Q,P,T \vdash R}\ \text{exchange} $$

Normalmente, estas reglas se utilizan de forma silenciosa diciendo que la colección de supuestos forma un conjunto. Se puede imaginar que no tenerlas como reglas estructurales lleva a lógica subestructural El más notable de ellos es lógica lineal que deja caer la contracción y el debilitamiento.

Ahora podemos describir su prueba (con la pequeña corrección): $P$ se introduce a través de $P \vdash P$ entonces $Q$ se añade a los supuestos mediante el debilitamiento ( $P,Q \vdash P$ ), entonces se utiliza la contracción para duplicar $P$ ( $P,P,Q \vdash P$ ) y el intercambio para llevarlo al frente del contexto ( $P,Q,P\vdash P$ ), entonces dos usos de la introducción de la implicación.