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.

  1. 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?

  2. 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?

  3. 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.

  • 1
    $\begingroup$ What proof system are you working with? (For example, in any natural deduction system that I'm aware of, it is indeed fairly straightforward to show that $(A \rightarrow B) \rightarrow (\lnot B \rightarrow \lnot A)$ is a tautology.) $\endgroup$ – Daniel Schepler Dec 29 '17 at 19:24
  • $\begingroup$ @DanielSchepler Thanks for the response. I'm honestly not sure since I've never encountered this question before. I would say that I'm using whatever the canonical system is for modern mathematics? Is that equivalent to the ZFC axiomatic system? As I said, I'm not sure what is meant by such a question. $\endgroup$ – The Pointer Dec 29 '17 at 19:26
  • 2
    $\begingroup$ Well, ZFC relies on an underlying system of "first-order logic". There are several equivalent formulations of the formal proof system to be used in first-order logic; but since they're equivalent, at a higher level we usually don't specify any particular one of these formulations to be the "canonical" one. On the other hand, this question is at a level which is directly concerned with a question of logic, so an answer would best be phrased in terms of a formal system of first-order logic. $\endgroup$ – Daniel Schepler Dec 29 '17 at 19:37
  • $\begingroup$ @DanielSchepler I see. Thanks for the insight. $\endgroup$ – The Pointer Dec 29 '17 at 19:40

The statement $A\implies B$ is logically equivalent to its contrapositive, $\lnot B\implies \lnot A$. So we can actually say that $$(A\implies B)\iff(\lnot B\implies\lnot A)$$ So if the statement $A\implies B$ holds, then its contrapositive must hold, and vice-versa.

  • $\begingroup$ I understand now. Thank you for the assistance. $\endgroup$ – The Pointer Dec 29 '17 at 19:28

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:

  1. $A \rightarrow B$ (assumption)
  2. $\quad \lnot B$ (assumption)
  3. $\quad \quad A$ (assumption)
  4. $\quad \quad \quad B$ (modus ponens from 1 and 3)
  5. $\quad \quad \quad \bot$ (modus ponens from 2 and 4)
  6. $\quad \quad A \rightarrow \bot$, or in other words $\lnot A$ ($\rightarrow$-intro from 3 through 5)
  7. $\quad \lnot B \rightarrow \lnot A$ ($\rightarrow$-intro from 2 through 6)
  8. $(A \rightarrow B) \rightarrow (\lnot B \rightarrow \lnot A)$ ($\rightarrow$-intro from 1 through 7)

(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.)


First, a word on notation. You ask whether the statement $A \Rightarrow B$ logically implies the statement $\neg B \Rightarrow \neg A$ ... and write this as $(A \Rightarrow B) \Rightarrow (\neg B \Rightarrow \neg A)$

But, the $\Rightarrow$ in $A \Rightarrow B$ and $\neg B \Rightarrow \neg A$ are meant here as the logical connective called the material implication, while the $\Rightarrow$ between those two statements is a logical implication.

To more clearly separate the two, many logicians will use the $\rightarrow$ for the material implication, and reserve the $\Rightarrow$ for the logical implication. As such, your question is therefore better put as: is it true that $(A \rightarrow B) \Rightarrow (\neg B \rightarrow \neg A)$?

Well, this is something we can very easily check on a combined truth-table (a combined truth-table is one on which you evaluate the truth-conditions of multiple statements):

\begin{array}{c|c|c|ccc} A&B&A \rightarrow B&\neg B & \rightarrow & \neg A\\ \hline T&T&\color{blue}T&F&\color{red}T&F\\ T&F&\color{blue}F&T&\color{red}F&F\\ F&T&\color{blue}T&F&\color{red}T&T\\ F&F&\color{blue}T&T&\color{red}T&T\\ \end{array}

We see that whenever $A \rightarrow B$ (in blue) is true, $\neg B \rightarrow \neg A$ (in red) is also true, and therefore it is indeed the case that $(A \rightarrow B) \Rightarrow (\neg B \rightarrow \neg A)$.

In fact, note that the opposite is true as well: Whenever $\neg B \rightarrow \neg A$ is true, $A \rightarrow B$ is also true, and so we also have $(\neg B \rightarrow \neg A)\Rightarrow (A \rightarrow B) $. Indeed, since the two statements have the exact same truth-conditions they are said to be logically equivalent, which we typically write as $(A \rightarrow B) \Leftrightarrow (\neg B \rightarrow \neg A)$.

On a final note: When you wrote $(A \Rightarrow B) \Rightarrow (\neg B \Rightarrow \neg A)$ it is possible to treat the $\Rightarrow$ to be a material implication, just like the other two, and so what you really have is $(A \rightarrow B) \rightarrow (\neg B \rightarrow \neg A)$. And that is of course a perfectly good statement in the language of formal logic, but if you are asking about logicL implication, you will have to be very careful how you analyze this statement.

For one, a material implication is true as soon as its antecedent (the 'if' part) is false. Thus, for example, it would be the case that $A \rightarrow B$ is true as soon as $A$ is false ... but $A$ clearly does not logically imply $B$. So, given that your question is about logical implication, you'll need to do something different from simply evaluating the truth of the statement $(A \rightarrow B) \rightarrow (\neg B \rightarrow \neg A)$.

Interestingly, it is a meta-logical theorem that any logical statement of the form $\phi \rightarrow \psi$ is a tautology if and only if $\phi$ logically implies $\psi$. So, to figure out whether or not $A \rightarrow B$ logically implies $\neg B \rightarrow \neg A$, one thing we can do is to see whether $(A \rightarrow B) \rightarrow (\neg B \rightarrow \neg A)$ is a tautology, i.e. whether or not it is a statement that is always true. And, for that, we can once again use a truth-table:

\begin{array}{c|c|cccc} A&B&(A \rightarrow B) &\rightarrow & (\neg B & \rightarrow & \neg A)\\ \hline T&T&T&\color{red}T&F&T&F\\ T&F&F&\color{red}T&T&F&F\\ F&T&T&\color{red}T&F&T&T\\ F&F&T&\color{red}T&T&T&T\\ \end{array}

Likewise, it is a meta-logical theorem that any logical statement of the form $\phi \leftrightarrow \psi$ is a tautology if and only if $\phi$ is logically equivalent to $\psi$. So, to demonstrate that $A \rightarrow B$ is logically equivalent to $\neg B \rightarrow \neg A$, we can see whether $(A \rightarrow B) \leftrightarrow (\neg B \rightarrow \neg A)$ is a tautology. And indeed it is:

\begin{array}{c|c|cccc} A&B&(A \rightarrow B) &\leftrightarrow & (\neg B & \rightarrow & \neg A)\\ \hline T&T&T&\color{red}T&F&T&F\\ T&F&F&\color{red}T&T&F&F\\ F&T&T&\color{red}T&F&T&T\\ F&F&T&\color{red}T&T&T&T\\ \end{array}


You're essentially correct. The small detail you're missing is that the contrapositive is logically equivalent to the initial statement. So, we don't have that $(A\implies B)\implies (\lnot B\implies\lnot A)$, but $(A\implies B)\iff (\lnot B\implies \lnot A)$. This encompasses your statement, so what you wrote isn't wrong, but just not the "full story".

  • $\begingroup$ I understand now. Thank you for the assistance. $\endgroup$ – The Pointer Dec 29 '17 at 19:28

If you have $A\implies B$ as an axiom, then $\neg B\implies \neg A$ follows (and in the usual classical, but not constructive, logic is logically equivalent as the other answers state).

To answer your questions with the above context:

  1. No, you need a proof. It will however be a very easy proof. Informally, though, people will treat these as identical (in classical logic) since the proof is so easy.

  2. Interpreting "true by definition" as "axiomatically true", then, again, no. One of the formulas is an axiom, the other is a derived theorem. Again, informally, they will often be treated identically. Since (in classical logic) they are equivalent, it would be "just as good" to take the other as an axiom, and, as in 1, each is easily derivable from the other.

  3. Yes, using truth tables you can show that $(A\implies B)\implies (\neg B \implies \neg A)$ is a classical tautology. You can then use modus ponens and the fact that $A\implies B$ is assumed axiomatically to deduce $\neg B \implies \neg A$. This is a (partially semantic, partially syntactic) proof of the sort referred to in 1.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.