О НЕПОЛНОТЕ ФОРМАЛЬНЫХ СИСТЕМ
О НЕПОЛНОТЕ ФОРМАЛЬНЫХ СИСТЕМ
И ШЕСТОЙ ПРОБЛЕМЕ ГИЛБЕРТА
Автор категорически запрещает использовать изложенное
для нанесения ущерба кому бы то ни было.
Копирование статьи для перепечатки и распространения
возможны исключительно с разрешения автора.
Если изложенное помогло найти решение какой-то задачи,
то ссылка на автора и статью обязательны.
Первую (слабую) теорему Гёделя можно сформулировать следующим образом:
Любая формальная система аксиом содержит неразрешённые предположения.
Вторую (сильную) теорему Гёделя можно сформулировать следующим образом:
Логическая полнота (или неполнота) любой системы аксиом не может быть доказана в рамках этой системы. Для её доказательства или опровержения требуются дополнительные аксиомы (усиление системы).
Занимаясь в 70-х годах теоремами Курта Гёделя меня заинтересовало не столько как (приёмы, с помощью которых) он доказал свои теоремы, а почему (причины, благодаря которым) он смог доказать свои теоремы. Причины успешного доказательства теоремы о неполноте меня заинтересовали потому, что в тот момент времени я столкнулся с ограничениями на машинное доказательство теорем и для преодоления этих ограничений мне было необходимо выяснить именно причины возникающих ограничений.
В слабой теореме Курт Гёдель доказал неполноту (противоречивость) арифметики, но не смог обосновать причины появления этой неполноты. Пользуясь формальной логикой Курт Гёдель лишь сделал построения, которые в конечном итоге и привели его к противоречию. Хотя, было бы логично, если бы одновременно с констатацией факта Курт Гёдель показал бы ещё и причины, приведшие его к противоречию. Но он этого не сделал, а значит у него были более чем серьёзные объективные причины помешавшие это сделать. Вот эти причины я и попробовал найти.
Я обратил внимание на то, что в 1931 году, когда Курт Гёдель опубликовал свою работу, ещё не была разработана теория автоматов и формальных языков. Занимаясь формальными языками я пришёл к выводу, что любую формальную систему можно представить как некий формальный язык. Действительно, для того, чтобы задать некую формальную систему достаточно задать некий конечный алфавит для описания объектов которыми оперирует формальная система, конечное множество аксиом формальной системы и задать конечный набор правил построения высказываний в этой формальной системе. Все высказывания, в том числе и теоремы, которые могут быть построены в рамках формальной системы, должны разбираться автоматом, реализующим формальную систему как формальный язык. Однако, было бы логично потребовать, чтобы теоремы включались в грамматику языка в виде синтаксических правил потому, что они устанавливают общие закономерности для объектов, которыми оперирует формальная система. Т.е., что грамматика языка формальной системы должна быть расширяемой. Проблема может возникнуть только в изобразительной мощности выбранного алфавита. Действительно, все теоремы планиметрии Евклида доказываются с использованием аксиом и правил вывода формальной логики, однако довольно сложно предложить алфавит, достаточный для описания объектов планиметрии.
Разработчики языка Algol-60 столкнулись с рядом проблем при задании языков с расширяемой в ходе трансляции грамматикой контекстно свободными формами Бэкуса-Наура (BNF). Эти проблемы вроде бы были преодолены ван Вейнгаарденом в двухуровневой, так называемой B-грамматике, которая была разработана при работе над языком Algol-68.
Однако, одно противоречие так и не было преодолено. Есть хотя бы одна конструкция, которая не может быть однозначно разобрана:
if A then if B then C else D
Действительно, не смотря на то, что это выражение полностью соответствует грамматике языка Algol-68, оно не может быть однозначно разобрано, поскольку непонятно к какой паре if then относится else. В результате вычисления этого выражения, если использовать различный порядок вычисления подвыражений, получаются различные результаты, из чего следует, что:
(if A then if B then C else D) ≠ (if A then if B then C else D)
Возникает противоречие вызванное отсутствием явного указания порядка вычисления подвыражений. С помощью задающих язык правил можно сгенерировать указанную строку, но нельзя эту строку однозначно разобрать с помощью автомата, реализующего заданный язык. Причиной этой неоднозначности является то, что одна и та же строка (выражение) может быть выведена на основе правил языка минимум двумя разными способами.
Рассмотренное выражение из языка Algol-68 является иллюстративно полным аналогом выражения на языке формальной логики
A ⊃ B ⊃ C ⋎ D
которое допускает большее, чем выражение из языка Algol-68, число вариантов расстановки скобок, устанавливающих порядок вычисления подвыражений. Очевидно, что эта неоднозначность и является причиной появления противоречий или неполноты в формальных системах, которые построены на основе формальной логики.
Если рассматривать формальную систему как некий язык, заданный B-грамматикой, то алфавит должен быть специфичен для описания оперируемых формальной системой объектов, правила первого уровня формируются на основе аксиом формальной системы, аксиом и правил выводов выражений формальной логики, а правила второго уровня (теоремы) формируются как разрешённые расширения синтаксиса языка и строятся на основе грамматики первого уровня.
Если некое выражение (высказывание) однозначно выводится (генерируется) и разбирается автоматом, реализующим язык формальной системы, то это выражение принадлежит формальной системе.
Если некое выражение (высказывание) может быть выведено (сгенерировано) несколькими разными способами на основе правил языка формальной системы, но не может быть однозначно разобрано реализующим язык формальной системы автоматом, то это выражение является противоречивым для данной формальной системы. Примером неоднозначности для формальной логики, приводящей в конечном итоге к противоречию, является выражение A ⊃ B ⊃ C ⋎ D.
Если некое выражение (высказывание) не может быть выведено (сгенерировано) на основе языка формальной системы, но может быть разобрано автоматом, реализующим язык формальной системы, то это выражение невыводимо в этой формальной системе. Примером невыводимого высказывания для планиметрии Евклида являются задачи трисекции угла и квадратуры круга.
Если некое выражение (высказывание) не может быть ни выведено (сгенерировано), ни разобрано в рамках языка формальной системы, то такое выражение не принадлежит формальной системе.
Из представления формальной системы как некоего формального языка, задаваемого двухуровневой В-грамматикой, следует, что если грамматика первого уровня допускает построение неоднозначно выводимых выражений, то и весь язык с генерируемыми расширениями синтаксических правил формальной системы (теоремами), так же должен содержать в себе допускающие неоднозначность правила хотя бы потому, что уже грамматика первого уровня содержит правила, влекущие за собой неоднозначность языка.
Изложенное, по большому счёту, является упрощённым изложением сделанного в 70-х годах прошлого века самостоятельного доказательства теорем Гёделя. Конечно, ход доказательства тогда был другим, с использованием математической нотации. Однако, позже, в конце 80-х годов, мне стало понятно, что сделанное доказательство так же основано на формальной логике, как причине появления неразрешимой неоднозначности, а значит само может содержать в себе некое скрытое противоречие или непреодолимую неоднозначность. Поэтому пришлось заняться поиском путей преодоления возможных противоречий. В результате фактически была создана непротиворечивая логика и на её основе была разработана алгебра непротиворечивых алгоритмов. В результате выяснилось, что слабая теорема Гёделя является продуктом неоднозначности языка формальной логики и для непротиворечивой логики она не действует. Так же была передоказана теорема о детерминизации для непротиворечивых алгоритмов для случая, когда уже имеется детерминированный автомат с N состояниями и в него добавляется ещё одно новое состояние, а результирующий автомат детерминизируется. Оказалось, что результирующий автомат может содержать не больше 2N состояний, а не (2^N)-1, как это доказано для потенциально противоречивых алгоритмов. Сложность алгоритма детерминизации конечного непротиворечивого автомата снизилась с O(N^3) до O(N*sqrt(N)).
Полученные результаты имеют очень важное прикладное значение не только для систем искусственного интеллекта, поскольку указывают путь построения систем ИИ, не только для проверки правильности доказательств, не только для автоматизации доказательства теорем, но так же и для технологии программирования, как процесса создания (конструирования) программ.
Надеюсь, теперь понятно почему насколько это возможно я стараюсь избегать использование математической нотации и предпочитаю излагать свои мысли на гораздо более мощном, чем любая формальная система, хорошо развитом неформальном языке.
Курт Гёдель выполнил свою работу для разрешения второй проблемы Гилберта, которая формулируется так: «являются ли непротиворечивыми аксиомы арифметики?». Предложенное понимание формальных систем, как неких формальных языков с расширяемым синтаксисом, как мне кажется, позволяет сразу разрешить шестую проблему Гилберта: «возможно ли математическое изложение аксиом физики?». Да, возможно. И не только возможно, но уже является свершившимся фактом, поскольку современная теоретическая физика в основе своей является формальной системой, предназначенной для описания явлений окружающего мира и полнота теоретической физики определяется лишь развитостью математического аппарата и полнотой наших знаний об окружающем мире. Проблема может быть только в изобразительных возможностях алфавита с помощью которого производится описание объектов и явлений окружающего мира.
Основные аксиомы, на которых основана современная физика, как формальная система, это, как минимум:
закон сохранения материи,
закон единообразия материи,
математический аппарат.
В основе математического аппарата лежит всё та же формальная логика. Закон единообразия материи - это распространение наблюдаемых закономерностей поведения объектов окружающего мира в ближней к нам области на любую сколь угодно удалённую от нас область окружающего мира. Из закона сохранения материи следуют, например, законы сохранения энергии, вещества, количества движения и т.д. В частности, следует понятие инерциальной системы.
Правила построения высказываний в физике, как в формальной системе, так же могут быть представлены в виде грамматики ван Вейнгаардена, где правила первого уровня формируются на основе аксиоматически задаваемых известных свойств окружающего мира, аксиом и правил вывода математического аппарата, а правила второго уровня (теоремы и гипотезы) формируются на основе постулируемых и уже выявленных закономерностей окружающего мира.
Физика, как система знаний, разделяется на две подсистемы, на теоретическую и на экспериментальную физику. Экспериментальная физика собирает факты об окружающем мире и проверяет экспериментально полученные теоретической физикой предположения (гипотезы), а теоретическая физика объясняет обнаруживаемые экспериментальной физикой явления и закономерности, побуждая развивать и видоизменять теоретические основы физики, как формальной системы, предназначенной для описания окружающего мира. Обнаруживаемые противоречия между теорией и экспериментом требуют объяснения, что приводит к развитию теоретической физики, как формальной системы, в точном соответствии с требованиями сильной теоремы Гёделя. Так, обнаруженные в XIX веке противоречия между теоретическими выкладками Ньютоновой физики и излучением нагретого тела, известное как «фиолетовая катастрофа», привело к добавлению в аксиомы физики понятия кванта энергии, что привело к созданию квантовой механики, а попытка объяснения эксперимента Майкельсона-Морли, установившего факт равенства скоростей распространения света в разных направлениях, привёл к появлению специальной теории относительности.
Как всякая формальная система, использующая основанный на формальной логике математический аппарат, теоретическая физика неизбежно должна содержать в себе противоречия. Ещё в 1975 или 1976 году я обнаружил, как мне кажется, противоречие в теоретической физике, как формальной системе. Речь идёт о «красном смещении», когда спектральные линии излучаемых квантов энергии удалёнными звёздами смещены в красную область, но при этом не происходит расширения спектральных линий, что свидетельствовало бы о взаимодействии (поглощении и переизлучении) фотонов с находящимся между удалённой звездой и земным наблюдателем веществом.
Если закон единообразия материи справедлив, то энергия испущенного фотона в связанной с удалённой звездой инерциальной системе отсчёта равна E=2πhν, где h - постоянная Планка, а ν - частота фотона. Однако, в связанной с земным наблюдателем инерциальной системе отсчёта энергия этого же фотона уже будет меньше из-за уменьшения его частоты на величину «красного смещения». Получается, что
величина энергии фотона (кванта энергии) зависит
от выбранной инерциальной системы отсчёта,
что противоречит положениям специальной теории относительности, основанной на законе единообразия материи и законе сохранения материи и производному от закона сохранения материи закона сохранения энергии. Отсюда следует, что либо нарушается закон сохранения материи, либо нарушается закон единообразия материи, не говоря уже о нарушениях положений квантовой теории и положений специальной теории относительности. Эффектом Доплера данное противоречие не может быть устранено, поскольку удалённая инерциальная система должна двигаться с ускорением относительно инерциальной системы связанной с Земным наблюдателем, а значит инерциальной системой не является по определению. Из этого следует, что существует единственная инерциальная система связанная с земным наблюдателем и Земля является центром мироздания, от которого остальные звезды движутся с ускорением, что противоречит аксиоме единообразия материи. Кроме того, масса покоя движущегося со скоростью света фотона должна быть равна нулю, а значит энергия фотона должна быть одинаковой в разных инерциальных системах отсчёта, иначе опять нарушается закон сохранения энергии.
Хотя, в случае «красного смещения» мы скорее всего столкнулись с невозможностью дать непротиворечивое описание наблюдаемого явления в силу недостаточности наших знаний об окружающем мире, что и проявляется в противоречивости теоретической физики, как формальной системы, предназначенной для описания явлений окружающего нас мира и основанной на математическом аппарате, построенном на потенциально противоречивой формальной логике.
1975 год -:- 1-2 ноября 2011 года
Urix / Юрий Аверьянов /