 | В этой статье не процитировать какие - либо источники . ( июль 2017 г. ) ( Узнайте, как и когда удалить это сообщение-шаблон ) |
В математической логике , то правило сечения является правилом вывода из секвенции исчисления . Это обобщение классического правила вывода modus ponens . Его смысл в том, что если формула A появляется как заключение в одном доказательстве и гипотеза в другом, то можно вывести другое доказательство, в котором формула A не появляется. В частном случае modus ponens, например , исключаются случаи появления человека из « Каждый человек смертен», Сократ - это человек, чтобы сделать вывод, что Сократ смертен .
Формальные обозначения [ править ]
Формальная нотация в нотации последовательного исчисления:
- резать
Устранение [ править ]
Правило разреза является предметом важной теоремы, теоремы об исключении разреза . В нем говорится, что любое суждение, имеющее доказательство в исчислении секвенций, которое использует правило отсечения, также обладает доказательством без отсечения, то есть доказательством, которое не использует правило отсечения.
