Predicate Logic - Natural deduction 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.
 A: 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,

($\land$-intro) From $A$ and $B$ infer $A\land B$.

tells you that $A\land B$ is at most as strong as the combination of $A$ and $B$, whereas

($\land$-elim) From $A\land B$ infer $A$ or $B$.

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

From $\bot$ infer $A$ or $B$.

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.
