Как логика первого порядка является полной, но неразрешимой?

НЕТ , полнота логики первого порядка не означает разрешимости.

Вы смешиваете два употребления полноты .

Первое использование касается полноты «стандартных» систем доказательств для логики первого порядка .

Это теорема Гёделя о полноте , которая гласит:

Теорема полноты утверждает, что если формула логически верна , то существует конечная дедукция (формальное доказательство) этой формулы.

Теорема Гёделя о полноте гласит, что дедуктивная система исчисления предикатов первого порядка является «полной» в том смысле, что для доказательства всех логически верных формул не требуется никаких дополнительных правил вывода. Обратной стороной полноты является правильность, тот факт, что в дедуктивной системе доказуемы только логически верные формулы. Вместе с обоснованностью (проверка которой несложна) эта теорема подразумевает, что формула логически верна тогда и только тогда, когда она является заключением формального вывода.

Его легко обобщить на отношение логического следствия между множеством Γ формул первого порядка и формулой φ в символах :

Г ⊨ ф .

В данном случае имеем вот что:

Γ ⊨ φ тогда и только тогда, когда Γ ⊢ φ (т . е. φ доказуемо из Γ ).

Для простоты рассмотрим случай, когда Г — пустое множество; в этом случае у нас есть предыдущая версия:

⊨ φ (т . е. φ действительно ) тогда и только тогда, когда ⊢ φ (т . е. φ доказуемо ).

Ваше заблуждение касается «основного свойства» действительности :

неверно, что если φ неверно , то ¬φ верно .

Рассмотрим формулу:

∃x∃y ¬(x = y).

Это означает: «есть по крайней мере две вещи x и y такие, что они не равны». Эта формула неверна во вселенной , состоящей только из одного элемента. Таким образом, оно недействительно (действительность означает: истинно в каждой вселенной).

Его отрицание:

¬∃x∃y ¬(x = y)

что составляет:

∀x∀y (x = y).

Это означает, что «все равны». Ни одна из этих формул не действительна, потому что она неверна во вселенной с более чем одним элементом.

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

В этом случае у нас есть процедура принятия решения : алгоритм таблицы истинности (он крайне «неэффективен», но работает…).

Примените его к любой формуле А : если в ее столбце у вас есть все «Т», то формула является тавтологией .

Также в этом случае имеет место теорема о полноте: если А является тавтологией, мы можем найти ее доказательство в «обычных» системах доказательств, таких как естественная дедукция .

Но заметьте, что и в этом случае неверно , что для какой бы то ни было формулы А А есть тавтология или ¬А есть.

Формула :

p V q

не является ни тавтологией, ни противоречием.

Второе значение полноты касается теорий и является ключом к знаменитой теореме Гёделя о неполноте, в которой говорится, что:

Первая теорема о неполноте утверждает, что никакая непротиворечивая система аксиом, теоремы которой могут быть перечислены с помощью «эффективной процедуры» (например, компьютерной программы, но это может быть любой алгоритм), не способна доказать все истины о соотношениях естественных явлений. числа (арифметические). Для любой такой системы всегда будут утверждения о натуральных числах, которые верны, но недоказуемы в рамках системы.

Этот (отрицательный) результат касается другого аспекта интуитивной «полноты» (в смысле адекватности): для математической теории, такой как арифметика или теория множеств, разумно ожидать, что аксиомы (формализованные логикой первого порядка) способны чтобы «уловить» всю математическую истину, выразимую в этой теории.

Для большинства «немного сложных» математических теорий это невозможно.

Добавлен

Разрешимость связана со вторым значением полноты .

Если теория T полна (во втором смысле плюс второе «техническое» условие: эффективно аксиоматизирована), т. е. T способна доказать все истинные предложения φ , выразимые на языке теории, благодаря тому факту, что либо φ истинно в T или ¬φ истинно в T , то T разрешимо .

[ Примечание . Если мы рассмотрим две приведенные выше формулы и рассмотрим их значение в отношении единственной арифметической интерпретации, то теперь мы получим, что одна из них истинна, а другая ложна. Ввиду того, что существует бесконечное число натуральных чисел (а значит, более одного), мы имеем, что формула : ∃x∃y ¬(x = y) верна в арифметической интерпретации (рассмотрим, например , 1 и 2 ), а его отрицание ∀x∀y (x = y) заведомо ложно (не все числа равны)].

Возвращаясь к разрешимости, почему полная теория такова?

Именно потому, что «процедура», описанная в вашем вопросе, работает: начните доказывать теоремы в T . Через конечное время, если φ истинно, вы найдете его доказательство; если это не так, то ¬φ истинно, и вы найдете этому доказательство.

