Обоснование логики

Оглавление:

Обоснование логики
Обоснование логики

Видео: Обоснование логики

Видео: Обоснование логики
Видео: Логика. Основы Логики. Логическое Мышление 2024, Март
Anonim

Это файл в архиве Стэнфордской энциклопедии философии. Информация об авторе и цитировании | Friends PDF Preview | InPho Поиск | PhilPapers Библиография

Обоснование логики

Впервые опубликовано ср 22 июня 2011 г.; основная редакция ср 20 июля 2011

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

  • 1. Почему логика оправдания?

    • 1.1 Эпистемическая традиция
    • 1.2 Математическая логика традиции
  • 2. Основные компоненты логики обоснования

    • 2.1 Язык логики оправдания
    • 2.2 Базовая логика обоснования J 0
    • 2.3 Логическая осведомленность и постоянные характеристики
    • 2.4 Факультет
    • 2.5 Положительный самоанализ
    • 2.6 Отрицательный самоанализ
  • 3. Семантика

    • 3.1 Возможные модели мирового обоснования для одного агента
    • 3.2 Слабая и сильная полнота
    • 3.3 Семья с одним агентом
    • 3.4 Модели оправдания единого мира
  • 4. Теоремы реализации
  • 5. Обобщения

    • 5.1 Смешение явных и неявных знаний
    • 5.2 Мультиагентные возможные модели мирового обоснования
  • 6. Пример Рассела: индуцированное притяжение
  • 7. Самостоятельность обоснований
  • 8. Квантификаторы в логике обоснования
  • 9. Исторические заметки
  • Библиография
  • Академические инструменты
  • Связанные Записи
  • Другие интернет-ресурсы

1. Почему логика оправдания?

Логика оправдания - это эпистемическая логика, которая позволяет «развернуть» знания и модальности в термины оправдания: вместо □ X пишется t: X, и читается как «X оправдывается причиной t». Можно рассматривать традиционные модальные операторы как неявные модальности, а оправдательные термины - как их явные разработки, которые дополняют модальные логики более тонким эпистемическим механизмом. Семейство оправдательных терминов имеет структуру и операции. Выбор операций порождает различные обоснования логики. Для всех распространенных эпистемических логик их модальности могут быть полностью развернуты в явной форме обоснования. В этом отношении логика оправдания раскрывает и использует явное, но скрытое содержание традиционной эпистемической модальной логики.

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

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

1.1 Эпистемическая традиция

Свойства знания и веры были предметом формальной логики, по крайней мере, со времен фон Райта и Хинтикки (Hintikka 1962, фон Райт 1951). Знание и вера воспринимаются как модальности таким образом, который сейчас очень знаком - эпистемическая логика. Но из трех критериев Платона для знания: оправданная, истинная, вера (Gettier 1963, Hendricks 2005) эпистемическая логика действительно работает только с двумя из них. Возможные миры и модель неразличимости верования - каждый верит в то, что так при любых обстоятельствах считалось возможным. Фантизм вносит в игру компонент правдивости - если что-то не так в реальном мире, его нельзя узнать, только поверить. Но нет представления для условия обоснования. Тем не менее,Модальный подход оказался чрезвычайно успешным в разрешении разработки богатой математической теории и приложений (Фагин, Халперн, Моисей и Варди, 1995, Ван Дитмарш, Ван дер Хук и Коой, 2007). Тем не менее, это не вся картина.

Модальный подход к логике познания в некотором смысле построен на универсальном квантификаторе: X известен в ситуации, если X истинен во всех ситуациях, неотличимых от этой. Обоснования, с другой стороны, привносят экзистенциальный квантификатор в картину: X известен в ситуации, если существует оправдание для X в этой ситуации. Эта универсальная / экзистенциальная дихотомия знакома логикам - в формальной логике существует доказательство для формулы X тогда и только тогда, когда X истинно во всех моделях логики. Человек думает о моделях как о неконструктивных по своей природе, а доказательства - как о конструктивных вещах. Никто не ошибется, думая об оправданиях в целом, так же как математические доказательства. Действительно, первая логика обоснования была явно разработана для сбора математических доказательств в арифметике,то, что будет обсуждаться далее в разделе 1.2.

В логике обоснования, помимо категории формул, есть вторая категория обоснований. Оправдания - это формальные термины, построенные из констант и переменных с использованием различных символов операций. Константы представляют собой обоснование общепринятых истин, обычно аксиом. Переменные обозначают неуказанные обоснования. Разные логики обоснования различаются в зависимости от того, какие операции разрешены (а также и другими способами). Если t является оправдывающим термином, а X является формулой, t: X является формулой и предназначен для чтения:

это оправдание X.

Одна операция, общая для всех логик обоснования, - это приложение, написанное как умножение. Идея состоит в том, что если s является обоснованием для A → B, а t является обоснованием для A, то [s ⋅ t] является обоснованием для B [1]. То есть, как правило, допустимо следующее:

(1) s:(A → B) → (t: A → [s ⋅ t]: B).

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

(2) □ (A → B) → (□ A → □ B).

Фактически, формула (2) стоит за многими проблемами логического всеведения. В нем утверждается, что агент знает все, что подразумевается под знанием агента, и поэтому он закрыт. В то время как познаваемое в принципе, познаваемость закрыто под последствиями, этого нельзя сказать о любой правдоподобной версии фактического знания. Различие между (1) и (2) может быть использовано при обсуждении парадигматического примера «Красный сарай» Гольдмана и Крипке; Вот упрощенная версия истории, взятой из (Dretske 2005).

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

В первой формализации примера «Красный сарай» логический вывод будет выполнен в базовой модальной логике, в которой □ интерпретируется как модальность «убеждения». Тогда некоторые случаи □ будут внешне интерпретироваться как «знание» в соответствии с описанием проблемы. Пусть B - это предложение «объект передо мной - это сарай», а R - предложение «объект передо мной - красный».

  1. □ B: «Я считаю, что передо мной находится сарай»;
  2. □ (B ∧ R), «Я считаю, что передо мной стоит красный сарай».

На метауровне 2 фактически является знанием, тогда как по описанию проблемы 1 не является знанием.

□ (B ∧ R → B) утверждение знания логической аксиомы

В рамках этой формализации оказывается, что эпистемическое замыкание в его модальной форме (2) нарушается: строка 2, □ (B ∧ R), и строка 3, □ (B ∧ R → B) - случаи знания, тогда как □ B (строка 1) это не знание. Модальный язык здесь, кажется, не помогает решить эту проблему.

Далее рассмотрим пример Red Barn в «Обосновании логики», где t: F интерпретируется как «Я верю F по причине t». Пусть u будет конкретным индивидуальным оправданием убеждения, что B, и v, убеждением, что B B R. Кроме того, пусть a будет оправданием логической истины B ∧ R → B. Тогда список предположений:

  1. U: B, «у вас есть основания полагать, что объект передо мной - сарай»;
  2. v:(B ∧ R), «v - причина полагать, что объект передо мной - красный сарай»;
  3. a:(B ∧ R → B).

На метауровне в описании проблемы говорится, что 2 и 3 - это случаи знания, а не просто убеждения, тогда как 1 - это убеждение, которое не является знанием. Вот как идут формальные рассуждения:

  1. a:(B ∧ R → B) → (v:(B ∧ R) → [a ⋅ v]: B) по принципу (1);
  2. v:(B ∧ R) → [a ⋅ v]: B, из 3 и 4, с помощью логики высказываний;
  3. [a ⋅ v]: B, от 2 и 5, с помощью логики высказываний.

Обратите внимание, что вывод 6 - это [a ⋅ v]: B, а не u: B; эпистемическое закрытие имеет место. Рассуждая в логике оправдания, был сделан вывод, что [a ⋅ v]: B - это случай знания, т. Е. «Я знаю B по причине a ⋅ v». Тот факт, что u: B не является случаем знания, не портит принцип замыкания, поскольку последний требует знания специально для [a ⋅ v]: B. Следовательно, после наблюдения красного фасада я действительно знаю B, но это знание не имеет ничего общего с 1, который остается делом веры, а не знания. Формализация логики обоснования представляет ситуацию справедливо.

Обоснование отслеживания представляет структуру примера «Красный сарай» таким образом, чтобы его не охватили традиционные эпистемологические модальные инструменты. Формализация Justification Logic моделирует то, что, по-видимому, происходит в таком случае; закрытие знаний под логическим следствием поддерживается, даже если «сарай» не воспринимается перцептивно. [2]

1.2 Математическая логика традиции

