Является ли логика первого порядка (FOL) единственной фундаментальной логикой?

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

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

Обоснование этого самого факта и является причиной этого вопроса. Все, что я читал о металогических достоинствах FOL и свойствах его «расширений», можно резюмировать в виде следующих утверждений:

  • ЛОЛ полна ( Gödel, 1929 ), компактна и надежна, и все ее частные формализации в виде дедуктивных систем эквивалентны ( Lindström, 1969 ). Это означает, что при заданном (непротиворечивом) наборе аксиом поверх дедуктивной системы FOL набор всех синтаксически доказуемых теорем семантически удовлетворяется по крайней мере одной моделью аксиом. Спецификация аксиом абсолютно влечет за собой все свои следствия; и тот факт, что каждая дедуктивная система первого порядка эквивалентна, предполагает, что FOL является контекстно-независимой (т.е. объективной) формальной структурой.
  • С другой стороны, теорема Левенгейма-Скулема подразумевает, что ЛЖ не может категорически характеризовать бесконечные структуры, и поэтому каждая теория первого порядка, которой удовлетворяет модель конкретной бесконечной мощности, также удовлетворяется несколькими дополнительными моделями любой другой бесконечной мощности. Эта особенность некатегоричности объясняется недостатком выразительной силы ЛЖ.
  • Результаты категоричности, которых не могут достичь теории, основанные на FOL, могут быть получены в рамках логики второго порядка (SOL). Примеров изобилует обычная математика, например, аксиома наименьшей верхней границы , которая позволяет определить вещественную систему счисления с точностью до изоморфизма . Тем не менее, SOL не может проверить аналог результатов полноты FOL, и поэтому нет общего соответствия между синтаксической доказуемостью и семантической выполнимостью (другими словами, он не допускает полного исчисления доказательств). Это означает, что, даже если выбранный набор аксиом может категорически охарактеризовать бесконечную математическую структуру, существует бесконечное множество wff, которым удовлетворяет уникальная модель аксиом , которые не могут быть получены посредством дедукции .
  • Синтаксико-семантический раскол в SOL также подразумевает, что не существует такой вещи, как эквивалентная формулировка потенциальных дедуктивных систем, как это имеет место в FOL и утверждается теоремой Линдстрема. Одним из результатов этого факта является то, что область, в которой должен быть указан диапазон переменных второго порядка , в противном случае определяется неправильно. Если домен может быть полным набором подмножеств домена переменных первого порядка, соответствующая стандартная семантикавключают формальные свойства, указанные выше (достаточную выразительную силу для установления результатов категоричности и неполноту потенциальных, неэквивалентных дедуктивных систем). С другой стороны, посредством соответствующего определения доменов второго порядка для диапазона переменных второго порядка результирующая логика демонстрирует нестандартную семантику (или семантику Хенкина ), которая может быть показана как эквивалентная многосортному FOL ; и, как односортный ЛЖ, он подтверждает те же самые металогические свойства, заявленные в начале (и, конечно же, отсутствие у него выразительной силы).
  • Расширение количественного определения переменных последовательных высших порядков может быть формализовано или даже устранено различие между отдельными переменными (первого порядка) и предикатами; в каждом случае получается - для каждого N - логика N-го порядка (NOL) и логика высшего порядка (HOL) соответственно. Тем не менее, можно показать ( Hintikka, 1955 ), что любое предложение в любой логике над FOL со стандартной семантикой будет эквивалентно (эффективным образом) предложению в полном SOL с использованием множественной сортировки.
  • Все это указывает на то, что принципиальное различие, с точки зрения логики, лежит между ВОЛ (будь то односортный или многосортный) и СОЛ (со стандартной семантикой ). Или, что кажется так, логические основы каждой математической теории должны быть либо некатегоричными, либо не иметь полного исчисления доказательств, и между этим компромиссом не должно быть ничего промежуточного.

Почему же тогда ВОЛ неизменно выбирается в качестве базовой логики, поверх которой устанавливаются теоретические аксиомы множества, в любой потенциально фундаментальной формализации математики?

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

