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

Эта статья в значительной степени или полностью основана на одном источнике . Соответствующее обсуждение можно найти на странице обсуждения . Пожалуйста, помогите улучшить эту статью, добавив ссылки на дополнительные источники . Найти источники:  «Cut rule» – новости  · газеты  · книги  · ученый  · JSTOR ( июль 2017 г. )

В математической логике правило сечения является правилом вывода секвенциального исчисления . Это обобщение классического правила вывода modus ponens . Его смысл в том, что если формула A появляется как заключение в одном доказательстве и гипотеза в другом, то может быть выведено другое доказательство, в котором формула A не появляется. Это применимо к случаям modus ponens , например, как примеры человека исключаются из Каждый человек смертен, Сократ — человек, чтобы вывести Сократ смертен .

Обычно в формальной записи в последовательном исчислении это записывается так:

${\displaystyle {\begin{array}{c}\Гамма \vdash A,\Дельта \quad \Гамма ',A\vdash \Дельта '\\\hline \Гамма ,\Гамма '\vdash \Дельта ,\Дельта '\end{array}}}$вырезать ^[1]

Правило сечения является предметом важной теоремы, теоремы об устранении сечения . Она утверждает, что любая секвенция, имеющая доказательство в исчислении секвенций, использующее правило сечения, также имеет доказательство без сечения, то есть доказательство, которое не использует правило сечения.

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

• в
• т
• е