I would like to prove by induction $p_k\wedge q_k$ but unfortunately I cannot directly apply the induction principle.
However, I can consider two proofs by induction (one inside the other) and this is the setup:
$\triangleright$ q-Base Case
$\quad q_0$ is true $\checkmark$
$\triangleright$ q-Inductive Step(s)
$\quad$Assume $q_{k}$ true for $k$ check for $k+1$
$\hspace{70pt}$$\triangleright$ p-Base Case
$\hspace{70pt}$$\quad p_0$ is true $\checkmark$
$\hspace{70pt}$$\triangleright$ p-Inductive Step(s)
$\hspace{70pt}\quad$Assume $p_{k}$ true for $k$ check for $k+1$
$\hspace{70pt}\quad$I can prove that $q_k\wedge p_k\implies p_{k+1} \checkmark$
$\hspace{70pt}\quad$so far so good, now
$\hspace{70pt}\quad$the question is here:
$\hspace{70pt}\quad$having just proved $p_{k+1}$ allows me to say $\forall n\ p_n$???
$\hspace{70pt}\quad$Allows me to say the usual right hand side of the induction principle???
$\quad$ (because if so I can prove that $p_{k+2}\implies q_{k+1}$ and I could close the outer induction)
Explanation:
my problem is that the only proofs that I find interconnect/link $q$ and $p$ and I cannot separate them into two distinct inductions, therefore, although disturbed by serious doubts from what I just wrote, I hope that someone can rigorously justify it otherwise I'm stuck. On the contrary, if it is patently wrong, well ... at least I won't waste any more time in this direction.
My thoughts
My infinitesimal silver lining think me that after "$q_k\wedge p_k\implies p_{k+1}$" what I get is $q_n \wedge (\forall n\ p_n)$ i.e. $p_n$ is true but with the constraint of $q_n$... Does this make sense? If so it would still be fine because $q_k$ it is assumed to be true in its inductive step.
My infinite negative side/downside (I don't know how to say in English: the opposite of "silver lining") tell me that I'm stuck until the end of the next ice age, period.
Thanks in advance