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?