How are formulas inserted into Hilbert style axiom proof? Given: $\vdash p\to p$
Axioms and proof:
$\begin{array}{l|l}\text{Ax 1.}&(\varphi\to(\psi\to\varphi))\\\text{Ax 2.}& (\varphi\to(\psi\to\theta))\to((\varphi\to\psi)\to(\varphi\to\theta))\\\text{Ax 3.}&((\lnot\varphi\to\lnot\psi)\to(\psi\to\varphi))\end{array}$
Proof:
$\begin{array}{r|ll}1.&(p\to((p\to p)\to p))&\text{Ax 1}\\
2.&((p\to ((p\to p)\to p))\color{red})\to \color{red}((p\to (p\to p))\to (p\to p)\color{red})&\text{Ax 2}\\
3.&(p\to (p\to p))\to (p\to p)&\text{MP 1,2}\\
4.&p\to(p\to p)&\text{Ax 1}\\
5.&p\to p&\text{MP 3,4}\end{array}$
I understand that it works but I don't understand why the conclusion (p→p) is placed into ψ. I understand that the axioms are definitionally logically equivalent so I can place any formula in Γ⊢φ into these axioms but I don't understand why it's placed in ψ necessarily. I also wonder if I should solve for φ first and why I'm taking p as an assumption when I'm solving for it.
 A: $\def\to{{\rightarrow}}$Work backwards.
Your target is to derive $p\to p$ and our only rule of inference is modus ponens (MP).  We will need to derive something that ends with $?\to (p\to p)$ from the axioms.
Looking at the axioms, we can discount axiom 3 (no negations). So we might use either:
$$\begin{array}{l|l}\text{Ax 1.}&(\varphi\to(\psi\to\varphi))&p\to(p\to p)\\\text{Ax 2.}& (\varphi\to(\psi\to\theta))\to((\varphi\to\psi)\to(\varphi\to\theta))& (p\to(\psi\to p))\to((p\to\psi)\to(p\to p))\end{array}$$
Okay, axiom one is of no immediate help, since cannot derive $p$.
So is there some substitution for $\psi$ in axiom two that might help?
Now, if we substituted $p$ for $\psi$ in axiom 2 we would then be able to use MP to derive $(p\to p)\to(p\to p)$ which is of no help at all.  We would have to derive $p\to p$ so we could use MP to derive $p\to p$, and round and round we go.
So, what else might we substitute?  Well, to make use of $p\to(p\to p)$ we could substitute $p\to p$. That gives us $(p\to((p\to p)\to p))\to(p\to (p\to p))\to(p\to p))$ which would be useable if we could derive $p\to((p\to p)\to p)$.
Oh, look, that's also obtainable from axiom 1.  That gives us the following to work with.
$$\begin{array}{l|l}\text{Ax 1.}&(\varphi\to(\psi\to\varphi))&p\to(\color{blue}{(p\to p)}\to p)\\\text{Ax 1.}&(\varphi\to(\psi\to\varphi))&p\to(p\to p)\\\text{Ax 2.}& (\varphi\to(\psi\to\theta))\to((\varphi\to\psi)\to(\varphi\to\theta))& (p\to(\color{green}{(p\to p)}\to p))\to((p\to\color{green}{(p\to p)})\to(p\to p))\end{array}$$
So we build the proof by adding modus ponens:-$$\begin{array}{r|ll}1.&(p\to((p\to p)\to p))\to((p\to(p\to p))\to(p\to p))&\text{Ax 2}\\2. &~p\to((p\to p)\to p)&\text{Ax 1}\\3.&(p\to(p\to p))\to(p\to p)&\text{MP 1,2}\\4.& ~p\to(p\to p) &\text{Ax 1}\\5.&p\to p &\text{MP 3,4} \end{array}$$
A: (p→p) gets put into the position of ψ, because it works for the proof, and possibly because wants to show that only one variable is necessary for this problem.  I think there exists a meta-theorem which says that using this axiom set, however many variable symbols exist in the conclusion (with the first 'p' and the second 'p' in (p$\rightarrow$(q$\rightarrow$p)) as the same variable), that many variables will suffice for proving the theorem.  Or in other words, if exactly x variables are in the conclusion C, then x variables will suffice to prove C.  Thus, the author might have chosen (p$\rightarrow$p) to suggest that meta-theorem.  I don't believe that meta-theorem holds for all axiom sets though, since I doubt it holds for the axiom set, in Polish notation, {CCpqCCqrCpr, CpCNpq, CCNppp}.
That said, the above is not the only possible proof, and in some other proofs (p→p) wouldn't get into the position of ψ.  (q→p) can work instead in some proof, given that Ax1 got instantiated differently in step 4 (and steps 2 and 3 also become slightly different).
You can put any formula into the variable positions of the axioms, because they always hold true, and thus no matter the value of the formula you put in place of a variable (provided each instance of a variable gets replaced by that same formula), you'll end up with a formula which is also true.  In other words, you can perform substitution, or instantiation, whichever way you think of it, because it's truth-preserving.
Solving for a variable doesn't happen in the study of propositional calculi, at least not in the same sense as solving for a letter gets done in the study of algebra.
When (p$\rightarrow$p) gets placed into the position of ψ, it's not getting asserted as true.  Nowhere in the above does 'p' get taken as an assumption.
A: $p \to p$ is the easiest one that works, but you could have used many other ones here ... anything of the form $\chi \to p$ would have worked, since the proof schema would look like this
$\begin{array}{r|ll}1.&p\to((\chi \to p)\to p)&\text{Ax 1}\\
2.&(p\to ((\chi \to p)\to p))\to ((p\to (\chi \to p))\to (p\to p))&\text{Ax 2}\\
3.&(p\to (\chi \to p))\to (p\to p)&\text{MP 1,2}\\
4.&p\to(\chi \to p)&\text{Ax 1}\\
5.&p\to p&\text{MP 3,4}\end{array}$
For a concrete proof, we could, for example, pick $\chi = q$:
$\begin{array}{r|ll}1.&p\to((q \to p)\to p)&\text{Ax 1}\\
2.&(p\to ((q \to p)\to p))\to ((p\to (q \to p))\to (p\to p))&\text{Ax 2}\\
3.&(p\to (q \to p))\to (p\to p)&\text{MP 1,2}\\
4.&p\to(q \to p)&\text{Ax 1}\\
5.&p\to p&\text{MP 3,4}\end{array}$
Or, we could have picked $\chi = (p \to p) \to p$:
$\begin{array}{r|ll}1.&p\to((((p \to p) \to p) \to p)\to p)&\text{Ax 1}\\
2.&(p\to ((((p \to p) \to p) \to p)\to p))\to ((p\to (((p \to p) \to p) \to p))\to (p\to p))&\text{Ax 2}\\
3.&(p\to (((p \to p) \to p) \to p))\to (p\to p)&\text{MP 1,2}\\
4.&p\to(((p \to p) \to p) \to p)&\text{Ax 1}\\
5.&p\to p&\text{MP 3,4}\end{array}$
A: (This should be a comment to Doug's post, but since I am new to the site I will post it as an answer)
The meta-theorem that Doug mentions is indeed true, and does not depend on the axiomatization: To prove the formula $p\rightarrow p$, you need to consider only axioms in the variable $p$. For assume you had a proof of $p\rightarrow p$ which uses the variable $q$ somewhere. Then you could simply replace $q$ everywhere in the proof by $p$, and the result would still be a valid proof of $p\rightarrow p$.
