# Usage of $\Rightarrow$ – Implication or type declaration?

I have another notational question about the usage of $\Rightarrow$. This symbol is usually understood to indicate "material implication" (that is, $A\Rightarrow B$ means that the truth value of $B$ is at least as big as $A$, there hasn't to be a causal link between the two statements $A, B$). $A\Rightarrow B$ is often prononounced "If $A$, then $B$", and if there are free variables involved, then these are implicitly understood to be universally quantified.

Now, I noticed that "If $A$, then $B$" is not always a material implication in mathematics. It could as well mean a type declaration (or universal quantification): The statement "If $f$ is a function $A\to B$ and $A$ a nonempty set, then: blablabla" shouldn't be understood to mean "For any $f$, if $f$ happens to be a function with nonempty domain, then blablabla". Also, "For all real numbers x, ..." shouldn't mean "for any object x, if x is a real number, then ..."

Question: When "If $A$, then $B$" is used in such a context where it shouldn't be understood as a material implication, but as a type declaration (or universal quantification), can this also be abbreviated by the $\Rightarrow$ sign?

For example, I think I've seen in the definition of the term "first-order formula" $$\text{\phi, \psi formulae \Rightarrow \phi\land\psi formula}$$

But on the other hand, it would seem strange to abbreviate the statement "For all natural numbers $n$, we have $n^0 = 1$" by

$$n\in\mathbb N\Rightarrow n^0 = 1.$$

• "if there are free variables involved, then these are implicitly understood to be universally quantified" -- um, what? Quantification is independent of implication. In prose mathematics quantifiers are often left implicit (which sometimes leads to ambiguities), but that again has nothing to do with the use of implication. – Henning Makholm Oct 25 '16 at 21:12
• There's nothing wrong with writing $$\text{\phi, \psi formulae \Rightarrow \phi\land\psi formula.}$$ It just means: $$\forall \varphi,\psi(\varphi \in \mathrm{formula} \wedge \psi \in \mathrm{formula} \rightarrow \varphi \wedge \psi \in \mathrm{formula}),$$ where $\mathrm{formula}$ is a set. – goblin Oct 26 '16 at 5:08
• @goblin: Obviously you are right. But my question is concerned with "how to think about it", and not "how to encode it in an obscure but technically correct formula". – user377104 Oct 26 '16 at 15:31

I am going to give two technically grounded arguments. One contradicting what you state, and one agreeing with what you state. They come to roughly the same conclusion (for different reasons).

First, the set theory view. In (material) set theory, e.g. ZFC, all the things you say "shouldn't be understood to mean" or "seem strange" are completely legitimate. While $f : A \to B$ is not usually a primitive of set theory (but it is in some), it is completely reasonable to define it as $$f\text{ is a function }\land \pi_1(f) = A \land \pi_2(f) \subset B$$ where "is a function" is an abbreviation for the set theoretic definition of a function as a binary relation satisfying certain properties and $\pi_1$, $\pi_2$ are projections lifted to sets. The upshot is: it very much can be viewed as stating "filter $f$ to the things that satisfy this property". The next example is even simpler. $\forall x \in \mathbb{R}.P(x)$ is often (in set theory) defined to mean $\forall x.x\in \mathbb{R} \Rightarrow P(x)$. This also addresses your last example: $\forall n.n \in \mathbb{N} \Rightarrow n^0 = 1$ is a completely legitimate formal term of ZFC (given suitable standard definitions). So this is not strange, this is what set theorists do all the time.

Now, a type theorist says all the above was drivel. In type theory a statement like $$n :\mathbb{N} \Rightarrow n^0 = 1$$ is simply syntactically meaningless. That is, it's not even a well-formed formula even in a context where $n$ is bound. A type declaration like $n : \mathbb{N}$ is not a proposition that can be true or false. In type theory, there is no alternative to $\forall x:\mathbb{R}.P(x)$. To a type theorist $(x \mapsto x^2) : \mathbb{R} \to \mathbb{R}$ and $(x \mapsto x^2) : \mathbb{R} \to \mathbb{R}^+$ are just totally different things even though they are literally identical as set theoretic functions. But in (dependent) type theory there is the dependent product type often written $\Pi x:T.E(x)$ for some type $T$ and term $E$. In (particularly constructive) type theory it is common for function types, universal quantification, and implication all to be special cases of $\Pi$-types. In most implementations of type theory, $A \to B$ is defined to be $\Pi x:A.B$ (where $x$ is not free in $B$, i.e. we just ignore $x$). In NuPRL, $\forall$ and $\Rightarrow$ are simply $\Pi$ and $\to$ at the type Prop. (NuPRL uses the syntax $x:A \to B(x)$ for $\Pi x:A.B(x)$.)

To summarize, in (material) set theory, the cases you are worried about are fine; a lot of high level syntax expands to the very constructs you are worried about. That said, implication and universal quantification and functions, while having interrelations are quite distinct concepts. In type theory, all of these concepts are literally special cases of the same concept.

• @Elkins: I am so sorry, I accidentally disliked this answer and now I cannot vote up anymore :-( It says I can vote up if the answer is edited. That's why I tried to edit it. Anyway, I will accept your answer. – user377104 Oct 26 '16 at 16:26
• Now it worked: I liked your answer! – user377104 Oct 27 '16 at 17:17

I agree with most of what Derek has written. But, I'd just like to add that we can always think of $\Rightarrow$ as external to the language we're trying to define. For example, we could interpret $$n :\mathbb{N} \Rightarrow n^0 = 1$$ as saying: "if $n:\mathbb{N}$ is a well-formed expression in the language of interest, then $n^0 = 1$ is a well-formed expression in the language of interest." In general, apparently "nonsensical" IF-THEN clauses can be made sense of in this way.

• While I agree with this, I really hope authors do try to avoid confusion between the meta-logic and the object language. Often the horizontal rule notation is used for examples like the formula one, e.g. $$\frac{\phi\text{ formula}\quad\psi\text{ formula}}{\phi\land\psi\text{ formula}}$$ This does keep things well separated but is additional notation to learn. – Derek Elkins Oct 26 '16 at 19:43

$A\Rightarrow B$ is often prononounced "If $A$, then $B$", and if there are free variables involved, then these are implicitly understood to be universally quantified.

Free variables are universally quantified over their entire deduction, not the formula they appear in.

Now, I noticed that "If $A$, then $B$" is not always a material implication in mathematics.

Yes it is.

It could as well mean a type declaration (or universal quantification):

No it can't.

The statement "If $f$ is a function $A \to B$ and $A$ a nonempty set, then: blablabla" shouldn't be understood to mean "For any $f$, if $f$ happens to be a function with nonempty domain, then blablabla".

Of course they aren't the same, you left off the restriction about the domain and codomain of $f$.

Also, "For all real numbers x, ..." shouldn't mean "for any object x, if x is a real number, then ..."

Yes it does mean that. Who told you it doesn't? Don't listen to that person.

Question: *When "If $A$, then $B$" is used in such a context where it shouldn't be understood as a material implication, but as a type declaration (or universal quantification),

There is no such situation.

But on the other hand, it would seem strange to abbreviate the statement "For all natural numbers $n$, we have $n^0 = 1$" by $$n\in\mathbb N\Rightarrow n^0 = 1.$$

Those are equivalent statements as long as no where else is anything assumed about $n$.

There is a very surprising isomorphism between $\Rightarrow$ in logic and $\rightarrow$ in set theory. But they are not the same thing. $A \rightarrow B$ is defined in set theory to be the set of all function with a domain of $A$ and a codomain of $B$, and is sometimes written $B^A$. For example:

$$\{x, y\} \rightarrow \{1, 2\} = \{ \{(x, 1), (y, 1)\}, \{(x, 1), (y, 2)\}, \{(x, 2), (y, 1)\}, \{(x, 2), (y, 2)\}\}$$

• Let me quote from Shulman's article From set theory to type theory: "When I say “for all $x\in \mathbb{R}$, $x^2\ge 0$”, I regard it as a property of every real number that its square is nonnegative. I don’t regard it as a property of every thing in mathematics that if it happens to be a real number, then its square is nonnegative. Under the material-set theory reading, one particular instance of “for all $x\in \mathbb{R}$, $x^2\ge 0$” is the statement “if the monster simple group happens to be a real number, then its square is nonnegative”. – user377104 Oct 26 '16 at 15:22
• I wouldn’t expect most mathematicians to naturally regard that statement as part of the content of “for all $x\in \mathbb{R}$, $x^2\ge 0$”." – user377104 Oct 26 '16 at 15:22
• You say: "Who told you it doesn't? Don't listen to that person." So basically you say that I shouldn't listen to the mathematician Michael Shulman. Please excuse me that when it comes to foundations of mathematics, I rather trust an expert (like him) than I trust you. – user377104 Oct 26 '16 at 15:27
• Also, I find your comment quite arrogant. – user377104 Oct 26 '16 at 15:27