Deduction of a tautology

Question

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$.

Answer 1

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.

Answer 2

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.