Согласно Брауэру, истина в конструктивной (интуиционистской) математике означает существование доказательства, ср. (Troelstra и van Dalen, 1988). В 1931–34 годах Хейтинг и Колмогоров дали неформальное описание предполагаемой доказательной семантики для интуиционистской логики (Колмогоров 1932, Хейтинг 1934), которая теперь называется семантикой Брауэра-Хейтинга-Колмогорова (BHK). Согласно условиям BHK, формула является «истинной», если она имеет доказательство. Кроме того, доказательство составного утверждения связано с доказательствами его компонентов следующим образом:

  • доказательство A ∧ B состоит из доказательства предложения A и доказательства предложения B;
  • доказательство A ∨ B дается представлением либо доказательства A, либо доказательства B;
  • доказательство A → B - конструкция, преобразующая доказательства A в доказательства B;
  • ложь ⊥ является пропозицией, не имеющей доказательств, ¬A является сокращением для A → ⊥.

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

Фундаментальная ценность семантики BHK заключается в том, что неформально, но однозначно она предлагает рассматривать обоснования, в данном случае математические доказательства, как объекты с операциями.

В (Gödel, 1933) Гедель сделал первый шаг к разработке строгой доказательной семантики для интуиционизма. Гедель считал классическую модальную логику S4 исчислением, описывающим свойства доказуемости:

  • Аксиомы и правила классической логики высказываний;
  • □ (F → G) → (□ F → □ G);
  • □ F → F;
  • □ F → □□ F;
  • Правило необходимости: если ⊢ F, то ⊢ □ F.

Основываясь на понимании Брауэром логической истины как доказуемости, Гедель определил перевод tr (F) пропозициональной формулы F на интуитивистском языке на язык классической модальной логики: tr (F) получается путем добавления к каждой подформуле F префикса доказуемости. модальность □. Неформально говоря, когда к tr (F) применяется обычная процедура определения классической истинности формулы, она проверяет доказуемость (а не истинность) каждой из подформул F в соответствии с идеями Брауэра. Из результатов Гёделя и работы Маккинси-Тарского по топологической семантике для модальной логики следует, что перевод tr (F) обеспечивает правильное вложение интуиционистского исчисления высказываний, IPC, в S4, то есть встраивание интуиционистской логики в классическую логику. продлен оператором доказуемости.

(3) Если МПК доказывает F, то S4 доказывает tr (F).

Тем не менее, первоначальная цель Геделя по определению интуиционистской логики в терминах классической доказуемости не была достигнута, поскольку связь S4 с обычным математическим понятием доказуемости не была установлена. Более того, Гёдель отметил, что прямая идея интерпретации модальности □ F как F доказуема в данной формальной системе T противоречила второй теореме Гёделя о неполноте. Действительно, □ (□ F → F) можно вывести в S4 по правилу необходимости из аксиомы □ F → F. С другой стороны, интерпретация модальности □ как предиката формальной доказуемости в теории T и F как противоречия превращает эту формулу в ложное утверждение о том, что согласованность T внутренне доказуема в T.

Ситуацию после (Gödel 1933) можно описать следующим рисунком, где «X ↪ Y» следует читать как «X интерпретируется в Y»

МПК ↪ S4 ↪? ↪ КЛАССИЧЕСКИЕ ДОКАЗАТЕЛЬСТВА

На публичной лекции в Вене в 1938 году Гедель заметил, что, используя формат явных доказательств:

(4) т является доказательством F

может помочь в интерпретации его исчисления доказуемости S4 (Gödel 1938). К сожалению, работа Гёделя (Gödel, 1938) оставалась неопубликованной до 1995 года, к этому времени логика явных доказательств Гёделя уже была вновь открыта и аксиоматизирована как логика доказательств ЛП и снабжена теоремами полноты, связывающими ее как с S4, так и с классическими доказательствами (Артемов). 1995).

LP Logic of Proofs стал первым в семействе Justification Logic. Термины доказательства в LP - не что иное, как термины BHK, понимаемые как классические доказательства. С LP пропозициональная интуиционистская логика получила желаемую строгую семантику BHK:

IPC ↪ S4 ↪ LP ↪ КЛАССИЧЕСКИЕ ДОКАЗАТЕЛЬСТВА

Для дальнейшего обсуждения традиции математической логики см. Раздел 1 дополнительного документа «Некоторые дополнительные технические вопросы».

2. Основные компоненты логики обоснования

В этом разделе представлены синтаксис и аксиоматика наиболее распространенных систем логики обоснования.

2.1 Язык логики оправдания

Чтобы создать формальное объяснение логики обоснования, необходимо сделать основное структурное предположение: обоснования - это абстрактные объекты, которые имеют структуру и операции над ними. Хорошим примером обоснований служат формальные доказательства, которые долгое время были объектами изучения математической логики и информатики (см. Раздел 1.2).

Логика обоснования - это формальная логическая структура, которая включает эпистемологические утверждения t: F, обозначающие «t является оправданием для F». Логика обоснования не анализирует напрямую, что значит для t обоснование F за пределами формата t: F, а скорее пытается охарактеризовать это отношение аксиоматически. Это похоже на то, как булева логика рассматривает свои связки, скажем, дизъюнкцию: она не анализирует формулу p ∨ q, а скорее предполагает некоторые логические аксиомы и таблицы истинности об этой формуле.

Есть несколько дизайнерских решений. Логика обоснования начинается с самой простой основы: классической логической логики и по уважительным причинам. Оправдания обеспечивают достаточно серьезную проблему даже на самом простом уровне. Парадигматические примеры Рассела, Голдмана-Крипке, Геттиера и других могут быть обработаны с помощью логической логики обоснования. Ядро Epistemic Logic состоит из модальных систем с классической булевой базой (K, T, K4, S4, K45, KD45, S5 и т. Д.), И каждая из них снабжена соответствующим компаньоном Justification Logic на основе булевой логики., Наконец, аргументация не всегда подразумевается. Это позволяет уловить суть дискуссий в эпистемологии, касающихся вопросов веры, а не знания.

Основной операцией по обоснованию являются приложение и сумма. Операция приложения принимает обоснования s и t и выдает обоснование s ⋅ t, такое, что если s:(F → G) и t: F, то [s ⋅ t]: G. Символично,

s:(F → G) → (t: F → [s ⋅ t]: G)

Это базовое свойство обоснований, принятых в комбинаторной логике и λ-вычислениях (Troelstra and Schwichtenberg 1996), семантика Брауэра-Хейтинга-Колмогорова (Troelstra и van Dalen 1988), реализуемости Клини (Kleene 1945), логики доказательств LP и т. Д., Любые два обоснования можно смело объединить во что-то более широкое. Это делается с помощью операции sum +. Если s: F, то какими бы ни были доказательства t, объединенное доказательство s + t остается оправданием для F. Точнее, операция «+» принимает обоснования s и t и выдает s + t, что является оправданием для всего, оправданного с помощью s или t.

s: F → [s + t]: F и t: F → [s + t]: F

В качестве мотивации можно рассматривать s и t как два тома энциклопедии, а s + t как набор этих двух томов. Представьте, что один из томов, скажем, s, содержит достаточное обоснование для предложения F, т. Е. S: F имеет место. Тогда большее множество s + t также содержит достаточное обоснование для F, [s + t]: F. В логике доказательств LP, раздел 1.2, 's + t' можно интерпретировать как объединение доказательств s и t.

2.2 Базовая логика обоснования J 0

Термины обоснования строятся из переменных обоснования x, y, z,… и констант оправдания a, b, c,… (с индексами i = 1, 2, 3,…, которые опускаются всякий раз, когда это безопасно) посредством операций ' And 'и' + '. Более сложные логики, рассмотренные ниже, также допускают дополнительные операции с обоснованиями. Константы обозначают атомные обоснования, которые система не анализирует; переменные обозначают неуказанные обоснования. Основная логика обоснования, J 0 аксиоматизируется следующим.

Классическая Логика
Классические пропозициональные аксиомы и правило Модуса Поненса
Аксиома применения
s:(F → G) → (t: F → [s ⋅ t]: G),
Аксиомы сумм
s: F → [s + t]: F, s: F → [t + s]: F.

J 0 - это логика общих (не обязательно косвенных) обоснований для абсолютно скептического агента, для которого никакая формула доказуемо не обоснована, т. Е. J 0 не выводит t: F для любых t и F. Такой агент, однако, способен сделать относительные обоснования выводов вида

Если x: A, y: B,…, z: C, то t: F.

Благодаря этому потенциалу J 0 может адекватно эмулировать другие системы Justification Logic на своем языке.

2.3 Логическая осведомленность и постоянные характеристики

Принцип логического осознания гласит, что логические аксиомы оправданы ex officio: агент принимает логические аксиомы как оправданные (включая те, которые касаются обоснований). Как только что было сказано, логическая осведомленность может быть слишком сильной в некоторых эпистемических ситуациях. Однако Justification Logic предлагает гибкий механизм постоянных спецификаций для представления различных оттенков логической осведомленности.

