$\omega$-consistency and related terms

We know that a theory $T$ is $\omega$-inconsistent if there is a formula $\psi$ such that $T$ proves $(\exists x)\psi(x)$, and $T$ also proves $\lnot \psi(n)$ separately for each standard natural number $n$. So $T$ is $\omega$-consistent if it is not $\omega$-inconsistent.

Is there a name for the following property: if for every formula $\psi$ such that $\psi(0), \psi(1), \psi(2),...$ can be proven in $T$, then $\forall x \psi(x)$ can be proven in $T$ ?

And what is the connection between this property and $\omega$-inconsistency / consistency?

Thank you.

-

In my Gödel book §21.6, I give the following definition, which I took/take to be pretty standard terminology:

An arithmetic theory $T$ is $\omega$-incomplete iff, for some open wff $\varphi\mathsf{(x)}$, $T$ can prove each $\varphi\mathsf{(\overline{m})}$ but $T$ can't go on to prove $\forall \mathsf{x}\varphi\mathsf{(x)}$.

So if $T$ is able to prove $\forall \mathsf{x}\varphi\mathsf{(x)}$ when $T$ can prove each $\varphi\mathsf{(\overline{m})}$, for any $\varphi\mathsf{(x)}$, then $T$ would (as Luca says) naturally be called $\omega$-complete.

What is the connection between $\omega$-incompleteness and $\omega$-inconsistency? Well, we can say this:

$\omega$-incompleteness in a theory of arithmetic is a regrettable weakness; if $T$ can prove each $\varphi\mathsf{(\overline{m})}$ it would be very nice if $T$ were always able to prove $\forall \mathsf{x}\varphi\mathsf{(x)}$ too. Sadly, Gödel's incompleteness theorem tells us that, surprisingly, nice enough theories $T$ can't be this nice! By contrast $\omega$-inconsistency is not just a regrettable weakness but a Very Bad Thing indeed (not quite as bad as outright inconsistency, maybe, but still bad). For evidently, a theory that can prove each of $\varphi\mathsf{(\overline{m})}$ and yet also prove $\neg\forall \mathsf{x}\varphi\mathsf{(x)}$ is just not going to be interpretable as being about the natural numbers.

-
thanks for eveyone! – user75221 Aug 14 '13 at 9:33

The rule you're referring to is called $\omega$-rule, and if you add it to the axioms and rules of inference of first-order logic you get the so called $\omega$-logic. Thus I would say that the name you're looking for is consistent with the $\omega$-rule, or consistent in $\omega$-logic. A shorter name is $\omega$-complete.

A theory $T$ has an $\omega$-model if and only if it is consistent in $\omega$-logic (see Proposition 2.2.13 in C. C. Chang and H. Jerome Keisler's Model Theory). It follows that consistency with the $\omega$-rule implies $\omega$-consistency, but it is actually a stronger condition.

-
I believe the property in the original question is that the theory is closed under the $\omega$-rule. – Carl Mummert Aug 13 '13 at 11:34