Формальная система: различия между версиями

[непроверенная версия][отпатрулированная версия]
Содержимое удалено Содержимое добавлено
→‎См. также: Ссылки на страницы Логика первого порядка Логика высшего порядка.
Метки: с мобильного устройства из мобильной версии через расширенный мобильный режим
→‎Важнейшие результаты: Ссылка на страницу Алонзо Чёрча.
Метки: с мобильного устройства из мобильной версии через расширенный мобильный режим
Строка 77:
* В 30-е гг. XX века [[Курт Гёдель]] показал, что есть целый класс теорий первого порядка, являющихся неполными. Более того, формула, утверждающая непротиворечивость теории, также невыводима средствами самой теории (см. [[Теоремы Гёделя о неполноте]]). Этот вывод имел огромное значение для математики, так как формальная арифметика (а также любая теория, содержащая ее в качестве подтеории) является как раз такой теорией первого порядка, а следовательно, неполна.
* Несмотря на это, теория {{iw|Вещественно замкнутое поле|вещественно замкнутых полей|en|Real closed field}} со сложением, умножением и отношением порядка является полной ([[теорема Тарского — Зайденберга]]).
* [[Чёрч, Алонзо|Алонзо Чёрчем]] было доказано, что задача определения общезначимости любой произвольно взятой формулы [[логика предикатов|логики предикатов]] является [[Алгоритмически неразрешимая задача|алгоритмически неразрешимой]].
* [[Исчисление высказываний]] является непротиворечивой, полной, разрешимой теорией.