Автор: Вольфрамовый клапан
Ну вот, например, Евклидова аксиоматика без аксиомы параллельных неполна. Есть уверенность, что она полна с аксиомой параллельных? |
|
Полнота элементарной геометрии факт общеизвестный. Все утверждения, выводимые в её системе аксиом, можно или опровергнуть, или доказать.
Автор: Вольфрамовый клапан
А известны недоказуемые теоремы арифметики? |
|
Естественно. Утверждение о непротиворечивости формальной арифметики в самой формальной арифметике невыводимо. Поэтому если брать какую-нибудь конкретную теорему, которая сейчас не доказана, то может быть, что когда-нибудь её доказать и удастся, однако всё истинные теоремы доказать всё равно нельзя. Согласно Гёделю, истинных формул в системе всегда будет больше, чем выводимых.
Суть теорем Гёделя в том, что он построил истинное, но недоказуемое утверждение — формулу, которая содержательно утверждает свою собственную недоказуемость. Только сформулирована эта формула на метаязыке (так называемая гёделевская нумерация), то есть это не некое конкретное утверждение, а «утверждение об утверждениях». Тем самым он доказал, что истинные, но недоказуемые утверждения в принципе всегда можно построить, а по факту они могут быть разными.
Причём заранее установить доказуемое утверждение или не доказуемое нельзя, то есть невозможно по формуле определить, выводима она из аксиом данной теории или нет. Это следует как из самой теоремы Гёделя (не все формулы могут быть разделены на выводимые и невыводимые), так и конкретно формулируется в так называемой проблеме остановки. Суть которой в следующем. Дано описание алгоритма и входные данные, исходя из чего требуется определить, остановится алгоритм, то есть задача будет решена, или процедура работы алгоритма будет выполняться бесконечно, то есть задача не имеет решения. Алан Тьюринг в 1936 году доказал, что проблема остановки неразрешима, то есть не существует универсального алгоритма решения этой проблемы. Поэтому проблема остановки считается аналогом доказательства теоремы Гёделя.
***
В то же время непротиворечивость формальной системы всегда может быть доказана средствами другой системы с более выразительным языком. Однако если правила вывода этой системы сильнее логических средств арифметики, то уверенности в непротиворечивости используемых в доказательстве допущений не будет, так как используемые методы не будут финитными, то есть методами конечными, наглядными, в полной мере ясными (конструктивными). Поэтому можно сказать, что Гёдель показывает невозможность именно финитного доказательства непротиворечивости арифметики.
Например, доказательство непротиворечивости формальной арифметики было проведено в 1936 году с использованием разновидности трансфинитной индукции — метода доказательства, обобщающего математическую индукцию на случай несчётного числа значений параметра.
Однако даже если удовлетвориться методами, которые предоставляет система с более выразительным языком, то потребуется доказательство непротиворечивости уже этой системы, для чего нужна будет система с ещё более выразительным языком, методы которой будут оставлять ещё больше вопросов.