Proof in Fitch and counterexample in Tarski's World Good official afternoon community, 
I am trying to prove (P → Q) ↔ (¬Q →¬P)  without premises. I do not understand why it is not working, I need to study such exercises to be able to pass the final. Please help me. I do not want just an answer I want someone to explain to me what I am doing wrong and how to fix it because that will help me understand the concept. 
Would you please help me, I appreciate your time
mark
 A: Fitch is not accepting your 'proof' because it really is not a proof, and that's because you rely on FO Con, which is not a formal inference rule, but rather a clever mechanism that is able to check whether some statement validly follows from some others or not .  Hey, if you would be allowed to use FO Con, you could just do:

... but clearly that shouldn't count as a proof!
OK,  set-up and organization are key to completing these formal proofs, and subproofs are the key to providing that organization. Take a look here for how to create the set-up for Fitch Proofs, and here for how to deal with subproofs in Fitch
OK, for your specific problem, you need to derive $P \rightarrow Q$ from $\neg Q \rightarrow \neg P$.  Since your goal is a $\rightarrow$, the thing to do is to use a Conditional Proof, i.e to set up a $\rightarrow$ Intro:

OK, so now you need to prove $Q$, which is an atomic statement. On strategy for trying to prove atomic statements is to do a Proof by Contradiction, i.e. assume the negation of that atomic statement, and show that leads to a contradiction. So, that would suggest the following proof skeleton:

OK, from here it should not be very hard ...
