A set of propositions $S$ is independent if $\forall t \in S$ we have $S-\{t\}\nvdash t$.
The syntactic axioms defined in our logic course are:
1) $\forall p,q \in L : p\Rightarrow (q \Rightarrow p)$
2) $\forall p,q,r \in L : (p\Rightarrow (q \Rightarrow r))\Rightarrow ( (p\Rightarrow q) \Rightarrow (p \Rightarrow r) )$
3) $ \forall p \in L : \neg \neg p \Rightarrow p$
The task is to prove their independence.
If it is too long to prove all three you can give me some hints on how to prove that $ \{1,2\} \nvdash {3}$.
I am new to the concept 'It can't be proved from p and q'; most of the standard results we deduced (completeness, compactness, decidability theorem) use the fact that all three axioms hold.
Edit: I just realised that the use of $\vdash$ is quite controversial in this case. $S \vdash t$ if you can prove t from S and modus ponens.
First an aside, which does have some importance. $\lnot$p in your system abbreviates (p⇒$\bot$). So, ($\lnot$$\lnot$p⇒p) abbreviates 3)' (((p⇒$\bot$)⇒$\bot$)⇒p). This matters, because although, even if all strings get fully parenthesized, {1), 2), 3)'} allows us to deduce all tautologies having ⇒ and $\bot$, but
{1), 2), 3)} does not allow us to deduce all tautologies having ⇒ and $\lnot$.
For example, without the abbreviation, (p⇒($\lnot$p⇒q)) is independent of {1), 2), 3)} (once each one gets parenthesized).
It sometimes works out to set up a model, such as an algebra, for the set of axioms {S$_1$, ..., S$_n$} such that the model satisfies every member of {S$_2$, ..., S$_n$}, but does not satisfy S$_1$.
For your example, let's consider an algebra where ⇒ computes as follows:
($\bot$⇒$\bot$) = $\bot$
($\bot$⇒$\top$) = $\top$
($\top$⇒$\bot$) = $\bot$
($\top$⇒$\top$) = $\bot$
You can check to see that 1) and 2) will always compute to $\bot$. But, suppose that p has truth value of $\top$. Then, (((p⇒$\bot$)⇒$\bot$)⇒p) equals (($\bot$⇒$\bot$)⇒$\top$) which equals ($\bot$⇒$\top$) which equals $\top$. Thus, in such an algebra 1) and 2) will always have truth value of $\bot$, but 3)' will not. So, if the axioms were dependent, a deduction wouldn't necessarily preserve the truth value of the axioms even when only substitution and detachment got used as rules of inference. Since the rules of inference still preserve truth values, there is no way to start with {1), 2)} and deduce 3)'.
I didn't come up with this model myself. I basically converted the axioms to a format for a freely available program called Mace4 and it produced the model.
Edit: A different approach:
For the system {1), 2)} the set of most general tautologies derivable are all conditionals without any instance of $\bot$ in them. We can insist that variables always appear in a certain order, since substitution allows us to derive any other tautologies when we do that. Thus, if we suppose that (((p⇒⊥)⇒⊥)⇒p) is derivable from some tautology Q it will have to come as derivable by substitution of variable(s) in Q only where Q has only "p", parentheses, and ⇒ in it. That leaves us with a number of possible candidates for Q:
So, 3)' is not derivable from {1), 2)}.