Краткий ответ (tl;dr)

Соответствующий исторический контекст для ответа на ваш вопрос — это долгие поиски логики для обеспечения основ всей математики . Аксиоматическая теория множеств Цермело вытеснила таких соперников, как теория типов, и сразу же выиграла гонку, потому что логики этой традиции разработали металогические инструменты (теорию моделей, теорию доказательств) для исследования систем аксиом. Вклад Цермело был сделан примерно в 1908 году, и благодаря работам Френкеля, Скулема и других в середине 20-х годов (до результата Гёделя о полноте) он быстро стал стандартной теорией множеств, которую мы знаем сегодня, теорией множеств Цермело – Френкеля + Выбор (ZFC)

То, что ZFC стала чистой теорией первого порядка, связано с ранней работой Дэвида Гильберта над подсистемой логики, которую он назвал ограниченным функциональным исчислением (фактически сегодняшняя логика первого порядка), и Торальфом Сколемом , который в 1923 году дал первоначальную теорию первого порядка . аксиоматизация теории множеств Цермело. Аксиоматическая теория множеств фактически стала доминирующей теорией первого порядка в середине 30-х годов и остается таковой по сей день. Большинству теоретиков множеств очень нравятся свойства логики первого порядка (полнота, компактность и т. д.). Тот факт, что теория множеств первого порядка отклоняется от математической практики, на самом деле рассматривается как особенность, а не как ошибка.

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

Сегодня это кажется тривиальным, но для того, чтобы принять логику первого порядка ( FOL ), нужно уметь изолировать ее от логики второго порядка ( SOL ) или логики более высокого порядка. И эта возможность сама по себе была важным завоеванием. Вплоть до Principia Mathematica несколько версий логики второго порядка (включая инфинитарную логику ) обычно использовались логиками без особой осторожности. FOL и SOL на самом деле не отличались (различались?) до тех пор, пока относительные достоинства и недостаткикаждого из них были исследованы. Или, говоря наоборот: это были фундаменталистские поиски, которые привели к изучению не только выразимости, но и свойств различных фрагментов, и именно через это место были выделены ВОЛ и СОЛ.

1. Две традиции в логике

Мне кажется, что все началось с открытия Расселом знаменитого парадокса в 1901 году в наивной теории множеств Кантора (открытого независимо Цермело, который сообщил о нем Гильберту). Поскольку парадокс также появился в формализованной версии наивной теории множеств Фреге, логики начали изобретать различные способы избежать этой проблемы и создавать новые теоретико-множественные подходы. Двумя наиболее важными предложениями, исправившими эти (и другие) парадоксы, были теоретико-типовая теория множеств Рассела и теория множеств Цермело .

Эти два решения обычно рассматриваются как выражение двух разных «напряжений» внутри логики: традиции Пеано-Фреге-Уайтхеда-Рассела и традиции (Пирса)-Шредера-Гильберта-Цермело .

2. Металогическое исследование

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

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

• отсутствовала какая-либо концепция метаязыка
• прямо отрицал возможность доказательства независимости своих аксиом
• считал невозможным доказать, что подстановка вообще применима в теории типов
• настаивал на том, что принцип математической индукции нельзя использовать для доказательства теорем об их системе логики

В наши дни трудно понять, что означает заниматься логикой, без различия языка и метаязыка и различия синтаксиса и семантики !

3. Появление ВОЛС

Я думаю, это не совпадение, что именно в этой метатеоретической обстановке и в традиции Шредера-Гильберта-Цермело логика была положена на операционный стол для, так сказать, вскрытия. Это было прямым следствием необходимости металогически исследовать свойства (обоснованность, полноту, компактность, непротиворечивость, категоричность и т. д.) различных логических фрагментов: В 1918 г. Бернейс дал первое строгое доказательство полноты такой подсистемы логики, т. е. пропозициональной логика. Еще одним фрагментом оказалось то, что мы сейчас называем ВОЛС . В частности, оно было впервые разработано Гильбертом в 1917 году под названием « ограниченное функциональное исчисление » как подсистема его функционального исчисления (фактическитеория разветвленных типов ), но была опубликована только в классическом учебнике, написанном в соавторстве с Аккерманном « Основы теоретической логики » в 1928 году, где она все еще рассматривалась как подсистема.

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

Тот факт, что теория множеств сегодня является теорией ФО, возможно, принадлежит Торальфу Скулему . В 1923 году Скулем представил оригинальную аксиоматизацию теории множеств Цермело. Теперь существует стандартная точка зрения, согласно которой «ось» Скулема-Гёделя побуждает принять теорию множеств FO и несет ответственность за окончательное утверждение теории множеств FO. Однако совершенно не ясно, что это было так, т. е. что Сколем (и Гёдель) продвигали объектный язык ФО в теории множеств. Хотя Скулем критически относился к теории множеств второго порядка как к основе математики, он доказал, что его (нисходящая) теорема выполняется в FOL . Результат - в счетной модели верно наличие несчетного множества - он назвал философским (хотя и не формальным) парадоксомчтобы утверждать, что и ВОЛ не может служить основой математики:

Я полагал настолько очевидным, что аксиоматизация в терминах множеств не является удовлетворительным окончательным основанием математики, что математиков по большей части это не слишком интересовало. Но в последнее время я, к своему удивлению, увидел, что так много математиков считают эти аксиомы теории множеств идеальным основанием для математики; поэтому мне казалось, что пришло время для критики. (Скулем, 1922 г.)

