= Solution
Let $T$ have a <semidecidable axiomatization>. If $T$ is inconsistent, the singleton axiom set $\{\bot\}$ is decidable and independent. If $T$ has no nonlogical axioms, the empty set already works. In the remaining case assume $T$ is consistent, choose a total computable enumeration $A_1,A_2,\ldots$ of its axioms, allowing repetitions, and conservatively enlarge the language by fresh nullary predicates $P_1,P_2,\ldots$.
For each $i\geq1$, let $B_i$ be the conjunction of $i$ copies of $P_i\land A_i$. The range $\{B_i:i\geq1\}$ is decidable by the <Craig trick>. Given a candidate formula of length $m$, only indices $i\leq m$ are possible; compute $A_1,\ldots,A_m$, form the corresponding $B_i$, and compare the finite list syntactically.
The new theory has exactly the same consequences in the original language. Every model of $T$ expands to a model of all $B_i$ by interpreting every $P_i$ as true, while the reduct of any model of all $B_i$ satisfies every $A_i$. The axioms are independent: after deleting $B_i$, take any model of $T$, interpret $P_j$ as true for $j\ne i$, and interpret $P_i$ as false. This expansion satisfies every remaining $B_j$ but not $B_i$. Hence the $B_i$ form an <independent tagged axiomatization> that is decidable. Here equivalence means a conservative extension, or equivalently equality of all consequences in the original language.
Back to article page
