Nonexistence of independent axiomatization of a theory in a finite language. This is a follow up to two previous questions. I mistakenly thought that the theory  of infinite sets in the language of equality had no axiomatization that was non-redundant. Now I am led to whether there is a theory in a finite language (necessarily non-finitely axiomatizable) that has no non-redundant axiomatization. Is there?
 A: 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). See also Wojtylak's survey paper Independent axiomatizability of sets of sentences.

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. The only papers I know of are Hjorth/Souldatos building off of X. Caicedo giving some positive results for $\mathcal{L}_{\omega_1,\omega}$, and Wojtylak's survey mentioned at the top of this answer (note that Wojtylak postdates all the others except Hjorth/Souldatos, which doesn't refer to it), but that's it as far as I'm aware.
