# What is the origin of the Bottom Type notation? Why does it look like... a bottom?

I couldn't help but notice the opening summary in Wikipedia's article on Bottom Types:

In type theory, a theory within mathematical logic, the bottom type is the type that has no values. It is also called the zero or empty type, and is sometimes denoted with the up tack (⊥) symbol.

Is the visual similarity to an actual bottom intentional? Or just an amusing coincidence?

• To the extent of my knowledge (I don't know type theory to begin with...), the "bottom" symbol is usually used for describing some "empty" object. So I think it would make sense in this case that it is intentional. Again, I have no clue about type theory or the notations there, this is just where I have seen the bottom notation appear... Commented Jul 21, 2021 at 8:28
• I suspect it's because it's an upside-down T (for 'top'). The same symbol can be used in other parts of logic for 'false', where I've heard but can't give a reference that it's because it's the opposite of the T used for 'true' Commented Jul 21, 2021 at 10:05
• Haha. I see your point. Without the brackets it is less appropriate: $\bot$ Commented Jul 22, 2021 at 1:14

The symbol $$(\bot)$$ usually represents the least element of a lattice. The least element often goes at the bottom part of a Hasse diagram. That is maybe the reason you're looking for. For example, in a Hasse diagram containing propositions with the logical consequence relation, one usually put falsehood, at the bottom of the diagram, mostly because from a falsity, any statement follows.