Nonexistence of independent axiomatization of a theory in a finite language.

This can't happen in any language whatsoever. This was proved by Tarski for countable languages, and by Reznikoff for uncountable languages (see the end of this answer).


For countable languages, there is a simple argument. Suppose I have a non-finitely-axiomatizable theory $T$ in a countable language. Since our language is countable we can enumerate $T$: $$T=\{\varphi_i: i\in \mathbb{N}\}.$$

First, we'll thin out $T$: let $$T'=\{\varphi_i: \bigwedge_{j<i}\varphi_j\not\vdash\varphi_i\}$$ be the set of "not-immediately-redundant" sentences in $T$. We trivially have that $T'$ is an axiomatization of $T$. This is not necessarily a redundant axiomatization, since we could have e.g. $\varphi_{17},\varphi_{42}\in T'$ with $\varphi_{42}\vdash\varphi_{17}$ still.

Enumerate $T'$ as $$T'=\{\psi_i: i\in\mathbb{N}\}.$$ We'll now "dominoize" everything: let $$\theta_i=(\bigwedge_{j<i}\psi_j)\implies\psi_i,$$ with the convention that $\theta_0=\psi_0$ (the empty hypothesis is vacuously true).

It's easy to see that $$T^*:=\{\theta_i:i\in\mathbb{N}\}$$ axiomatizes $T$, the key point being that $\bigwedge_{j\le i}\theta_j\vdash\psi_i$. I claim that $T^*$ is in addition irredundant.

To see this, fix $i\in\mathbb{N}$ and consider the sentence $$\eta_i=(\bigwedge_{j<i}\psi_j)\wedge\neg\psi_i.$$ We have $\eta_i\vdash\theta_k$ for all $k\not=i$: for $k<i$ this is built directly into $\eta_i$, and for $k>i$ this is because the hypothesis of the conditional becomes vacuous. But also clearly $\eta_i\vdash\neg\theta_i$. And finally, by definition of $T'$ we know that $\eta_i$ is consistent and hence $\eta_i\not\vdash\theta_i$. Putting this all together we get $$\{\theta_k: k\not=i\}\not\vdash\theta_i$$ as desired.


What about uncountable languages? The above argument breaks down almost immediately when we try to generalize it in this way.

It turns out that this broader question was answered by Reznikoff in 1965: every first-order theory has a non-redundant axiomatization. Reznikoff's paper is in French, and an English version of the argument was presented by Souldatos a while ago. An interesting feature of the argument is the role of Craig's interpolation theorem. The non-triviality of this result leads naturally to further questions about irredundancy in other logics, and I think a lot is open here; Hjorth/Souldatos, building off of X. Caicedo, gave some positive results for $\mathcal{L}_{\omega_1,\omega}$, but that's it as far as I'm aware.