Something that I sometimes find useful is to consider what's called the Curry-Howard Isomorphism: statements of logic correspond to the types of computer programs, and the statements are theorems if and only if the corresponding type is the type of a program that can actually exist.
In this correspondence, $A\to B$ represents the type of a function in a program that takes an argument of type $A$ and calculates a value of type $B$.
A function of type $A\to A$ is obviously possible, because the function just takes the $A$ that it got and gives it right back:
define function f(a) {
return a;
}
And $A\to(B\to A)$ is also possible: the function needs to take an argument of type $A$ and then give back a function of type $B\to A$. It can do this, because it can give back a second function that ignores the $B$ that it got, and that gives back the $A$ that the first function got to begin with:
define function f(a) {
define function g(b) {
return a;
}
return g;
}
But in contrast, $A\to B$ is not a theorem, because how can you write a function that gets an argument of type $A$ and gives back a result of some other, completely arbitrary type? Where could it get a $B$ from if all it has is an $A$?
The isomorphism also identifies logical AND with pairing: a value of type $A\land B$ is a pair that contains both an $A$ and a $B$, and either (or both) can be extracted. It identifies logical OR with what's called a disjoint union: A value of type $A\lor B$ is either an $A$ or a $B$, but not both, and the program can tell which of the two it is. Similarly there are interpretations for negation, for constant true and false values, and so forth.
For a more elaborate example, a program that corresponds to the theorem $\lnot\lnot(P\lor\lnot P)$,
see this answer.
The only catch is that not every classically true theorem corresponds to a program in a completely straightforward way. Some theorems of logic, such as $((A\to B)\to A)\to A$, (Peirce's law) don't correspond to a simple program. Instead they correspond to programs that use advanced features like continuations or exceptions.
Still it's often helpful to think of logical theorems as specifications for programs; if you can think of a program which performs the corresponding calculation, then the statement must be a theorem.
Viewed in this way, the statement you originally asked about, $((P\to Q)\to Q)\to Q$, seems quite unlikely: you need a function $f$ which gets an argument $x$, which is itself a function of type $(P\to Q)\to Q$, and $f$ needs to produce a value of type $Q$. If $f$ could call $x$, then $x$ would return the needed value. But it can't call $x$ because to do so it needs to give it an argument of type $P\to Q$, and it doesn't have one.
In Natural Deduction we can prove the "usual" relationships between quantifiers starting from the basic rules.
E.g.
1) $\forall x Px$ --- premise
2) $\exists x \lnot Px$ --- assumed [a]
3) $\lnot Py$ --- assumed [b] from 4) for $\exists$-elim
4) $Py$ --- from 1) by $\forall$-elim (Universal Instantiation)
5) $\bot$ --- contradiction: from 3) and 4)
6) $\bot$ --- from 2), 3) and 4) by $\exists$-elim, discharging [b]
7) $\lnot \exists x \lnot Px$ --- from 2) and 6) by $\to$-intro, dicharging [a]
8) $\forall x Px \vdash \lnot \exists x \lnot Px$ --- from 1) and 7).
1) $\lnot \exists x \lnot Px$ --- premise
2) $\lnot Py$ --- assumed [a]
3) $\exists x \lnot Px$ --- from 2) by $\exists$-intro
4) $\bot$ --- contradicition: from 1) and 3)
5) $\lnot \lnot Py$ --- from 2) and 4) by $\to$-intro, discharging [a]
6) $Py$ --- from 5) by Double Negation (it holds only classically)
7) $\forall x Px$ --- from 6) by $\forall$-intro
8) $\lnot \exists x \lnot Px \vdash \forall x Px$ --- from 1) and 7).
As you can see, some of the "usual" equivalences (see also; $¬∀x¬ Px \to ∃xPx$) hold only in classical logic, because their proof needs Double Negation; see Intuitionistic Logic.
For more details, see e.g.:
For a different approach you can see:
Best Answer
Let $S$ be a set of (logical) formulae and $\psi$ be a formula. Then $S \vdash \psi$ means that $\psi$ can be derived from the formulae in $S$. Intuitively, $S$ is a list of assumptions, and $S \vdash \psi$ if we can prove $\psi$ from the assumptions in $S$.
$\vdash \psi$ is shorthand for $\varnothing \vdash \psi$. That is, $\psi$ can be derived with no assumptions, so that in some sense, $\psi$ is 'true').
More precisely, systems of logic consist of certain axioms and rules of inference (one such rule being "from $\phi$ and $\phi \to \psi$ we can infer $\psi$"). What it means for $\psi$ to be 'derivable' from a set $S$ of formulae is that in a finite number of steps you can work with (i) the formulae in $S$, (ii) the axioms of your logical system, and (iii) the rules of inference, and end up with $\psi$.
In particular, if $\vdash \psi$ then $\psi$ can be derived solely from the axioms by using the rules of inference in your logical system.