Disproving well-quasi-order by providing an infinite anti-chain I am currently studying the theory behind Well-Quasi-Orders. However I am having some issues in understanding how an infinite   anti-chain can be produced to disprove the claim that a partial order $P$ is a w.q.o.

In particular I am wondering whether it is  logically sound to   present  as proof not the infinite anti-chain  but rather an algorithm to produce it.

More specifically, I've been trying to solve  an exercise from the following lecture
which asks whether the class of $P_{3}\text{-free}$ graphs is a w.q.o or not on the induced subgraph operation $\leq_{i}$

I've proved that said class contains unions of  cliques and defined an ordering of this set as follows  $P=\lbrace G_{0},G_{1},G_{2},.... \rbrace$ with $G_{i}$ representing all  $P_{3}\text{-free}$ graphs on $i$ vertices  (and graphs in $G_{i}$  being  represented in a  touple-like alpharithmetic form $(a_{1},....,a_{i})$ such that $a_{1} \leq a_{2} \leq.... \leq a_{i}$ to avoid repetitions and $\sum_{j=1}^{i} a_{j}=i$ to define  an order. For example $(0,0,2,2)$ $\in G_{4}$  encodes the graph with two disconnected $P_{2}$ components.

I have defined an algorithm $B$ that produces an anti-chain that grows bigger and bigger at each step

The algorithm uses gadgets  defined as $B_{a,c}$ which  represent the graph  with $c+1$ connected components, the first $c$ of which are $K_{1}$(i.e a sole vertice) and the last component representing $K_{a}$

The steps of my algorithm are the following:


Define $L$ as the sequence
Add $B_{a,0}$ to $L$    ($a$ any number $&gt;$ 0)
repeat $\infty$ times:

4.Replace each  item  $B_{a,c} \in L$ by $B_{a^{'}=a+1 + 10^{6},c}$ and produce $L^{'}$  this way.  

5.Let $X=B_{a^{'},c}$ be the graph with the maximum $c$  amongst those in $L^{'}$

6.Add to $L=L^{'}$ the graph $B_{a^{'}-2,c+1}$


Certainly, this algorithm does create an   anti-chain( in each step I create a graph with more connected components yet less  vertices). However I am not sure that such  a technique is valid for disproving w.q.o  on the infinite anti-thesis claim because of the fact that it works on a step by step basis.

Any help is appreciated. Thank you very much!
Your algorithm produces an infinite sequence of antichains whose size is unbounded. However, it doesn't produce a single antichain of infinite size.

It is perfectly fine to specify an infinite chain by giving an algorithm that enumerates its members, and even more complicated constructions are possible (e.g. the priority method). However, the end result of the construction should be a single infinite chain rather than a sequence of antichains of unbounded size.

I suggest taking a look at Higman's lemma.