A "T" that interprets arithmetic is ω-inconsistent if, for some property "P" of natural numbers (defined by a formula in the language of "T"), "T" proves "P"(0), "P"(1), "P"(2), and so on (that is, for every standard natural number "n", "T" proves that "P"("n") holds), but "T" also proves that there is some natural number "n" (necessarily nonstandard) such that "P"("n") "fails". This may not generate a contradiction within "T" because "T" may not be able to prove for any "specific" value of "n" that "P"("n") fails, only that there "is" such an "n".