Судя по вашим разработкам, вполне может быть, что вы знаете следующие темы или их содержание, но я укажу на эту тему на доске по математике и особенно на размещенные в ней ссылки. Кроме того, вопрос, который я задал здесь , оказался в значительной степени и по этой теме.
Я думал об этом, и отсутствие ответа от сообщества философов может быть связано с тем, что это слишком математический вопрос, и поэтому я должен попытаться опубликовать его в Math.SE. Я периодически посещаю сеть SE в течение некоторого времени из-за качества предоставленных ответов, но только несколько дней назад я решил присоединиться, поэтому я довольно неосведомлен обо всех правилах и возможностях сайта. . Итак, я могу спросить вас: 1) Есть ли способ «перенести» вопрос с сайта вопросов и ответов на другой в сети без «ручного» (т.е. копирования и вставки) репоста?
2) Мой недавний опыт на сайте физики, по-видимому, показывает, что слишком длинные, сложные вопросы, которые не дают простого, краткого и легко узнаваемого ответа из учебника, не очень хорошо принимаются (по крайней мере, там). Является ли это общей функцией, или подобные вопросы могут не быть закрытыми, если они будут размещены на Math.SE? Времени, которое я проторчал, было недостаточно, чтобы убедиться в этом.
(i) Исходя из структуры stackExchange, я считаю, что ни один из этих сайтов (физика или философия, а также, в некоторой степени, и математика) не является хорошим местом для вопросов, которые действительно интересны, потому что из вопросов такого типа вы обычно учитесь в ходе обсуждения. . Вопросы на математической доске обычно имеют ответ, имхо, если они носят «философский» характер, то это не настоящие математические вопросы, или они касаются определенных понятий, определение которых неясно. Что касается этого вопроса, то я не понимаю, зачем ФОЛу нужно больше аргументов, чем та куча моментов, о которых вы уже знаете.
(ii) Я думаю, что вы можете сделать основу теории SOL-множества. Но по ссылкам люди рассуждают, что скорее не видели, поэтому делаю вывод, что ресурсов просто не хватает - ведь можно смоделировать SOL и FOL, как говорится. Возвращаясь, в основном сайты хороши для вопросов, на которые вы могли бы ответить сами, если бы уделили время чтению правильных книг. Конечно, это тоже важные вопросы, потому что у людей ограниченное время. Я готов к некоторому обсуждению, но опять же вы говорите, что не хотите, чтобы неспециалисты открывали рот, и у меня в основном меньше знаний, чем у вас;)
(iii) Да, и да, кто-то (модераторы?) может переместить вопрос с одной доски на другую.
Спасибо, что нашли время ответить мне, Ник. Я должен согласиться с тем, что картина, которую вы даете, верна: нельзя жаловаться на сайты вопросов и ответов, которые пытаются сосредоточиться на своих первоначальных целях. Но опять же, неловкость в том, что у нас здесь много умных людей, которых вы вряд ли найдете где-либо еще, и все же во имя чистоты трибуны от нас ожидают, что мы не будем вступать в более глубокую дискуссию между нами. Возможно, мне следует изучить приложение чата — я еще не проверял его, — но, похоже, это в основном способ личного обсуждения тем один на один. Хотя я, несомненно, предпочитаю публичное обсуждение.
А насчет цитаты "не хочу, чтобы неспециалисты открывали рот": я только что разъяснил свое состояние неспециалиста (и могу добавить, того, кто не планирует зарабатывать на жизнь этим материалом ), чтобы поставить вопрос в контексте. Возможно, кто-то, кто полностью понимает все последствия резюме, которое я изложил выше, сочтет вопрос вопиюще очевидным. Я просто не могу знать. В каком-то смысле я попытался четко указать, что все остальные должны интерпретировать в отношении моего понимания области, чтобы дать ответ. Но ваша готовность к обсуждению приветствуется, конечно!
Кажется, что в ссылке, которую вы разместили в комментарии к ответу, вы ссылаетесь на то, что я взад и вперед с одним ответчиком относительно необходимости контекста для различения утверждений FOL и SOL. Если это так, я рад косвенно предоставить вам некоторую информацию, и я рад, что есть люди, задающиеся такими же вопросами ^^
addon: В обсуждениях одной из ваших тем вы, кажется, удовлетворены FOL, потому что есть теорема о полноте. Пока вы боретесь с семантикой логики второго порядка, у меня еще хватает проблем с семантикой логики первого порядка, хе-хе. См., например, мою ветку здесь (обсуждение у меня там), а затем я пытаюсь разобраться здесь .
Я полагаю, вы цитируете последнюю ссылку, которую я оставил в этом моем вопросе , и да, то, что туда и обратно, в котором вы участвовали , действительно было очень полезным. Как вы правильно поняли, мы, кажется, беспокоимся об одном и том же. В вашем аддоне есть вполне объяснимая причина, по которой я не слишком беспокоюсь о семантике FOL, но я хотел бы изложить все это в ответе, если вы написали это как вопрос.
Дело обстоит так: в FOL вы обходите семантические проблемы, потому что вы никогда не узнаете, о чем говорите, когда записываете аксиомы и правила вывода вашей формализованной теории. Это буквально означает, что (например) к нему можно добавить отрицание гёделевского предложения «G» теории FO «T», чтобы получить совершенно непротиворечивую более сильную теорию «T + ¬G» (при условии непротиворечивости T), и тогда вы видите, что ваша первоначальная теория имела очень эзотерические модели — потому что остальные модели, в которых истинно ¬G, не являются стандартными, т. е. в них это не означает то, что вы «читаете» —.
Итак, если T = PA и G = Con(PA), в модели «T + ¬G» ¬G означает не то, что вы читаете, то есть PA на самом деле несовместимо. Это всего лишь формальное свойство, которое нуждается в другой интерпретации, чтобы быть обоснованной (построение соответствующей модели и есть способ найти нужную интерпретацию). Конечно, в «стандартной интерпретации» G истинно, а ¬G ложно; но это значит, что вы уже знаете, о чем говорили, например, что такое натуральное число, поэтому толкование было закреплено вами заранее. Это, формально говоря, не имеет смысла.
Если вы хотите, чтобы я что-то видел, вы должны указать мое имя. Кроме того, я не думаю и не вижу, что то, что вы говорите, решает мои проблемы. Ветка G vs. not G — это способ ответить на проблемы из раздела комментариев другой ветки, которую я разместил. А именно, в каком смысле люди считают что-то истинным без необходимости доказательства. Моя проблема чуть ли не перед теорией множеств и моделями — люди чувствуют, что есть истина, которая указывает, что моделировать. На самом деле это только платонизм против (возможно, моего личного варианта) формализма. И я хочу быть в состоянии понять платоников, потому что математическая история полна ими.
Я не понимаю, на что вы жалуетесь в первом предложении. Я не пытался убедить вас «посмотреть что-нибудь», и я не понимаю, откуда взялась «личная ссылка». С другой стороны, в платонизме нет ничего непроницаемого: если вы считаете, что строки символов — это просто царапины на бумаге, если вы не можете отождествить их с каким-либо известным вам математическим свойством (например, вы могли бы увидеть «%<$!$<%» и распознать коммутативное свойство абелевой группы, где «%» и «$» — метапеременные, «<» — групповая операция, а «!» — символ равенства), тогда вы один.
Смысл, в котором «люди считают что-то истинным без необходимости доказательства», лежит в основе дискуссий об аксиоматизации любой достаточно сложной математической области, т. е. там, где имеет место неполнота. Аксиомы (если вы платоник, каким на самом деле является большинство математиков) могут быть не просто набором символов, но мы должны быть в состоянии интерпретировать их как значимые свойства абстрактных объектов; проблема в том, что неполнота приводит к множеству непротиворечивых аксиоматических систем, и некоторые из них обладают странными свойствами, удовлетворяемыми их семантикой.
В сущности, платоник «предпочитает» один вид семантики (в FOT, подобном ZFC , это означает «вселенная» множеств V , а в PA это означает «натуральные числа N » ) для формализмов, которые он записывает, но есть и другие. всегда странная семантика, альтернативная тем («стандартным»), которые, тем не менее, удовлетворяют аксиомам — и действительно делают их «истинными» в соответствии с этой семантикой. Как платоник находит «правильную» семантику? Геделевская позиция состоит в том, что (математическая) интуиция делает свое дело. Мое личное мнение по этому поводу таково, что интуиция работает только в конечной сфере, но терпит неудачу в трансфинитной.
В прошлый раз я не получил комментарий, именно об этом было первое предложение, и под ссылкой я имею в виду использование @.
@NickKidman: Прошу прощения, если я вас неправильно понял. Я не логик, но вот что я сделал, прочитав об этом предмете. FOL, кажется, имеет уровень «свободы» в своей семантике, что делает проблему платоника вопросом «знакомства» или «интуитивного распознавания образов», когда математик взаимодействует с формальной системой. При этом я думаю, что множественность независимых семантик (взаимно несовместимых моделей), способных удовлетворить один и тот же набор аксиом ФО, в некотором смысле предполагает случайность любой интерпретации, даже стандартной (платонистской).
Я действительно не понимаю вас и не знаю, как вы интерпретируете мои проблемы, но все равно спасибо за вклад.
@NickKidman: поскольку это становится слишком длинным, могу ли я предложить вам снова опубликовать это как прямой вопрос? Если, конечно, вы уже это сделали.
Я не вижу способа задать вопрос, на который можно было бы получить нейтральный или даже окончательный ответ.
@NickKidman: ну, это уже другая история. Что я понял из ваших ответов здесь, так это то, что вы озадачены тем фактом, что кто-то может верить в истинность математического утверждения, потому что оно «чувствует», что оно имеет место — интуиция, стоящая за идеями, на которых построены аксиоматические системы. Моя позиция состоит в том, что (в FOL) это, вероятно, не проблема, потому что мы обманываемся интуицией, когда имеем дело с бесконечными структурами, поэтому нет никакого фундаментального обоснования понятия «стандартная семантика», т. е. что V или N являются идеально определенными объектами . . Это не так.
Только что заметил ваш комментарий про В. По поводу проблемы поиска нужной модели, возможно, вас заинтересует этот пост . Во всяком случае, я не очень понимаю ваш вопрос здесь. Реальность, кажется, полностью подчиняется классической ЛОЛ. Разве этого недостаточно, чтобы захотеть работать в FOL? В любом случае, что вы подразумеваете под "основным"? Все широко разрекламированные версии «математического платонизма» плохо определены, так что же здесь означает «фундаментальный»?

