Logical Proof: Theorem (Truths of Logic) A iff ~~A

[VeraMason]

Homework Statement

Prove that the following sentences are theorems (Truths of Logic):
A iff ~~A *Do not use Double Negation*

Relevant Equations

NA

My thought was to break up the sentence into its equivalent form: (A ->~~A) & (~~A -> A)
From there I assumed the premise of both sides to use indirect proofs, so:
1. ~(A -> ~~A) AP
2. ~(~A or ~~A) 1 Implication
3. ~~A & ~~~A 2 DeMorgan's
4. A -> ~~A 1-3 Indirect Proof
5. ~(~~A -> A) AP
6. ~(~~~A or A) 5 Implication
7. ~~~~A & ~A 6 DeMorgan's
8. ~~A -> A 5-7 Indirect Proof
9. (A ->~~A) & (~~A -> A) 4,8 Conjunction
10. A iff ~~A 9 EquivalenceTo me, this looks like it would be correct. Obviously, lines 3 and 7 would look a lot cleaner if I was allowed to use double negation, but in my mind, it shouldn't matter since both lines are a contradiction that essentially says: A & ~A.
Is this correct?

 

[Mark44]

Homework Statement:: Prove that the following sentences are theorems (Truths of Logic):
A iff ~~A *Do not use Double Negation*
Relevant Equations:: NA

My thought was to break up the sentence into its equivalent form: (A ->~~A) & (~~A -> A)
From there I assumed the premise of both sides to use indirect proofs, so:
1. ~(A -> ~~A) AP
2. ~(~A or ~~A) 1 Implication
3. ~~A & ~~~A 2 DeMorgan's
4. A -> ~~A 1-3 Indirect Proof
5. ~(~~A -> A) AP
6. ~(~~~A or A) 5 Implication
7. ~~~~A & ~A 6 DeMorgan's
8. ~~A -> A 5-7 Indirect Proof
9. (A ->~~A) & (~~A -> A) 4,8 Conjunction
10. A iff ~~A 9 EquivalenceTo me, this looks like it would be correct. Obviously, lines 3 and 7 would look a lot cleaner if I was allowed to use double negation, but in my mind, it shouldn't matter since both lines are a contradiction that essentially says: A & ~A.
Is this correct?

It looks OK to me, but it seems that you could also do this as a direct proof.
Here's for the first part:
$A \Rightarrow \neg \neg A$
$\Leftrightarrow \neg A \vee \neg \neg A$ ( implication is equivalent to a disjunction)
$\Leftrightarrow \neg (A \wedge \neg A)$ (de Morgan)
$\Leftrightarrow \neg (\text F)$ (A and ~A is false)
$\Leftrightarrow \text T$ (negation of false is true)

All the steps are reversible, which makes the first implication true.

 

[nuuskur]

@VeraMason Since this statement is not true in general, you should also point out, where you are using the law of excluded middle.