Конечно, можно различить предположение и обоснованное предположение. В Обосновании логические константы используются для представления обоснований допущений в ситуациях, когда они больше не анализируются. Предположим, что желательно постулировать, что аксиома A оправдана для знающего. Один просто постулирует e 1: A для некоторой доказательной константы e 1 (с индексом 1). Кроме того, если желательно постулировать, что этот новый принцип e 1: A также оправдан, можно постулировать e 2:(e 1: A) для константы e 2.(с индексом 2). И так далее. Отслеживание индексов не является необходимым, но это легко и помогает при принятии решений (Кузнец 2008). Набор всех предположений такого рода для данной логики называется Спецификацией констант. Вот формальное определение:

Константа Спецификация CS для данного логического обоснования L представляет собой набор формул вида

e n: e n -1:…: e 1: A (n ≥ 1),

где A - аксиома L, а e 1, e 2,…, e n - аналогичные константы с индексами 1, 2,…, n. Предполагается, что CS содержит все промежуточные спецификации, т. Е. Всякий раз, когда e n: e n -1:…: e 1: A находится в CS, тогда e n -1:…: e 1: A также находится в CS.

Существует ряд особых условий, которые были помещены в постоянные спецификации в литературе. Ниже приведены наиболее распространенные.

пустой
CS = ∅. Это соответствует абсолютно скептическому агенту. Это равносильно работе с логикой J 0.
конечный
CS - это конечный набор формул. Это полностью репрезентативный случай, так как любой конкретный вывод в логике обоснования будет включать только конечный набор констант.
Аксиоматически уместно
Каждая аксиома, в том числе вновь приобретенная посредством самой константной спецификации, имеет свои обоснования. В формальной постановке для каждой аксиомы A существует постоянная e 1 такая, что e 1: A находится в CS, а если e n: e n −1:…: e 1: A ∈ CS, то e n +1: e n: e n −1:…: e 1: A ∈ CS, для каждого n ≥ 1. Аксиоматически соответствующие константные спецификации необходимы для обеспечения свойства интернализации, обсуждаемого в конце этого раздела.
Общее количество

Для каждой аксиомы A и любых констант e 1, e 2,… e n,

e n: e n −1:…: e 1: A ∈ CS.

Имя TCS зарезервировано для полной спецификации констант (для данной логики). Естественно, полная константная спецификация является аксиоматически подходящей.

Теперь мы можем указать:

Логика обоснований с заданной константной спецификацией:

пусть CS будет константной спецификацией. J CS - логика J 0 + CS; аксиомы - это аксиомы J 0 вместе с членами CS, и единственное правило вывода - это Modus Ponens. Обратите внимание, что J 0 есть J .

Логика обоснований:

J - логика J 0 + Правило интернализации аксиом. Новое правило гласит:

Для каждой аксиомы А и любые константы е 1, е 2, …, е п Infer е н: е п -1: …: е 1: а.

Последний воплощает идею неограниченного логического осознания для J. Аналогичное правило появилось в «Logic of Proofs LP», а также ожидалось в Goldman's (Goldman 1967). Логическая осведомленность, выраженная аксиоматически соответствующими константными спецификациями, является явным воплощением правила необходимости в модальной логике: ⊢ F ⇒ ⊢ □ F, но ограничена аксиомами. Обратите внимание, что J совпадает с J TCS.

Ключевой особенностью систем Justification Logic является их способность усваивать собственные выводы как доказуемые обосновывающие утверждения на своих языках. Это свойство было ожидаемо в (Gödel 1938).

Теорема 1. Для каждой аксиоматически подходящей константы спецификации CS, J CS пользуется интернализацией:

Если ⊢ F, то ⊢ p: F для некоторого обосновывающего члена p.

Доказательство. Индукция по длине деривации. Предположим, что ⊢F. Если F является членом J 0 или членом CS, существует постоянная e n (где n может быть 1), так что e n: F находится в CS, поскольку CS является аксиоматически подходящим. Тогда e n: F выводимо. Если F получается модусом Поненсом из X → F и X, то по гипотезе индукции ⊢ s:(X → F) и ⊢ t: X для некоторого s, t. Используя Аксиому Приложения, ⊢ [s ⋅ t]: F.

См. Раздел 2 дополнительного документа «Некоторые дополнительные технические вопросы» для примеров конкретных синтаксических выводов в логике обоснования.

2.4 Факультет

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

Факультативная аксиома t: F → F.

Аксиома Фактивности имеет ту же мотивацию, что и Аксиома Истины Эпистемической Логики, □ F → F, которая широко принята как базовое свойство знания.

В отличие от принципов применения и суммы, в базовых системах логики обоснования не требуется произвольность обоснований, что делает их способными представлять как частичные, так и косвенные обоснования. Аксиома факультативности появилась в разделе «Логика доказательств LP», раздел 1.2, как главная особенность математических доказательств. Действительно, в этом параметре Factivity явно верен: если существует математическое доказательство t для F, то F должно быть истинным.

Факультативная аксиома принята для обоснования, приводящего к знанию. Тем не менее, само по себе не является свидетельством знания, что было продемонстрировано на примерах Геттье (Gettier 1963).

Логика факультативных оправданий

  • JT 0 = J 0 + Коэффициент;
  • JT = J + Фасилити.

Системы JT CS, соответствующие константным спецификациям CS, определены в разделе 2.3.

2.5 Положительный самоанализ

Одним из общих принципов знания является определение знания и знания того, что каждый знает. В модальном режиме это соответствует □ F → □□ F. Этот принцип имеет адекватный явный аналог: тот факт, что агент принимает t в качестве достаточного доказательства для F, служит достаточным доказательством для t: F. Часто такие «мета-доказательства» имеют физическую форму: отчет судьи, подтверждающий, что доказательство в документе является правильным; вывод проверки компьютера с заданным формальным доказательством t для F; формальное доказательство того, что t является доказательством F и т. д. Операция положительного самоанализа '!' может быть добавлен к языку для этой цели; тогда предполагается, что с учетом t агент дает оправдание! t из t: F такой, что t: F →! т:(т: F). Позитивный самоанализ в этой операционной форме впервые появился в Logic of Proofs LP.

Аксиома позитивного самоанализа: t: F →! т:(т: F).

Затем мы определяем:

  • J4: = J + положительный самоанализ;
  • LP: = JT + положительный самоанализ. [3]

Логики J4 0, J4 CS, LP 0 и LP CS определяются естественным образом (см. Раздел 2.3). Прямой аналог теоремы 1 справедлив и для J4 CS и LP CS.

При наличии положительной аксиомы самоанализа можно ограничить область действия правила интернализации аксиомы до аксиом усвоения, которые не имеют форму e: A. Вот как это было сделано в LP: затем можно эмулировать Axiom Internalization с помощью !! e:(! e:(e: A)) вместо e 3:(e 2:(e 1: A)) и т. д. Понятие спецификации констант также может быть соответственно упрощено. Такие модификации незначительны и не влияют на основные теоремы и приложения логики обоснования.

2.6 Отрицательный самоанализ

(Pacuit 2006, Rubtsova 2006) рассматривал операцию отрицательного самоанализа '?' который проверяет, что данное обоснование является ложным. Возможной мотивацией для рассмотрения такой операции является то, что операция позитивного самоанализа '!' вполне может считаться способным предоставить убедительные проверочные суждения относительно обоснованности обоснования утверждений t: F, поэтому, когда t не является оправданием для F, такое «!» следует сделать вывод, что ¬t: F. Обычно это относится к компьютерным верификаторам доказательств, контролерам доказательств в формальных теориях и т. Д. Однако эта мотивация нюансирована: примеры верификаторов доказательств и контролеров проверок работают как с t, так и с F в качестве входных данных, тогда как формат Пакью-Рубцова? т предполагает, что единственный вход для «?» это оправдание т, а результат? Предполагается, что для обоснования предложений ¬t:F равномерно для всех F s, для которых t: F не выполняется. Такая операция "?" не существует для формальных математических доказательств с тех пор? Тогда t должно быть единственным доказательством бесконечного числа предложений ¬t: F, что невозможно.

Аксиома отрицательного самоанализа ¬t: F →? т: (¬ т: F)

Мы определяем системы:

  • J45 = J4 + отрицательный самоанализ;
  • JD45 = J45 + ¬t: ⊥;
  • JT45 = J45 + факультатив

и естественно расширить эти определения до J45 CS, JD45 CS и JT45 CS. Прямой аналог теоремы 1 справедлив для J45 CS, JD45 CS и JT45 CS.

