Логика в вычислениях нормативных позиций
Sergot M., A Computational Theory of Normative Positions. Логические формализмы вроде презентованного здесь читать непросто, да и не очень интересно. Интересны границы метода. Например, ввод-вывод в формализм. Приведённый ниже отрывок взят из примера практического использования логики (формализм Norman-G):
Note [2]. We are supposing for the purpose of the example that if one of the administrator a’s cars is parked, then a must be at least one of those responsible for the car’s being parked, i.e., that O(p(a1) ->Ea p(a1)) holds. It might be tempting to read this as saying that if car-a1 is parked then it must have been the administrator a who parked it. But note that expression Ea p(a1) does not necessarily signify that a parks car-a1; a may bring about p(a1) in some different way, perhaps even unintentionally. See [Sergot and Richards 2000] for further discussion of this point.
Там ситуация с разрешениями на парковку авто. Логический вывод «not necessarily», сделан не логическим способом, а на основании обобщённого прагматического опыта, который пытаются затолкать в формализм. Значительная часть интеллектуальных усилий в логике тратится на то, чтобы с помощью синтаксически компактных конструктов, имеющих высокую абстракцию опыта, вроде группы «Еа A», означающей «агент а вызывает A» (Ex A stand for «agent x brings it about that A»), которые при этом ещё и имеют очень низкую параметризацию (в этой всего три параметрических места), описать ситуации и сценарии с существенно более высокой вариативностью.
Логическая формула, чтобы оставаться читабельной, должна быть низковариативной (слева — нотационный максимум), но описывать должна более высоковариативные ситуации. Как? Комбинацией формул.
Но это стратегически не спасает. Чем больше формул, тем сложнее отследить непротиворечивость. Возникают семантические или аксиоматические вопросы вроде такого, влияющие на всю систему вывода
It employs what some authors refer to as the Meinong-Chisholm analysis, whereby ‘x ought to bring it about that F ’ is taken to mean ‘it ought to be that x brings it about that F ’. It is possible to question whether these expressions are in fact equivalent.
Введение дополнительного параметра, например — времени, или места, или чего угодно ещё, влияющего на нормативное суждение, должно повлиять на всю конструкцию. Но рефакторинг представляет собой задачу как минимум весьма трудоёмкую. А то и просто невозможную
The number of normative positions in the target partition is then 22(m+1)n−1. Estimate how long it would take to examine even a small example: scanning the list of positions for 2 agents and 2 propositions at, say, 10 positions per second would still take 58 billion (58 × 109) years to go through the entire list.
Ещё раз прихожу к мнению, что логические формализмы для нормативного вывода сами по себе бесполезны. Часть наработок, например, «атомарные типы» Кангер-Линдаля (Kanger-Lindahl) могут быть интересны, как частное упражнение.