What is the difference between type inhabitant and subtyping?

Question

I am confused with the terms inhabitant vs. subtyping.

For example,

1. We usually think that "john is an inhabitant of Human". This sentence is correct, because john is an individual, and an individual belongs to the set Human (that reflects the meaning of inhabitant). However, if we think of john as a subset with only one element, we could also say "john is a subtype of Human", is that right?

2. As we all know Cat is a subtype of Animal. However, it seems no problem if we think Cat as an inhabitant of the Animal? (Suppose in the discourse, the sets Dog, Fish, Human, etc are not overlapping, i.e. treat Dog, Fish, Human, etc as individuals)?

My question is that

1. How to formally distinguish inhabitant and subtyping?

2. Does subtyping-framework actually need the concept of inhabitant? (because it seems useless).

Thanks.

Answer 1

There is an obvious difference: you are an inhabitant (member) of humankind, but since you are not a collection of little humans you are not a subset of humanity. And as Bertrand Russell taught us all, one should not conflate an object $x$ with the singleton set $\{x\}$.

The relevant analogy is $$\frac{\text{element}}{\text{subset}} = \frac{\text{inhabitant}}{\text{subtype}},$$ with the caveat that subtyping can be quite different from the subset relation (for instance in object-oriented languages with a class hierarchy).

We can also note that $\in$ and $\subseteq$ are expressible in terms of each other, as already noticed by the OP: $$x \in A \iff \{x\} \subseteq A$$ and $$A \subseteq B \iff \forall{x \in A} . x \in B.$$ But just because two concepts are expressible in terms of each other, that does not mean they are the same concept.

Answer 2

I'll answer using the words instanceof (instead of inhabitant) and Class (instead of Type) since these are the terms in UML.

It seems to me that you are thinking about classes anb subclasses like sets of individuals and subsets of individuals. However, I would suggest, following [1], interpreting a class as a set of properties (e.g. Person is the set of properties of being Animal and being Rational), and a subclass as a superset of such properties (e.g. Child is the set of properties of Person, together the property of being underage). In some sense, we are used to say that a Child inherits all the properties of Person, and adds some additional properties (being underage).

A subtyping, then, only says which classes "inherits" which properties from which other classes (Child inherits from Person, Person inherits from Animal, etc). Do note that this is a relation among classes (e.g., sets of properties).

An instanceof, however, states which objects satisfies such properties (john is an instance of Child because it satisfies all the properties of Person plus being underage).

Saying that john is a subtype of Human sounds strange because, in essence, you are saying that john is a set of properties, whereas john is, as you were saying, a real world individual.

Saying that Cat is an instanceof Animal sounds strange too because, in essence, you are saying that (the concept of) Cat is a real world object satisfying the properties of Animal. The concept of Cat, as a set of Properties, inherits all the properties of Animal, but it does not satisfy them (i.e., the concept of Cat is not mortal).

If you like (first-order logic) formalism, again, following [1] you can formalize these as:

• Objects can be seen as logic constants: $John$, $Mary$, etc
• Classes can be seen as logic Predicates: $Person$, $Child$
• instanceof can be seen as a logic ground atom: $Person(John)$
• subtypeof can be seen as a logic constraint: $\forall x. Child(x) \rightarrow Person(x)$

[1] Olivé, A. (2007). Conceptual modeling of information systems. Springer Science & Business Media.