When can we have "each subtheory is satisfiable iff it is recursively axiomatizable"?

Question

Weak Version: Is there a 1st order language $L$ (with only countably-many formulas) such that for each recursive coding $C$ of the formulas of $L$, there is a theory $T$ of $L$ where

1. $T$ is not satisfiable,

2. every $C$-recursive proper subtheory of $T$ (meaning the set of $C$-codes of the sentences in the subtheory is not recursive) is satisfiable, and

3. every proper subtheory of $T$ that isn’t $C$-recursive is unsatisfiable?

Strong Version: Is there a 1st order language $L$ (with only countably-many formulas) such that there is a theory $T$ of $L$ where

4. $T$ is not satisfiable,

5. every recursively axiomatizable proper subtheory of $T$ is satisfiable, and

6. every proper subtheory of $T$ that isn’t recursively axiomatizable is unsatisfiable?

Restricting to languages with only countably-many formulas excludes uncountable theories (which trivially fail to be recursively axiomatizable), but this restriction could be relaxed if we require that the theory T also be countable.

Answer 1

Perhaps this is the kind of example for which you are searching.

Let's use the logic $L_{\omega_1,\omega}$, which allows for countable conjunctions and disjunctions. Let $A\subset\mathbb{N}$ be any infinite set with no infinite computably enumerable subset. In the language with a constant symbol $c$ and infinitely many constant symbols $d_i$ for $i\in\mathbb{N}$, let $T$ be the theory consisting of the axioms:

• $\bigvee_{j\in\mathbb{N}} c=d_j$.
• the axiom $\sigma_i=\bigwedge_{j\leq i} c\neq d_j$, where $i$ is any element of $A$.

The first axiom is a single assertion in $L_{\omega_1,\omega}$. The second item is a list of infinitely many first-order axioms $\sigma_i$, one for each $i\in A$.

The theory is not satisfiable, since in any model of the theory, $c$ must be interpreted as one of the $d_j$'s, but it cannot be interpreted as any particular $d_j$, by the second axiom.

But I claim that any computable subset of the axioms is satisfiable, and indeed, any c.e. subset of the axioms is decidable. The reason is that if $S\subset T$ is c.e., then $S$ must involve only finitely many of the axioms $\sigma_i$, for otherwise, we could computably enumerate an infinite c.e. subset of $A$, which is impossible since $A$ contains no such set. So $S$ has only finitely many $\sigma_i$, and so forbids $c$ from only finitely many $d_j$'s, and so we can easily build a model of $S$. Indeed, the model needs to have only two elements.