Why are [W-types](https://ncatlab.org/nlab/show/W-type) called "W"?


Probably "W" means either "wellordered" or "wellfounded". ([Martin-Löf](https://www.csie.ntu.edu.tw/~b94087/ITT.pdf) uses the term "wellorder".) But these are notions associated to order theory, whereas W-types don't directly have to do with order relations (if at all).



Why are W-types called "W"?
You write:



> 
> Probably "W" means either "wellordered" or "wellfounded". […] But these are notions associated to order theory, whereas W-types don't directly have to do with order relations (if at all).
> 
> 
> 


I don’t know an official source for this, but I’ve always assumed W stands for “well-founded” as you suggest. *(Edit: I asked Per Martin-Löf, and he confirmed that this was what he meant by it.)* The justification for this is several-fold.


On the one hand, W-types do naturally carry well-founded partial orders (the *structurally smaller* relation), and the recursion/induction principles of W-types can be seen as well-founded induction over these orders.


On the other hand, well-foundedness was originally defined and developed to analyse and explain induction principles — it ended up becoming part of “order theory”, but it was motivated by Cantor’s analysis of induction. W-types give an alternative analysis of induction principles, not starting with an order relation — so as such, they can be seen as an alternative exploration of the original intention of well-foundedness.


And on the third hand, an important way of viewing W-types is as *types of well-founded labelled trees*, in exactly the traditional order-theoretic sense of *well-founded trees*. This can be made precise in two directions. If you are modelling type theory with W-types inside set theory (or indeed any other foundation without native inductive types), one way to model W-types is to define them as sets of isomorphism classes of suitably-labelled well-founded trees. On the other hand, inside type theory, you can associate to each element of a W-type a well-founded labelled tree, and show that elements of the W-type correspond precisely to isomorphism classes of such trees.


