Стандартная деонтическая логика SDL: авторское изложение

ru · official · sha256:a20c828fca55999936d70c772bdbd2353d33c7a547229738f1a4fb92ae494b50

СТАНДАРТНАЯ ДЕОНТИЧЕСКАЯ ЛОГИКА SDL: АВТОРСКОЕ ИЗЛОЖЕНИЕ Настоящий документ является АВТОРСКИМ ИЗЛОЖЕНИЕМ, составленным для целей формализации пакета logic.deontic. Он не является переводом и не воспроизводит текст ни одного из названных ниже источников: изложение пересказывает их своими словами и в каждом разделе называет источник. БАЙТЫ НАЗВАННЫХ ИСТОЧНИКОВ НЕ ЗАКРЕПЛЯЮТСЯ. Статья G. H. von Wright «Deontic Logic» (Mind, том 60, 1951), глава R. Hilpinen и P. McNamara «Deontic Logic: A Historical Survey and Introduction» в издании «Handbook of Deontic Logic and Normative Systems», том 1 (College Publications, 2013), статьи A. Ross «Imperatives and Logic» (Theoria, 1941), R. M. Chisholm «Contrary-to-duty imperatives and deontic logic» (Analysis, том 24, 1963), J. W. Forrester «Gentle murder, or the adverbial Samaritan» (Journal of Philosophy, том 81, 1984) охраняются авторским правом; открытого пина байтов у репозитория нет. Источники названы декларациями без закрепления, страницы не называются вовсе — печатных изданий у репозитория нет, и выдумывать номера страниц запрещено. ЧТО ЗАКРЕПЛЕНО БАЙТАМИ. Байтами закреплено настоящее изложение. Модальная часть — нормальность, схема K, правило необходимости, схема D и серийность отношения достижимости — анкеруется в закреплённые байты Open Logic Project через пакет logic.modal и здесь не пересказывается. Настоящее изложение не является нормативным актом и не имеет силы источника права ни в одной юрисдикции.

ru · official · sha256:7b480b23fb7ca855b4fe8d69b9b58a070c034dff0b7e4351ec914b3a7a624845

Раздел 1. Что называется стандартной деонтической логикой. Стандартной деонтической логикой (SDL) называется нормальная модальная логика KD, прочитанная деонтически: единственный примитивный оператор O читается «обязательно, что», отношение достижимости читается как отношение «мир, идеальный с точки зрения мира w», а схема D — как утверждение, что идеальный мир существует всегда. Отождествление SDL с KD и деонтическое прочтение изложены в: R. Hilpinen, P. McNamara, «Deontic Logic: A Historical Survey and Introduction», Handbook of Deontic Logic and Normative Systems, том 1, College Publications, 2013, раздел о стандартной системе. Первое построение системы этого вида принадлежит G. H. von Wright, «Deontic Logic», Mind, 1951; система фон Вригта отличается от современной SDL и здесь не отождествляется с нею.

Ссылаются нормы: SDL

ru · official · sha256:83c45cd7b9e8f6381732294447c1b2af201ebcd313f98cfc47721fd81f5cf52c

Раздел 2. Выбранная формализация. В настоящем пакете SDL берётся в следующей, явно названной формализации: язык — язык логики высказываний с одним одноместным оператором O; аксиомные схемы — все тавтологии, схема K вида «O(A → B) → (OA → OB)» и схема D вида «OA → ¬O¬A»; правила — modus ponens и правило необходимости, позволяющее заключить OA из доказанного A. Разрешение и запрет определены, а не примитивны: PA есть сокращение для ¬O¬A, FA есть сокращение для O¬A. Иная формализация того же названия — с примитивным P, с оператором «должно, чтобы не» или с добавленной схемой T — здесь НЕ описывается, и утверждения этого пакета к ней не относятся.

Ссылаются нормы: L_DEONTIC, OBLIGATION, PERMISSION, PROHIBITION, SDL_CALCULUS, formalisation_choice

ru · official · sha256:97a4ae03cbb801d6cccebfee1d3e06ce9fa2e023202865628d0d3d938f30af1e

Раздел 3. Семантика. Моделью SDL называется тройка из непустого множества миров, серийного бинарного отношения достижимости и оценки атомарных высказываний. OA истинна в мире w, если A истинна во всяком мире, достижимом из w. Серийность — у каждого мира есть хотя бы один достижимый — есть в точности то условие на модель, которому соответствует схема D. Соответствие «серийность ↔ схема D» есть утверждение модальной теории соответствия и взято из пакета logic.modal, где оно закреплено байтами источника.

Ссылаются нормы: IDEAL_WORLD

ru · official · sha256:9e92fb3210d5893c282baa585beb86c94c80ca7bee3347ce25cc9acf31296bbb

Раздел 4. Как читать обязанность и разрешение. Инструкция чтения формулы SDL состоит из четырёх шагов. Шаг первый: назвать мир оценки. Шаг второй: определить главный оператор формулы. Шаг третий: если главный оператор есть O, обойти все достижимые из мира оценки миры и прочесть в них аргумент; если главный оператор есть P, прочесть его как ¬O¬ и применить тот же обход. Шаг четвёртый: назвать использованное определение или схему. Шаги три и четыре описываются пакетом как ДЕЙСТВИЯ; никакой модели пакет не строит и не обходит.

Ссылаются нормы: DeonticReadingAvailable, reading_available_for, reading_step

ru · official · sha256:051b7f5c8e0a8e5fc1b1a4fd99f6d4c7de86dbb273e844d8da3bdd8fb81a3d48

Раздел 5. Правило необходимости и его ограничение в деонтическом прочтении. Правило необходимости позволяет заключить OA из ДОКАЗАННОГО A. Ограничение существенно и в деонтическом прочтении читается прямо: обязательным объявляется всякая логическая истина, но не всякое истинное утверждение. Правило применимо к теоремам системы и неприменимо к посылке, введённой допущением; отсюда, в частности, что из A не следует OA. Это ограничение принадлежит определению нормальной модальной логики и закреплено в пакете logic.modal.

ru · official · sha256:b006aa472b5a8448a8dcc864366ce796a1bd4cf4503683ea3263001753e73374

Раздел 6. Границы формализации: разбор источниковых примеров. Ниже перечислены четыре примера, названные в литературе и показывающие, чего SDL не выражает. Каждый приводится как СВИДЕТЕЛЬСТВО ГРАНИЦЫ, а не как опровержение системы. Пример 1 — парадокс Росса. Из «обязательно отправить письмо» в SDL выводится «обязательно отправить письмо или сжечь его», потому что O замкнут по следованию. Нормативно второе не читается как разрешение сжечь, но система различия не выражает. Источник: A. Ross, «Imperatives and Logic», Theoria, 1941. Пример 2 — контрарные долгу императивы Чизома. Набор из четырёх утверждений — «обязательно помочь соседу»; «обязательно, если помогаешь, предупредить о приходе»; «если не помогаешь, обязательно не предупреждать»; «не помогает» — интуитивно непротиворечив и взаимно независим, но во всякой естественной записи в SDL оказывается либо противоречивым, либо зависимым. Источник: R. M. Chisholm, «Contrary-to-duty imperatives and deontic logic», Analysis, том 24, 1963. Пример 3 — «мягкое убийство» Форрестера. Из «запрещено убивать» и «если убиваешь, обязательно убивать мягко» вместе с «убивает» в SDL выводится «обязательно убивать», потому что мягкое убийство влечёт убийство, а O замкнут по следованию. Источник: J. W. Forrester, «Gentle murder, or the adverbial Samaritan», Journal of Philosophy, том 81, 1984. Пример 4 — парадокс доброго самаритянина. «Обязательно помочь ограбленному» влечёт в SDL «обязательно, чтобы кто-то был ограблен», поскольку помощь ограбленному влечёт ограбление. Пример восходит к A. N. Prior; обзор — в названной главе Hilpinen и McNamara.

Ссылаются нормы: limit_example

ru · official · sha256:5b75a04791659451a03b8013089dbe37804ab0b5e6f192c98787f9549c178098

Раздел 7. Чем эти примеры не являются. Ни один из четырёх примеров не показывает, что SDL противоречива: все они показывают, что ЗАМКНУТОСТЬ обязанности по логическому следованию, унаследованная от нормальной модальной логики, не совпадает с нормативным рассуждением. Литература отвечает на них разными средствами — диадической деонтической логикой, логиками с приоритетами, императивной семантикой, — и настоящий пакет ни одного из этих ответов не описывает: он описывает SDL и называет её границы. Объявлять SDL исчерпывающей моделью нормативного рассуждения пакету запрещено, и утверждения такого рода в нём нет.

Ссылаются нормы: LimitsAreNamed, limits_are_named

ru · official · sha256:4b2961be6be459682c02bd72402974afb812c2f87fbd95c9a903e7c0f848e6ed

Раздел 8. Отношение к деонтике самого движка Arxo. Позиции §120 движка Arxo — duty, liberty, power, immunity — суть механизм исполнения норм, а не модель SDL. Оператор O настоящего пакета есть ОПИСЫВАЕМЫЙ объект чужой системы, и он не отождествляется ни с одной позицией движка. Соответствие между ними не утверждается и не подразумевается.

Ссылаются нормы: BoundaryDeclared, boundary_declared, not_identified_with