Deduction of a tautology I am wondering what it means to "find a deduction for a tautology, say $((\neg(\neg A_0))\rightarrow A_0).$
I'm not really sure what a deduction is. Is it a sequence of formulas that satisfy the axioms for a proof?
$\Gamma$ proof axioms
(Group I axioms)
(1) $((ϕ_1 → (ϕ_2 → ϕ_3)) → ((ϕ_1 → ϕ_2) → (ϕ_1 → ϕ_3)))$
(2) $(ϕ_1 → ϕ_1)$
(3) $(ϕ_1 → (ϕ_2 → ϕ_1))$
(Group II axioms)
(1) $(ϕ_1 → ((¬ϕ_1) → ϕ_2))$
(Group III axioms)
(1) $(((¬ϕ_1) → ϕ_1) → ϕ_1)$
(Group IV axioms)
(1) $((¬ϕ_1) → (ϕ_1 → ϕ_2))$
(2) $(ϕ_1 → ((¬ϕ_2) → (¬(ϕ_1 → ϕ_2))))$ 
Definition of proof:
Suppose that
$s = \langleϕ_1, . . . , ϕ_n\rangle$
is a finite sequence of propositional formulas. The finite sequence s is a
Γ-proof if for each i ≤ n at least one of
$a) ϕ_i ∈ Γ;$ or
$b) ϕ_i$
is a logical axiom; or
c) there exist $j_1 < i$ and $j_2 < i$ such that
$ϕ_{j_2} = (ϕ_{j_1} → ϕ_i)$.
where $\Gamma\subseteq \mathcal{L_0}$
Definition of $\mathcal{L}_0$
$\mathcal{L}_0$ is the set of all formulas of the form
a)$A_n$, $n\in \mathbb{N}$ where $A_n$ is a propositional symbol.
b)$\phi\rightarrow \theta $,  where $\phi,\theta\in \mathcal{L}_0$
c)$\neg\phi,$ where $\phi \in \mathcal{L}_0$.
 A: Whenever one mentions deductions, one has a proof system in mind. In your case, it is probably what is known as a Hilbert-style proof system. A Hilbert-style proof system consists of a set of axioms and rules (actually axioms are a special case of rules, ones without any premises). A deduction is a set of statements (propositions) called lines, where each one is either an axiom or follows by a rule from previous lines.
Each axiom or rule is more properly a scheme of axioms or rules, a concept best explained by an example. A common axiom is $\varphi \to \varphi$. This means that for every formula $\varphi$, $\varphi \to \varphi$ is an axiom. For example, $p \to q$ is a formula, so $(p \to q) \to (p \to q)$ is an instance of the axiom scheme $\varphi \to \varphi$. An example of a derivation rule is Modus Ponens: Given $\varphi$ and $\varphi \to \psi$, deduce $\psi$.
A deduction of a tautology like $\lnot\lnot A \to A$ is a concept that depends on the proof system. Given a proof system, it is a sequence of lines, each either an axiom or follows by a rule from previous lines, where the last line is the required tautology. Since you haven't specified a proof system, I can't help you any further.
A: The proof is quite easy with the Deduction Theorem.
The theorem can be proved [see Elliott Mendelson, Introduction to mathematical logic (4ed - 1997), page 37] with axioms Group I (Axiom (2) is provable from (1) and (3)).

Lemma : $\varphi \rightarrow (\psi \rightarrow \sigma) \vdash \psi \rightarrow (\varphi \rightarrow \sigma)$

Proof
i) $\varphi \rightarrow (\psi \rightarrow \sigma)$ --- assumed
ii) $\varphi$ --- assumed
iii) $\psi$ --- Assumed
iv) $\psi \rightarrow \sigma$ --- from i) and ii) by modus ponens
v) $\sigma$ --- from iii) and iv) by mp
vi) $\varphi \rightarrow \sigma$ --- from ii) and v) by Deduction Th
vii) $\psi \rightarrow (\varphi \rightarrow \sigma)$ --- from iii) and vi) by Deduction Th.

Now we will prove :

$\vdash \lnot \lnot \varphi \rightarrow \varphi$

Proof
i) $\vdash \lnot \varphi \rightarrow (\lnot \lnot \varphi \rightarrow \varphi)$ --- from Axiom (1) Group II : $ϕ_1→((¬ϕ_1)→ϕ_2)$, with $\lnot \varphi$ in place of $ϕ_1$ and $\varphi$ in place of $ϕ_2$
ii) $\vdash \lnot \lnot \varphi \rightarrow (\lnot \varphi \rightarrow \varphi)$ --- from Lemma above and i)
iii) $\lnot \lnot \varphi \vdash (\lnot \varphi \rightarrow \varphi)$ --- from iii), assuming $\lnot \lnot \varphi$
iv) $\vdash (\lnot \varphi \rightarrow \varphi) \rightarrow \varphi$  --- from Axiom (1) Group III : $((¬ϕ_1)→ϕ_1)→ϕ_1$ with $\varphi$ in place of $ϕ_1$
v) $\lnot \lnot \varphi \vdash \varphi$ --- from iii) and iv) by mp


vi) $\vdash \lnot \lnot \varphi \rightarrow \varphi$ --- from v) by DT.