3. Семантика

Нынешняя стандартная семантика для логики обоснования берет свое начало в (Фитинге 2005) - используемые в литературе модели обычно называются моделями Фиттинга, но здесь мы будем называть их возможными моделями мирового обоснования. Возможные модели мирового оправдания представляют собой смесь знакомой возможной мировой семантики для логики знаний и убеждений, благодаря Hintikka и Kripke, с механизмом, специфичным для терминов оправдания, введенным Мкртычевым в (Mkrtychev 1997) (см. Раздел 3.4).

3.1 Возможные модели мирового обоснования для одного агента

Чтобы быть точным, семантика для J CS, где CS - любая постоянная спецификация, должна быть определена. Формально, возможной моделью логического обоснования мира для J CS является структура M = ⟨G, R, E, V⟩. Из этого ⟨G, R⟩ - стандартный K-кадр, где G - множество возможных миров, а R - бинарное отношение к нему. V - отображение пропозициональных переменных на подмножества G, определяющее атомную истину в возможных мирах.

Новый элемент E, функция доказательства, которая возникла в (Mkrtychev 1997). Это сопоставляет термины и формулы обоснования множествам миров. Интуитивная идея заключается в том, что если возможный мир Γ находится в E (t, X), то t является релевантным или допустимым доказательством для X в мире Γ. Не следует считать соответствующие доказательства убедительными. Скорее, воспринимайте это как свидетельство, которое может быть допущено в суде: это свидетельство, этот документ - это то, что следует изучить присяжным, что-то подходящее, но что-то, чей статус, определяющий правду, еще предстоит рассмотреть. Доказательственные функции должны удовлетворять определенным условиям, но они обсуждаются чуть позже.

Для модели J CS возможного обоснования мира M = ⟨G, R, E, V⟩ истинность формулы X в возможном мире Γ обозначается через M, Γ ⊩ X и должна удовлетворять следующим стандартным условиям:

Для каждого Γ ∈ G:

  1. M, Γ ⊩ P тогда и только тогда, когда Γ ∈ V (P) для P буква высказывания;
  2. это не тот случай, когда M, Γ ⊩ ⊥;
  3. M, Γ ⊩ X → Y тогда и только тогда, когда M, Γ ⊩ X или M, Γ ⊩ Y.

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

M, Γ ⊩ (t: X) тогда и только тогда, когда Γ ∈ E (t, X) и для каждого Δ ∈ G с Γ R Δ имеем M, Δ ⊩ X

Это условие разбивается на две части. Предложение, требующее, чтобы M, Δ ⊩ X для каждого Δ ∈ G, такого, что Γ R Δ, было знакомым условием Хинтикки / Крипке для X, которому можно верить или быть правдоподобным в Γ. Предложение, требующее, чтобы Γ ∈ E (t, X), добавляло, что t должно быть релевантным доказательством для X в Γ. Тогда, неофициально, t: X верно в возможном мире, если X правдоподобно в этом мире в обычном смысле эпистемической логики, и t является соответствующим доказательством X в этом мире.

Важно понимать, что в этой семантике можно не верить чему-то по определенной причине в мире, либо потому, что это просто неправдоподобно, либо потому, что это так, но причина неуместна.

Некоторые условия все еще должны быть наложены на функции доказательства, и постоянная спецификация также должна быть введена в картину. Предположим, что в качестве оправдания приводятся s и t. Можно объединить их двумя различными способами: одновременно использовать информацию из обоих; или используйте информацию только одного из них, но сначала выберите, какой именно. Каждый из них приводит к базовой операции на терминах обоснования ⋅ и +, аксиоматически введенной в разделе 2.2.

Предположим, что s является релевантным доказательством для подтекста, а t - релевантным доказательством для антецедента. Тогда s и t вместе предоставляют соответствующие доказательства для последующего. Предполагается следующее условие для функций доказательств:

E (s, X → Y) ∩E (t, X) ⊆ E (s ⋅ t, Y)

При добавлении этого условия срок действия

s:(X → Y) → (t: X → [s ⋅ t]: Y)

обеспечен.

Если s и t являются объектами доказательства, можно сказать, что что-то оправдано одним из s или t, не удосужившись указать, какое именно, и это все еще будет доказательством. Следующее требование предъявляется к функциям доказывания.

E (s, X) ∪ E (t, X) ⊆ E (s + t, X)

Не удивительно, что оба

s: X → [s + t]: X

и

t: X → [s + t]: X

сейчас подожди.

Наконец, CS спецификации констант должен быть принят во внимание. Напомним, что константы предназначены для представления оснований для базовых допущений, которые принимаются напрямую. Модель M = ⟨G, R, E, V⟩ соответствует спецификации CS констант при условии: если c: X ∈ CS, то E (c, X) = G.

Возможная модель мирового обоснования Возможная модель мирового оправдания для J CS - это структура M = ⟨G, R, E, V⟩, удовлетворяющая всем перечисленным выше условиям и отвечающая спецификации CS.

Несмотря на их сходство, возможные модели мирового обоснования позволяют провести детальный анализ, что невозможно с моделями Крипке. См. Раздел 3 дополнительного документа «Некоторые дополнительные технические вопросы» для получения более подробной информации.

3.2 Слабая и сильная полнота

Формула X действительна в конкретной модели для J CS, если она верна во всех возможных мирах модели. Аксиоматика для J CS была дана в разделах 2.2 и 2.3. Теорема полноты теперь принимает ожидаемый вид.

Теорема 2: Формула X доказуема в J CS тогда и только тогда, когда X верна во всех моделях J CS.

Теорема полноты, как только что было сказано, иногда называется слабой полнотой. Может быть немного удивительно, что это значительно легче доказать, чем полнота для модальной логики K. Комментарии к этому пункту следуют. С другой стороны, он очень общий, работает для всех постоянных спецификаций.

В (Fitting 2005) была также введена более сильная версия семантики. Модель M = ⟨G, R, E, V⟩ называется полностью объяснительной, если она удовлетворяет следующему условию. Для каждого Γ ∈ G, если M, Δ ⊩ X для всех Δ ∈ G таких, что Γ R Δ, то M, Γ ⊩ t: X для некоторого оправдывающего члена t. Отметим, что условие M, Δ ⊩ X для всех Δ ∈ G, таких что Γ R Δ, является обычным условием для правдоподобия X в Γ в смысле Хинтикки / Крипке. Таким образом, полное объяснение действительно говорит о том, что если формула правдоподобна в возможном мире, то для этого есть основания.

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

Доказательство полноты в отношении сильных моделей имеет близкое сходство с доказательством полноты с использованием канонических моделей для модальной логики K. В свою очередь, сильные модели могут использоваться для семантического доказательства теоремы реализации (см. Раздел 4).,

3.3 Семья с одним агентом

До сих пор обсуждалась возможная мировая семантика для одной логики обоснования, для J, аналога K. Теперь все расширяется, чтобы охватить аналоги обоснования других знакомых модальных логик.

Просто добавив рефлексивность отношения доступности R к условиям для модели в Разделе 3.1, можно получить достоверность t: X → X для каждого t и X и получить семантику для JT, аналога логики обоснования модальной логики. Т, самая слабая логика знания. Действительно, если M, Γ ⊩ t: X, то, в частности, X верно в любом состоянии, доступном из Γ. Поскольку отношение доступности должно быть рефлексивным, M, Γ ⊩ X. Теоремы слабой и сильной полноты доказуемы, используя тот же механизм, который применялся в случае J, и также доступно семантическое доказательство теоремы реализации, связывающей JT и T. То же самое относится к логике, обсуждаемой ниже.

Для обоснования аналога K4 дополнительный унарный оператор '!' добавлен к термину язык, см. раздел 2.5. Напомним, этот оператор отображает обоснования в обоснования, где идея состоит в том, что если t является оправданием для X, то! t должно быть оправданием для t: X. Семантически это добавляет условия к модели M = ⟨G, R, E, V⟩ следующим образом.

Во-первых, конечно, R должен быть транзитивным, но не обязательно рефлексивным. Во-вторых, требуется условие монотонности функций доказательств:

Если Γ R Δ и Γ ∈ E (t, X), то Δ ∈ E (t, X)

И, наконец, необходимо еще одно условие функции доказательства.

E (t, X) ⊆ E (! T, t: X)

Эти условия в совокупности влекут справедливость t: X →! t: t: X и создаем семантику для J4, аналога обоснования K4, с теоремой реализации, соединяющей их. Добавление рефлексивности приводит к логике, которая называется LP по историческим причинам.

