Note: This is a guest post by my friend Eaton Liu.
Everyone is equal. People are saying this way too often, to an extent that they no longer understand what it means. For example, some people may think that it contradicts with ‘everyone is special’. Oh wait. Due to euphemism treadmills, ‘special’ is now correlated with negative implications. Whatever, let’s just say ‘everyone is unique’ instead.
This is absurd. ‘equal’ in ‘everyone is equal’ refers to rights, not generic properties, however quantifiability. Let’s see what ridiculous consequences we would get if we were to admit generalisations of ‘everyone is equal’. For the sake of simplicity, let Human denote the class of all humans.
If ‘equal’ is treated as mathematical identity, i.e. ‘everyone is equal’ stands for $\forall p \in \mathrm{Human} \forall q \in \mathrm{Human} (p=q)$, one immediately gets $\lvert \mathrm{Human}\rvert \leq 1$ by applying the Law of the Excluded Middle (LEM), so there are either zero or one human, which is nonsense. Even if one does not admit LEM, if we have two exemplifications of humans (e.g. you and me), the equality axiom proves that we are equal, an equally ludicrous result (unless I am reading my own post).
What if we relax a little bit and quantify ‘equality’ over formulae, i.e. ‘everyone is equal’ means $\forall p \in \mathrm{Human} \forall q \in \mathrm{Human} (\varphi(p) \leftrightarrow \varphi(q))$ for all formulae $\varphi$ with one free variable and $p$, $q$ free in it. Hence, all humans are indiscernibles, thus, assuming Leibnizian identity of indiscernibles, all humans are, again, equal in the mathematical sense. On the other hand, if one uses the Frego-Russellian (I don’t really know the name prefix of Frege, maybe it should be Fregean-Russellian or Frege-Russellian or something) descriptive theory of names, they cannot name any person at all, because everyone validates the same cluster of properties, and no unique object is named in any case.
Finally, let’s see what we get if we switch to homotopy type theory instead (of course, using propositional equality instead of judgemental equality). Then, ‘everyone is equal’ corresponds to $(p, q: \mathrm{Human}) \to (p =_{\mathrm{Human}} q)$, i.e. $\mathrm{IsProp}(\mathrm{Human})$. Somehow by not ‘objectifying’ any individual human and ensuring equality between all humans, we have ‘objectified’ the entire human race by concluding it is but a proposition, while humans are merely proofs of propositions by the Curry-Howard correspondence (Platonic utopia?).
The analysis under homotopy type theory motivates us to consider alternative equality axioms, such as $\mathrm{IsSet}(\mathrm{Human})$, $\mathrm{IsGroupoid}(\mathrm{Human})$ or even the general $\mathrm{Is-}n\mathrm{-Groupoid}(\mathrm{Human})$. Let’s try to rephrase the simplest $\mathrm{IsSet}(\mathrm{Human})$ in some natural language, namely, English. A possible interpretation of \((x,y : \mathrm{Human}) \to (p, q: x =_\mathrm{Human} y) \to (p =_{x =_{\mathrm{Human}} y} q)\) is ‘all arguments for the equality of any two persons are the same’, which seems to be hinting at a view against the equality axiom. However, if one considers the theorems $\mathrm{IsProp}(\mathrm{IsProp}(\mathrm{Human}))$, $\mathrm{IsProp}(\mathrm{IsSet}(\mathrm{Human}))$ and so on, they seem to be hinting at arguments against $\mathrm{IsProp}(\mathrm{Human})$, $\mathrm{IsSet}(\mathrm{Human})$ and so on, which is kinda counterintuitive. I guess that’s just the inferior nature of natural languages.
Now, $\mathrm{IsProp}(\mathrm{Human})$ is definitely preposterous, but what about $\mathrm{IsSet}(\mathrm{Human})$? What if someone believes in $\mathrm{Is-}874569420\mathrm{-Groupoid}(\mathrm{Human})$ but not $\mathrm{Is-}874569419\mathrm{-Groupoid}(\mathrm{Human})$? Though I guess humans are better modelled as time-dependent types instead, so this is basically useless, probably equally useless as the equality axiom.