Ответы (3)

Является ли логика первого порядка (FOL) единственной фундаментальной логикой?

Короткий ответ

нет . Это просто самая популярная логика среди математиков и философов, прежде всего по историческим и культурным причинам.

Длинный ответ

Поскольку вы написали длинный вопрос, вот длинный ответ :-)

Первоначально Фреге предложил форму логики второго порядка в качестве основы математики в своих « Основах арифметики» (1884 г.). Эта основа вышла из моды после того, как Рассел лихо нашел противоречие в этой системе (все об этом можно прочитать на SEP ).

С тех пор очень немногие философы и математики выступали за возрождение логики второго порядка как основы математики. Знаю только троих: Йоуко Вяянянен, Стюарт Шапиро и Джордж Булос. У Стюарта Шапиро есть книга об этом: «Основы без фундаментализма: пример логики второго порядка» (2000) .

Однако SOL уродлив. У него нет полной системы аксиом для его стандартной семантики; единственные полные исчисления предназначены для нестандартных моделей (см. Henkin (1950) ). Кроме того, теоремы о компактности не работают для обычной семантики SOL; Теория моделей для ВОЛС в целом может считаться более надежной. Väänänen (2001) дает хороший обзор свойств логики второго порядка. Кроме того, хотя теорема Левенгейма-Скулема неверна для стандартной семантики SOL, она верна для нестандартной семантики Хенкина. Вяэнянен утверждает: «Если логика второго порядка истолковывается как наша примитивная логика, нельзя сказать, имеет ли она полную семантику или семантику Хенкина, и мы не можем осмысленно сказать, аксиоматизирует ли она категорически ℕ и ℝ».