Можно также добавить отрицательный оператор самоанализа, '?,' См. Раздел 2.6. Модели для логики обоснования, которые включают этот оператор, добавляют три условия. Первый R симметричен. Во-вторых, добавляется условие, которое стало известно как убедительное доказательство: M, Γ ⊩ t: X для всех Γ ∈ E (t, X). Наконец, есть условие для функции доказывания:

E (t, X) ⊆ E (? T, ¬ t: X)

Если этот механизм будет добавлен к J4, мы получим логику J45, оправдание K45. Аксиоматическая обоснованность и полнота могут быть доказаны. Аналогичным образом могут быть сформулированы соответствующие логики JD45 и JT45.

Теорема реализации, учитывающая этот оператор, была показана в (Рубцова 2006).

3.4 Модели оправдания единого мира

Модели оправдания единого мира были разработаны значительно раньше, чем обсуждаемые нами более общие модели оправдания мира (Мкртычев, 1997). Сегодня о них проще всего думать как о возможных моделях мирового оправдания, которые имеют один мир. Доказательство полноты для J и других логик обоснования, упомянутых выше, можно легко изменить, чтобы установить полноту в отношении моделей оправдания единого мира, хотя, конечно, это не был первоначальный аргумент. Полнота в отношении моделей оправдания единого мира говорит нам о том, что информация о возможной мировой структуре моделей обоснования может быть полностью закодирована с помощью функции допустимого доказательства, по крайней мере, для логики, обсуждавшейся до сих пор. Мкртычев использовал модели оправдания единого мира, чтобы установить разрешимость LP,и другие фундаментально использовали их для установления границ сложности для логики обоснования, а также для демонстрации результатов консервативности для логики обоснования веры (Кузнец 2000, Кузнец 2008, Милникель 2007, Милникель 2009). Результаты сложности были также использованы для решения проблемы логического всеведения.

4. Теоремы реализации

Естественным модальным эпистемическим аналогом утверждения о доказательствах t: F является □ F, читаемое для некоторого x, x: F. Это наблюдение приводит к понятию забывчивой проекции, которое заменяет каждое вхождение t: F на □ F и, следовательно, преобразует предложение S логики оправдания в соответствующее предложение S o модальной логики. Забывчивая проекция естественным образом простирается от предложений до логики.

Очевидно, что разные предложения логики обоснования могут иметь одну и ту же забывчивую проекцию, поэтому S o теряет определенную информацию, которая содержалась в S. Однако легко заметить, что забывчивая проекция всегда отображает действительные формулы логики обоснования (например, аксиомы J) на действительные формулы соответствующей эпистемической логики (в данном случае K). Справедливо и обратное утверждение: любая действительная формула эпистемической логики является забывчивой проекцией некоторой действительной формулы логики оправдания. Это следует из теоремы 3 о соответствии.

Теорема 3: J o = K.

Это соответствие справедливо для других пар систем оправдания и эпистемологии, например, J4 и K4 или LP и S4, и многих других. В такой расширенной форме теорема соответствия показывает, что основные модальные логики, такие как K, T, K4, S4, K45, S5 и некоторые другие, имеют точные аналоги логики обоснования.

В основе теоремы соответствия лежит следующая теорема реализации.

Теорема 4: Существует алгоритм, который для каждой модальной формулы F, выводимой в K, присваивает доказательственные термины каждому вхождению модальности в F таким образом, что результирующая формула F r выводима в J. Более того, реализация назначает переменные-доказательства к негативным вхождениям модальных операторов в F, таким образом, уважая экзистенциальное чтение эпистемической модальности.

Известные алгоритмы реализации, которые восстанавливают доказательные термины в модальных теоремах, используют деривации без вырезов в соответствующих модальных логиках. Альтернативно, Теорема Реализации может быть установлена семантически методом Фиттинга или его собственными модификациями. В принципе, эти семантические аргументы также создают процедуры реализации, основанные на исчерпывающем поиске.

Было бы ошибкой делать вывод, что любая модальная логика имеет разумный аналог логики обоснования. Например, логика формальной доказуемости GL (Boolos 1993) содержит принцип Лёба:

(5) □ (□ F → F) → □ F,

который, кажется, не имеет эпистемически приемлемой явной версии. Рассмотрим, например, случай, когда F - пропозициональная константа ⊥ для false. Если бы аналог теоремы 4 охватывал принцип Лёба, были бы обосновывающие члены s и t, такие что x:(s: ⊥ → ⊥) → t: ⊥. Но это интуитивно неверно для объективного оправдания. Действительно, s: ⊥ → ⊥ является примером аксиомы Фактивизма. Примените Аксиому Интернализация, чтобы получить c:(s: ⊥ → ⊥) для некоторой константы c. Этот выбор c делает предшественник c:(s: ⊥ → ⊥) → t: true интуитивно верным, а вывод ложным [4]. В частности, принцип Лёба (5) недопустим для доказательной интерпретации (см. (Goris 2007) для полного описания того, какие принципы GL реализуемы).

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

Семантика оправдания играет в модальной логике ту же роль, что и реализуемость Клини в интуиционистской логике. В обоих случаях предполагаемая семантика является экзистенциальной: интерпретация Интуиционистской логики Брауэра-Хейтинга-Колмогорова (Heyting 1934, Troelstra и van Dalen 1988, van Dalen 1986) и чтение Гёделя для доказуемости S4 (Gödel 1933, Gödel 1938). В обоих случаях возможна мировая семантика универсального характер, который является очень мощным и доминирующим техническим инструментом. Однако это не касается экзистенциального характера предполагаемой семантики. Потребовалась реализуемость Клини (Kleene 1945, Troelstra 1998), чтобы раскрыть вычислительную семантику интуиционистской логики и логику доказательств, чтобы обеспечить точную семантику доказательств BHK для интуиционистской и модальной логики.

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

См. Раздел 4 дополнительного документа «Некоторые дополнительные технические вопросы» для получения дополнительной информации о теоремах реализации.

5. Обобщения

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

5.1 Смешение явных и неявных знаний

Поскольку логики обоснования предоставляют явные обоснования, в то время как обычные логики знаний предоставляют неявный оператор знаний, естественно рассмотреть возможность объединения двух в одной системе. Наиболее распространенной объединенной логикой явного и неявного знания является S4LP (Артемов и Ногина, 2005). Язык S4LP похож на язык LP, но с добавленным оператором неявного знания, написанным либо на K, либо на □. Аксиоматика подобна таковой в LP, в сочетании с таковой в S4 для неявного оператора, вместе с аксиомой связности t: X → □ X, все, что имеет явное обоснование, известно.

Семантически возможные модели мирового обоснования для LP не нуждаются в модификации, так как они уже имеют все механизмы моделей Hintikka / Kripke. Один моделирует оператор □ обычным способом, используя только отношение доступности, а другой моделирует термины обоснования, как описано в разделе 3.1, используя как доступность, так и функцию доказательства. Поскольку обычное условие истинности □ X в мире является одним из двух условий условия истинности t: X, это немедленно дает справедливость t: X → □ X, и правильность следует легко. Аксиоматическая полнота также довольно проста.

В S4LP представлены как неявные, так и явные знания, но в возможной семантике модели обоснования мира одно отношение доступности служит для обоих. Это не единственный способ сделать это. В более общем смысле, явное отношение доступности знаний может быть правильным расширением для неявных знаний. Это представляет видение явного знания как имеющего более строгие стандарты для того, что считается известным, чем неявное знание. Использование различных отношений доступности для явного и неявного знания становится необходимым, когда эти эпистемологические понятия подчиняются различным логическим законам, например, S5 для неявного знания и LP для явного. Случай множественных отношений доступности широко известен в литературе как модели Артемова-Фиттинга, но здесь мы будем называть его возможными моделями мира с несколькими агентами. (см. раздел 5.2).

Любопытно, что хотя логика S4LP кажется вполне естественной, теорема реализации была для нее проблематичной: такую теорему невозможно доказать, если настаивать на том, что называется нормальными реализациями (Кузнец 2010). Реализация неявных модальностей знаний в S4LP с помощью явных обоснований, учитывающих эпистемологическую структуру, остается главной проблемой в этой области.

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

(6) ¬ t: X → □ ¬ t: X.

С точки зрения доказуемости, это правильная форма негативного самоанализа. Действительно, пусть □ F интерпретируется как F доказуемо, а t: F как t является доказательством F в данной формальной теории T, например, в арифметике Пеано PA. Тогда (6) устанавливает доказуемый принцип. Действительно, если t не является доказательством F, то, поскольку это утверждение разрешимо, оно может быть установлено внутри T, следовательно, в T это предложение доказуемо. С другой стороны, доказательство p 't не является доказательством F', зависит как от t, так и от F, p = p (t, F) и не может быть вычислено только при t. В этом отношении, □ не может быть заменено каким-либо конкретным доказательственным термином, зависящим только от t, и (6) не может быть представлен в полностью явном формате стиля выравнивания.

