How to prove A<—>not A

So basically there are no premises, but the file I have received to start this problem has a contradiction symbol as step one. I’m not sure if this was a mistake or purposeful, and if it was purposeful, how or why I use this step.

First off, I know that I should use biconditional introduction, which means I will have to have two sub-proofs, one for each way the conditional goes. This is where I find my first problem. When I assume A and try to reach notA, I am stumped. If I assume A and then do another subproof and assume notA, then I can get a contradiction symbol with contradiction intro, but then all I can conclude from this is P again. So I can just conclude A from A. But how do I conclude not A from A?

• Proving contradictions from no premises is dangerous! The universe might implode! Seriously though, I think you may have misunderstood what you are being asked to do. Jun 17, 2020 at 23:04
• Well I actually guess the contradiction symbol in step 1 is a premise. My instructor said in his instructions that we are proving “A<—>not A” from a contradiction. Not sure how to do that! Jun 17, 2020 at 23:21
• Obviously you cannot prove it without premise: propositional logic is consistent. But you say that "the file I have received to start this problem has a contradiction symbol as step one"; this means that what are you asking to prove is: ⊥ ⊢ A ↔ ¬A, and this is correct. A single line proof with EFQ will be enough. Jun 18, 2020 at 9:42

In (X iff ~X) the truth value of X is unstable (if true, then false; if false, then true). So it looks similar to the Liar Paradox. (This statement is false.) As far as I know, there is not yet any satisfactory "solution" to the Liar Paradox.

the file I have received to start this problem has a contradiction symbol as step one

Usually, contradictions are not allowed. So when one is encountered, you have to back up to undo the assumptions that led to the contradiction. This is how proof by contradiction works.

The usual truth table for "implication" has (F ⇒ T/F) being "true". Since contradiction (X and ~X) is always "false", you can say (almost) anything you want follows to end up with a "true" statement. You'd still need to make the case that the instability of X can be ignored.

Suppose (A <-> ~A) for proof by reductio. Unpacked, this is to assume ((A -> ~A) & (~A -> A)).

From this both (A -> ~A) and (~A -> A) follow. Substituting for the conditionals, that implies both (~A v ~A) and (A v A).

Suppose A. Then (A & (~A v ~A)) entails ~A. Hence, (A & ~A), i.e. contradiction. Repeat this to show that (A v A) entails a contradiction.

That implies your supposition was false. Hence, ~(A <-> ~A).