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

Классически, аксиоматическая система устанавливается с формальной системой вывода и интерпретацией в модели. В общем случае это правильно , то есть: формально выведенная теорема верна и при интерпретации в модели. Обратное называется полнотой, если предложение в модели истинно, то оно также формально выводимо. Это утверждение теоремы Гёделя о полноте .

Сбивающая с толку теорема Гёделя о неполноте относится к понятию разрешимости (это отличается от понятия разрешимости в теории вычислений, таких как машины Тьюринга и т.п.) - утверждение разрешимо, когда мы можем определить (решить), что оно имеет либо доказательство, либо опровержение. Если все утверждения в языке разрешимы, мы называем его полным. Теорема говорит о том, что аксиоматические системы, содержащие ПА, неполны, т. е. всегда есть утверждения, доказательство или опровержение которых мы не можем найти.

Что произойдет, если формальная система вывода будет не классической, а интуиционистской? Интуиционистская логика многозначна, но вместо моделирования истины моделируется конструируемость/доказуемость, которая вместо использования семантики теории множеств использует семантику Крипке. В настоящее время:

  1. Он все еще звучит ? То есть: формально выведенная теорема тоже конструируема?

  2. Он неполный ? Существует конструируемое предложение, которое формально не выводимо?

  3. Есть ли в нем неразрешимые утверждения?

Далеко не очень хорошо читается по этой теме, но на странице SEP, посвященной интуиционизму , есть несколько упоминаний теоремы о неполноте, и они могут быть полезны.
как упоминалось в ответах Гедле, теоремы о неполноте применимы к интуиционистской логике только в том случае, если они формализованы как своего рода классическая логика без LEM , но это не охватывает интуиционизм, как предложил Брюэр. По сути , IL — это не просто классическая логика без LEM, так как семантика отличается не только несколькими изменениями i (модифицировать пару правил) в синтаксисе.
Более того, конструктивная мантематика — это не просто классическая математика без аксиомы выбора (из которой следует ЛЭМ), а в цитатах проводится эта аналогия. Он воплощает в себе иной взгляд, связанный прежде всего с семантикой. В этом смысле наличие суждений, которые могут быть неразрешимыми, эффективно включает теоремы Геде как неотъемлемую часть интиоционизма с самого начала.
хороший пост «Доказательство Гёделя и интуитивизм» в том же направлении и значении, что и мои предыдущие комментарии ( аналогичный вопрос на math.SE )

Ответы (3)

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

Поскольку он и здравый, и полный , он не является неполным. Тот факт, что они относятся к «истине» как к чему-то вроде «доказуемости», не имеет отношения к ситуации.

Итак, является ли интуиционистская логика неполной? Нет, но это не относится и к классической логике первого порядка, и неполнота имеет тенденцию сопутствовать более сильным логическим системам, чем FOL, а не более слабым.

Я полагаю, что вопрос, который вы имеете в виду (хотя я извиняюсь за то, что предположил, что могу читать ваши мысли), заключается в том , подвержена ли интуиционистская/конструктивная математика неполноте. Ответ здесь - да. Гёдель представил доказательства конструктивно/интуиционистски приемлемым способом (т. е. используя только выводы, которые они подтверждают), и поэтому результат будет справедлив для интуиционистской теории чисел.

Стоит отметить, что вам не нужна такая сильная арифметика, как PA, чтобы стать жертвой неполноты. Все, что требуется, — это рекурсивно аксиоматизируемая теория чисел.

Арифметика Робинсона (Q) — теория намного слабее, чем PA (я полагаю, что это PA без индукции), но неполнота все же возникает. Это может быть (точно не помню) самая слабая система, все еще подверженная теоремам о неполноте. На самом деле она была задумана как слабая система — система, которая может представлять все и только рекурсивные теоретико-числовые функции.

Вот интересную статью, которую я нашел по теме --- похоже, хорошо читается. Эти конспекты лекций (опять же от Кевина Клемента) неплохо справляются с теоремами Гёделя, если хотите. В противном случае запись SEP , на которую ссылается @commando, также должна быть полезной.