Первые примеры явных / неявных систем знаний появились в области логики доказуемости. В (Sidon 1997, Yavorskaya (Sidon) 2001) была введена логическая LPP, которая объединила логику доказуемости GL с логикой доказательств LP, но для обеспечения того, чтобы полученная система имела желаемые логические свойства, некоторые дополнительные операции были выполнены за пределами исходных языков. GL и LP были добавлены. В (Nogina 2006, Nogina 2007) была предложена полная логическая система, GLA, для доказательств и доказуемости, в сумме исходных языков GL и LP. И LPP, и GLA обладают полнотой относительно класса арифметических моделей, а также относительно класса возможных моделей мирового обоснования.

Другим примером принципа доказуемости, который нельзя сделать полностью явным, является принцип Лёба (5). Для каждого из LPP и GLA легко найти проверочный член l (x) такой, что

(7) x: (□ F → F) → l (x): F

держит. Однако нет реализации, которая делает все три □ s в (5) явными. Фактически, набор реализуемых принципов доказуемости - это пересечение GL и S4 (Goris 2007).

5.2 Мультиагентные возможные модели мирового обоснования

В мультиагентных моделях возможного обоснования мира используются множественные отношения доступности со связями между ними (Артемов 2006). Идея состоит в том, что существует несколько агентов, каждый с неявным оператором знаний, и существуют термины обоснования, которые понимает каждый агент. В общем, все понимают явные причины; это составляет доказательное общее знание

N -агентная модель возможного оправдания мира - это структура ⟨G, R 1,…, R n, R, E, V⟩, удовлетворяющая следующим условиям. G - это множество возможных миров. Каждый из R 1,…, R n является отношением доступности, по одному для каждого агента. По желанию они могут быть рефлексивными, транзитивными или симметричными. Они используются для моделирования неявных знаний агента для семьи агентов. Отношение доступности R соответствует условиям LP, рефлексивности и транзитивности. Используется при моделировании явных знаний. E является функцией доказательства, отвечающей тем же условиям, что и для LP в Разделе 3.3. V отображает пропозициональные буквы на множество миров, как обычно. Существует специальное условие: для каждого i = 1,…, n, R i ⊆ R.

Если M = ⟨G, R 1,…, R n, R, E, V⟩ - это модель с несколькими агентами для обоснования возможного мира, то отношение истина к миру, M, Γ ⊩ X, определяется с большинством обычные пункты. Особый интерес представляют следующие:

  • M, Γ ⊩ K i X тогда и только тогда, когда для каждого Δ ∈ G с Γ R i Δ имеем M, Δ ⊩ X.
  • M, Γ ⊩ t: X тогда и только тогда, когда Γ ∈ E (t, X) и для каждого Δ ∈ G с Γ R Δ имеем M, Δ ⊩ X.

Условие R i ⊆ R влечет справедливость t: X → K i X для каждого агента i. Если существует только один агент и отношение доступности для этого агента является рефлексивным и транзитивным, это обеспечивает другую семантику для S4LP. Независимо от количества агентов, каждый агент принимает явные причины для установления знаний.

Версия LP с двумя агентами была введена и изучена в (Яворская (Сидон) 2008), хотя она может быть обобщена для любого конечного числа агентов. При этом у каждого агента есть свой набор операторов, переменных и констант выравнивания, а не один набор для всех, как указано выше. Кроме того, может быть разрешено некоторое ограниченное взаимодействие между агентами с использованием нового оператора, который позволяет одному агенту проверять правильность обоснований другого агента. Версии как единого мира, так и более общей возможной семантики оправдания мира были созданы для логики с двумя агентами. Это включает в себя прямое расширение понятия функции доказательства и для возможных моделей мирового обоснования с использованием двух отношений доступности. Теоремы реализации были доказаны синтаксически,хотя предположительно семантическое доказательство также будет работать.

Недавно было проведено исследование роли публичных объявлений в логике обоснования нескольких агентов (Renne 2008, Renne 2009).

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

6. Пример Рассела: индуцированное притяжение

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

Если человек считает, что фамилия покойного премьер-министра началась с буквы «В», он считает, что это правда, поскольку покойным премьер-министром был сэр Генри Кэмпбелл Баннерман [5]. Но если он считает, что г-н Бальфур был покойным премьер-министром [6], он все равно будет верить, что фамилия покойного премьер-министра начиналась с буквы «В», однако это убеждение, хотя и верное, не будет рассматриваться как знание. (Рассел 1912)

Как и в примере «Красный сарай», рассмотренном в разделе 1.1, здесь приходится иметь дело с двумя обоснованиями истинного утверждения, одно из которых является правильным, а другое - нет. Пусть B - предложение (пропозициональный атом), w - обозначенная переменная обоснования по неправильной причине для B, а ra - обозначенная переменная обоснования по правильной (следовательно, косвенной) причине для B. Затем в примере Рассела предлагается следующий набор предположений [7]:

R = {w: B, r: B, r: B → B}

В некоторой степени противоречащей интуиции, можно логически вывести коэффициент w из R:

  1. r: B (предположение)
  2. r: B → B (предположение)
  3. B (из 1 и 2 от Модуса Поненса)
  4. B → (w: B → B) (аксиома высказываний)
  5. w: B → B (из 3 и 4 от Модуса Поненса)

Тем не менее, этот вывод использует тот факт, что r является косвенным обоснованием для B, чтобы заключить w: B → B, что составляет случай «индуцированной очевидности» для w: B. Вопрос в том, как отличить «реальное» свойство r: B от «индуцированного» от w: B? Здесь требуется некое подобие отслеживания правды, и логика обоснования является подходящим инструментом. Естественный подход заключается в рассмотрении множества предположений без r: B, т.е.

S = {w: B, r: B → B}

и установить, что удельный вес w, т. е. w: B → B, не выводится из S. Вот возможная модель оправдания мира M = (G, R, E, V), в которой S имеет место, но w: B → B не имеет:

  • G = { 1 },
  • R = ∅,
  • V (B) = ∅ (и поэтому нет- 1- B),
  • E (t, F) = { 1 } для всех пар (t, F), кроме (r, B), и
  • E (r, B) = ∅.

Легко видеть, что условия закрытия Application и Sum на E выполнены. На 1 выполняется w: B, т.е.

1 ⊩ ш: В

поскольку w является допустимым доказательством для B в 1 и нет возможных миров, доступных из 1. Более того,

не- 1 р: B

поскольку, согласно E, r не является допустимым доказательством для B в 1. Следовательно:

1 ⊩ р: B → B

С другой стороны,

не- 1 ⊩ w: B → B

так как B не имеет места в 1.

7. Самостоятельность обоснований

Алгоритмы Реализации иногда создают Спецификации констант, содержащие самообращающиеся обоснованные утверждения c: A (c), то есть утверждения, в которых обоснование (здесь c) встречается в утвержденном утверждении (здесь A (c)).

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

Основной результат Кузнеца в (Брежнев и Кузнец 2006) утверждает, что самореференциальность оправданий неизбежна при реализации S4 в LP. Текущее положение вещей определяется следующей теоремой Кузнеца:

Теорема 5. Самореференцируемости можно избежать в реализациях модальных логик K и D. Самостоятельной ссылочности нельзя избежать в реализациях модальных логик T, K4, D4 и S4.

Эта теорема устанавливает, что система оправдывающих терминов для S4 обязательно будет самоссылочной. Это создает серьезное, хотя и не видимое, ограничение семантики доказуемости. В контексте арифметических доказательств Гёделя эта проблема решалась с помощью общего метода присвоения арифметической семантики самореференциальным утверждениям c: A (c), утверждающим, что c является доказательством A (c). В «Логике доказательств» речь шла о нетривиальной конструкции с фиксированной точкой.

Самостоятельность дает интересный взгляд на парадокс Мура. Подробности см. В разделе 6 дополнительного документа «Некоторые дополнительные технические вопросы».

8. Квантификаторы в логике обоснования

Хотя исследование логики обоснования высказываний еще далеко от завершения, также были отдельные работы над версиями первого порядка. Количественные версии Modal Logic уже предлагают сложности, выходящие за рамки стандартной логики первого порядка. Квантификация имеет еще более широкое поле для игры, когда задействована логика обоснования. Классически каждый дает количественную оценку по «объектам», а модели оснащены доменом, по которому квантификаторы располагаются. Модально у одного может быть один домен, общий для всех возможных миров, или у каждого могут быть отдельные домены для каждого мира. Роль формулы Баркана здесь хорошо известна. Для логики обоснования доступны как постоянные, так и изменяющиеся параметры домена. Кроме того, существует возможность, которая не имеет аналогов для модальной логики: можно количественно оценить сами оправдания.

