Proving ∀k{[P(1)⋀···⋀P(k)] → P(k + 1)} Natural Deduction

Question

This is what I have currently.

$\begin{array}{|l}\forall k [P(k)\rightarrow P(k+1)]\quad premise \\\hline\begin{array}{|l} x_0 \\ P(x_0) \rightarrow P(x_0 + 1) \quad \forall \text{elim 1} \ \\\begin{array}{|l} [P(1)\wedge\dots\wedge P(x_0)] \quad Assumption \\\hline P(x_0) \quad\wedge \text{Elim 4} \\ P(x_0 + 1) \quad \rightarrow \text{Elim 3, 5} \\\end{array} \\ [P(1)\wedge\dots\wedge P(x_0)] \rightarrow P(x_0 +1) \quad \rightarrow \text{Intro 4-6} \\\end{array} \\\forall\{[P(1)\wedge\dots\wedge P(k)] \rightarrow P(k+1)\}\quad\forall \text{ Intro 2-7} \\\end{array}$

How would I get $P(1)\wedge\dots\wedge P(k)$? It doesn't make any sense for me on where these other elements will be coming from.

Would my overarching proof structure be correct?

Answer 1

Note that you need to have $[P(1)\wedge\dots\wedge P(x_0)] \rightarrow P(x_0+1)$ as the second to last line (i.e. the last line of the subproof) ... the $k$ only comes back in once you ad the universal quantifier on the last line.

And, given that you want to prove $[P(1)\wedge\dots\wedge P(x_0)] \rightarrow P(x_0+1)$, the inside subproof should assume $P(1)\wedge\dots\wedge P(x_0)$, so that when you get to $x_0+1$, you can do a conditional proof and get $[P(1)\wedge\dots\wedge P(x_0)] \rightarrow P(x_0+1)$ as desired.

So, it should look like:

$\begin{array}{|l}\forall k [P(k)\rightarrow P(k+1)]\quad premise \\\hline\begin{array}{|l} x_0 \\ P(x_0) \rightarrow P(x_0 + 1) \quad \forall \text{elim 1} \\\begin{array}{|l} P(1)\wedge\dots\wedge P(x_0) \quad Assumption \\P(x_0) \quad \land \ Elim \\ P(x_0 + 1) \quad \rightarrow Elim \\\end{array} \\ [P(1)\wedge\dots\wedge P(x_0)] \rightarrow P(x_0+1) \quad \rightarrow Intro \\\end{array} \\\forall k\{[P(1)\wedge\dots\wedge P(k)] \rightarrow P(k+1)\}\quad\forall Intro \\\end{array}$

OK ... and now I think it will become clear how you get $P(x_0+1)$ ...