It's a [standard exercise](https://math.stackexchange.com/a/3289290/28111) to show that every *countable* first-order theory has an irredundant axiomatization. For *uncountable* first-order theories, the result is much more difficult and was [proved by Reznikoff](https://arxiv.org/abs/1108.5171). For $\mathcal{L}\_{\omega\_1,\omega}$, I believe the state-of-the-art for the analogous question is due to [Hjorth/Souldatos](https://arxiv.org/abs/1012.3422) following [X. Caicedo](https://math.uniandes.edu.co/archivos/publicaciones/IndependentsetsofaxiomsinL-kappa,alpha.pdf), *Independent sets of axioms in $L\_{\kappa,\alpha}$*, Canadian Mathematical Bulletin 22 (1981), 219–223.


I don't recall seeing anything, however, about *second-order* logic:



> 
> Suppose $T$ is a second-order theory - of arbitrary cardinality, in an arbitrary language. Must there be a second-order theory $S$ in the same language such that $(i)$ $S$ and $T$ are semantically equivalent (= have the same classes of models) but $(ii)$ no proper subset of $S$ is semantically equivalent to $S$?
> 
> 
> 


Again the countable case is easy, but the uncountable case is unclear to me (at a glance I don't think Reznikoff's argument generalizes). More generally, I'd be interested in any sources treating the "irredundance property" in a broader class of logics than just the $\mathcal{L}\_{\kappa\lambda}$s.



Do second-order theories always have irredundant axiomatizations?
Here is a proof of Reznikoff’s theorem I found among my notes, not quite following Reznikoff’s proof. I stared at it for a while, and it seems to apply to second-order logic just the same; in fact, the only property of first-order logic it uses is that any sentence contains only finitely many non-logical symbols, and there are only countably many sentences in any given finite language. Let me know if I missed something.


We say that a theory $T$ in a language $L$ *depends* on a predicate or function symbol $s\in L$ if there are models $A\models T$, $B\let\nmodels\nvDash\nmodels T$ such that $A\let\res\restriction\res(L\let\bez\smallsetminus\bez\{s\})=B\res(L\bez\{s\})$. Let $L\_T$ denote the set of symbols $s\in L$ on which $T$ depends. If $L'\subseteq L$, let $T\res L'$ be the set of $L'$-sentences valid in $T$.



> 
> **Lemma 1:** If $A\models T$ and $A\res L\_T=B\res L\_T$, then $B\models T$.
> 
> 
> 


**Proof:** Fix $\phi\in T$, we will show $B\models\phi$. Let $\{s\_i:i<n\}$ enumerate the symbols of $L\bez L\_T$ occurring in $\phi$, and for $i\le n$, let $A\_i$ denote $A$ with the interpretation of $s\_j$ changed to $s\_j^B$ for each $j<i$. Applying $n$ times the definition of $L\_T$, we see that $A\_i\models T$ for each $i\le n$, thus $A\_n\models\phi$. But $A\_n$ and $B$ agree on all symbols that occur in $\phi$, hence $B\models\phi$. **QED**



> 
> **Lemma 2:** $T\res L\_T$ is equivalent to $T$.
> 
> 
> 


**Proof:**
For every $L$-sentence $\phi$, we define an $L\_T$-sentence $\phi'$ by replacing all predicates $P\in L\bez L\_T$ with $\bot$, and all functions $F\in L\bez L\_T$ by a fixed fresh variable $x$, and putting a universal quantifier $\forall x$ in front of the whole formula. Similarly, if $A$ is an $L\_T$-model and $c\in A$, we define an $L$-model $A\_c$ expanding $A$ by $P^{A\_c}=\varnothing$ and $F^{A\_c}(\vec a)=c$. Clearly,
$$A\models\phi'\iff\forall c\in A\:A\_c\models\phi.$$
If $T\models\phi$ and $A\models T$, then $(A\res L\_T)\_c\models T$ for each $c\in A$ by Lemma 1, hence $(A\res L\_T)\_c\models\phi$, and $A\models\phi'$. That is, if $T\models\phi$, then $\phi'\in T\res L\_T$.