Авраам Робинсон, вероятно, согласился с Вяэняненом в этом вопросе. В своем опусе « Нестандартный анализ» (1960), глава 2, он представляет семантику Хенкина для логики более высокого порядка. Он продолжает доказывать компактность, Левенгейма-Скулема и теорему Лоша. Робинсон почти не обращает внимания на класс стандартных моделей более высокого порядка (которые он называет «полными моделями»). То, что Робинсон принял нестандартную семантику Хенкина, конечно, имеет смысл. Вся острота нестандартного анализа исходит из того факта, что ℝ не является категоричным, а теорема Лоша работает .

Кроме Робинсона (и, может быть, Вяэнянена) никто на самом деле не считает семантику Хенкина основой. Никто из работающих над фундаментом не интересуется неаксиоматизируемыми системами. Весь смысл исследовательской программы обратной математики Харви Фридмана в том, что у нас есть различные аксиоматические системы, и мы можем рассуждать об их доказуемости.

Конечно, идея о том, что FOL против SOL для основ математики, в любом случае является ложной дихотомией.

Почему же тогда ВОЛ неизменно выбирается в качестве базовой логики, поверх которой устанавливаются теоретические аксиомы множества, в любой потенциально фундаментальной формализации математики?

Это не всегда выбрано . Его первенство в математике и философии связано с его ранним успехом и быстрым развитием по сравнению с конкурентами.

