Монотонность вывода

Монотонность следствия - это свойство многих логических систем, которое утверждает, что гипотезы любого производного факта могут быть свободно расширены с дополнительными предположениями. В последовательных исчислениях это свойство может быть зафиксировано правилом вывода, называемым ослаблением, а иногда и прореживанием, и в таких системах можно сказать, что следствие является монотонным тогда и только тогда, когда правило допустимо. Логические системы с этим свойством иногда называют монотонными логиками, чтобы отличать их от немонотонных логик.

Для иллюстрации рассмотрим естественный вычет секвенции :

Γ C ${\ displaystyle \ vdash}$

То есть на основе списка предположений Γ можно доказать C. Ослабление, добавляя предположение A, позволяет заключить:

Γ, A C ${\ displaystyle \ vdash}$

Например, силлогизм «Все люди смертны. Сократ - человек. Следовательно, Сократ смертен». можно ослабить, добавив посылку: «Все люди смертны. Сократ - человек. Коровы производят молоко. Следовательно, Сократ смертен». Срок действия первоначального заключения при добавлении помещений не изменяется.

В большинстве логик ослабление - это либо правило вывода, либо метатеорема, если логика не имеет явного правила. Примечательные исключения:

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

• Сокращение
• Правило обмена
• Субструктурная логика
• Теорема о запрете клонирования