---
tag: FFH6M3M077
kind: concept
name: Redundant proof
sources:
  - wikipedia: en:42158532@r1191444096
    locator: Redundant proof
    note: adopted
    mention: wikipedia://en/42158532
    sections: [Summary]
same_as:
  wikidata: Q15964428
  wikipedia: Redundant proof
inventory: [MG1QZ4NM1A]
---

## Summary

In mathematical logic, a **redundant proof** is a [[proof|0B94TKFQJX]] 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$.