Как было сказано ранее, эта «процедура» не работает для обеспечения достоверности , потому что неправда, что формула или ее отрицание являются действительными.

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

Таким образом, приведенные выше теории неразрешимы .

Какова «связь» между двумя употреблениями полноты ?

Рассмотрим теорию первого порядка T , включающую язык арифметики.

«Основа» логики полна (в первом смысле): т. е. она способна доказать все логические следствия аксиом теории Т .

Но теория T неполна ( согласно теореме Гёделя о неполноте), т. е. существует истинное арифметическое предложение φ , не доказуемое из аксиом теории T .

И что ?

Это не противоречие. Рассмотрим определение логического следствия, примененное к T :

T ⊨ φ тогда и только тогда, когда φ истинно в каждой модели T .

Поскольку φ истинно в «предполагаемой модели» арифметики («обычных» числах), мы заключаем, что оно неверно в какой-то другой модели [см. комментарий Фрэнсиса Дэви]: существуют нестандартные модели арифметики .

В таком случае это не является логическим следствием аксиом Т , и по этой причине его недоказуемость в Т не противоречит полноте лежащей в основе логики.

Поскольку Тейлор Хорнби уже самостоятельно исправил определение полноты (благодаря первому определению Мауро АЛЛЕГРАНЦА), я просто хочу указать, где именно его рассуждения сбиваются с пути.

Почему полнота не подразумевает разрешимость логики первого порядка? Тейлор Хорнби рассуждает следующим образом:

Почему это не работает: перечислить все строки x. Если x кодирует действительное происхождение B от A, принять. Если x кодирует правильное происхождение ~B от A, отклонить.

Из-за полноты этот процесс в конце концов наткнется на x, который является либо доказательством B, либо ~B из A. Если B, то A подразумевает B во всех интерпретациях. Если ~B, то это не тот случай, когда A подразумевает B во всех интерпретациях. Таким образом, FOL разрешима.

что здесь неправильно, так это фраза:

Из-за полноты этот процесс в конце концов наткнется на x, который является либо доказательством B, либо ~B из A.

Полнота по определению означает: «Если B логически следует, то B доказуемо». Это условное утверждение. Теперь, вообще говоря, мы не знаем, вытекает ли данное В заранее логически или нет. Поэтому мы не знаем, существует ли доказательство B или нет. Итак, на самом деле происходит следующее:

в конце концов этот процесс наткнется на x, который является либо доказательством B, либо ~B из A, ИЛИ этот процесс будет продолжаться вечно.

То есть этот алгоритм не всегда определяет, является ли B логическим следствием (или, что то же самое, доказуемо ли B благодаря свойствам достоверности и полноты FOL). Если либо B, либо ~B доказуемы, мы в конце концов найдем их доказательство. Но если ни B, ни ~B не доказуемы, то мы никогда не сможем сказать, нет ли доказательств или нам просто нужно продолжать поиски. Таким образом, этот алгоритм не дает нам ответа для каждого B, но мы можем спросить, существует ли лучший алгоритм, который дает нам ответ для каждого B. Проблема остановки Тьюринга используется, чтобы показать, что не существует алгоритма для определения того, является ли B логически вытекает.

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

У машин есть окончательные пределы, независимо от того, насколько умно они спроектированы. В 1936 году Тьюринг математически доказал, что общий алгоритм решения задачи для всех возможных пар программа-ввод не может существовать никогда. То есть ни один алгоритм не может быть написан так, чтобы он всегда правильно определял для любой заданной пары программа-ввод, остановится программа или нет. В информатике это называется проблемой остановки. Тьюринг доказал, что любой алгоритм можно заставить противоречить самому себе и, следовательно, он не может принимать правильные решения. В качестве иллюстрации мы можем использовать «патологическую» пару «программа-ввод», разработанную для того, чтобы делать противоположное тому, что предсказывает алгоритм.

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

Важнейший вопрос касается полноты и разрешимости (относительно того, является ли теорема либо истинной, либо ложной, но не тем и другим), что эквивалентно проблеме остановки в информатике. Неполнота открывает дверь к возможности неразрешимости. Успешное доказательство конкретной проблемы подразумевает, что она не является неразрешимой в теории (или системе), в которой она сформулирована. Но такое доказательство не означает, что сама теория полна или разрешима. В теории могут быть и другие проблемы, которые неразрешимы, и в этом случае решения не существует. Например, в неполной теории есть теоремы или уравнения, которые интуитивно кажутся верными, но недоказуемыми. Поэтому невозможно предсказать, будет ли когда-нибудь решена конкретная проблема, сформулированная в неполной теории.

