Proof Using Truth Tables Pleae forgive the very basic question, but I know nothing really of formal logic and so
would appreciate some feedback.
The truth table defining the implication operator 
P    Q    P implies Q
T    T         T 
T    F         F 
F    T         T 
F    F         T 

together with the negation operator ~ defined in the obvious way enables one
to construct the following table for ~Q $\implies$ ~P:
P  Q  ~P  ~Q  ~Q implies ~P
T  T   F   F        T 
T  F   F   T        F 
F  T   T   F        T 
F  F   T   T        T 

Evidently, truth values for ~Q $\implies$ ~P are the same as those
for P $\implies$ Q. Is this enough to prove that $P \implies Q$ if and only if 
~Q $\implies$ ~P ? My thinking is that yes, it is, because I belive that
the logical operators involved are defined by their respective truth tables
and this being the case the observations above should be sufficient to prove
the equivalence.
 A: In the context of formal logic, such will usually not consist of a proof... or more perhaps more clearly, a formal proof.  It will "show" that iff (P ⟹ Q), then (~Q ⟹ ~P) comes as valid.  For informal logic settings, that will usually suffice, and it could suffice as an argument of some sort in a formal logic setting given that you've already established the completeness metatheorem of classical propositional logic.  However, it does not consist of a formal proof, since in formal logic, a formal proof gets defined something like "a sequence of well-formed formulas (often just called "formulas") such that every well-formed formula is either an axiom, a hypothesis made under a certain scope which will get discharged eventually, or a well-formed formula permissible according to the rules of inference and well-formed formulas already in the proof."  What you've given above, does not give us such a sequence of well-formed formulas.
A: Yes what you're saying is indeed the case and is the idea behind the technique of proof by contrapositive.