Исследования математиков и философов в области основ математики раскололись в нескольких направлениях после увольнения Grundlagen Фреге . Вы можете прочитать о них в антологии Хейеноорта « От Фреге до Гёделя: Справочник по математической логике» (1999) :

  • Логики Первого Ордена : первое, подавляющее большинство. К ним относятся Гиссеппе Пеано, К.С. Пирс, Дэвид Гильберт, Джордж Кантор, Рихард Дедекинд, Скулем, Лёвенгейм, Цермело, Френкель, Хербранд, ребята из Бурбаки, Куайн, Тарский, (ранний) Витгенштейн и т. д.
  • Многие сортированные логики : Рассел, Уайтхед и (иногда) Гёдель.
  • Отцы вычислений : Моисей Шенфинкл, Алонзо Чёрч и его ученики.
  • Конструктивисты : Кронекер, Колмогоров, Брауэр и его ученики.

Следует отметить, что Пеано, Пирс и Гильберт разработали логику первого порядка примерно независимо друг от друга; это подтверждает идею о том, что ЛОЛ является естественной основой математики.

Хотя другие подходы не исчезли, все они столкнулись с трудностями на раннем этапе.

Теория типов была разработана слабо: всем известно, насколько легендарно непрозрачна Principia Mathematica Рассела и Уайтхеда . Рассел долго боролся, прежде чем разработать разветвленные типы , с которыми было сложно работать. В конечном итоге Леон Чвистек и Фрэнк Рэмси продемонстрировали, что систему можно упростить, что привело к созданию теории простых типов в 1920-х годах. К сожалению, Рэмси умер очень молодым, поэтому любой вклад, который он мог бы внести, был прерван. Вдобавок Рассел отказался от логики после написания « Начал », а его ученик Витгенштейн не приложил усилий для ее развития.

«Отцы вычислений» также столкнулись с проблемами, хотя они также появились позже, чем теория множеств FOL и ZF. После публикации «Основных элементов математической логики» в 1924 году Моисей Шенфинкель оказался в ловушке за железным занавесом и больше никогда не публиковался. Позже его работу подхватил Черч, который соединил ее со своим λ-исчислением. λ-исчисление, хотя и более выразительное, чем FOL, никогда не подходило в качестве основы для математики. Ряд основополагающих систем, построенных на λ-исчислении, был предложен в 30-х годах Чёрчем и другими. Было показано, что наиболее популярные из этих систем противоречат тому, что сейчас известно как парадокс Карри (см. Карри (1941) ).

Наконец, у конструктивизма и интуиционизма были свои проблемы. Очевидный недостаток конструктивизма — слишком ограничительный. Математик всегда примет конструктивное доказательство, но найти неконструктивное доказательство легче и общеприемлемо. Другая проблема связана с логикой: интуиционистская логика и арифметика не были аксиоматизированы до Гейтинга в конце 1920-х гг. Адекватная семантика для интуиционистской логики предикатов (IPC) также долгое время оставалась открытой проблемой. Слабое доказательство полноты было предоставлено Крайзелем в 1950-х годах с использованием предполагаемой семантики Брауэра (т . е. последовательностей выбора ). Позже Крипке дал строгое доказательство полноты.для IPC в 1960-х годах с использованием структур Крипке. «Расцвет» интуиционистской теории моделей в 50-х и 60-х годах опоздал на 30 лет, чтобы оказать какое-либо влияние на основы математики.

