"let" vs "suppose" vs "if" and the contrapositive

Question

Sometimes you will see theorems of the form "Let $H_1, \dots, H_n$. If $A$, then $B$". Sometimes "suppose" or "if" is used instead of "let". Here's an example:

1. Let $x\in\mathbb{R}$. If $x\geq 0$, then $|x|=x$.

2. Suppose $x\in\mathbb{R}$. If $x\geq 0$, then $|x|=x$.

3. If $x\in\mathbb{R}$ and $x\geq 0$, then $|x|=x$.

I'm under the impression that these are all equivalent ways of saying the same thing. In this example, I would call "$x\in\mathbb{R}$" a hypothesis and "$x\geq 0$" the antecedent. But in the third statement, is there an unambiguous contrapositive? In certain contexts, I think it is understood that we're not really considering the case when $x\notin\mathbb{R}$. But "$x\in\mathbb{R}$" is nevertheless part of the antecedent in statement (3). So if we agree (1-3) are equivalent, then I see two contrapositives:

a) If $x\in\mathbb{R}$ and $|x|\neq x$, then $x<0$.

b) If $|x|\neq x$, then $x<0$ or $x\notin\mathbb{R}$.

I think Halmos' Naive Set Theory is an example where form (3) is preferred to (1,2).

The questions are:

1. Are those statements equivalent?

2. In the third statement, what is The contrapositive? EDIT: Generally, if you see a theorem of the form "Let $H_1, \dots, H_n$. If $A$, then $B$", what is its contrapositive? How do you know?

3. Do mathematicians make any effort to separate the hypotheses ($H_1,\dots,H_n$) from the antecedent ($A$) of the claim? If so, how? Or is this one of those things everybody understands and no one is explicit about?

Answer 1

1. Technically the third one is different because there are two conditions in the antecedent. Depending on context the third one can be interchangeable with the first two, pretty much for the reason you mentioned. I wouldn't say "I think everybody knows that we don't really care about the case when $x \notin \Bbb{R}$" in general, but if we're in a context where we really do only care about $x \in \Bbb{R}$ then the third one is no different from the others.

2. The contrapositive is this: "If $|x| \ne x$ then $x \notin \Bbb{R}$ or $x < 0$." I know this because that's the definition of contrapositive. If we have a statement "If $P$ then $Q$" then the contrapositive is "If not $Q$ then not $P$." And in this case, $P$ is "$x \in \Bbb{R}$ and $x \ge 0$," which means (by deMorgan) that "not $P$" is "$x \notin \Bbb{R}$ or $x < 0$."

3. I think it varies from person to person but what I seemed to notice is for most it's something everybody understands and isn't generally explicit about.

Answer 2

I would say that all three forms are equivalent. They all express your assumptions followed by the consequence of those assumptions. The third one would be more easily translated into a purely symbolic representation, but it's worth noting that mathematics was a rhetorical art long before symbolism. With that in mind, they all state the same idea, that a certain property follows inevitably from certain other properties, and the rest is just stylistic.

You can see some guides for the difference between "suppose" and "let" here. It boils down to "Let $x$ be something" means you're telling me that you're using $x$ as a shorthand for an object with a certain property, while "suppose" can be used for the same thing and also for pretending something is true, such as "Suppose this theorem is true, here are the consequences". It wouldn't make much sense to say, "Let this theorem be true," because you can't just declare a theorem to be true the same way you can claim your arbitrary label $x$ represents a object with a certain property.

It's all very subtle, I hadn't thought about it before with absolute rigor. I doubt most people do. The difference is almost colloquial to math writing, a linguistic quirk rather than a mathematical one.

About finding the contrapositive, all the statements are the same, so we can choose one arbitrarily. I'll pick the third formulation for clarity. If we start with "If $H$ and $A$, then $B$", the contrapositive is clearly "If $\neg B$, then $\neg H$ or $\neg A$", with the antecedent being flipped around by DeMorgan's law. Also note that I combined all the $H_i$'s into one $H$ since it amounts to the same thing.

