Propositional Calculus basic rules I've been learning propositional calculus and proofs and I'm not sure if we are able to write $(P \lor Q) \leftrightarrow (\lnot P \rightarrow Q)$. If I am doing a proof will i be able to replace (P v Q) with the other one? I was also wondering if there are any rules that allow me to switch some proposition from AND to OR or vice versa. I'm also doing a Vacuous Proof but would it be considered a Vacuous Proof(of let's say $P \to Q$) if I assume $P$ and get a contradiction out of it? 
 A: 1) There is no fixed set of "basic rules" for the propositional calculus. Even if you fix on a general style of calculus (e.g. linear proofs in Hilbert style vs a natural deduction calculus vs a sequent calculus vs a tableau system), and fix on a particular set of connectives you are going to treat as basic, you can still choose different (but equivalent) sets of rules to govern the system.
2) In some systems $(P \lor Q)$ is defined to be just shorthand for $(\neg P \to Q)$, In other systems, the equivalence of these two is a theorem to be derived from more basic rules. There is no right or wrong way of doing this. You will have to look at the details of the particular system in your course text book to find out the local rules of the game!
3) Similarly, in some systems AND is defined in terms of OR (or vice versa), in other systems you have to prove the equivalence of e.g. $(P \lor Q)$ and $\neg(\neg P \land \neg Q)$. Again there is no right or wrong way of doing this. Whether there is a rule that allows you to pass between ANDs and ORs will depend on the system -- though there is always a derived theorem proving the De Morgan equivalences.
4) "I'm also doing a Vacuous Proof but would it be considered a Vacuous Proof (of let's say $P \to Q$ if I assume $P$ and get a contradiction out of it?" Well, if $P$ implies a contradiction, then by reductio we can infer $\neg P$. And then from $\neg P$ we can infer $P \to Q$. Now I believe that a few people do call the second inference here a "vacuous proof" of the conditional. But that certainly isn't standard terminology. And in fact, talk of vacuous cases usually refers to something quite different (where we assume $P$, then infer $Q$ without actually using $P$, but still discharge the assumption and infer $P \to Q$).
