The Arithmetized Completeness Theorem is a formalization of Goedel's Completeness Theorem within arithmetic. It is one of the most powerful tools in constructing end extensions of models of arithmetic. In this talk, I will present some non-standard applications about expansions and omega-submodels that satisfy the Weak Koenig Lemma. I will discuss, in particular, the problems one has to face when, instead of
Sigma1-induction, we only have Sigma1-collection with exponentiation. This research is joint with Ali Enayat in Gothenburg.