Идемпотентность следствия

Идемпотентность следствия — характерное свойство формальных систем, которое заключается в том, что из множества возможных вариантов гипотезы можно вывести те же следствия, что и из конкретного её экземпляра. Данное свойство может быть отражено структурным правилом^[англ.], называемым контракцией, и в таких системах принято утверждать, что следствие является идемпотентным, тогда и только тогда, когда контракция является допустимым правилом^[англ.].

Например, если знать, что А влечёт за собой В, и С влечёт В, то можно сократить рассуждение до одного из этих утверждений и получить В.

Это правило контракции можно записать так:

A,C,C → B

отсюда выводится умозаключение,

A,C → B.

Или в системе исчисление секвенций:

${\displaystyle {\frac {\Gamma ,C,C\vdash B}{\Gamma ,C\vdash B}}}$

В линейной и аффинной логике следствие не является идемпотентным.

Пусть А означает «идёт дождь», а В означает «солнечная погода». Тогда можно вывести, что А влечёт В, если знать, что после пасмурной погоды, рано или поздно, появится солнце. Но также можно вывести, что А, А влечёт В, потому что повторение утверждения не меняет его истинности. То есть, если сегодня идёт дождь, то когда-нибудь будет солнце, и если сегодня дождь и завтра дождь, то после всех дождей, на небе появится солнце. Это значит, что следствие идемпотентно: от A → B можно перейти к A, A → B.

Допустим А означает «съедена шаурма», а В означает «прекрасное состояние». Тогда можно вывести, что А влечёт В, если допустить, что одной шаурмы достаточно для вкусного перекуса и удовлетворения потребности в пище. Но нельзя вывести, что А, А влечёт В, потому что в линейной логике нельзя использовать одно и то же утверждение дважды. То есть, если съедена одна шаурма, то голод утолён, но если [вдруг] съедено две шаурмы, то возможно произошло перенасыщение и желудок теперь излишне полный, состояние испытателя неизвестное или вовсе странное. Это значит, что следствие не идемпотентно: от A → B нельзя перейти к A, A → B.

Допустим, A означает «поцелуй спящей принцессы», а B означает «пробуждение». Тогда можно вывести, что A влечёт B, если предполагать, что поцелуй обладает волшебной силой, которая может снимать разные чары и заклятия. Но нельзя вывести, что A, A влечёт B, потому что в аффинной логике нельзя использовать одно и то же утверждение дважды. То есть, если поцеловать одну принцессу, то она проснётся, но если поцеловать сначала одну принцессу и затем, сразу же, вторую принцессу, то это может привести к неожиданным последствиям и сбою волшебства. Это значит, что следствие не идемпотентно: от A → B нельзя перейти к A, A → B.

• Теорема о недопустимости удаления^[англ.]