Теорема о сокращении-исключении
-
Теорема об исключении сокращений
- Доказана Герхардом Гентценом в 1934 году для систем LJ и LK.
- Утверждает, что любое суждение с доказательством через правило отсечения также имеет доказательство без него.
-
Правило отсечения
- Последовательность в секвенциальном исчислении связывает формулы и следует читать как «A1, A2, A3, … доказывает B1, B2, B3, …».
- LHS может содержать любое количество формул, RHS — не более одной.
- В LK RHS может содержать любое количество формул, в LJ — только одну или не содержать вообще.
-
Исключение сокращений и секвенциальное исчисление
- Секвенциальное исчисление позволяет использовать множество формул в RHS, что расширяет выразительность.
- Из логики LC Жирара можно получить формализацию классической логики с одной формулой в RHS.
-
Правило сокращения
- Позволяет «сокращать» вхождения формулы A из логически вытекающего отношения.
- Теорема об исключении сокращений утверждает, что последовательность, доказуемая с помощью правила отсечения, может быть доказана без него.
-
Следствия из теоремы
- Аналитические доказательства без использования правила отсечения обычно более длительны и не всегда тривиальны.
- Система считается непоследовательной, если она допускает доказательство абсурда.
- Если система обладает теоремой об исключении сокращений, то она должна быть непротиворечивой.
- Системы с теоремой об исключении сокращений обычно обладают свойством подформулы.
- Исключение сокращений важно для доказательства теорем интерполяции и поиска доказательств в Prolog.
-
Ссылки
- Ссылки на дополнительные материалы и внешние ссылки не предоставлены.