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.
Best Answer
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.