Структурное правило

Чтобы узнать о типе правила, используемого в лингвистике, см. Правило структуры фразы .

В логической дисциплине теории доказательств структурное правило — это правило вывода секвенционного исчисления , которое не относится к какой-либо логической связке , а вместо этого действует на секвенции . непосредственно Структурные правила часто имитируют предполагаемые метатеоретические свойства логики. Логики, отрицающие одно или несколько структурных правил, классифицируются как субструктурные логики .

Общие структурные правила

Три общих структурных правила:

• Ослабление , когда гипотезы или выводы последовательности могут быть расширены дополнительными членами. В символической форме правила ослабления можно записать как ${\frac {\Gamma \vdash \Sigma }{\Gamma ,A\vdash \Sigma }}$ слева от турникета и ${\frac {\Gamma \vdash \Sigma }{\Gamma \vdash \Sigma ,A}}$ справа. Известен как монотонность следствия в классической логике.
• Сокращение , когда два равных (или объединяемых) члена на одной стороне секвенции могут быть заменены одним членом (или общим экземпляром). Символически: ${\frac {\Gamma ,A,A\vdash \Sigma }{\Gamma ,A\vdash \Sigma }}$ и ${\frac {\Gamma \vdash A,A,\Sigma }{\Gamma \vdash A,\Sigma }}$. Также известен как факторинг в доказательства теорем автоматизированных системах с использованием разрешения . Известен как идемпотентность следствия в классической логике.
• Обмен , при котором два члена на одной стороне секвенции могут быть заменены местами. Символически: ${\frac {\Gamma _{1},A,\Gamma _{2},B,\Gamma _{3}\vdash \Sigma }{\Gamma _{1},B,\Gamma _{2},A,\Gamma _{3}\vdash \Sigma }}$ и ${\frac {\Gamma \vdash \Sigma _{1},A,\Sigma _{2},B,\Sigma _{3}}{\Gamma \vdash \Sigma _{1},B,\Sigma _{2},A,\Sigma _{3}}}$. (Это также известно как правило перестановки .)

Логика без каких-либо из вышеперечисленных структурных правил интерпретировала бы стороны секвенции как чистые последовательности ; при обмене их можно считать мультимножествами ; и как при сжатии, так и при обмене их можно считать множествами .

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

См. также

• Аффинная логика - субструктурная логика, теория доказательства которой отвергает структурное правило сокращения. Страницы, отображающие описания викиданных в качестве запасного варианта.
• Линейная логика - Система ресурсоориентированной логики.
• Упорядоченная логика (линейная логика)
• Логика релевантности - система математической логики, которая накладывает определенные ограничения на выводы. Страницы, отображающие описания викиданных в качестве запасного варианта.
• Логика разделения