Redundant proof

Summary

In mathematical logic, a redundant proof is a proof that has a subset that is a shorter proof of the same result. In other words, a proof is redundant if it has more proof steps than are actually necessary to prove the result. Formally, a proof $\psi$ of $\kappa$ is considered redundant if there exists another proof $\psi^{\prime}$ of $\kappa^{\prime}$ such that $\kappa^{\prime}\subseteq\kappa$ (i.e. $\kappa^{\prime} \;\text{subsumes}\; \kappa$) and $|\psi^{\prime}|<|\psi|$ where $|\varphi|$ is the number of nodes in $\varphi$.