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.

enter image description here

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

  • $\begingroup$ 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... $\endgroup$
    – nir shahar
    Commented Jul 21, 2021 at 8:28
  • 2
    $\begingroup$ 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' $\endgroup$
    – Silver
    Commented Jul 21, 2021 at 10:05
  • $\begingroup$ Haha. I see your point. Without the brackets it is less appropriate: $\bot$ $\endgroup$ Commented Jul 22, 2021 at 1:14

1 Answer 1


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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.