Между тем, пока соперничающие фонды боролись, FOL/ZF в конечном итоге завоевали сердца основных математиков и философов. Современные фундаментальные математики в основном занимаются тонкой настройкой существующего фундамента. После того, как Пол Коэн продемонстрировал независимость гипотезы континуума ( 1963 ), математики начали исследовать независимость различных утверждений в ZF и некоторых расширениях. Одним из важных аксиоматических расширений является Аксиома Вселенной Гротендика , которая эквивалентна существованию сильно недостижимого кардинала. Эта аксиома широко популярна в алгебраической геометрии и использовалась Уайлсом в его доказательстве Великой теоремы Ферма (хотя здесьХарви Фридман утверждает, что использование аксиомы на самом деле не обязательно). Говоря о Харви Фридмане, еще одной важной фундаментальной исследовательской программой является обратная математика , изучающая силу доказательств систем, расширяющих арифметику Пеано, но более слабых, чем ZF.

Также была разработана теория моделей первого порядка. Старым триумфом теории моделей является теоретико-модельное доказательство гипотезы Лэнга, данное Грушовским ( 1998 ). Несмотря на категоричность ℕ и ℝ в SOL, немногие математики изучали теорию моделей второго порядка с 50-х годов. В FOL также есть результаты категоричности: например, (ℚ,<) является ω-категоричным в FOL.

А в философии ни один философ не проповедовал ЛЖ больше, чем Куайн. Я бы сказал, что превосходство Куайна, вероятно, является причиной того, что философы знают только FOL и ZF и ничего больше не знают.

В то время как основные математики и философы игнорировали их, другие фундаментальные исследовательские программы укреплялись и в конечном итоге процветали.

После неудачи с использованием λ-исчисления в качестве основы Черч и многие его ученики обратились к использованию простых типов. В результате исследовательская программа Рассела объединилась с программой Черча.

Дальнейшим развитием стала неожиданная, не голландская интерпретация интуиционистской логики: конструируемые типы в просто типизированном λ-исчислении в точности соответствуют пропозициональной интуиционистской логике. Это так называемая переписка Карри-Ховарда .

Переписка Карри-Ховарда в конечном итоге вдохновила Пера Мартина-Лёфа на изобретение интуиционистской теории типов в начале 70-х годов как новой альтернативной основы математики. Первоначальная формулировка страдала дефектом, известным как парадокс Жирара , хотя систему можно было спасти, и Мартин-Лёф не отказался от нее.

Студентам, изучающим информатику, хорошо известно, что λ-исчисление вдохновило Джона Маккарти и Стива Рассела на изобретение LISP. То же самое произошло с просто типизированным λ-исчислением в начале 70-х годов. Дана Скотт, бывший студент церкви Алонзо, изобрел «Логику для вычислимых функций » для рассуждений о семантике обозначений типизированных функциональных программ в конце 60-х годов. В 1973 году Робин Милнер и компания внедрили LCFпервого помощника по компьютерной проверке. Это было сделано после разработки первого функционального языка программирования с простой типизацией ML(«MetaLanguage»), на котором он был написан.

С тех пор фундаментальные исследования, не относящиеся к FOL / ZF, в основном проводились с сообществом компьютерных наук.

Одним из примеров является HOL, или «логика высшего порядка», примерно смоделированная по образцу простого лямбда-исчисления Черча ( 1940 ). После ряда доработок Майк Гордон выпустил HOL88, предназначенный для аппаратной проверки. Как признает Гордон в своей короткой истории на эту тему, его код взламывал части LCF, когда это было удобно, и был довольно случайным ( 1996 ). Позже HOL был преобразован Джоном Харрисоном и Конрадом Слиндом в HOL-Light ; HOL-Light имеет 9 элементарных правил, которые отдаленно напоминают Equational Logic , и три аксиомы ( аксиома бесконечности , аксиома выбора с использованием ε Гильберта и закон Лейбница ).

