 Omega-consistency of an arithmetic theory

A first-order theory is omega-consistent when it never proves $\exists x\varphi (x)$ while proving $\neg \varphi (\bar{n})$ for every standard natural number $n$. Restricting the matrix to arithmetic bounded arithmetic formulas gives one-consistency. This condition concerns standard instances and is stronger tha first-order consistency.