Consistent, but $ω$-contradictory first-order theory? Can anyone give an example of consistent, but $ω$-contradictory first-order theory?
In his formulation of the incompleteness theorem, Gödel used the notion of an $ω$-consistent formal system, a stronger condition than mere consistency. A formal system is called $ω$-consistent if, for any formula $A(x)$ of this system, it is impossible to simultaneously derive the formulas $A(0)$, $A(1)$, $A(2)$, … and $∃x ¬A(x)$ (in other words, from the fact that for every natural number n the formula A(n) is derivable, it follows that the formula $∃x ¬A(x)$ is not derivable).
 A: I've ever given two two examples in my book.
Example 1. Let $n$ be a constant symbol for all $n\in\mathbb{N}$ and $c$ a new constant symbol. Then the theory generated by $\mathsf{PA}\cup\{c\neq n\mid n\in\mathbb{N}\}$ is consistent but $\omega$-inconsistent (which is usually used instead of $\omega$-contradictory).
Proof. Since the theory produced by $\mathsf{PA}\cup\{c\neq n\mid n\in\mathbb{N}\}$ is finitely satisfiable, then by compactness it's  satisfiable, and hence by completeness consistent. And the formula $c=x$ is a witness that it's $\omega$-inconsistent.
Example 2. Let $T$ be a recursively enumerable (or recursively axiomatizable) and consistent theory. Then the theory generated by $T\cup\{T\text{ is inconsistent}\}$ is consistent but $\omega$-inconsistent. Clearly $\mathsf{PA}$ is a typical instance of $T$, and note that "$T$ is inconsistent" is a sentence in first-order language not a sentence in natural language.
Proof. By Gödel's Second Incompleteness Theorem, we have $T\not\vdash\text{"}T\text{ is consistent}\text{"}$, and hence $T\cup\{\neg(T\text{ is consistent})\}$ is consistent, i.e., $T\cup\{T\text{ is inconsistent}\}$ is consistent. To see it's $\omega$-inconsistent, the formula $\mathsf{Proof}_{T\cup\{T\text{ is inconsistent}\}}(x,\ulcorner\bot\urcorner)$ is the witness (it needs some more details which are already existed in my book).
A: A footnote to M. Logic.
Here's another freely available resource which spells things out. You can download my intro to Gödel's theorems book from https://www.logicmatters.net/igt -- then take a look at the key §21.6.
There is obviously a lot more in the book which is relevant too!
