I have a mathematical proposition of the form "If $A$, then $B$". I'm thinking about this problem from several different perspectives, so I will segment these different perspectives into separate paragraphs as follows.
-
If I have a statement $A \implies B$ that is true by definition (no proof provided), is it then correct to say that the contrapositive statement $\neg B \implies \neg A$ (NOT $B \implies$ NOT $A$) must also be true, without providing any proof?
-
In other words, if $A \implies B$ that is true by definition, then does this imply that the contrapositive statement $\neg B \implies \neg A$ is also true by definition?
-
Trying to think of this from the perspective of logic notation and truth tables, would it be correct to write that $(A \implies B) \implies (\neg B \implies \neg A)$? This way, since we know that $A \implies B$ is true, we must logically have (according to truth tables) that $\neg B \implies \neg A$ is also true, right?
I would greatly appreciate it if people would please take the time to clarify this.
Best Answer
Your (1) would be something to prove in whatever formalization of propositional or first-order logic you're using; most of the formal proof systems I'm familiar with don't have the contrapositive principle directly stated as an axiom, but it follows from the other axioms.
Then, the argument in (2) and (3) is fairly directly in the style of proof that comes under a "natural deduction" type of formal proof system. In these systems, if you can start with a hypothesis $p$ which you assume to be true and reach a conclusion $q$, then a rule of the formal proof system, often known as "$\rightarrow$-introduction", will allow you to "abstract" or "encapsulate" that into a proof of the implication $p \rightarrow q$. Thus, the form of your argument would look like:
\begin{align*} (A \rightarrow B) & \vdash (\lnot B \rightarrow \lnot A) \\ \hline & \vdash [(A \rightarrow B) \rightarrow (\lnot B \rightarrow \lnot A)]. \end{align*}
(In Hilbert-style proof systems, we similarly have the Deduction Theorem which fills a similar role.)
Now, as to how you would actually prove (1), that depends more on the details of the formal proof system. In the system I personally prefer to use, $\lnot A$ is defined as being the same as $A \rightarrow \bot$ where $\bot$ is an atomic formula representing a "false" proposition. (Think of the humorous way we sometimes use to negate a statement: instead of saying just "it's not raining," somebody might say "if it's raining, then I'm a frog.") Then the overall proof might look something like:
(Here, the indentation is used to indicate that "assumption" lines above the current line, with a smaller amount of indentation, are part of the current proof context of what we are assuming to be true.)
Another way of representing the same proof would be as a proof tree:
$$ \frac{ \frac{ \displaystyle \frac{ \frac{ \displaystyle A \rightarrow B, \lnot B, A \vdash B \rightarrow \bot \qquad \frac{ \displaystyle A \rightarrow B, \lnot B, A \vdash A \rightarrow B \qquad A \rightarrow B, \lnot B, A \vdash A}{\displaystyle A \rightarrow B, \lnot B, A \vdash B} }{\displaystyle A \rightarrow B, \lnot B, A \vdash \bot} }{A \rightarrow B, \lnot B \vdash \lnot A} }{\displaystyle A \rightarrow B \vdash \lnot B \rightarrow \lnot A} }{\vdash (A \rightarrow B) \rightarrow (\lnot B \rightarrow \lnot A)} $$ This representation has the advantage that it makes it clear at each element of the proof what propositions are (provisionally) being assumed to be true, and what is being concluded. (It obviously has the disadvantage of taking up a great deal of space, though.)