Proof of the Formula of the Principle of Non-Contradiction I'm starting to study logic and I just found this exercise:


*

*In these exercises you start from the axioms and must arrive at the
requested formula. The use of the The Deduction Theorem is not
allowed.

*

*c. Prove the following theorem using only Kleene's axioms and the rule of
Modus Ponens. You are not allowed to use any additional theorems.
⊢ ~( A ∧ ~A ) (Principle of Non-Contradiction)

This are the 8 axioms I need to work with:
├ A → ( B → A)
├ (A → B) → ((A → (B → (B → C) ) → (A → C))
├ A → (B → A ∧ B)
├ A ∧ B → A,,    A ∧ B → B
├ A → A ∨ B,,    B → A ∨ B
├ (A → C) → ((B → C ) → (A ∨ B → C))
├ (A → B) → (( A → ~B) → ~A )
├ ~~A → A

I understand the intuition behind the Principle of Non-Contradiction, but cannot figure out where to start with the proof.
I have done this, using the identity theorem which is not allowed in the exercise:

├ A → A
├ ~(~(A → A))
├ ~(~(A → ~~A))
~(A → ~B) ↔ A ∧ B
~( A ∧ ~A )


Is this proof valid? Although I am using the identity theorem I would like to know if this is a valid demonstration or am I doing something wrong. I have a second question, how would this exercise be done without using theorems?
 A: Mauro Allegranza has already pointed out that your argument is extremely flawed; you use the operator ${\leftrightarrow}$ which is undefined in this logical calculus.  Here's a solution from scratch.
The outermost operation in $\neg(A\wedge\neg A)$ is ${\neg}$, so let's start by figuring out how that can arise.  The only axiom with ${\neg}$ in the conclusion is axiom 7: $$\vdash(a\to b)\to((a\to\neg b)\to\neg a)$$  So let's try that.  Comparing, we'll need $a=A\wedge\neg A$, but are free to choose $b$.  I'll figure out what $b$ needs to be later, and then come back and pencil it in.
To get $\neg a$ out of axiom 7, we'll need to use modus ponens a bunch.  So we also need \begin{gather*}
\vdash A\wedge\neg A\to b \\
\vdash A\wedge\neg A\to\neg b \tag{*}
\end{gather*}  Luckily, axiom 4 matches that schema: changing variable names to avoid confusion, axiom 4 says \begin{gather*}
\vdash x\wedge y\to x \\
\vdash x\wedge y\to y
\end{gather*}  So let's take $x=A$, $y=\neg A$; then we have \begin{gather*}
\vdash A\wedge\neg A\to A \\
\vdash A\wedge\neg A\to\neg A
\end{gather*}  Comparing with (*), we see that we should have chosen $b=A$.
Putting it all together, we have:

*

*$\vdash A\wedge\neg A\to A$ (Axiom 4)

*$\vdash A\wedge\neg A\to\neg A$ (Axiom 4)

*$\vdash(A\wedge\neg A\to A)\to((A\wedge\neg A\to\neg A)\to\neg(A\wedge\neg A))$ (Axiom 7)

*$\vdash(A\wedge\neg A\to\neg A)\to\neg(A\wedge\neg A)$ (Step 1, Step 3, MP)

*$\vdash\neg(A\wedge\neg A)$ (Step 2, Step 4, MP)

