I have the following:
Objects: $a$
Functions: $f$
Now, the following are the premises:
Premises:
$p(a)$
$AX:(p(X) \implies p(f(X)))$
In other words,
$p(a)$
$\forall X.(p(X) \implies p(f(X)))$
Now, how can I show that $p(f(f(X)))$ holds (the goal statement)? If this is not possible, is there a way to prove $AX:(p(f(X))\implies p(f(f(X))))$? I am also able to use this intermediate conclusion from this subproof for my full proof.
I am trying to solve this as an intermediate step, but since I am new to using induction from a logic perspective (and using second order logic), I am not sure how to proceed. This is an intermediate step in a tree induction proof, and all things such as propositional logic and relational logic steps such as And/Or/Negation/Implication/Biconditional Introduction/Elimination are defined, and Assumptions are given (which can be closed out by Implication Intros), as well as quantifier logic such as Universal/Existential Introduction/Elimination.
For this intermediate step, I'm not sure if I even need to apply any type of induction, as tree induction will not allow linear induction as far as the Fitch system proof I am using goes (due to there not being a successor in a linear sense).