Axiomatic derivation - what does instancing an axiom practically entail? I'm stunned by the chapter in my coursebook (which is in Dutch, so please advice if I am mistranslating any of the terms) about deriving from a system of axioms and derivation rules. The exercise is to prove the following:
$$p \vdash_S q \rightarrow p$$
Step one is to assume p. That makes sense to me: if p is true then p is true.
$$ p \vdash_S p $$
Step two is to make an instance of the axiom $\varphi \rightarrow (\psi  \rightarrow \varphi)$; replacing $\varphi$ with p and  $\psi$ with q. That yields:
$$\vdash_S p \rightarrow (q \rightarrow p)$$
Final step is modus ponens which I also logically understand so I won't repeat it here. My befuddlement is with step two, with instancing an axiom. What does that mean in practical terms?
I recognise that $\varphi \rightarrow (\psi  \rightarrow \varphi)$ is a tautology, it is technically true for every two propositions regardless of whether they are related. But by instancing the axiom I am introducing a relation between p and q out of thin air; in fact q did not exist in my original assumptions.
By taking "I see a bird in the sky" for p, and "Tom Hanks releases a new movie" for q, by doing this I can "prove" that Tom Hanks has some relation to birds. While the technical definition of $\rightarrow$ allows for the right term to be true when the left isn't, so there could still be birds without Tom Hanks, there's still a relation in the opposite direction: when Hanks releases a movie, birds have to appear. So I feel that instancing an axiom is just making stuff up.
What am I missing here?
 A: 
That makes sense to me: if $p$ is true then $p$ is true.


I recognise that $\phi\to(\psi\to\phi)$ is a tautology, it is technically true for every two propositions regardless of whether they are related.

These two remarks suggest to me that you are approaching logic from a biased perspective: it seems that a proof needs to make sense to you intuitively in order to be a proof.
In a certain sense, this is of course desirable, since we use proofs to make conclusions that ultimately make sense to other people (or at least to other mathematicians). But formal logic is actually far more than that. It studies the parts of "making sense" by removing all baggage that is introduced by our intuition, and reducing arguments to nothing but the utmost essential.
So, let's get rid of our intuition first, and then reintroduce it later.

A logical proof can be seen as a recipe of sorts. You start with basic ingredients, which are axioms and inference rules, and then you cook up a proof by instantiating axioms (i.e. producing a sentence with the same structure as the axiom, although the variables may be replaced) and applying inference rules. And that's all. There is nothing telling us that the axioms or the inference rules should make sense, or that they should satisfy certain requirements motivated by our intuition. In a certain sense, a proof is therefore nothing more than the manipulation of symbols, and these symbols can be lacking of any "meaning" as far as the proof is concerned.
Let's take a look at your proof.
Step one is to assume $p$, because our goal is to derive $p\vdash q\to p$, therefore $p$ can be taken as an assumption, since it's one of the expressions before the $\vdash$ symbol.
Step two is to make an instantiation of the axiom $\phi\to(\psi\to\phi)$, not because this axiom makes sense, but because it's an axiom, and the rules dictate that we may always instantiate axioms. Instantiating axioms means that we can replace its variables with anything we like, thus we can replace $\phi$ with $p$ and $\psi$ with $q$. We have therefore derived that $\vdash p\to (q\to p)$.
Finally, since we have derived both $\vdash p$ and $\vdash p\to(q\to p)$ the modus ponens inference rule tells us that we are allowed to derive $\vdash q\to p$.
Since we did things exactly by following the rules (taking assumptions, instantiating axioms, using inference rules), we have made a valid proof.

Now, to get our intuition back into the picture, the axioms and rules of propositional calculus are chosen to make intuitive sense as well. We can see $p\to q$ as symbolising the meaning of "$p$ must be true, or $q$ must be false". This is the semantics of the expression $p\to q$, and indeed, the semantics of the axioms and rules of propositional calculus make intuitive sense for many people.
Note that this also answers your second question: there does not have to be a (causal) relation between $p$ and $q$ under these semantics of $p\to q$. Your intuition should be that this stands for either $p$ is true, or $q$ is false.
You can totally create a logic where $p\to q$ has different semantics, such as one where $p\to q$ can only be valid if $p$ and $q$ are related to each other. An example of such a (collection of) logic(s) is relevance logic. But that is a different system than the classical propositional logic that you're studying. It has different axioms, different inference rules, and different semantics.

As an example to challenge your intuition, I could define a logic with the axioms:

*

*$\psi \sim \bigcirc \psi$

*$\bigcirc \psi \sim \triangle \psi$
and the inference rule:

*

*$\phi,\phi\sim \psi\vdash \psi$
Then you could prove that $p\vdash \triangle p$. Does it make any intuitive sense? No, because we have no idea what these symbols mean. But can you create a valid proof? Absolutely:
We assume $p$, then by the first axiom we can derive $p\sim \bigcirc p$, so by the inference rule $p,p\sim\bigcirc p\vdash \bigcirc p$. Now by the second axiom we can derive $\bigcirc p\sim \triangle p$, so since we have derived $\bigcirc p$ and $\bigcirc p\sim \triangle p$ we can use the inference rule to derive $\triangle p$. Therefore $p\vdash \triangle p$.
A: 
there's still a relation in the opposite direction: when Hanks releases a movie, birds have to appear

No, this is not correct. You have:
$q$ = Tom Hanks releases a new movie
$p$ = I see a bird the sky
The axiom you are instancing is: $p \rightarrow (q \rightarrow p)$.
This does not say, "when Hanks releases a movie, birds have to appear". That would be $q \rightarrow p$.
Instead you have $p \rightarrow (q \rightarrow p)$, which is "If there is [already] a bird in the sky, then if Tom Hanks releases a movie, then there is a bird in the sky." Of course, this is true.
