When can we have "each subtheory is satisfiable iff it is recursively axiomatizable"? 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


*

*$T$ is not satisfiable,

*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

*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


*$T$ is not satisfiable,

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

*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.
 A: 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.
