Как определяется полная семантика SOL и HOL?

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

Я думаю о том, что компьютерные системы рассуждают с помощью логики, такие как помощники по доказательствам на основе HOL, такие как Isabelle .

Итак, как определяется предполагаемая семантика SOL и HOL в компьютерной системе?

PS : я понял, что эта тема на самом деле не нова на этом сайте и поднималась в других вопросах, подобных этому .

См. также хорошую обзорную статью HOL «Семь достоинств простой теории типов» автора. У. Фармер ( imps.mcmaster.ca/doc/seven-virtues.pdf )

Ответы (3)

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

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

Я думаю, вы поняли, о чем я спрашиваю. По сути, меня беспокоит вся концепция «полной семантики». Как его можно воспринимать как «четко определенный» термин, если логики более высокого порядка, выполняющие категоричность, нуждаются в метатеории ФО с теоретико-множественным привкусом, чтобы доказать категоричность того, что «они говорят» с их «более выразительной силой»? Откуда берется «выразительность», если для ее доказательства вы использовали некатегориальную теорию множеств? Если я правильно понял, это почти та же проблема, что и при рассмотрении «стандартной вселенной» теории множеств. Это просто интуиция? Что в этом "формального"?
Правильно, логика более высокого порядка с полной семантикой не является «формальной» в этом смысле, и проблема очень связана с проблемой «стандартной модели» теории множеств.
Большое спасибо. Этот вопрос был связан с другим, который я цитирую в первом абзаце; смысл слова «фундаментальный», который я использовал там, более или менее такой же, как мы обсуждали здесь под прилагательным «формальный», за исключением дополнительного значения способности «моделировать» другие логики с математической точки зрения. (например, нечеткая логика может быть формализована в математической теории FO, которая поддерживает действительные числа и определяет «нечеткое членство» как упорядоченную пару).
Я был бы очень признателен, если бы вы оставили там ответ , потому что я не нашел ни один из текущих ответов удовлетворительным.

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

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

Что меня смущает, так это то, что даже если ваш аргумент абсолютно правилен (компьютеры следуют только синтаксическим правилам и не заботятся о семантике), из этого следует, что каждая логика более высокого порядка, чем FOL, обязательно вычисляется, как если бы она была многосортный FOL (т. е. не признает, например, что переменные второго порядка охватывают подмножества того же множества , что и переменные первого порядка). Я подозреваю, что я что-то упускаю здесь, хотя.
@Mono: Это правда, что синтаксический характер проверки доказательств для HOL такой же, как и для многосортного FOL. Что характеризует HOL, так это то, что обычно существуют определенные логические аксиомы и / или правила вывода , касающиеся переменных более высокого порядка и гарантирующие, например, что все, что можно определить по явной формуле, также учитывается, когда мы квантифицируем переменную более высокого порядка соответствующую подпись. ...(продолжение)
... Мы можем считать эти специальные правила частью собственно теории, а не частью логики, и результатом будет теория первого порядка, которая может доказать то же самое - по сути, исходную теорию более высокого порядка. теория будет встроена в (возможно, слабую) версию теории множеств первого порядка. Позиция, согласно которой вся логика высшего порядка является просто аббревиатурой для теории множеств, отстаивалась Куайном и в значительной степени сохраняла свою актуальность до тех пор, пока появление практических систем компьютерных доказательств не показало, насколько громоздко все время явно приводить все к первому порядку.
Также обратите внимание, что тот факт, что логические аксиомы для переменных более высокого порядка всегда одни и те же (в отличие от того, если бы они были просто случайными частями предметной теории), делает более практичным для разработчиков помощников по доказательству предоставлять общие стратегии для особых случаев для используя их, которые позволяют пользователям легко указывать общие шаблоны рассуждений.
Что ж, я полагаю, что логические аксиомы, на которые вы ссылаетесь, — это, например, аксиомы понимания и выбора в SOL. Если я не понял, что вы сказали, то и SOL, и HOL можно эффективно согласовать с подходящим MS-FOL; Таким образом, можно утверждать, что единственное различие между ними заключается в том, как формализуются переменные «высшего порядка» (в первом случае посредством понимания, а во втором — с помощью надлежащей подписи многосортной модели, т. е. сортировки переменных). арности функций и отношений)? Просто формализация ФО громоздкая , а больше ничего нет?
Кроме того: не является ли тогда абсолютная категоричность (т.е. заявленный результат для таких теорий, как формализация SO действительных чисел в соответствии с его полной семантикой) значимым свойством для теорий, основанных на любом логическом порядке, если нам нужен (например) дополнительный FO установить теоретический, некатегориальный метаязык, чтобы создать для него модель, которая именно тогда может быть доказана как уникальная по отношению к его аксиомам? Или, что сводится к тому же заключению: не является ли тогда только относительная категоричность значимым свойством формальной теории при любой логике?
@Mono: Мне неясно, почему вы вдруг заговорили о категоричности и моделях - это семантические свойства, которые не заботят проверяющих/помощников. Все, что их волнует, — это существование действительного доказательства в какой-то формальной системе; соответствует ли формальная система какому-либо семантическому понятию модели, это не их проблема.
@Mono: Как и Хеннинг, я думаю, что это отдельный вопрос. Но вы действительно обнаружили ключевой момент полной семантики второго порядка, а именно то, что они просто переносят проблему категоричности из объектной теории в метатеорию. Эффект полной семантики заключается в простом исключении из рассмотрения многих моделей, рассматриваемых в логике первого порядка. Если мы исключим достаточное их количество, теории, у которых раньше было много моделей, могут оказаться категоричными или вообще не иметь моделей! Но это не потому, что изменилась теория, а потому, что мы исключили множество возможных моделей.
@HenningMakholm: я поднял вопрос о категоричности и моделях только потому, что изначально хотел спросить об этом (о полной семантике логики выше, чем FOL). Если синтаксис HOL всегда «переводится» в синтаксис теории множеств FO — будь то односортный, как ZFC, или многосортный, как двухсортная аксиоматизация NBG-, то единственное, что делает HOL, — это формализация вывода. системы менее громоздкие (за счет «перемещения линии» того, что можно с философской точки зрения считать пределом между логикой и математикой), тогда вы должны добавить это к своему ответу.
@CarlMummert: вся проблема в том, что я говорю о формализации семантики логики внутри нее только потому, что мне кажется, что это единственный осмысленный способ утверждения категоричности (если это возможно). В FOL это не включает метауровень, потому что его полнота гарантирует соответствие между доказуемостью и удовлетворением (по крайней мере) одной моделью. Но в логиках более высокого порядка отсутствие полноты означает, что их семантика обязательно должна рассматриваться с мета-уровня; и поэтому, как вы говорите, устранение возможных моделей должно осуществляться на этом уровне.
Тогда я не понимаю, почему предложение « SOL может определить действительные числа как единственное полное архимедово поле с точностью до изомофизма » можно формально считать осмысленным. Если мы запишем теорию SO, а затем добавим дедуктивную систему FO, дополненную аксиомами понимания и выбора, окажется, что она теряет выразительную силу (и становится эквивалентной FOL по теореме Линдстрема ) ; но если мы не включаем эти аксиомы, то «это категорично» и «более выразительно», но только тогда, когда предоставляется модель из метауровня, а не «сама по себе».

