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

эта статья не цитировать Любые источники. Пожалуйста помоги улучшить эту статью от добавление цитат в надежные источники. Материал, не полученный от источника, может быть оспорен и удалено. Найдите источники: «Структурное правило»  – Новости  · газеты  · книги  · ученый  · JSTOR (Декабрь 2009 г.) (Узнайте, как и когда удалить этот шаблон сообщения)

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

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

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

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

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

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

Смотрите также

• Аффинная логика
• Линейная логика
• Упорядоченная логика
• Строгая логика
• Логика разделения