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

Question

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

Answer 1

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.

Answer 2

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.

Answer 3

$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)\}\}$$