The Wikipedia article on WQOs does not mention a strict version. I came across a particular relation, which I could only describe as a strict WQO, but I am wondering if my reasoning is correct and if the notion of a "strict WQO" even makes sense (I think it does).
Consider the set $X \times \mathbb{N}$ where $X = \{1,\ldots,k\}$ for some integer $k$ and $\mathbb{N}$ denotes the set of natural numbers. We define the relation $\prec$ as: $$ (x_1,n_1) \prec (x_2,n_2) \quad \text{iff} \quad (x_1 \leq x_2) \wedge (n_1 < n_2) $$
Strict Quasi Order: Clearly $\prec$ is irreflexive and transitive, and therefore a strict quasi order.
No Infinite Antichains: It's also easy to observe that there are no infinite antichains. Due to the Pigeonhole principle, any sequence $(x_1,n_1), (x_2,n_2), \ldots$ of length $\geq k$ must have at least one pair $\langle (x_i,n_i),(x_j,n_j)\rangle$ such that $x_i = x_j$. Then, since either $n_i < n_j$ or $n_j < n_i$ must hold, we have at least one pair in the sequence on which $\prec$ holds.
Well-Foundedness: Finally, we show that there are no infinite descending chains. For any element $(i,j)$, there are only $|\{1,\ldots,i\} \times \{1,\ldots,(j-1)\}| = i(j-1)$ elements that can precede $(i,j)$.
Is this reasoning correct? Then is $\prec$ a strict WQO on $X \times \mathbb{N}$?
Related questions: Since antisymmetry is implied by irreflexivity and transitivity, is any strict quasi order also a strict partial order? And so is any strict WQO also a strict WPO?
Thanks.
If $\leq$ is any relation, let $<$ be the strict version when $x<y$ if and only if ($x\leq y$ and $x\neq y$). There's really not much more to defining a strict relation. Note that we can alternatively start with $<$ and define $x\leq y$ as ($x<y$ or $x=y$).
So, to check that your $\prec$ relation is a strict WQO, we define $\preceq$ as $x\preceq y$ if and only if ($x\prec y$ or $x=y$).
Now, the relation $\preceq$ is antisymmetric as well: if $(x,n)\neq(y,m)$ and $(x,n)\preceq(y,m)$, then $n<m$, thus $m\not <n$, thus $(y,m)\not\preceq(x,n)$. Therefore $\preceq$ is in fact a WPO.
It is true that antisymmetry is implied by irreflexivity and transitivity. However, it is not true that a strict WQO is transitive.
As a very simple example, take $\{a,b\}$ with the universal relation ${\trianglelefteq}=\{(a,b),(b,a),(a,a),(b,b)\}$. It is easy to see this is a WQO and not a WPO. However, the strict relation $\triangleleft=\{(a,b),(b,a)\}$ is no longer transitive.