We prove a finite model theorem and infinitary completeness result for the propositional -calculus. The construction establishes a link between finite model theorems for propositional program logics and the theory of well-quasi-orders.