Consequently, if $A\res L\_T\models T\res L\_T$, then $A\res L\_T\models\{\phi':T\models\phi\}$, i.e., $(A\res L\_T)\_c\models T$ for any $c\in A$, and therefore $A\models T$ by Lemma 1. Thus, every model of $T\res L\_T$ is a model of $T$. **QED**


**NB:** Alternatively, Lemma 2 can be proved using the Craig interpolation lemma.



> 
> **Lemma 3:** If $T$ depends on $\kappa\ge\omega$ symbols, there exist models $\{A\_\alpha:\alpha<\kappa\}$ and sentences $\{\phi\_\alpha:\alpha<\kappa\}$ valid in $T$ such that
> 
> 
> $$A\_\alpha\models\phi\_\beta\iff\alpha\ne\beta\tag1$$
> 
> 
> for all $\alpha,\beta<\kappa$, and
> 
> 
> $$T\models\phi\implies\{\alpha<\kappa:A\_\alpha\nmodels\phi\}\text{ is finite}\tag2$$
> for all sentences $\phi$.
> 
> 
> 


**Proof:**
Assume that $T$ depends on all symbols in $\{s\_\alpha:\alpha<\kappa\}$, and pick models $A\_\alpha\nmodels T$, $A'\_\alpha\models T$ such that $A\_\alpha$ and $A'\_\alpha$ differ only in the interpretation of $s\_\alpha$. For each $\alpha<\kappa$, fix a sentence $\xi\_\alpha$ such that $T\models\xi\_\alpha$ and $A\_\alpha\nmodels\xi\_\alpha$.


Since $A'\_\alpha\models T$, we see that $A\_\alpha\nmodels\phi$ for $T\models\phi$ can only happen when $s\_\alpha$ appears in $\phi$. Since only finitely many symbols appear in $\phi$, this implies (2). Moreover, considering $\phi=\xi\_\alpha$, it implies that for each $\alpha<\kappa$, only finitely many $A\_\beta$ can satisfy the same sentences as $A\_\alpha$, thus there are $\kappa$ inequivalent models on the list; w.l.o.g., we may assume that $A\_\alpha\not\equiv A\_\beta$ whenever $\beta\ne\alpha$.


Fix $\alpha<\kappa$. We already know that $\{\beta\ne\alpha:A\_\beta\nmodels\xi\_\alpha\}$ is finite; let us enumerate it as $\{\beta\_{\alpha,i}:i<n\_\alpha\}$. For each $i<n\_\alpha$, we fix a sentence $\zeta\_{\alpha,i}$ such that $A\_{\beta\_{\alpha,i}}\models\zeta\_{\alpha,i}$ and $A\_\alpha\nmodels\zeta\_{\alpha,i}$. Then we put


$$\phi\_\alpha=\xi\_\alpha\lor\bigvee\_{i<n\_\alpha}\zeta\_{\alpha,i},$$


and observe that it makes (1) hold. **QED**



> 
> **Theorem:** Every theory $T$ has an independent axiomatization.
> 
> 
> 


**Proof:**
Put $\kappa=|L\_T|$, and assume first that $\kappa$ is infinite. Let $\{A\_\alpha:\alpha<\kappa\}$ and $\{\phi\_\alpha:\alpha<\kappa\}$ be as in Lemma 3. Enumerate $T\res L\_T$ as $\{\chi\_\alpha:\alpha<\kappa\}$, and define


$$\begin{align\*}
\psi\_\alpha&=\Bigl(\let\ET\bigwedge\ET\_{\beta\colon A\_\beta\nmodels\chi\_\alpha}\phi\_\beta\Bigr)\to\chi\_\alpha,\\
S&=\{\phi\_\alpha\land\psi\_\alpha:\alpha<\kappa\}.
\end{align\*}$$
Since $T\equiv T\res L\_T$ by Lemma 2, it is clear that $S\equiv T$. Moreover, $A\_\alpha\models\phi\_\beta\land\psi\_\beta$ for $\beta\ne\alpha$, but $A\_\alpha\nmodels\phi\_\alpha$, hence $S$ is independent.


If $\kappa$ is finite, $T$ has a countable axiomatization $\{\phi\_n:n<\omega\}$ by Lemma 2. Put


$$\begin{align\*}
\psi\_n&=\Bigl(\ET\_{i<n}\phi\_i\Bigr)\to\phi\_n,\\
S&=\{\psi\_n:n\in\omega,\text{ $\psi\_n$ is not logically valid}\}.
\end{align\*}$$


Since $\ET\_{i\le n}\psi\_i$ is equivalent to $\ET\_{i\le n}\phi\_n$, $S\equiv T$. Moreover, since $\psi\_n\in S$ is not valid, there is $A\_n\models\neg\psi\_n$. This means $A\_n\models\phi\_i$ for $i<n$ and $A\_n\models\neg\phi\_n$, which implies $A\_n\models\{\psi\_i:i\ne n\}$. Thus, $S$ is independent. **QED**


