Теоремы Гёделя о неполноте и вычисления

Теоремы Гёделя о неполноте показывают, что любая достаточно сильная, непротиворечивая формальная система содержит истинные утверждения, которые она не может доказать, — результат, тесно связанный с неразрешимостью, обнаруженной в теории вычислимости.

Definition

Теоремы о неполноте утверждают, что любая непротиворечивая формальная система, способная выражать базовую арифметику, является неполной, содержит истинные арифметические утверждения, которые она не может доказать, и не может доказать свою собственную непротиворечивость; в вычислительных терминах, множество доказуемых утверждений распознаваемо, но его дополнение — нет, что отражает неразрешимость.

Scope

Эта тема охватывает первую и вторую теоремы о неполноте, технику арифметизации и самореференции посредством нумерации Гёделя, тесную взаимосвязь между неполнотой и неразрешимостью проблемы остановки и логики первого порядка, а также последствия для пределов формального рассуждения и автоматического доказательства.

Core questions

• Почему ни одна непротиворечивая, достаточно сильная формальная система не может доказать все истинные арифметические утверждения?
• Как самореференция посредством нумерации Гёделя порождает недоказуемое истинное предложение?
• Как неполнота и неразрешимость проблемы остановки являются двумя взглядами на одно явление?
• Что означает неполнота для пределов автоматического доказательства теорем?

Key theories

Первая теорема о неполноте

Любая непротиворечивая формальная система, достаточно сильная для кодирования арифметики, содержит истинное утверждение, которое она не может ни доказать, ни опровергнуть, построенное предложением, которое фактически утверждает свою собственную недоказуемость.

Неполнота через вычислимость

Неполнота следует из неразрешимости проблемы остановки: если бы каждая арифметическая истина была доказуема, можно было бы решить проблему остановки путем поиска доказательств, поэтому существование неразрешимых проблем вынуждает существование недоказуемых истин.

Clinical relevance

Неполнота и ее вычислительный аналог устанавливают жесткие ограничения на автоматизированное рассуждение: ни один алгоритм не может решить все арифметические истины или ответить на каждый математический вопрос, поэтому системы доказательства теорем и верификации должны полагаться на человеческое руководство, ограниченные теории или интерактивное доказательство, а не на полное автоматическое решение.

History

Гёдель доказал теоремы о неполноте в 1931 году, разрушив надежду Гильберта на полную и самообосновывающуюся формализацию математики. В течение пяти лет Чёрч и Тьюринг связали эти ограничения с неразрешимостью, и вычислительная интерпретация неполноты через проблему остановки стала основным элементом теории вычислимости.

Key figures

• Kurt Gödel
• Alan Turing
• Alonzo Church
• John Barkley Rosser

Seminal works

• godel1931
• boolos2007

Frequently asked questions

Означает ли неполнота, что математика неисправна?

Нет. Это означает, что ни одна отдельная непротиворечивая формальная система не может доказать каждую арифметическую истину, а не то, что математика непоследовательна или ненадежна. Математики работают внутри и между формальными системами, и неполнота просто отмечает внутренний предел того, что может охватить любая фиксированная система.

Как теорема Гёделя связана с проблемой остановки?

Они тесно связаны. Неразрешимость проблемы остановки подразумевает неполноту: если бы формальная система могла доказать каждую истину о том, какие программы останавливаются, можно было бы решить проблему остановки путем поиска доказательств, что противоречит результату Тьюринга. Оба выражают, в логике и в вычислениях, одни и те же фундаментальные пределы формального метода.