Я почти уверен, что это правильно, но не уверен на 100%:

Одно из возможных заблуждений состоит в том, что мы можем думать, что говорим об одной модели, когда на самом деле мы говорим обо всех возможных моделях, удовлетворяющих определенному набору аксиом. Итак, если мы говорим об одной модели, то истинно Р или НЕ Р, но если мы говорим о множестве, то Р может быть валидным, НЕ Р может быть валидным или может быть смешанным (здесь валидный = всегда истинный).

Полнота означает, что если P действительно, мы в конце концов докажем это, и поскольку NOT P - это просто еще одно предложение, если оно действительно для этого. Однако это ничего не гарантирует в отношении смешанных предложений. Мы никогда не узнаем, что, если бы мы не продолжали поиски дольше, мы бы не нашли доказательства для P или для NOT P.

Или, чтобы уточнить еще больше, следующие два утверждения отличаются:

• "НЕ П" действительно
• НЕ "P допустимо"

Последний также включает смешанный P

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

Например, абелеву группу можно представить как алгебру, содержащую одну операцию («-» для вычитания), выделенный объект («0») и следующие тождества: 0 — 0 = 0, x — (x — y ) = у и х - (у - z) = z - (у - х).

Кроме того, например, аффинная геометрия A над конкретным полем F может быть выражена как двухсортная алгебра, содержащая тернарные операторы a,f,b ∈ A×F×A ↦ [a,f,b] ∈ A и a ,b,c ∈ A×A×A ↦ abc ∈ A, воплощающий операции [a,f,b] = (1 - f)a + fb и abc = a - b + c. Пример аксиом (подходящих, за исключением двух полей F = GF(2) размера 2 и F = GF(3) размера 3): [a,0,b] = a, [a,1,b ] = b, [a,rt(1-t),[b,s,c]] = [[a,rt(1-s),b],t,[a,rs(1-t),c ]], abc = [[b,1/(1-t),a],t,[b,1/t,c]], где t произвольно выбран как любой член поля F, отличный от 0 или 1 .

Для алгебраических теорий «свободная алгебра» — это та, которая содержит только выделенные объекты и любые другие объекты, которые можно сделать из них с помощью операций алгебры. Можно также говорить о «свободной алгебре, порожденной из множества X», когда члены множества X добавляются в список выделенных объектов. Например, приведенная выше алгебра вычитания, свободно порожденная из множества {1}, является одной и той же алгеброй целочисленного вычитания и содержит также алгебру целочисленного сложения посредством определений -x = (x - x ) - х и х + у = х - (-у). (Можно доказать x - x = 0, используя аксиомы, а именно: x = 0 - (0 - x) = x - (0 - 0) = x - 0, и x - x = x - (x - 0) = 0, поэтому -x = 0 - x является эквивалентным определением, но менее самодостаточным.)

Таким образом, теории первого порядка всегда могут быть реализованы моделями, что делает логику первого порядка полной. Это более точно указано в реферате, приведенном ниже, к «Теориям первого порядка как многосортные алгебры» (Notre Dame Journal Of Formal Logic 25 (1), январь 1984 г. https://www.researchgate.net/publication/ 38355700_теории_первого_порядка_как_множество_сортированных_алгебр )

Полнота гарантирует, что доказательство любого действительного утверждения может быть найдено с помощью конечного поиска. Неспособность найти доказательство, когда утверждение неверно, происходит только после того, как бесконечный поиск среди всех возможных доказательств никогда не заканчивается. Таким образом, вам придется ждать целую вечность, чтобы никогда не закончиться, прежде чем увидеть ответ «нет» на вопрос «действительно ли это?». Чтобы быть решаемым, ответ «нет» должен появиться за некоторое время до того, как вечность никогда не завершится.

Ключевой отрывок из аннотации:

«В этой статье, развивая изучение логики первого порядка с помощью многосортных алгебр, мы показываем, что каждая теория первого порядка является частной алгеброй, проверяющей аксиомы в эквациональной форме (см. раздел 2); поэтому мы можем применить теорию Биркгофа. теоремы о многообразиях (см. раздел 1 [и две ссылки, содержащиеся в статье]) и получить модели Хенкина алгебраически, откуда теорема о полноте логики первого порядка (см. раздел 3)».

Изюминка: ключевая фраза — «множественная сортировка», поэтому добавьте логический тип и переделайте предикаты как операторы с логическими значениями.