Идемпотентность вывода

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

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

А , С , С → Б

получен

А , С → В.

{\frac {\Гамма ,C,C\vdash B}{\Гамма ,C\vdash B}}

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

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

Эта статья, связанная с логикой, является заглушкой . Вы можете помочь Википедии, расширив ее.