Is there a non-finitely axiomatizable theory in a finite language with an independent set of axioms? Let $L$ be a finite language, and $T$ an $L$-theory that is not finitely axiomatizable. Can it ever be the case that there is a subset $S$ of $T$ with the same consequences as $T$, but such that every axiom of $S$ is non-redundant? Certainly, in some cases, like the theory of infinite sets in the language of pure equality, there is no independent set of axioms.
 A: Yes, there is: consider the theory $T$ in the language of a single binary relation $R$, consisting of - for each $n\in\mathbb{N}$ - the sentence $\varphi_n$ asserting that there is an $R$-cycle of length $n$. Precisely: $\varphi_n$ is the sentence asserting that there are $x_1,...,x_n$ such that for $1\le i,j\le n$, $R(x_i,x_j)$ holds iff $i=n, j=1$ or $i+1=j$.

Here's a brief explanation of why $T$ is not redundant. For each $n\in\mathbb{N}$ consider the structure $\mathcal{A}_n$ consisting of the disjoint union of $k$-cycles for each $k\not=n$. This is a model of $\{\varphi_k: k\not=n\}$ but doesn't satisfy $\varphi_n$ - the point being that large cycles do not have small sub-cycles. So removing any sentence from $T$ results in a theory with strictly more models - that is, a strictly weaker theory.

And here's two ways to see why $T$ is not finitely axiomatizable:
The easiest argument (and contra an earlier comment of mine) is to simply apply the irredundance of the specific axiomatization $T$ above, together with the compactness theorem: it's a good exercise to show that in a compact logic no finitely axiomatizable theory has an irredundant infinite axiomatization.
A more "hands-on" argument can be given by Ehrenfeucht-Fraisse games. Roughly, it proceeds as follows. Let $\mathcal{S}$ be the "obvious model" of $T$ - the disjoint union of a single $n$-cycle for each $n\in\mathbb{N}$. For each $n$ we can then consider the "truncation" of $\mathcal{S}$ - for each $k>n$ we replace each $k$-cycle in $\mathcal{S}$ by a "$\mathbb{Z}$-chain." It's a standard exercise to show (usually via Ehrenfeucht-Fraisse games) that for each $a$ there is some $b$ such that $\mathcal{S}_b$ and $\mathcal{S}$ satisfy the same $a$-quantifier sentences.  (In fact in the course of this proof we compute $b$ exactly, but I'm lazy and am not going to do that. If you want a concrete value, certainly $b=2^{2^{a+17}}$ is more than large enough.) But this means that no single sentence can hold in $\mathcal{S}$ while failing in each $\mathcal{S}_n$; and this proves the claim, since $\mathcal{S}\models T$ but $\mathcal{S}_n\not\models T$ for each $n\in\mathbb{N}$.