Хочу кое-что прояснить: HOL — это не просто многосортный FOL.

Ключевое различие заключается в выразительности двух систем. FOL не может выражать транзитивное замыкание. Вот хорошая заметка, объясняющая, почему. С другой стороны, HOL может выражать транзитивное замыкание. Вот исходный код реализации Isabelle/HOL, если вам интересно.

РЕДАКТИРОВАТЬ 1 : Обратите внимание на предостережение в комментариях: FOL, расширенный с помощью ZF или механизма арифметики, может выражать транзитивное закрытие. Однако я не утверждаю, что ни одно расширенное исчисление не может этого сделать.

РЕДАКТИРОВАТЬ 2 : Точно так же неуместно слепо использовать интуицию из семантики Хенкина для его логики более высокого порядка, поскольку ее применение к компьютерным HOL не является прямым . Во-первых, помощники по проверке основаны на HOL Черча, который предшествует работе Хенкина и имеет свои особенности. Семантика для HOL Черча может быть дана с использованием аппликативных структур, согласно Харви Фридману (1975) и последующим статьям.

[Как] предполагаемая семантика SOL и HOL указана в компьютерной системе?

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

В Isabelle вы можете загрузить либо Isabelle/ZF, либо Isabelle/HOL. В зависимости от того, какую систему вы загружаете, Икс е А интерпретируется по-разному.

В Isabelle/ZF это то значение, которое вы узнали на уроке теории множеств: е является бинарным отношением в FOL и подчиняется различным аксиомам теории множеств.

В Isabelle/HOL S :: 'x set(т. е. " Sявляется набором объектов типа 'x") на самом деле является просто оболочкой для объекта типа f :: 'x -> bool(т. е. " fявляется индикаторной функцией , принимающей 'xзначения True/False"). Понимание множества и принадлежность эффективно определяются эквивалентностью а е { Икс   |   п ( Икс ) } ⟺ п ( а ) . Вы можете прочитать об этом в источнике Isabelle/HOL, если вам нравятся такие вещи.