Now we're trying to prove an OR statement. You could prove it by cases, but there's another way. The statement "If $P$, then $Q$" is equivalent to the statement "$\neg P$ or $Q$". So likewise, if we have "$P$ or $Q$", we equivalently prove "If $\neg P$, then $Q$". It's like proving the OR statement by saying, "Ok, first assume $P$ is true. So the OR statement is true and we're done. Now assume $P$ is not true. We have to show $Q$ is true or else the OR statement isn't always true."

Applying it back to our example, we can prove "If $H$, then $\neg A$" instead of the OR statement in the consequent. So now we're saying, "If $\neg B$, then if $H$, then $\neg$A". That's the same as "If $\neg B$ and $H$, then $\neg A$", just use the earlier trick to rearrange it. So now you can rephrase it as "Suppose $H$. If $\neg B$ then $\neg A$" since those formulations are the same.

So you can keep it in the same domain, it all amounts to the same thing. It all depends on what you want to emphasize.

Answer 3

In response to your third question, there is a setting in which mathematicians make a clear distinction between a hypothesis of the form "$x \in \mathbb{R}$" and an assumption of the form "$x \ge 0$". It's type theory.

In type theory there are types and elements, and an element always belongs to exactly one type. This is in stark contrast with set theory, in which there are only sets, and a set always belongs to many other sets. But in practice, we can now think of a type as a set.

In many versions of type theory, like the Calculus of Constructions, types are allowed to be elements of other types, and there is a type called $\mathrm{Prop}$ the elements of which are special types called propositions. Indeed, one can view a proposition as a type, the elements of which are its proofs. For example, the conjunction $A \land B$ can be seen as the Cartesian product of $A$ and $B$, because a proof of $A \land B$ consists of a proof of $A$ and a proof of $B$, i.e. a pair $(a, b)$ with $a \in A$ and $b \in B$. This reasoning can be applied to all the other logical connectives and quantifiers, and goes by the name of Brouwer–Heyting–Kolmogorov interpretation.

Let us see how implications and universal quantifications can be thought of as types. The implication $A \Rightarrow B$ is the type of functions from $A$ to $B$, because a proof $f$ of $A \Rightarrow B$, together with a proof $a$ of $A$, produces a proof $f(a)$ of $B$. Similarly, the quantification $\forall a \in A. B(a)$ is a type of functions, but this time an element is a function $f$ that associates to any $a \in A$ a proof of $B(a)$. In set theory, this would be the the set $\{ f \colon A \to \bigcup_{a \in A} B(a) \mid \forall a \in A. f(a) \in B(a) \}$.

In this setting, your statements (1) and (2) would correspond to the type $\forall x \in \mathbb{R}. (x \ge 0 \Rightarrow \lvert x \rvert = x)$. Notice that $x \in \mathbb{R}$ here is not a proposition. Indeed, an element of this type is a function $f$ that associates to a real number $x$ a proof $f(x)$ of the implication $x \ge 0 \Rightarrow \lvert x \rvert = x$, so it's a function from a set-like type to a family of propositions. Then, once $x$ is chosen, a proof of $x \ge 0 \Rightarrow \lvert x \rvert = x$ is a function $f(x)$ that associates to a proof of $x \ge 0$ a proof of $\lvert x \rvert = x$, so it's a function from a proposition to a proposition. In this way, you see that the difference between the two kind of assumptions can be made formal.

Your statement (3) would correspond to the type $\forall z \in (\Sigma x \in \mathbb{R}. \pi_1(z) \ge 0). \lvert \pi_1(z) \rvert = \pi_1(z)$, where the $\Sigma$ type is an indexed sum and $\pi_1$ is the first projection: in set theory, $\Sigma a \in A. B(a)$ corresponds to $\{ (a, b) \in A \times \bigcup_{a \in A} B(a) \mid b \in B(a) \}$, with $\pi_1((a, b)) = a$. Now, an element of this type is a function from a family of propositions indexed by a set-like type to another family of propositions. So again, this kind of assumption is different from those seen before.