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