Matematické Fórum

Ahoj, potrebuju poradit. Moje axiomatická schémata jsou (podle Kleeneho):

1a [mathjax]A \rightarrow (B \rightarrow A)[/mathjax]

1b [mathjax](A \rightarrow B) \rightarrow ((A \rightarrow (B \rightarrow C)) \rightarrow (A \rightarrow C))[/mathjax]

3 [mathjax]A \rightarrow (B \rightarrow A \land B)[/mathjax]

4a [mathjax]A \land B \rightarrow A[/mathjax]

4b [mathjax]A \land B \rightarrow B[/mathjax]

5a [mathjax]A \rightarrow A \lor B[/mathjax]

5b [mathjax]B \rightarrow A \lor B[/mathjax]

6 [mathjax](A \rightarrow C) \rightarrow ((B \rightarrow C) \rightarrow (A \lor B \rightarrow C))[/mathjax]

7 [mathjax](A \rightarrow B) \rightarrow ((A \rightarrow \lnot B) \rightarrow \lnot A)[/mathjax]

8 [mathjax]\lnot \lnot A \rightarrow A[/mathjax]

9a [mathjax](A \rightarrow B) \rightarrow ((B \rightarrow A) \rightarrow (A \leftrightarrow B))[/mathjax]

10a [mathjax](A \leftrightarrow B) \rightarrow (A \rightarrow B)[/mathjax]

10b [mathjax](A \leftrightarrow B) \rightarrow (B \rightarrow A)[/mathjax]

Rád bych vyřešil tento příklad:
[mathjax](\lnot A \rightarrow A) \rightarrow A[/mathjax]

Snažil jsem to dokázat tímto způsobem:

1. [mathjax]\lnot A \rightarrow \lnot A[/mathjax] (již dokázaná věta [mathjax]A \rightarrow A[/mathjax])
2. [mathjax](\lnot A \rightarrow \lnot A) \rightarrow ((\lnot A \rightarrow \lnot \lnot A) \rightarrow \lnot \lnot A[/mathjax] (axiom 7)
3. [mathjax](\lnot A \rightarrow \lnot \lnot A) \rightarrow \lnot \lnot A[/mathjax] (modus ponens 1, 2)

Očekávám, že by se dalo využít nějak axiomu 8, ale nejsem si jistý, zda to mohu udělat s odvozovacím pravidlem modus ponens (případně tranzitivnost implikace?).

Předem mockrát děkuji za jakoukoli radu. Očekávám, že jde o nějakou ocividnost.