Идемпотентность следствия - Idempotency of entailment

Идемпотентность следствия является собственностью логические системы который гласит, что можно вывести те же последствия из многих примеров гипотезы, что и из только одной. Это свойство может быть захвачено структурное правило называется сокращение, и в таких системах можно сказать, что логическое следствие является идемпотент тогда и только тогда, когда сжатие допустимая норма.

Правило сокращения: от

А,C,C → B

выводится

А,C → B.

Или в последовательное исчисление обозначение

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

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

Смотрите также

• Теорема о запрете удаления