Теорема о замене естественной дедукции принимает форму структурного правила или структурной теоремы, известной как сокращение в последовательном исчислении.

Дата: 2025-04-30; Просмотры: 3
Оценка:
0.00 из 5.00 — оценок
Скачиваний: 0

Сокращение (подстановка)

Если Γ ⇒ π 1 : A и Γ , u : A ⇒ π 2 : C , тогда Γ ⇒ [ π 1 / u ] π 2 : C .

В большинстве логик с хорошим поведением отсечение не требуется как правило вывода, хотя оно остается доказуемым как мета-теорема ; избыточность правила отсечения обычно представляется в виде вычислительного процесса, известного как устранение отсечения. У этого есть интересное применение для естественной дедукции; обычно чрезвычайно утомительно доказывать определенные свойства непосредственно в естественной дедукции из-за неограниченного числа случаев. Например, подумайте о том, чтобы показать, что данное утверждение не доказуемо с помощью естественной дедукции. Простой индуктивный аргумент терпит неудачу из-за таких правил, как ∨ E или E , которые могут вводить произвольные предложения . Однако мы знаем , что последовательное исчисление является полным по отношению к естественной дедукции , поэтому достаточно показать эту недоказуемость в посл едовательном исчислении. Теперь, если cut недоступен в качестве правила вывода, то все правила последовательного вывода либо вводят связку справа, либо слева, так что глубина последовательного вывода полностью ограничена связками в окончательном выводе. Таким образом, доказать недоказуемость намного проще, потому что существует лишь конечное число случаев для рассмотрения, и каждый случай полностью состоит из подпозиций заключения. Простым примером этого является теорема о глобальной непротиворечивости: " ⋅ ⊢ ⊥ истинно" недоказуемо. В версии последовательного исчисления это очевидно верно, потому что нет правила, которое могло бы иметь " ⋅ ⇒ ⊥ " в качестве вывода ! Специалисты по теории доказательств часто предпочитают работать с формулировками последовательного исчисления без разрезов из-за таких свойств.

Смотри также

Примечания

1.

 Jaśkowski 1934 .