Does the set of inference rules of Gentzen’s Natural Deduction have redundancy in the sense that without some rule of the system it can still be complete?
My thoughts: I came across this question and could not form a bold argument whether there is redundancy in the system or not. Note that specifically, inference rules of Gentzen’s Natural Deduction include $\forall$-intro, $\forall$-elim, $\exists$-intro, $\exists$-elim, $\wedge$-intro, $\wedge$-elim, $\lor$-intro, $\lor$-elim, $\Rightarrow$-intro, $\Rightarrow$-elim, $\neg$-intro, and $\neg$-elim.
There is no such redundancy, and here's an idea how to prove it.
[EDIT: I rephrased the argument to make it, hopefully, more intuitive.]
Let us focus just on the connective $\land$ for simplicity. Put yourself in the mind of someone who does not know what the expression $A\land B$ means, but wants to find out by looking at the Natural Deduction rules. One way you can read the introduction and elimination rules for $\land$ is that they impose lower and upper bounds on the logical strength of the expression $A\land B$. For example,
tells you that $A\land B$ is at most as strong as the combination of $A$ and $B$, whereas
tells you that $A\land B$ is at least as strong as both $A$ and $B$.
Assume now you omit the rule ($\land$-intro). The resulting system tells you no upper bound on the logical strength of the expression $A\land B$. So intuitively, $A\land B$ could be anything which is at least as strong as $A$ and $B$. But then nothing prevents you from interpreting $A\land B$ in the resulting system as the strongest possible expression: a logical contradiction ($\bot$ if this atom is contained, or otherwise $p\land\lnot p$ for some fresh variable $p$). Note in particular that in replacing $A\land B$ by $\bot$ in ($\land$-elim), you obtain the sound rule
It follows that you cannot prove anything in the system which contradicts the interpretation of $A\land B$ as a contradiction. For example, the theorem $q\rightarrow (q\land q)$ will not be provable because $q\rightarrow \bot$ is not valid.
To make this intuition into a formal argument, consider a translation $\pi$ which replaces every subformula $A\land B$ in a formula by $\bot$. Then you can show by induction on proof length that if a formula $F$ is provable in Natural Deduction without the rule ($\land$-intro), then $\pi(F)$ is provable in Natural Deduction without ($\land$-intro) as well. It follows that the theorem $q\rightarrow (q\land q)$ is not provable without ($\land$-intro), as then so would be $\pi(q\rightarrow (q\land q))=q\rightarrow \bot$, which is not valid. Hence Natural Deduction without ($\land$-intro) is incomplete.
A similar argument can be found for the omission of other rules.