спасибо за ссылки, они выглядят полезными. Не надо извиняться - Вы правильно поняли мои намерения! Я думаю, что путал полноту, которая относится к синтаксису и семантике, и неполноту, которая относится исключительно к синтаксису «формального доказательства» только через систему вывода/дедукции/доказательства, если я вас правильно понял. Какое стандартное название использовать — умозаключение/дедуктивное/доказательство — кажется, все они используются?!
@MoziburUllah Боюсь, я не совсем понимаю, на какую разницу вы указываете. Насколько мне известно, существует только одна форма (не)полноты: (не)способность формально доказать каждую истинность вашей теории.
Вы сказали, что «это и правильно, и полно, но не неполно », а затем «подвержено ли это неполноте . Ответ здесь - да». Я думаю, что эти два понятия полноты я перепутал - просто потому, что у них похожие названия.
@ Деннис Меня удивляет, что интуиционистская логика завершена, а конструктивная математика - нет, что означало бы, что есть дополнительные аксиомы, вызывающие неполноту?
@mcb На самом деле это не так уж и удивительно. (Классическая) Логика первого порядка — это язык, на котором формализована большая часть математики. Логика первого порядка полна, но очень немногие математические теории, основанные на ней, будут таковыми. Так что да, вы правы, есть дополнительные аксиомы, которые вы добавляете к основе интуиционистской логики, что приводит к неполноте конструктивной математики. В частности, любые аксиомы, которые вы добавляете и которые позволяют определить арифметику, по крайней мере столь же сильную, как арифметика Робинсона, являются аксиомами, которые заставят применить теорему о неполноте.
@Dennis Логика первого порядка - это язык, на котором формализована большая часть математики. Я думаю, что большая часть математики на самом деле формализована в том, что можно назвать логикой «второго порядка», поскольку вам серьезно необходимо довольно часто проводить количественную оценку функциональных символов.
@DavidTonhofer Да, я думаю, что в этом посте я несколько преувеличил свой случай. На первый взгляд, большая часть математики представлена ​​в форме первого порядка, а стандартная семантика — это теоретико-множественная семантика, в которой «сущности второго порядка» (свойства, функции, отношения и т. д.) рассматриваются как сущности первого порядка — множества. различных видов (например, 2-местное отношение — это просто набор упорядоченных пар, функция — это просто набор упорядоченных пар, где первый член пары никогда не связан более чем с одним другим объектом и т. д.) (продолжение .)
Однако, конечно, наиболее стандартной семантикой для логики второго порядка является теоретико-множественная, и поэтому это действительно мутит воду. За годы, прошедшие с тех пор, как я опубликовал этот ответ, я несколько озадачился тем, к чему сводится логический спор первого и второго порядка. Является ли теория второго порядка, если она синтаксически второго порядка, но с кажущейся семантикой первого порядка? Забудьте о полной семантике второго порядка и просто рассмотрите семантику Хенкина. Это доказуемо сводится к логике первого порядка и поэтому кажется различием без различия. (продолжение)
Может показаться, что решающее различие заключается в том, апеллирует ли семантика к понятию произвольного подмножества/свойства/множества, т. е. является ли это полной семантикой для SOL. Ясно, что это выходит за рамки логики первого порядка. Но мне все еще не ясно, выходит ли она за пределы теории множеств первого порядка, особенно учитывая, что у вас совершенно параллельные вопросы, например, к континуум-гипотезе, в обоих случаях — вопрос лишь в том, возникают ли эти вопросы для объект или метаязык. (продолжение)
Я думаю, единственное, в чем я в какой-то степени уверен, это то, что FOL — лучшая логика для захвата логических паттернов, а SOL — лучшая логика для решения вопросов определимости и значения. По сути, это разделение синтаксиса и семантики. Если вы думаете, что синтаксическое (дедуктивное) следствие — это конечная цель логики, идите первым порядком. Если вы думаете, что логика связана с моделированием определенных понятий, особенно с созданием категориальных теорий, касающихся этих понятий, то, возможно, вам подойдет логика второго порядка. (продолжение)
Ко всему этому перемежаются трудные вопросы о том, где провести грань между логикой и математикой. Ясно, что ЛОЛ — это логика, но как насчет теоретико-свойственной интерпретации логики второго порядка? Это может показаться прекрасным, но обычно считалось, что теоретико-множественные интерпретации слишком далеко отклоняются в математическом направлении (например, Куайн о логике второго порядка назвал «теорию множеств в овечьей шкуре»). Философия TL;DR остается сложной.
(Последний комментарий по этим вопросам на данный момент.) Я определенно соглашусь с тем, что большая часть обычной математики — т. е. все, что находится за пределами математической логики и кое-какой остальной части чистой математики — делается несколько менее формально и таким образом, что кажется более поддающимся лечению второго порядка (в том, что, как вы говорите, они, кажется, количественно определяют функции). Однако я не знаю, в какой степени эти математики считают себя работающими в рамках системы первого или второго порядка. Это не скептическое беспокойство, а просто искреннее невежество.
Что касается вашего комментария, учтите, что большинство математиков не используют индукцию как схему первого порядка, а рассматривают ее как единую аксиому, которая дает индукцию для каждого свойства натуральных чисел . Возможно, это металогический характер, что в чем-то похоже на логику более высокого порядка с семантикой Хенкина. Вот почему большинство из них назовут это «аксиомой индукции», а не «примером схемы аксиом индукции».

