Структурное правило - Structural rule
В теории доказательств , структурное правило является правило вывода , что не относится к какой - либо логической связке , но вместо этого работает на суждении или секвенции непосредственно. Структурные правила часто имитируют предполагаемые метатеоретические свойства логики. Логики, отрицающие одно или несколько структурных правил, классифицируются как субструктурные логики .
Общие структурные правила
Три общих структурных правила:
- Ослабление , когда гипотезы или выводы секвенции могут быть расширены дополнительными членами. В символическом виде правила ослабления можно записать как слева от турникета , так и справа.
- Сужение , где две равные (или unifiable) члены на одной и той же стороне секвенции могут быть заменены одним элементом (или общий) , например. Символически: а . Также известен как факторинг в автоматизированных системах доказательства теорем с использованием разрешения . Известный как идемпотентность следствия в классической логике.
- Обмен , при котором два участника с одной стороны секвенции могут поменяться местами. Символически: а . (Это также известно как правило перестановки .)
Логика без каких-либо из вышеперечисленных структурных правил интерпретировала бы стороны секвенции как чистые последовательности ; при обмене они являются мультимножествами ; и как при сжатии, так и при обмене они являются наборами .
Это не единственные возможные структурные правила. Известное структурное правило известно как сокращение . Теоретики доказательства тратят немало усилий на то, чтобы показать, что правила сокращения излишни в различных логиках. Точнее, показано, что разрез - это только (в некотором смысле) инструмент для сокращения доказательств и не добавляет к доказываемым теоремам. Успешное «удаление» правил отсечения, известное как исключение отсечения , напрямую связано с философией вычислений как нормализации (см. Соответствие Карри – Ховарда ); она часто дает указание хорошего о сложности в решении данной логики.