How to use natural deduction for introducing implication

Question

I am doing some propositional logic and we learned about the natural deduction rule. Everything was going fine until the rule of introducing implication arose. I am slightly confused as to how it works. This is the basically how it was worked out. The thing that is confusing me is that the turnstile was introduced for line 2. How and why is that introduced?

p ⇒ (q ∧ r ) |- p ⇒ q
1      p ⇒ (q ∧ r ) ass 0
2      p |- q
2.1    p ass 2
2.2    q ∧ r ⇒-E 1, 2.1
2.3    q ∧-E 2.2
3      p ⇒ q ⇒-I 2

I just do not seem to understand it. Would someone be able to explain to me of how this all works?

Answer 1

The notation is a little bit "weird", but the meaning of:

2) $p \vdash q$

is to states that what follows: 2.1)-2.3), is a sub-proof aimed at deriving $q$ under the assumption $p$.

Thus, having derived $q$ (in 2.3) under assumption $p$ (in 2.1), we can apply the $\to$-intro rule to derive :

3) $p \to q$

"discharging" the assumption $p$.

---

You can see: Ian Chiswell & Wilfrid Hodges, Mathematical Logic (2007), page 16-17, for the formal rule and its explanation.