Другим расширением является Isabelle/HOL , которое консервативно расширяет систему типов HOL с помощью «контекста». Еще одна система — HOL-Omega от Homeier , которая консервативно расширяет систему типов еще дальше.

Еще одна разработка — NuPRL из Корнельского университета, реализующая интуиционистскую теорию типов Мартина-Лёфа. Агда похожа. Связанной системой INRIA является Coq , которая реализует исчисление конструкций Тьерри Коканда, которое расширяет интуиционистскую теорию типов.

Разработка новых систем замедлилась за последнее десятилетие или около того, но не остановилась. Несколько систем FOL/ZF (а именно, Isabelle/ZF и Mizar ) относительно неактивны.

Я бы резюмировал свою позицию следующим образом: сказать, что FOL неизменно выбирается в качестве базовой логики , все равно что сказать, что Windows неизменно выбирается в качестве базовой платформы для компьютерных игр .

В обоих случаях это культурная вещь.

Одна из основных проблем, с которыми я сталкиваюсь, пытаясь рассуждать об отношениях между HOL (и любой другой логикой более высокого порядка, чем FOL) и компьютерными системами, заключается в том, что я не совсем понимаю, как такая логика — с ее стандартной семантикой — работает в «механической» системе, такой как компьютер.
Например, в этом посте у вас есть пример предложения на языке теории множеств, которое не может быть распознано как FO или SO , если контекст явно не указан . Создается впечатление, что «семантическое принуждение к интерпретации» в формальных системах, основанных на логике выше ФОЛ, не может быть включено в сам формализм. Отсутствие у меня опыта в CS делает это особенно трудным для понимания, и это, конечно же, причина большинства моих проблем с принятием «разнообразия» возможных логик.
Кстати, это очень хороший, продуманный ответ. Спасибо, что уделили этому время.
@Mono: у меня действительно нет места, чтобы адекватно ответить на ваши вопросы в этих комментариях; может быть, вы могли бы написать несколько новых вопросов, которые вас озадачивают, здесь, CSTheory, Mathematics или MathOverflow?
Ты прав. Вот я задал новый на Math.SE:
Это фантастический ответ! Хотелось бы, чтобы у меня было больше голосов. знак равно
Это Кронекер.
@NikolajK Исправлено!
«Это было сделано после разработки первого функционального языка программирования с простой типизацией ML» — разве ML не был основан на системе типов Хиндли-Милнера, а не на лямбда-исчислении с простым типом? Или вы имели в виду систему типов LCF?

Кто-то должен указать, что семантика, которую математики фактически используют изо дня в день, все еще является логикой второго порядка или ее эквивалентом, несмотря на все беспокойства по поводу основ.

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

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

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

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

Этот ответ совершенно неверен и явно написан кем-то, кто не знает, о чем говорит. Абсолютно никто не может использовать SOL с полной семантикой. SOL с семантикой Хенкина может быть тривиально отнесена к FOL. И спрашивающий уже заявил это!! И все разумные фундаментальные системы страдают от обобщенных теорем о неполноте; это предрешено .

Фонды имеют цели:

  1. Представить подход к математике, в котором мы можем быть уверены, что он непротиворечив.
  2. Представить язык и методологию, с помощью которых мы действительно можем заниматься математикой.

Эти цели в основном диаметрально противоположны. Самый простой способ достичь первой цели — это иметь очень минимальный набор инструментов, чтобы можно было рассуждать об их правильности. Однако вторая цель настоятельно побуждает нас использовать множество различных инструментов для конструирования, манипулирования и проверки вещей.

Очень хорошим решением этой проблемы является простое разделение фундамента на два слоя: первый слой очень минимальный, в правильности которого мы уверены, и на его основе мы строим второй слой, который имеет все практические функции, которые мы хотим использовать. для занятий математикой.

Это то, что вы видите сегодня; логика первого порядка является обычным выбором для первого уровня, а затем некоторая форма теории множеств в качестве второго уровня.

Заметьте, между прочим, что логика высшего порядка сама по себе является своего рода теорией множеств.

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

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