Правило вывода: различия между версиями

[отпатрулированная версия][отпатрулированная версия]
Содержимое удалено Содержимое добавлено
мНет описания правки
кое-что дописал, маловато текста для секционирования, но {{stub}} уже можно не ставить
Строка 3:
В непротиворечивой теории теоремы получаются путём цепочки применения правил вывода этой теории. При этом если формула <math>{\cal B}</math> выводится за некоторое количество шагов из формул <math>{\cal A_1},</math> <math>\dots,</math> <math>{\cal A_n}</math>, то для выражения этого факта применяется обозначение <math>{\cal A_1},\dots,{\cal A_n}\vdash{\cal B}</math>. Если в таком случае рассматриваемая теория [[Непротиворечивая теория|непротиворечива]], а каждое из утверждений <math>{\cal A_1},</math> <math>\dots,</math> <math>{\cal A_n}</math> является либо аксиомой, либо теоремой, то <math>{\cal B}</math> также является теоремой.
 
В [[Исчисление предикатов|исчислении предикатов]] в {{iw|исчисление гильбетровского типа|гильбетровском варианте|en|Hilbert system}} правилами вывода являются [[модус поненс]] и [[правило обобщения]]. По [[Теорема Гёделя о полноте|теореме Гёделя о полноте]] формула является выводимой в исчислении предикатов первого порядка тогда и только тогда, когда она [[Общезначимость|общезначима]], то есть истинна в любой [[Интерпретация (математическая логика)|интерпретации]] этого исчисления предикатов.
== В исчислении предикатов ==
В [[Исчисление предикатов|исчислении предикатов]] правилами вывода являются [[модус поненс]] и [[правило обобщения]]. По [[Теорема Гёделя о полноте|теореме Гёделя о полноте]] формула является выводимой в исчислении предикатов первого порядка тогда и только тогда, когда она [[Общезначимость|общезначима]], то есть истинна в любой [[Интерпретация (математическая логика)|интерпретации]] этого исчисления предикатов.
 
В [[исчисление генценовского типа|исчислениях генценовского типа]] ([[Исчисление секвенций|исчислениях секвенций]], системах {{iw|натуральный вывод|натурального вывода|en|natural deduction}}) правила вывода играют основную роль — в них используется небольшое количество аксиом и развитые системы правил вывода. В [[теория доказательств|теории доказательств]] применяются именно такие исчисления, поскольку благодаря подбору симметричных систем правил вывода возможно получить конструктивные результаты о [[Непротиворечивость|непротиворечивости]] систем.
{{stub}}
 
== Литература ==
* {{книга | автор = Драгалин А. Г. | заглавие = Математический интуиционизм. Введение в теорию доказательств| место = М. | издательство = [[Наука (издательство)|Наука]] | год = 1979 | страниц = 256 | серия = Математическая логика и основания математики }}