In set theory, we have the following:
Observation 0. Let $X$ denote a set. Let $A$ and $B$ denote subsets of $X$. Then if $A$ has at least one element, $B$ has at most one element, and $A \subseteq B$, then $B \subseteq A$.
Rehashing this into logical language, we have:
Observation 1. $$\frac{\exists a P(a) \quad !bQ(b) \quad \forall a(P(a) \rightarrow Q(a))}{\forall a(Q(a) \rightarrow P(a))}$$
(Where $!$ is the uniqueness quantifier: in particular, $!bQ(b)$ is to be read: "there is at most one $b$ such that $Q(b)$.")
I find this second version quite interesting.
Firstly, it tells us something about the logic of the uniqueness quantifier that makes no mention of the equality relation that we used to define it. In other words, it expresses a purely logical feature of uniqueness quantification.
Secondly, I think it has a lot of pedagogical utility; explaining it may help certain kinds of students (namely, the critical thinkers) to understand the material better. For example, suppose we assume that $3n+1=4$ and deduce that $n=1$. Well, there's really no need to check the converse: the fact that $n=1$ implies $3n+1=4$ is immediate from the fact that:
- $3n+1=4$ has a solution
- $n=1$ has at most one solution
- we've checked that $\forall n(3n+1=4 \rightarrow n=1)$.
More involved examples of this kind arise in e.g. solving differential equations, etc.
Question. Is there a name for the principle of logic stated in Observation 1?
