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



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