И в Isabelle/ZF, и в Isabelle/HOL знакомый синтаксис { Икс е С   |   ф ( Икс ) } также интерпретируется как синтаксический сахар. В обоих случаях синтаксический анализатор отвечает за компиляцию расширенного синтаксиса в базовый синтаксис; и то, как это делается, зависит от основания.

Наконец, хотя помощники по компьютерной проверке обычно не используют собственную семантику, есть исключение. Джон Харрисон разработал два доказательства относительной непротиворечивости HOL-Light внутри HOL-Light здесь .

Сначала он демонстрирует, как построить полную модель HOL-Light без аксиомы бесконечности в HOL-Light. Затем он показывает, как построить полную модель всего HOL-Light в расширенном HOL-Light с сильно недоступным кардиналом.

Утверждение «FOL не может выражать транзитивное замыкание» несколько расплывчато. ZFC, безусловно, может определить транзитивное замыкание отношения и является теорией первого порядка. Все, что может быть выражено в HOL, может быть выражено точно таким же предложением в FOL. Разница только в семантике — но у HOL есть несколько семантик, самая слабая из которых имеет ту же силу, что и FOL. Все, что делает Изабель, совместимо с этой семантикой; Изабель не может сказать, какую семантику я использую для интерпретации ее вывода. Если я использую семантику Хенкина, Изабель будет иметь те же семантические ограничения, что и FOL.
@Carl Mummert: я полагаю, я должен сделать различие. В то время как в ZF вы можете выразить транзитивное замыкание отношения между множествами, он не может выразить замыкание логических отношений, таких как е ; ФОЛ так не может. С другой стороны, у Isabelle/HOL такой проблемы нет. Точно так же Isabelle/HOL не просто кодирует исчисление высшего порядка Хенкина; он также включает расширения, такие как аксиома выбора. Isabelle/HOL можно встроить в ZFC, но это не то же самое, что встроить в simpliciter FOL (как это может сделать исчисление более высокого порядка Хенкина).
Метод Хенкина работает с добавленными аксиомами произвольного выбора и понимания; действительно, они обычно используются в логике второго порядка, даже с семантикой Хенкина. Более того, внутри ZFC, безусловно, можно выразить транзитивное замыкание произвольного множества или класса. А под е отношение: множество б находится в транзитивном замыкании А тогда и только тогда, когда существует конечная цепь б е а н + 1 е а н е ⋯ е а 1 где а 1 е А . Это можно записать как одно предложение ZFC.
(Это транзитивное замыкание в теоретико-множественном смысле. Для транзитивного замыкания в теоретико-порядковом смысле мы могли бы положить б е * а если есть конечная цепь б е а н + 1 е ⋯ е а 1 "=" а где а н + 1 , а н , … , а 1 все в А . Это снова одно предложение ZFC. В общем, если мы можем определить транзитивное замыкание любого отношения р то мы можем определить транзитивное замыкание е просто заменив р с е в определении.)
@Carl Mummert: Хорошо, теперь, когда я немного проснулся, я вижу ваше определение закрытия е верно. В любом случае, у компьютерных помощников HOL нет аксиом понимания. Кроме того, у них есть лямбда-термы; это другая традиция, чем карандашно-бумажный материал Хенкина. Я действительно не понимаю, каков алгоритм для встраивания компьютерных HOL в многосортный FOL; может быть, вы можете дать цитату?
Я думаю, дело в том, что ВОЛ - это не единая логика. Существует множество логик "первого порядка" с немного другим синтаксисом. Все они относятся к первому порядку в том смысле, что обладают эффективными дедуктивными системами, семантикой, использующей обычные структуры первого порядка, и теоремами полноты. FOL, который люди обычно видят первым, не имеет типов, λ термины или наборы квантификаторов, но их легко добавить, сохранив полноту. Обычно λ термины встречаются только в теории доказательств или вычислительных установках, например, в арифметике высшего порядка, как в теории прикладных доказательств Коленбаха .
Верно; Помощники для проверки HOL основаны на более ранней формулировке Черча, которая предшествовала формулировке Хенкина. Похоже, что встраивание HOL Черча в FOL требует встраивания терм-алгебры HOL, поэтому вам придется ввести полиморфную бинарную операцию, @представленную приложением. Похоже, Харви Фридман придумал это в 70-х. Излишне говорить, что я не думаю, что интуиция из HOL Хенкина напрямую применима к компьютерным HOL. Я почерпнул большую часть этого после беглого просмотра этой магистерской диссертации: ps.uni-saarland.de/theses/kaminski/mthesis/kaminski-mthesis.pdf
Как определяется полная семантика SOL и HOL?
СпросиСетьПолитика конфиденциальности1y, 0v