Is the decidability of all possible axiomatizations equivalent to decidability?

Introduction

This is a weird take on a few different topics in logic, so bear with me.

To frame this question, consider that "axiomatization" is to "theory" as "parameterization" is to "manifold," and, bearing this in mind, define "axiomatization" as follows:

For any theory $T$, call $A\subseteq T$ an axiomatization of $T$ iff for any wff $\phi$ of $T$, $A\vdash \phi$.

The reason for using this definition in place of the usual one is to emphasize 1) the nonuniqueness of axiomatizations for a given theory, and 2) the varying "degrees" of computability of different theories. By "degree of computability" I mean the manner in which a theory may behave like a computable, recursive, decidable, etc. one without actually being computable, etc. For instance, we might extend a recursively axiomatizable theory $T$ by constructing a sufficiently "nice" function $\Phi:\Bbb R\to L'$, where $L'$ is the language of $T$ extended by $\Bbb R$-many constant symbols (indexed by real numbers), and adding $\Phi[\Bbb R]$ to the axioms of $T$. Obviously the extension is not axiomatizable in the traditional sense, since it is uncountable - but it remains "quasicomputable," for lack of a better term, in a very obvious way. Similarly, we can think of a non R.E. theory - let's say the theory of of True Arithmetic - as being "$X$-axiomatizable" for some condition $X$. I suspect that there are key properties of "well-behaved" theories that are easily explained in terms of "$X$-axiomatizability."

The Question

Let $T$ be an arbitrary and, for now, first-order theory. Trivially, $T$ is an axiomatization of $T$, so if $T$ is decidable then there is a decidable axiomatization of $T$. For the same reason, if every axiomatization of $T$ is decidable, then $T$ is decidable.

Now it is a well known result in mathematical logic that the decidability of an axiomatization does not imply the decidability of the resulting theory. However, in the event that $T$ is nondecidable it is obvious that $T$ has at least one nondecidable axiomatization - that being $T$ itself. But this alone does not suffice to show that the existence of a nondecidable axiomatization implies nondecidability. In fact, it seems plausible that every decidable theory might have a nondecidable axiomatization.

Consider that for a decidable theory $\Gamma$, we can construct a function $\Theta:\Bbb N\to\Gamma$ which enumerates the theorems of $\Gamma$. Choose an undecidable $V\subset \Bbb N$, then $\Theta[V]$ is undecidable; so at the very least every decidable theory - under a given enumeration, at least - can be shown to have an undecidable fragment. There's no obvious reason that such a fragment cannot be an axiomatization of $\Gamma$.

(As a side note, it seems reasonable that previous method of enumeration should suffice to show that every decidable theory has [globally] undecidable subsets, since there are countably many recursive enumerations and uncountably many subsets of $\Bbb N$.)

On the other hand, it seems equally plausible that every axiomatization of a decidable theory should be decidable. Consider $\Gamma$ and $V$ as above. Supposing that $V$ is never an axiomatization of $\Gamma$, let $A$ be a decidable axiomatization of $\Gamma$. Trivially, $A\cup V$ is an axiomatization of $\Gamma$, but there's nothing to suggest that $A\cup V$ is undecidable. In fact, using the same enumeration trick, we can almost always find an undecidable fragment of $\Gamma$ whose union with $A$ is decidable!

All of this leads me to the question: what if every axiomatization of $T$ is decidable? More significantly, can we that if $T$ is decidable, then every axiomatization of $T$ is decidable?

Summary of known results:

For any [first-order] theory, $T$...

1. If $T$ is decidable, then $T$ has a decidable axiomatization.

2. If $T$ is nondecidable, then $T$ has a nondecidable axiomatization.

3. If every axiomatization of $T$ is decidable, then $T$ is decidable.

4. If every axiomatization of $T$ is nondecidable, then $T$ is nondecidable.

5. $T$ contains a nondecidable subset

Solution 1:

Presburger Arithmetic is well-known to be decidable. Let $T$ be the theory of Presburger arithmetic.

Let $R$ be the usual axiomatisation of T. Of course, $R$ is decidable.

For each (external) natural number (n), let $\bar{n}$ be the term $S^n(0)$ in the vocabulary of $T$. Let $\phi_n$ be the statement $\bar{n} = \bar{n}$; clearly, each $\phi_n$ is a theorem of $T$. Also, note that $\phi_n \notin R$ by inspecting the definition of $R$.

Given any $V \subseteq \mathbb{N}$, let $\phi_V = \{\phi_n \mid n \in V\}$. Then $R \cup \phi_V$ is an axiomatisation of $T$.

But note that if $R \cup \phi_V$ is decidable, then so is $V$, since $n \in V \iff \phi_n \in R \cup \phi_V$. So if we take $V$ to be undecidable, then $R \cup \phi_V$ is an undecidable axiomatisation of the decidable theory $T$.

Solution 2:

In fact every theory has axiomatizations of arbitrarily high complexity, as follows. For example, let $$\tau_i=\forall x(x=x\wedge x=x\wedge ...\wedge x=x)\quad\mbox{($i$ conjuncts)}$$ and let $\mathsf{Triv}=\{\tau_i:i\in\mathbb{N}\}$. Then for any set of numbers $X\subseteq\mathbb{N}$ and any set of sentences $S$ the set $$S_X:=(S\setminus \mathsf{Triv})\cup\{\tau_i:i\in X\}$$ has the same deductive closure as $S$ and is at least as complicated as $X$. (To be precise: $S_X$$\ge_T$$X$, and in particular if $X$ is undecidable then $S_X$ is undecidable.)

So some further subtleties are needed to make the notion "all axiomatizations are simple" non-trivial.