Deducción natural de (p -> (p-> q)) -> q sobre la hipótesis de que p

Question

Estoy luchando con la deducción natural. Estoy haciendo los ejercicios de Fitch del libro y ahora se supone que debo dar un intelim prueba del teorema anterior (un intelim prueba es uno que utiliza solamente la introducción y eliminación de reglas y ciertos axiomas).

Entiendo que será por implicación introducción que puedo demostrar esto. Pero me resulta difícil, porque yo enredarse en el subproofs. Es este intento por debajo de la correcta?

1. p hipótesis
   2. p->(p->q) hipótesis de subproof
   3. p->q por 1,2, modus ponens
   4. p reiteración de 1
   5. q
2. (p->(p->q)->q por 2-5 implicación introducción

Ayuda muy apreciada!

Answer 1

$\newcommand\lthen{\Rightarrow}$ \begin{align} p&\vdash p&&\text{by assumption}\\ p\lthen(p\lthen q)&\vdash p\lthen(p\lthen q)&&\text{by assumption}\\ p,p\lthen(p\lthen q)&\vdash p\lthen q&&\text{by %#%#%-elimination}\\ p,p\lthen(p\lthen q)&\vdash q&&\text{by %#%#%-elimination}\\ p&\vdash(p\lthen(p\lthen q))\lthen q&&\text{by %#%#%-introduction}\\ \end {align}

Answer 2

Sí, eso está bien. Con un menor de edad tenga en cuenta que si usted puede utilizar modus ponens en la línea 3 sin reiterando la premisa, no es necesario reiterar la premisa de hacerlo en el segundo tiempo. (Bueno, no es malo hacerlo, simplemente innecesario.) $$\def\fitch#1#2{\hspace{2ex}\begin{array}{|l} #1\\\hline #2\end{array}} {\fitch{1.~p\hspace{18ex}\textsf{Premisa (Hipótesis de la prueba)}}{\fitch{2.~p\(p\q)\hspace{4ex}\textsf{Suposición (Hipótesis de la condicional subproof)}}{3.~p\q\hspace{10.5 ex}\textsf{Eliminación Condicional 1, 2 (también conocido como modus ponens)}\\4.~q\hspace{15.5 ex}\textsf{Eliminación Condicional 1, 3}}\\5.~(p\(p\q))\q\hspace{1ex}\textsf{Introducción Condicional 2-4 (aka deducción)}}\\\blacksquare\quad p\vdash (p\(p\q))\q}$$