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