Чем «логика высшего порядка» отличается от «нормальной» логики предикатов? Я предполагаю, что последнюю последовательно называют «логикой первого порядка». Так где же между ними различия? Какие утверждения можно выразить или доказать с помощью логики высшего порядка, но не с помощью логики первого порядка? Интуитивные (в разговорном смысле) примеры приветствуются.
Этот вопрос начинался как предложенный вопрос для предлагаемого Logic SE , который теперь был объявлен дубликатом op Philosophy.
Вы можете обратиться к http://plato.stanford.edu/entries/logic-higher-order/ для пояснений, примеров и дополнительных ссылок.
У вас есть теорема о полноте Геделя в классической логике первого порядка, которая недоступна в логике более высокого порядка. Эта теорема устанавливает эквивалентность между синтаксической или формальной истиной и семантической истиной. Формальная истина — это то, что может быть доказано вашей логикой путем манипулирования логическими предложениями в соответствии с вашей дедуктивной системой, семантическая истина устанавливается в модели вашей логики, фактически говорят, что предложение семантически истинно, если оно истинно в каждой модели вашей логики.
Теорема Линдстрема показывает, что логика первого порядка характеризуется среди логик как наиболее сильная, удовлетворяющая некоторым естественным (по крайней мере, в математической логике) свойствам.
Выходя за рамки классической логики, теория топосов устанавливает связь между абстрактной теорией множеств, интуиционистской логикой высшего порядка и геометрией. В настоящее время это область интенсивного расследования. Можно двигаться дальше — существует также теория топосов более высокого порядка, в которой логика становится теорией гомотопических типов , это моделирует зависимые типы, в частности, интенсиональную разновидность, разработанную Мартином-Лофом . Это уже используется в компьютерных науках в качестве основы для средств доказательства теорем, таких как Coq . Здесь типы моделируются не как множества, а как гомотопические типы топологических пространств.
В связи с этим, хотя синтез логики, теории множеств и геометрии кажется захватывающим и совершенно новым, с философской точки зрения он уже очевиден в математике средней школы: логике высказываний, теории множеств и диаграммах Венна. Просто сложность на несколько величин выше и гораздо более тесно сплетена, но с объективной точки зрения, то есть вне собственно математики, эта дополнительная сложность не имеет значения.
Редактировать:
Каждый топос имеет связанный с ним внутренний язык , он скорее интуиционистский , чем классический (поэтому закон исключенного третьего не выполняется) и более высокого порядка . Это верно, потому что каждый топос является гейтинговой категорией, что означает, что его частичное множество подобъектов для любого объекта является гейтинговой алгеброй. (Обратите внимание, что в то время как классическая логика высказываний алгебраически моделируется как булева алгебра, интуиционистская логика высказываний моделируется алгеброй Гейтинга ). Его более высокий порядок, потому что каждый топос имеет возведение в степень, и это переводит через его внутренний язык, что доступны предикаты предикатов (и так далее).
Питер Смит
Мозибур Улла