Два понятия (полнота и неполнота) не противоположны, а очень тесно связаны (не только именем Гёделя в названии двух теорем).

Примите во внимание, что гёделевская полнота Th логики первого порядка такова:
если предложение истинно во всех моделях аксиом (т. е. оно является логическим следствием аксиом), то оно также формально выводимо (в FOL) с помощью аксиомы.

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

Это не противоречит Полноте Th : вышеприведенное утверждение верно в стандартной модели, но НЕ верно в какой-то другой «странной» модели (их много): по этой причине оно не выводится из указанных аксиом.

Арифметическое утверждение, построенное Гёделем в его доказательстве, довольно «странно», но, исходя из результата Пэрис и Харрингтон (1977), в математической логике стало возможным найти утверждения, которые истинны (в стандартной модели), но недоказуемы. в арифметике Пеано и более «естественны». Это был первый «естественный» пример истинного утверждения о целых числах, которое могло быть сформулировано на языке арифметики, но не доказано в арифметике Пеано.

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

(адаптировано из моего поста на MathSE)

ПРИМЕЧАНИЕ 1. Интуиционистская логика НЕ ​​многозначна! (а ведь имя Геделя опять связано с исследованиями в этом направлении)

Справедливы ли теоремы Гёделя о неполноте как для классической, так и для интуиционистской логики?

В некотором смысле ДА.

НО

  1. Теорема (ы) Геделя о неполноте сначала применяется к классической логике .

  2. Теорема Геделя о неполноте и ее доказательство конструктивны , но не интуиционистски конструктивны ( статья Геделя )

Почему?

Сам Гедель заявил в своей статье, что вышеуказанная процедура « конструктивно не вызывает возражений », однако

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

б) вариации LEM (закона исключенного третьего) используются на протяжении всего доказательства Гёделя.

в) в сочетании с использованием процедуры диагонализации

(см. также Доказательство и интуитивизм Гёделя для другого анализа)

Применимо ли это то же самое к интуиционистской логике?

В некотором смысле ДА.

НО

  1. Отрицательный перевод Геделем классической логики в интуиционистскую логику является лишь формальным ( статья Геделя ) .

Почему?

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

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

в) сам Брауэр предвидел результаты Геделя как минимум на десять лет (примечание: сам Гедель посещал лекции Брауэра по основам математики)

Цитата из «Понимания конструктивной сематики» Артемова (лекция Спинозы)

введите описание изображения здесь

А также отсюда

Интуиционистская и классическая точки зрения

Интуиционисты обычно основывают свои формальные системы на интуиции конструктивной, например, неформальной семантики в стиле БХК , а не на классических основаниях...

Классические математики (такие, как Гёдель, Колмогоров, Клини, Новиков и др.)

классическое определение конструктивной семантики.

В свете вышеизложенного результаты Геделя о неполноте действительно верны для интуиционистской логики формальным образом (с классической семантикой), но не для интуиционизма (который в любом случае не нуждается в каком-либо результате неполноты, поскольку они уже встроены в практику и семантику)

Как интерпретируется теорема Гёделя о неполноте в интуиционистской логике?
СпросиСетьПолитика конфиденциальности1y, 0v