Первоначальные результаты относительно возможности количественной логики обоснования были особенно неблагоприятными. Семантика арифметической доказуемости для Logic of Proofs LP, естественно, обобщает на версию первого порядка с обычными квантификаторами и на версию с квантификаторами над доказательствами. В обоих случаях на вопросы аксиоматизируемости были даны отрицательные ответы.

Теорема 6: Логика доказательств первого порядка не рекурсивно перечислима (Артемов, Яворская (Сидон), 2001). Логика доказательств с кванторами над доказательствами не рекурсивно перечислима (Яворский, 2001).

Хотя арифметическая семантика невозможна, в (Fitting 2008) возможная мировая семантика и аксиоматическая теория доказательств была дана для версии LP с квантификаторами, расположенными над оправданиями. Обоснованность и полнота доказаны. На этом этапе возможная мировая семантика отделяется от арифметической семантики, которая может быть или не быть причиной для тревоги. Также было показано, что S4 встраивается в количественную логику путем перевода □ Z как «существует оправдание x такое, что x: Z * », где Z * - перевод Z. Хотя эта логика несколько сложна, она нашла применение, например, в (Dean and Kurokawa 2009b) она используется для анализа парадокса Знающего, хотя были высказаны возражения против этого анализа в (Arlo-Costa and Kishida 2009).

Также была проделана работа над версиями Justification Logic с квантификаторами над объектами, как с аналогом формулы Баркана, так и без него. Ничего из этого не было опубликовано, и это следует считать еще в стадии разработки.

9. Исторические заметки

Первоначальная система логики обоснования, Logic of Proofs LP, была введена в 1995 г. в (Артемов 1995) (см. Также (Артемов 2001)), где впервые были установлены такие базовые свойства, как интернализация, реализация, арифметическая полнота. LP предлагает предполагаемую семантику доказуемости для логики доказуемости Гёделя S4, обеспечивая тем самым формализацию семантики Брауэра-Хейтинга-Колмогорова для интуиционистской логики высказываний. Эпистемическая семантика и полнота (Fitting 2005) были впервые установлены для LP. Символические модели и разрешимость для ЛП принадлежат Мкртычеву (Мкртычев, 1997). Оценки сложности впервые появились в (Брежнев и Кузнец 2006, Кузнец 2000, Милникель 2007). Подробный обзор всех результатов по разрешимости и сложности можно найти в (Кузнец 2008). Системы J, J4,и JT впервые были рассмотрены в (Брежнев, 2001) под разными именами и в несколько ином контексте. JT45 появился независимо в (Pacuit 2006) и (Рубцова 2006), а JD45 в (Pacuit 2006). Логика единогласных доказательств была найдена в (Krupski 1997). Более общий подход к общему знанию, основанный на обоснованных знаниях, был предложен в (Артемов 2006). Семантика игровой логики обоснования и динамической эпистемической логики с обоснованиями изучалась в (Renne 2008, Renne 2009). Связи между логикой оправдания и проблемой логического всеведения были рассмотрены в (Артемов и Кузнец 2009, Ван 2009). Название «Логика оправдания» было введено в (Артемов 2008), в котором примеры Крипке, Рассела и Геттье были формализованы; эта формализация была использована для разрешения парадоксов, проверки,скрытый анализ предположений и устранение избыточности. В (Dean and Kurokawa 2009a) логика оправдания использовалась для анализа парадоксов Знающего и Познания.

