Алгоритмическая разрешимость: различия между версиями
| [отпатрулированная версия] | [отпатрулированная версия] |
Содержимое удалено Содержимое добавлено
Строка 12:
== Общие сведения ==
[[Формальная система|Формальное исчисление]] в общем случае должно определять [[язык]], правила построения [[Терм (логика)|терм]]ов и [[Математическая формула|формул]], аксиомы и правила вывода. Таким образом, для каждой теоремы '''T''', всегда можно построить цепочку '''A<sub>1</sub>''', '''A<sub>2</sub>''', … , '''A<sub>n</sub>'''='''T''', где каждая формула '''A<sub>i</sub>''' либо является аксиомой, либо выводима из предыдущих формул, по одному из правил вывода. Разрешимость означает, что существует алгоритм, который для каждого правильно построенного предложения '''T''', за конечное время выдаёт однозначный ответ: да, данное предложение выводимо в рамках исчисления или нет — оно не выводимо.
Очевидно, что противоречивая теория разрешима, так как любая формула будет выводимой. С другой стороны, если исчисление не обладает [[рекурсивно перечислимое множество|рекурсивно перечислимым множеством]] аксиом, как например, [[логика второго порядка]], оно, очевидно, не может быть разрешимым.
| |||