Calculas F0 - Deduction Theorem By using the deduction theorem, and other formulas (i.e Transitivity of implication, inconsistency, double negation etc.) we can prove something like below.
$⊢(¬q→¬(q→r))→¬¬q$
By applying deduction theorem, it is sufficient to show
$(¬q→¬(q→r))⊢¬¬q$.
My question is, what is the rule to make assumptions to do the proof?
i.e I found below example from a book
${A→(B→C),B,A} ⊢ C$
steps
${A→(B→C),B,A} ⊢ A$   Assumption
${A→(B→C),B,A} ⊢ A→(B→C)$   Assumption
${A→(B→C),B,A} ⊢ (B→C)$   Assumption
and so on.
I want to know how can I make those assumptions? What is the theory behind it? It would be nice if someone can explain it using this problem 
$⊢(¬q→¬(q→r))→¬¬q$.
 A: \begin{array}{rcll}
\{A→(B→C),B,A\} &⊢& A &\text{Assumption}\\[2ex]
\{A→(B→C),B,A\} &⊢& A→(B→C) &\text{Assumption}\\[1ex]
\{A→(B→C),B,A\} &⊢& (B→C) &\require{cancel}\cancelto{\text{Modus Ponens}}{\text{Assumption}}\\
\end{array}
The "Assumptions" here are really just the rule of identity: $\Sigma\cup\{\phi\}\vdash \phi$. 
The other rule is modus ponens, $\frac{\Gamma\vdash \phi\quad\Delta\vdash \phi\to\psi}{\Gamma\cup\Delta\vdash \psi}$ , or "conditional eliminaton".
$\begin{array}{r:rcll}
1&\{A\} &⊢& A &\text{Assumption}\\[1ex]
2&\{A→(B→C)\} &⊢& A→(B→C) &\text{Assumption}\\[1ex]
3&\{A→(B→C),A\} &⊢& (B→C) &\text{Modus Ponens},1,2  \\[1ex]
4&\{B\} &⊢& B &\text{Assumption}\\[1ex]
5&\{A→(B→C),B,A\} &⊢& C &\text{Modus Ponens}, 3,4\\[1ex]
\end{array}$
A: The assumptions are listed to the left of the $\vdash$ symbol.  That is, statement $$\{A, B, \ldots \} \vdash C$$ means $C$ is provable from the assumptions $A, B, \ldots$.  In particular this is true "by assumption" if $C$ is one of $A, B, \ldots$.
A: Typically, the Assumption rule is that at any point in the proof you can add a line that looks like:
$\{ \varphi \} \vdash \varphi$ Assumption
So your example is a bit weird.  It would make more sense as:


*

*$\{ A \} \vdash A$ Assumption

*$\{ A \rightarrow (B \rightarrow C) \} \vdash A \rightarrow (B \rightarrow C)$ Assumption

*$\{ A, A \rightarrow (B \rightarrow C) \} \vdash B \rightarrow C$ MP 1,2
etc.
