Излишнее доказательство

Эта статья может быть слишком технической для понимания большинства читателей . Пожалуйста, помогите улучшить ее, чтобы сделать ее понятной для неспециалистов , не удаляя технические детали. ( Апрель 2014 ) ( Узнайте, как и когда удалять это сообщение )

В математической логике избыточное доказательство — это доказательство , имеющее подмножество, которое является более коротким доказательством того же результата. Другими словами, доказательство избыточно, если оно имеет больше шагов доказательства, чем фактически необходимо для доказательства результата. Формально доказательство считается избыточным, если существует другое доказательство , такое что (т.е. ) и где — число узлов в . ^[1]${\displaystyle \пси}$${\displaystyle \каппа}$${\displaystyle \psi ^{\prime }}$${\displaystyle \ каппа ^ {\ prime }}$${\displaystyle \каппа ^{\prime }\subseteq \каппа }$${\displaystyle \ каппа ^ {\ prime } \; {\ text {subsumes}} \; \ каппа }$${\displaystyle |\psi ^{\prime }|<|\psi |}$${\displaystyle |\varphi |}$${\displaystyle \varphi}$

Доказательство, содержащее поддоказательство форм (здесь пропущенные опорные точки ^{[ необходимо дополнительное объяснение ]} указывают на то, что резольвенты должны быть определены однозначно)

${\displaystyle (\eta \odot \eta _{1})\odot (\eta \odot \eta _{2}) {\text{ или }}\eta \odot (\eta _{1}\odot ( \eta \odot \eta _{2}))}$

локально избыточно.

Действительно, оба этих поддоказательства могут быть эквивалентно заменены более коротким поддоказательством . В случае локальной избыточности пары избыточных выводов, имеющих один и тот же опорный элемент, встречаются в доказательстве близко друг к другу. Однако избыточные выводы могут также встречаться далеко друг от друга в доказательстве.${\displaystyle \eta \odot (\eta _ {1} \ odot \eta _ {2})}$

Следующее определение обобщает локальную избыточность, рассматривая выводы с той же точкой опоры, которые происходят в разных контекстах. Мы пишем для обозначения контекста доказательства с одним заполнителем, замененным на поддоказательство .${\displaystyle \psi \left[\eta \right]}$${\displaystyle \psi \left[-\right]}$${\displaystyle \эта}$

Доказательство

${\displaystyle \psi [\psi _{1}[\eta \odot _{p}\eta _{1}]\odot \psi _{2}[\eta \odot _{p}\eta _{2 }]]{\text{ или }}\psi [\psi _{1}[\eta \odot _{p}(\eta _{1}\odot \psi _{2}[\eta \odot _{ p}\eta _{2}])]]}$

потенциально (глобально) избыточно. Более того, оно (глобально) избыточно, если его можно переписать в одно из следующих более коротких доказательств:

${\displaystyle \psi [\eta \odot _{p}(\psi _{1}[\eta _{1}]\odot \psi _{2}[\eta _{2}])]{\text { или }}\eta \odot _{p}\psi [\psi _{1}[\eta _{1}]\odot \psi _{2}[\eta _{2}]]{\text{ или }}\psi [\psi _{1}[\eta _{1}]\odot \psi _{2}[\eta _{2}]].}$

Доказательство

${\displaystyle {\cfrac {{\cfrac {{\cfrac {\eta :\,p,q\,\,\,\,\eta _{1}:\,\neg p,r}{q,r}}p\,\,\,\,\,\,{\begin{array}{c}\\\eta _{3}:\,\neg q\end{array}}}{r}}q\,\,\,\,\,\,\,\,\,\,\,\,\,\,{\cfrac {{\cfrac {\eta \,\,\,\,\,\,\,\,\,\,\,\,\,\,\eta _{2}:\,\neg p,s,\neg r}{q,s,\neg r}}p\,\,\,\,{\begin{array}{c}\\\eta _{3}\end{array}}}{s,\neg r}}q}{\psi :\,s}}r}$

локально избыточно, так как является экземпляром первого шаблона в определении${\displaystyle ((\eta \odot _{p}\eta _{1})\odot \eta _{3})\odot ((\eta \odot _{p}\eta _{2})\odot \eta _{3}).}$

• Узор такой${\displaystyle \psi [\psi _{1}[\eta \odot _{p}\eta _{1}]\odot \psi _{2}[\eta \odot _{p}\eta _{2 }]]}$
• ${\displaystyle \psi _{1}[-]=\psi _{2}[-]=\_\odot \eta _{3}{\text{ и }}\psi [-]=\_}$

Но это не глобально избыточно, поскольку заменяющие термины согласно определению содержат во всех случаях и не соответствуют доказательству. В частности, ни то, ни другое не может быть разрешено с помощью , поскольку они не содержат литерала .${\displaystyle \psi _{1}[\eta _{1}]\odot \psi _{2}[\eta _{2}]}$${\displaystyle \psi _{1}[\eta _{1}]\odot \psi _{2}[\eta _{2}]=(\eta _{1}\odot \eta _{3}) \odot (\eta _{2}\odot \eta _{3})}$${\displaystyle \эта _{1}}$${\displaystyle \эта _{2}}$${\displaystyle \эта _{3}}$${\displaystyle д}$

Вторая модель потенциально глобально избыточных доказательств, появляющаяся в определении глобальной избыточности, связана с хорошо известным ^{[ требуется дальнейшее объяснение ]} понятием регулярности ^{[ требуется дальнейшее объяснение ]} . Неформально, доказательство является нерегулярным, если существует путь от узла к корню доказательства, такой, что литерал используется более одного раза в качестве опорной точки на этом пути.