(Есть даже подозрение, что аксиоматизация Скулема была FO случайно …! Есть несколько веских свидетельств того, что многие лучшие умы своего времени, такие как Френкель и фон Нейман, не могли реально понять разницу между FOL и SOL. в середине 20-х!).

А Гёдель, хотя и выступал за *мета*язык ФО, использовал вариант теории типов в своей знаменитой статье 1931 года!

Безусловно, нельзя отрицать, что и Скулем, и Гёдель внесли важные теоремы, помогающие установить ВОЛ, но на самом деле они не приводили доводов в пользу этого. По правде говоря, здесь нет простой истории успеха с героями . Более правильное объяснение, вероятно, включало бы несколько причинных факторов.

Заявление ОП о том, что

полнота логики первого порядка была доказана Куртом Гёделем только в то время, когда логика первого порядка уже вытеснила логику второго порядка.

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

4. Почему (не) теория множеств первого порядка?

Тем не менее, я все еще удивляюсь, почему […] почему неспособность логики первого порядка охарактеризовать бесконечную структуру не считается проблемой.

Что ж, прагматичный ответ заключается в том, что это не считается проблемой из -за неспособности FOL ;)

Поскольку невозможно охарактеризовать (т.е. категорически аксиоматизировать ) бесконечные структуры в ВОЛС, как вы говорите, теоретики множеств просто работают с предполагаемой моделью и заботятся о нестандартных моделях только тогда, когда они необходимы. Это настолько хорошо, насколько это возможно, я беспокоюсь.

Более общий спор касается размышлений о достоинствах и недостатках FOL и SOL. На первый взгляд кажется, что

• ВОЛС

   + complete, compact, nice model theory 
   - deviating from mathematical practice
  

• соль

   + adherent to mathematical practice
   - completeness does not hold
  

Так как достоинства ВОЛ никто не оспаривает, то сводится к вопросу, в чем действительно хорошо соблюдение математической практики и как оценивается потеря достоинств ВОЛ. Из моего опыта общения с логиками

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

• сторонники SOL не сочли бы фатальной потерю комплектности и т.п. Они рассматривают теорию множеств не столько как основу математики. Наоборот, теория множеств должна быть скорее описанием математики, т. е. чем больше она соответствует математической практике, тем лучше (= точнее) становится описание.

• некоторые видят промежуточный путь между ними, принимая другую теорию множеств FO, такую ​​​​как теория множеств Морса-Келли. MK, который допускает правильные классы вместе с наборами, синтаксически почти идентичен ZFC второго порядка, но сильно отличается по своей семантике.

Выбирайте на свой вкус :)

Источники и дополнительная литература:

• Немного истории логики
• Грегори Х. Мур: Возникновение логики первого порядка (статья)
• Матти Эклунд: О том, как логика стала первопорядковой (статья)
• У. Д. Харт: Эволюция логики (книга)
• Джеральдин Брэди: От Пирса до Скулема: забытая глава в истории логики (книга)
• Итан Джерзак: Логика второго порядка, или Как я перестал волноваться и полюбил теоремы о неполноте (статья)
• Основы Стюарта Шапиро без фундаментализма: пример логики второго порядка (книга)

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

До начала 20 века логика не существовала в какой-либо достаточно точной формулировке, которая позволяла бы машине выводить следствия из аксиом. Это означает, что вся философская работа по логике со времен Аристотеля до времен Буля и Фреге имела отрицательную ценность --- она ​​создавала иллюзию того, что логика каким-то образом понята, когда люди понятия не имеют. Ни одна из этих работ не представляет собой ничего, кроме исторической ценности.

Суть схем дедукции начала 20 века заключалась в том, чтобы математические рассуждения могли выполняться механически, без какого-либо человеческого понимания. Цель состояла в том, чтобы сделать теорию множеств свободной от противоречий, рассматривая математику как формальное манипулирование текстом, то, что мы сегодня назвали бы вычислением над строками. Развитие дедукции Гильберта и теоремы Геделя о полноте вместе с разумными теоретико-множественными аксиомами завершили эту программу и показали, что логика первого порядка подходит для этой цели. Учитывая любой набор аксиом, логика первого порядка выведет любое следствие и создаст модель этих аксиом.

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

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

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

Логика первого порядка стала доминирующей формальной логикой, потому что она лежит в основе всей логики. Любое отклонение от FOL создает неясности, которые необходимо разрешить. Например, предложение второго порядка «мужчина вошел в комнату с цветами» неоднозначно. Это могло означать, что мужчина нес цветы в комнату или что мужчина вошел в комнату, где уже стояли цветы.

Джон Сова написал о FOL следующее:

«Среди всех разновидностей логики классическая логика первого порядка имеет привилегированный статус. Она обладает достаточной выразительной силой, чтобы определить всю математику, каждый цифровой компьютер, который когда-либо был построен, и семантику каждой версии логики, включая ее саму. логика, модальная логика, нейронные сети и даже логика более высокого порядка могут быть определены в [логике первого порядка]... Помимо выразительной силы, логика первого порядка имеет наиболее точно определенную, наименее проблематичную теорию моделей и теорию доказательств, и она может быть определена в терминах абсолютного минимума примитивов… Поскольку логика первого порядка обладает такой огромной силой, многие философы и логики, такие как Куайн, решительно утверждали, что классическая [логика первого порядка] в некотором смысле является «единственной истинной». логика», а другие версии избыточны, ненужны или непродуманны».