Библиография

  • Antonakos, E. (2007). «Оправданные и общеизвестные знания: ограниченная консервативность», в работах С. Артемова и А. Нероде (ред.), «Логические основы информатики», Международный симпозиум, LFCS 2007, Нью-Йорк, Нью-Йорк, США, 4–7 июня 2007 г., Труды (Конспект лекций в области компьютерных наук: том 4514), Берлин: Springer, стр. 1–11.
  • Arlo-Costa, H. and K. Kishida (2009). «Три доказательства и знающий в количественной логике доказательств», на семинаре по формальной эпистемологии / FEW 2009. Труды, Университет Карнеги-Меллона, Питсбург, Пенсильвания, США.
  • Артемов С. (1995). «Операционная модальная логика», Технический отчет MSI 95–29, Корнельский университет.
  • ---. (2001). «Явная доказуемость и конструктивная семантика», Бюллетень символической логики, 7 (1): 1–36.
  • ---. (2006). «Обоснованное общее знание», Теоретическая информатика, 357 (1–3): 4–22.
  • ---. (2008). «Логика оправдания», Обзор символической логики, 1 (4): 477–513.
  • Артемов С. и Р. Кузнец (2009). «Логическое всеведение как проблема сложности вычислений», в A. Heifetz (ed.), Теоретические аспекты рациональности и знаний, Труды двенадцатой конференции (TARK 2009), ACM Publishers, стр. 14–23.
  • Артемов С. и Е. Ногина (2005). «Введение оправдания в эпистемическую логику», Журнал логики и вычислений, 15 (6): 1059–1073.
  • Артемов С. и Яворская Т. (Сидон) (2001). «О логике доказательств первого порядка», Московский математический журнал, 1 (4): 475–490.
  • Boolos, G. (1993). The Logic of Provability, Кембридж: издательство Кембриджского университета.
  • Брежнев В. (2001). «О логике доказательств», в книге К. Стригница (ред.), Материалы шестой студенческой сессии ESSLLI, 13-й Европейской летней школы логики, языка и информации (ESSLLI'01), стр. 35–46.
  • Брежнев В., Р. Кузнец (2006). «Объяснение знаний: насколько это сложно», Теоретическая информатика, 357 (1–3): 23–34.
  • Cubitt, RP и R. Sugden (2003). «Общие знания, значимость и условность: реконструкция теории игр Дэвида Льюиса», «Экономика и философия», 19: 175–210.
  • Дин, В. и Х. Курокава (2009a). «От парадокса познания к существованию доказательств», Synthese, 176 (2): 177–225.
  • ---. (2009b). «Знание, доказательство и знающий», в A. Heifetz (ed.), Теоретические аспекты рациональности и знаний, Материалы двенадцатой конференции (TARK 2009), ACM Publications, стр. 81–90.
  • Дрецке Ф. (2005). «Знание закрыто под известным влиянием? Дело против закрытия », в М. Стеуп и Э. Соса (ред.),« Современные дебаты в эпистемологии », Оксфорд: Блэквелл, с. 13–26.
  • Фагин Р., Дж. Халперн, Ю. Моисей и М. Варди (1995). Рассуждение о знаниях, Кембридж, Массачусетс: MIT Press.
  • Фиттинг, М. (2005). «Логика доказательств семантически», Анналы Чистой и Прикладной Логики, 132 (1): 1–25.
  • ---. (2006). «Теорема замены для LP », Технический отчет TR-2006002, Факультет компьютерных наук, Городской университет Нью-Йорка.
  • ---. (2008). «Количественная логика доказательств», Annals of Pure и Applied Logic, 152 (1–3): 67–83.
  • ---. (2009). «Реализации и LP », Анналы чистой и прикладной логики, 161 (3): 368–387.
  • Геттиер Э. (1963). «Оправдано ли истинное знание веры?» Анализ, 23: 121–123.
  • Girard, J.-Y., P. Taylor и Y. Lafont (1989). Доказательства и типы (Кембриджские трактаты в области компьютерных наук: Том 7), Кембридж: издательство Кембриджского университета.
  • Гедель К. (1933). «Eine Interpretation des intuitionistischen Aussagenkalkuls», Ergebnisse Math. Kolloq. 4: 39–40. Перевод на английский язык: S. Feferman et al. (ред.), Собрание сочинений Курта Гёделя (том 1), Оксфорд и Нью-Йорк: издательство Оксфордского университета и Кларендон Пресс, 1986, стр. 301–303.
  • ---. (1938). «Vortrag bei Zilsel / Лекция у Зильселя» (* 1938a), в книге С. Фефермана, Дж. Дж. Доусона, В. Голдфарба, С. Парсонса и Р. Соловая (ред.), Неопубликованные очерки и лекции (Сборник работ Курта Гёделя: том III), Оксфорд: издательство Оксфордского университета, 1995, с. 86–113.
  • Голдман А. (1967). «Причинная теория значения», The Journal of Philosophy, 64: 335–372.
  • Goodman, N. (1970). «Теория конструкций эквивалентна арифметике», в J. Myhill, A. Kino и R. Vesley (eds.), Интуиционизм и теория доказательств, Амстердам: Северная Голландия, стр. 101–120.
  • Горис Э. (2007). «Явные доказательства в формальной логике доказуемости», в работах С. Артемова и А. Нероде (ред.), «Логические основы информатики», Международный симпозиум, LFCS 2007, Нью-Йорк, Нью-Йорк, США, 4–7 июня 2007 г., Труды (заметки в компьютерных науках: Том 4514), Берлин: Springer, стр. 241–253.
  • Хендрикс, В. (2005). Мейнстрим и формальная эпистемология, Нью-Йорк: издательство Кембриджского университета.
  • Хейтинг А. (1934). Mathematische Grundlagenforschung. Intuitionismus. Beweistheorie, Берлин: Springer.
  • Hintikka, J. (1962). Знание и вера, Итака: издательство Корнеллского университета.
  • Kleene, S. (1945). «Об интерпретации интуиционистской теории чисел», Журнал символической логики, 10 (4): 109–124.
  • Колмогоров А. (1932). «Zur Deutung der Intuitionistischen Logik», Mathematische Zeitschrift, 35: 58–65. Английский перевод В. М. Тихомирова (ред.), Избранные труды А. Н. Колмогорова. Том I: Математика и механика, Дордрехт: Kluwer, 1991, с. 151–158.
  • Крейзель Г. (1962). «Основы интуиционистской логики», Э. Нагель, П. Суппес и А. Тарский (ред.), «Логика, методология и философия науки». Материалы Международного конгресса 1960 года, Стэнфорд: издательство Стэнфордского университета, с. 198–210.
  • ---. (1965). «Математическая логика», в T. Saaty (ed.), Лекции по современной математике III, Нью-Йорк: Wiley and Sons, стр. 95–195.
  • Крупский В. (1997). «Оперативная логика доказательств с условием функциональности предиката доказательства», в работах С. Адяна и А. Нероде (ред.), «Логические основы информатики», 4-й Международный симпозиум, LFCS'97, Ярославль, Россия, 6–12 июля 1997 г., Труды (Конспект лекций в области компьютерных наук: Том 1234), Берлин: Springer, с. 167–177.
  • Курокава Х. (2009). «Таблицы и гиперсеквенты для логики обоснования», в работе С. Артемова и А. Нероде (ред.), «Логические основы информатики», Международный симпозиум, LFCS 2009, Дирфилд-Бич, Флорида, США, 3–6 января 2009 г., Proceedings (Конспект лекций в области компьютерных наук: том 5407), Берлин: Springer, с. 295–308.
  • Кузнец Р. (2000). «О сложности явной модальной логики», в работах P. Clote и H. Schwichtenberg (eds.), Computer Science Logic, 14-й международный семинар, CSL 2000, ежегодная конференция EACSL, Фишбахау, Германия, 21–26 августа 2000 г., Труды (Конспект лекций в области компьютерных наук: том 1862), Берлин: Springer, стр. 371–383.
  • ---. (2008). Проблемы сложности в логике обоснования, кандидатская диссертация, факультет компьютерных наук, Университетский центр нью-йоркского университета.
  • ---. (2010). «Записка о ненормальности реализации S4LP », в работе К. Брюннлера и Т. Штудера (ред.), Доказательство, Вычисления, Сложность PCC 2010, Международный семинар, Труды, Технические отчеты IAM IAM-10-001, Институт компьютера Наука и прикладная математика, Университет Берна.
  • McCarthy, J., M. Sato, T. Hayashi и S. Igarishi (1978). «О модельной теории знаний», Технический отчет STAN-CS-78-667, факультет компьютерных наук, Стэнфордский университет.
  • Милникель Р. (2007). «Выводимость в некоторых подсистемах логики доказательств является p 2 p -полной», Annals of Pure and Applied Logic, 145 (3): 223–239.
  • ---. (2009). «Консервативность для логики оправданной веры», в работах С. Артемова и А. Нероде (ред.), «Логические основы информатики», Международный симпозиум, LFCS 2009, Дирфилд-Бич, Флорида, США, 3–6 января 2009 г., Труды (Конспект лекций в области компьютерных наук: том 5407), Берлин: Springer, стр. 354–364.
  • Мкртычев А. (1997). «Модели для логики доказательств», в работе С. Адяна и А. Нероде (ред.), «Логические основы информатики», 4-й Международный симпозиум, LFCS'97, Ярославль, Россия, 6–12 июля 1997 г., Труды (лекция) Заметки по информатике: Том 1234), Берлин: Springer, с. 266–275.
  • Ногина Е. (2006). «О логике доказательств и доказуемости», в 2005 г. Летнее собрание Ассоциации символической логики, Logic Colloquium'05, Афины, Греция (28 июля - 3 августа 2005 г.), Бюллетень символической логики, 12 (2): 356,
  • ---. (2007). «Эпистемическая полнота GLA », ежегодное собрание Ассоциации символической логики 2007 года, Университет Флориды, Гейнсвилл, Флорида (10–13 марта 2007 г.), Бюллетень символической логики, 13 (3): 407.
  • Pacuit, E. (2006). «Замечание о некоторых явных модальных логиках», Технический отчет PP – 2006–29, Институт логики, языка и вычислений, Университет Амстердама.
  • Plaza, J. (2007). «Логика общественных коммуникаций», Synthese, 158 (2): 165–179.
  • Ренн, Б. (2008). Динамическая эпистемическая логика с обоснованием, кандидатская диссертация, факультет компьютерных наук, CUNY Graduate Center, Нью-Йорк, Нью-Йорк, США.
  • ---. (2009). «Устранение доказательств в многоагентной логике оправдания», в A. Heifetz (ed.), Теоретические аспекты рациональности и знаний, Материалы двенадцатой конференции (TARK 2009), ACM Publications, стр. 227–236.
  • Rose, G. (1953). «Исчисление высказываний и реализуемость», Труды Американского математического общества, 75: 1–19.
  • Рубцова Н. (2006). «О реализации S5- модальности с точки зрения доказательств», Журнал логики и вычислений, 16 (5): 671–684.
  • Рассел Б. (1912). Проблемы философии, Оксфорд: издательство Оксфордского университета.
  • Сидон, Т. (1997). «Логика доказуемости с операциями над доказательствами», в работах С. Адяна и А. Нероде (ред.), «Логические основы информатики», 4-й Международный симпозиум, LFCS'97, Ярославль, Россия, 6–12 июля 1997 г., Труды (лекция) Заметки в области компьютерных наук: том 1234), Берлин: Springer, стр. 342–353.
  • Troelstra, A. (1998). «Реализуемость», в S. Buss (ed.), Handbook of Proof Theory, Amsterdam: Elsevier, pp. 407–474.
  • Troelstra, A. and H. Schwichtenberg (1996). Базовая теория доказательств, Амстердам: издательство Кембриджского университета.
  • Troelstra, A. and D. van Dalen (1988). Конструктивизм в математике (тома 1, 2), Амстердам: Северная Голландия.
  • Ван Дален, Д. (1986). «Интуиционистская логика», в D. Gabbay и F. Guenther (eds.), Handbook of Philosophical Logic (Volume 3), Bordrecht: Reidel, pp. 225–340.
  • van Ditmarsch, H., W. van der Hoek и B. Kooi (ed.), (2007). Динамическая эпистемическая логика (Synthese Library, том 337), Берлин: Springer.
  • фон Райт, Г. (1951). Очерк модальной логики, Амстердам: Северная Голландия.
  • Ван Р.-Дж. (2009). «Знание, время и логическое всеведение», в H. Ono, M. Kanazawa и R. de Queiroz (eds.), «Логика, язык, информация и вычисления», 16-й международный семинар, WoLLIC 2009, Токио, Япония, 21 июня -24, 2009, Proceedings (Конспект лекций по искусственному интеллекту: том 5514), Берлин: Springer, стр. 394–407.
  • Яворская (Сидон), Т. (2001). «Логика доказательств и доказуемости», Annals of Pure and Applied Logic, 113 (1–3): 345–372.
  • ---. (2008). «Взаимодействующие системы явных доказательств», Теория вычислительных систем, 43 (2): 272–293.
  • Яворский Р. (2001). «Логика доказуемости с квантификаторами на доказательствах», Annals of Pure and Applied Logic, 113 (1–3): 373–387.

Академические инструменты

значок сеп человек
значок сеп человек
Как процитировать эту запись.
значок сеп человек
значок сеп человек
Предварительный просмотр PDF-версию этой записи в обществе друзей SEP.
значок Inpho
значок Inpho
Посмотрите эту тему в Проекте по онтологии в Индиане (InPhO).
Фил документы
Фил документы
Расширенная библиография для этой записи в PhilPapers со ссылками на ее базу данных.

Другие интернет-ресурсы

Рекомендуем: