Лестница уровней абстракции

Семь уровней: от риторики до вычислимой процедуры. Один и тот же довод — на каждом уровне. Работает уровень 2 (Аристотель): разбор ведётся строго понятиями его эпохи.

Тезис
Предъявлено против тезиса
Условное «если P, то Q» — уровень 3, стоики
Связь
Что известно и что выводят
Факты запроса — уровень 4, булева алгебра
Силлогизм (три суждения)
Бо́льшая посылка
Меньшая посылка
Заключение
1. Риторика и убеждение
Сначала люди учились не доказывать, а убеждать
ещё не реализовано
отличать убедительную речь от верного доказательства
Пример: уверенное утверждение руководителя, что доступ надо дать всем менеджерам
Что теряется при переходе: различие между убедительностью и логической правильностью
Что достигается: речь, которая убеждает
Разбора нет. Уровень «Риторика и убеждение» ещё не реализован кодом — здесь не будет правдоподобной заглушки.
↓ переход: осознание разницы между «хочу согласиться» и «это действительно следует»
2. Силлогизм и форма вывода
Аристотель отделяет форму от содержания
видеть общую форму под разными историями
Пример: банковские правила доступа: разным действующим лицам — разные типы
Что теряется при переходе: невозможно проверить истинность самих посылок
Что достигается: каркас, сохраняющийся при замене содержания буквами
Тезис: Все человек есть смертный
Предъявлено: Ни один человек не есть смертный
ἄγνοια τοῦ ἐλέγχου — подмена тезиса (contrary_not_contradictory)

Четыре условия тождества предмета

  • о том же самом (τοῦ αὐτοῦ) — субъект человек / человек
  • о том же самом — предикат смертный / смертный
  • в том же отношении (πρὸς τὸ αὐτό) не оговорено
  • в то же время (ἐν τῷ αὐτῷ χρόνῳ) не оговорено

Отношение по квадрату суждений

противность (контрарность) — НЕ противоречие

Ход разбора — 7 шагов

  1. Тезис: «Все человек есть смертный». Субъект тезиса — «человек», предикат — «смертный».
    тезистерминсубъектпредикат
    Тезис разложен на два термина; спор идёт о том, что сказано о субъекте.
  2. Тезис по количеству — общее, по качеству — утвердительное.
    тезисколичествокачествообщееутвердительное
    Опровергать его придётся суждением, которое ему противоречит, а не любым несогласным.
  3. Предъявлено: «Ни один человек не есть смертный». Его субъект — «человек», предикат — «смертный».
    доводтерминсубъектпредикат
    Теперь видно, об одном ли предмете идёт речь.
  4. Предъявленное по количеству — общее, по качеству — отрицательное.
    доводколичествокачествообщееотрицательное
    Оба суждения приведены к виду, в котором их можно сопоставить.
  5. Об одном ли предмете речь: субъект — тот же; предикат — тот же; в том же отношении — не оговорено ни там, ни там; в то же время — не оговорено ни там, ни там.
    тождество_предметато_же_отношението_же_времятот_же_образтермин
    Четыре условия соблюдены: спор об одном и том же.
  6. По квадрату суждения противны: вместе истинными не бывают, но вместе ложными — бывают.
    логический_квадратпротиворечиепротивность
    Взято более сильное, чем нужно: противность вместо противоречия.
  7. Условие опровержения нарушено: взята противность вместо противоречия — доказано более сильное, чем требовалось.
    софистическое_опровержениеопровержениетезисспорящийзаключение
    Опровержения нет: доказано нечто иное, тезис остался нетронутым. Это ἄγνοια τοῦ ἐλέγχου — подмена тезиса.

Словарь уровня

Использовано понятий: 21. Проверка на анахронизмы: :ok (по шагам: :ok).
На этом уровне нет множеств, переменных, таблиц истинности, функций и категорий — только термин, посылка, заключение, фигура, противоречие, опровержение.

Силлогизм: форма отдельно от истинности

Все человек есть смертный
Все Сократ есть человек
следовательно: Все Сократ есть смертный
форма верна — AAA-1 Barbara
форма проверена; истинность посылок программа не знает и не выдумывает
↓ переход: отделение скрытых предположений от явной структуры
3. Логика высказываний (стоики)
Стоики переходят от вещей к условиям
различать достаточную причину и единственно возможную
Пример: дождь делает дорогу мокрой, но мокрая дорога не доказывает, что шёл дождь
Что теряется при переходе: представление конкретных объектов и их отношений
Что достигается: различение достаточной причины от единственно возможной
Условное: если учётная запись заблокирована, то отчёт открыть нельзя
Известно: отчёт открыть нельзя
Выводят: учётная запись заблокирована
ошибка: утверждение консеквента (affirmatio consequentis) — вывод не следует

Преобразования условного

  • противопоставление: если не (отчёт открыть нельзя), то не (учётная запись заблокирована) равносильно исходному
  • обращение: если отчёт открыть нельзя, то учётная запись заблокирована НЕ равносильно; расходится при %{p: true, q: false}

Ход разбора — 5 шагов

  1. Дано: если учётная запись заблокирована, то отчёт открыть нельзя; отчёт открыть нельзя. Вывод: учётная запись заблокирована.
    высказываниесвязьдовод
    Разбираем не части высказываний, а связь между целыми высказываниями.
  2. Условное: если учётная запись заблокирована, то отчёт открыть нельзя. Основание (антецедент) — «учётная запись заблокирована», следствие (консеквент) — «отчёт открыть нельзя».
    условноеантецедентконсеквентоснованиеследствие
    Связь идёт в одну сторону: от основания к следствию.
  3. Известно: отчёт открыть нельзя. Это утверждение СЛЕДСТВИЯ.
    высказываниеотрицаниесвязь
    Видно, с какого конца связи заходит второе высказывание.
  4. Довод идёт по связи не в ту сторону: утверждение консеквента (affirmatio consequentis).
    ошибка_выводасвязьоснованиеследствие
    Вывод НЕ следует.
  5. Дождь делает дорогу мокрой, но мокрая дорога не доказывает дождя: могла проехать поливальная машина. Следствие бывает и по другой причине.
    равносильностьобращениепротивопоставлениеистинность
    Достаточное основание перепутано с единственно возможным.

Словарь уровня

Проверка на анахронизмы: :ok
У стоиков нет терминов, фигур и среднего термина — это аппарат предыдущего уровня. Здесь единица разбора — целое высказывание и связь между высказываниями.
↓ переход: от классов к условным связям между утверждениями
4. Булева алгебра
Лейбниц мечтает о вычислении, Буль строит алгебру
одинаково применять правило ко всем случаям
Пример: простое правило доступа, которое становится двусмысленным на масштабе
Что теряется при переходе: причины отказа остаются неявными в булевых результатах
Что достигается: одинаковая обработка одинаковых случаев
Правило как формула: доступ = ((owner ИЛИ auditor) И (recheck И НЕ blocked))
Факты: учётная запись заблокирована=0тот же tenant=1владелец=1аудитор=0повторная проверка=1
Значение формулы: 1
разрешено (версия политики access-policy/1)
Голое решение: 1. Решение с причиной: {:allowed, "access-policy/1"}. Из первого причина отказа не восстанавливается — в этом бедность boolean как результата.

Таблица решений — сработала строка №4

заблокирован тот же tenant владелец/аудитор решение
1 1 любое любое deny: account-blocked
2 0 0 любое deny: tenant-mismatch
3 0 1 0 deny: missing-grant
4 0 1 1 allow (access-policy/1)
первое совпадение выигрывает, дальше строки не смотрим. локальные проверки идут раньше удалённого сервиса ролей: иначе система тратит сеть на заведомо отказные случаи и даёт утечку через разницу во времени ответа
Расхождение таблицы и формулы: таблица решений не знает про «повторную проверку», которая есть в формуле: расхождений 3, все при recheck=0 — формула отказывает, таблица разрешает.

Таблица истинности формулы доступа

auditorblockedownerrecheck доступ
1111 0
1110 0
1101 0
1100 0
1011 1
1010 0
1001 1
1000 0
0111 0
0110 0
0101 0
0100 0
0011 1
0010 0
0001 0
0000 0

Де Морган как инструмент ревью

исходное: НЕ (owner ИЛИ auditor)
правильно: (НЕ owner И НЕ auditor)
типовая ошибка: (НЕ owner ИЛИ НЕ auditor) — расходится при %{owner: false, auditor: true}

Восемь групп законов — проверены перебором

коммутативность: 8 наборов, нарушений 0 ассоциативность: 16 наборов, нарушений 0 дистрибутивность: 16 наборов, нарушений 0 тождества: 8 наборов, нарушений 0 дополнения: 6 наборов, нарушений 0 идемпотентность: 4 наборов, нарушений 0 де Морган: 8 наборов, нарушений 0 поглощение: 8 наборов, нарушений 0

Ход разбора — 6 шагов

  1. Правило стало формулой: доступ = ((owner ИЛИ auditor) И (recheck И НЕ blocked)).
    формулаоперациябулева_переменная
    Спор о правиле теперь решается вычислением, а не пересказом.
  2. Набор значений: blocked=0, same_tenant=1, owner=1, auditor=0, recheck=1.
    набор_значенийзначениебулева_переменная
    Каждое условие — да или нет; ничего третьего на этой ступени нет.
  3. Значение формулы на этом наборе: 1 (доступ по формуле есть).
    формулазначениетаблица_истинности
    Одинаковые наборы обязаны дать одинаковый ответ — в этом вся польза.
  4. Сработала строка №4 таблицы решений: разрешить (версия политики access-policy/1).
    таблица_решенийпорядок_правилкороткое_замыкание
    Первое совпадение выигрывает; порядок строк — архитектурное решение.
  5. Голое решение: 1. Решение с причиной: разрешено, версия access-policy/1.
    причина_отказаверсия_политикитаблица_решений
    «Нельзя» без причины — это ответ, из которого нельзя понять, что исправить: решение должно нести основание.
  6. Отрицание правила: «НЕ (owner ИЛИ auditor)» — это «(НЕ owner И НЕ auditor)», а не «(НЕ owner ИЛИ НЕ auditor)». Вторая запись меняет правило, расходясь на наборе %{owner: false, auditor: true}.
    законравносильностьотрицаниеревью
    Отрицание вносится внутрь по закону, а не на глаз.
Проверка на анахронизмы: :ok
На этом уровне нет предикатов, кванторов и отношений между объектами: переменная тут булева, а не обозначающая человека или отчёт.
↓ переход: от словесного описания к алгебраической формуле
5. Предикатная логика (Фреге)
Фреге добавляет переменные, отношения и кванторы
ещё не реализовано
не путать «для каждого» и «существует»
Пример: каждый сотрудник читает какой-то отчёт против «один отчёт читают все»
Что теряется при переходе: усложнение выражений, риск подмены масштаба кванторов
Что достигается: оставить места для конкретного пользователя и отчёта
Разбора нет. Уровень «Предикатная логика (Фреге)» ещё не реализован кодом — здесь не будет правдоподобной заглушки.
↓ переход: от замкнутых высказываний к открытым формулам с параметрами
6. Формальные системы с границами
Парадоксы и формальные системы проводят границы
ещё не реализовано
признавать пределы любой формальной системы
Пример: парадоксы, показывающие врождённые пределы логической системы
Что теряется при переходе: типы гарантируют форму, но не справедливость
Что достигается: сделать недопустимые состояния непредставимыми
Разбора нет. Уровень «Формальные системы с границами» ещё не реализован кодом — здесь не будет правдоподобной заглушки.
↓ переход: от универсальной формализации к осознанным границам модели
7. Вычислимость и процедура (Тьюринг, Шеннон)
Тьюринг превращает правило в процедуру, Шеннон — в схему
ещё не реализовано
превратить правило в исполняемый процесс
Пример: политику возврата мало объявить — нужна процедура исполнения
Что теряется при переходе: новые классы ошибок между проверкой и действием
Что достигается: правило превращается в реальный процесс с условиями
Разбора нет. Уровень «Вычислимость и процедура (Тьюринг, Шеннон)» ещё не реализован кодом — здесь не будет правдоподобной заглушки.
↓ переход: от математической чистоты к инженерной реальности сетей и времени

Две редакции одного рассказа

две редакции одного рассказа — идут параллельно

Доказательная

  1. неясное требование
  2. аргумент и скрытые посылки
  3. форма силлогизма
  4. условные связи (логика высказываний)
  5. булева алгебра
  6. предикаты и отношения
  7. формальные границы
  8. вычислимая процедура

Инженерная

  1. неясное требование
  2. аргумент и скрытые посылки
  3. доменные понятия (ubiquitous language)
  4. предикаты и таблица решений
  5. типы и инварианты
  6. исполнимая политика
  7. эффекты и явные отказы
  8. архитектурная граница

Маршрут статьи и маршрут схемы — разные

excalidraw-схема и статья — РАЗНЫЕ маршруты, не путать

Только в статье

  • стоики / логика высказываний
  • Фреге / предикатная логика
  • формальные системы с границами
  • вычислимость (Тьюринг, Шеннон)

Только на схеме

  • теория множеств (Эйлер, Рассел, Гёдель)
  • теория групп
  • теория категорий (функторы, монада как моноид в категории эндофункторов)

Общее

  • риторика/Аристотель
  • силлогистика
  • булева алгебра