Гёдель говорит, что есть истинные утверждения, которые невозможно доказать при наличии надежной аксиоматической системы. Кто-нибудь говорит что-нибудь о доказуемости доказуемости утверждений?
До сих пор остается открытым вопрос, что каждое доказуемое логическое утверждение может быть доказано как доказуемое? Или, что то же самое, что каждое недоказуемое утверждение может быть доказано как недоказуемое?
Или, более конкретно, все еще остается открытым вопрос, всегда ли можно доказать доказуемость/недоказуемость подмножества доказуемых утверждений (например, истинных), так что однажды мы могли бы прийти к выводу, что все истинные доказуемые теоремы могут быть доказаны. быть доказуемым?
Я думаю, что мой вопрос может быть немного нестандартным. Я постараюсь быть более ясным.
Гёдель не указал класс неразрешимых утверждений. Что, если, например, все истинные теоремы, которые нельзя доказать, обладают некоторым свойством P.
P является свойством «бесполезным для всех практических целей».
Тогда бы мы знали, что хотя и существуют истинные теоремы, которые невозможно доказать, они бесполезны. Минуточку... есть ли такая вещь, как бесполезная теорема?
Центральная черта всех основных формальных систем состоит в том, что если утверждение доказуемо, то оно доказуемо. Действительно, это свойство является одним из условий выводимости, которое обычно используется при доказательстве теоремы о неполноте, и оно играет центральную роль в доказательстве Геделя второй теоремы о неполноте.
Но также, я мог бы добавить, этот принцип явно является тем, что мы хотим иметь в наших формальных системах. Если вы можете доказать утверждение, это означает, что у вас есть конечное доказательство, последовательность утверждений, каждое из которых является либо аксиомой, либо следует из предыдущих утверждений по одному из правил вывода, и которое заканчивается доказываемым утверждением. Проверка того, что доказательство действительно является доказательством, должна стать рутинной задачей. Таким образом, всякий раз, когда утверждение доказуемо, мы должны ожидать, что мы можем доказать, что оно доказуемо, поскольку это сводится к доказательству того, что доказательство действительно является доказательством, по поводу чего не будет особых разногласий.
Так что да, действительно, в любой из обычных формальных систем всякий раз, когда утверждение доказуемо, мы также можем доказать, что оно доказуемо.
Можно ввести модальность доказуемости, написав Box φ для обозначения того, что φ доказуема (в некоторой обсуждаемой фиксированной формальной системе). В этой модальной терминологии принцип, согласно которому каждое доказуемое утверждение доказуемо, является аксиомой:
и эта аксиома известна как аксиома 4 в модальной теории S4 .
Существует доказательство того, что определенный класс геометрических утверждений разрешим машиной Тьюринга за конечное время.
Этот результат был ответвлением 10-й проблемы Гильберта, где он задал вопрос, все ли арифметические уравнения разрешимы с помощью алгоритма, на который в 1970 году был дан отрицательный ответ.
Возник аналогичный вопрос о возможности алгоритма, доказывающего любое истинное утверждение элементарной геометрии и опровергающего любое ложное утверждение. Оказывается, такой алгоритм действительно существует, хотя для практических целей он бесполезен, поскольку настолько неэффективен, что для решения проблемы по такому алгоритму потребуется больше времени, чем существование Вселенной.
Однако, поскольку описанный выше алгоритм в принципе существует, его существование можно считать доказательством того , что все истинные геометрические утверждения доказуемы.
БРК
Майкл
БРК