Modeling Deontic Modal Logic in ASP

あなたは、コンピュータの脳内で繰り広げられる巨大で目に見えない「もしも（What If?）」ゲームのレフェリーであると想像してください。論理の世界には、ルールについて語るための2つの主要な方法があります。1つ目は、厳格な数学の方程式のようなものです。「Aが真ならば、Bは必ず真でなければならない」。これは古典論理であり、事実を扱うのには適しています。しかし、2つ目はもっと人間的なものです。「Bをすべきである」、「Aをすることは禁止されている」、あるいは「Bをしてもよい」といった表現です。これは義務論理（deontic logic）（ギリシャ語の「義務」に由来）と呼ばれます。これはルール、法律、または道徳的義務の論理です。厄介なのは、現実の世界は混沌としていることです。何かをしなければならないのに、それができないことがあります。何かを禁止されているのに、それをやってしまうこともあります。何十年もの間、コンピュータ科学者や哲学者は、コンピュータがこれらの「すべき」や「禁止」を理解しようとして、論理的な矛盾、すなわち「パラドックス」に陥ってクラッシュすることなく処理する方法に苦心してきました。

「Modeling Deontic Modal Logic in ASP」という題名のこの論文は、まさにその問題に取り組んでいます。著者たちのチーム（アメリカとスペインの研究者）は、コンピュータにルールを理解させるための、巧妙で新しい方法を提案しています。彼らは、すでに「もしも」のシナリオや不完全な情報を扱う能力で有名なプログラミング言語である**回答集合プログラミング（ASP: Answer Set Programming）**を使用しています。論文では、ルールを「事実を強制する硬直したコマンド」としてではなく、グローバル制約（ルールが破られたときに鳴るレフェリーの笛のようなもの）として扱うことで、コンピュータは論理学者たちを悩ませてきた数十年来のパズルをついに解くことができるのだと主張しています。彼らは、この手法が、「義務違反（Contrary-to-Duty）」のパラドックス（以前のルールを守れなかったときに、ルールが自己矛盾を起こしているように見える現象）のような有名な論理の罠を、エレガントに解決できることを示しています。

「すべき」と「必ず」のマジック

著者たちが何を行ったかを理解するために、まず物語の2つの主要な登場人物である**「義務（Obligation）」と「許可（Permission）」*を紹介する必要があります。日常生活において、私たちは「太陽が昇ることは必然である」（自然の事実）と、「図書館の本を返すべきである」（破る可能性のあるルール）の違いを知っています。論理の世界では、前者はアレティック（alethic）（真理と必然性に関するもの）、後者は義務論的（deontic）*（義務や規範に関するもの）と呼ばれます。

著者たちは、コンピュータにはこれら異なるタイプの思考を扱うための2つの特別なツールがすでに備わっているものの、それらが誤った方法で使用されていることに気づきました。

1. 強否定（Strong Negation）: これは、明確な「ノー」のようなものです。もしコンピュータが「雨は降っていない」と（強否定で）言えば、それは雨が降っていないという確実な証拠を持っていることを意味します。これは事実です。
2. デフォルト否定（Default Negation / Negation-as-Failure）: これは、「おそらく降っていない」のようなものです。もしコンピュータが「雨は降っていない」と（デフォルト否定で）言えば、それは単に雨が降っているという証拠を見つけられなかったことを意味します。これは欠落した情報に基づいた推測です。

論文の大きなアイデアは、これら2つのコンピュータツールを、2つの論理タイプに直接マッピングすることです。彼らは、「Pは必然である」（事実）と言うときには強否定を使い、「Pは必然ではない」（Pが偽である可能性がある、あるいは単にわからない）と言うときにはデフォルト否定を使うことを提案しています。この単純な切り替えにより、コンピュータは硬い事実と、破られる可能性のあるルールを区別できるようになります。

「レフェリー」のアプローチ

この論文の最も独創的な部分は、義務をどのように扱うかという点です。多くの古いシステムでは、「車を返さなければならない」という義務は、コンピュータに車を返させることを強制するコマンドとして扱われていました。しかし、もし車が盗まれたらどうなるでしょうか？コンピュータは、車を返すことを強制できないため、クラッシュしてしまいます。

著者たちは異なるアプローチを提案しています。義務をグローバル制約（Global Constraints）（または「否定（Denials）」）として扱うことです。サッカーの試合におけるレフェリーを想像してみてください。レフェリーは選手にゴールを決めるよう強制するのではなく、反則が起きたときに笛を吹くだけです。著者たちのシステムでは、義務とは何かを真にするためのコマンドではなく、「もしあるルールが破られている世界にいるならば、その世界は無効である」というルールなのです。

例えば、「シートベルトを着用しなければならない」というルールがあるとします。コンピュータはあなたにシートベルトを着用させるよう強制しません。代わりに、「シートベルトなしで運転している世界」を一つの制約として設定します。「あなたがシートベルトなしで運転している世界は、無効である」という制約です。もしあなたが運転していてシートベルトをしていない場合、コンピュータは単に「そのシナリオはこのルール下では不可能である」と言い、あなたがシートベルトをしている別のシナリオを探します。しかし、決定的なのは、もしあなたがシートベルトをしない正当な理由（医療上の緊急事態など）を持っている場合、コンピュータはそのルールを「先取り（preempt）」することができます。コンピュータはその特定の状況において制約を外し、そのシナリオが存在することを許容します。

「チズムのパズル」を解く

この論文が最も輝くのは、「義務違反のパラドックス（Contrary-to-Duty Paradox）」（別名：チズムのパラドックス）を解決するときです。これは次のような有名な論理の頭痛をもたらす問題です。

1. あなたはパーティーに行くべきである。
2. もし行くならば、母親に伝えるべきである。
3. もし行かないならば、母親に伝えてはならない。
4. あなたは行かない。

古い論理システムでは、これは混乱を引き起こします。コンピュータは、あなたが母親に伝えるべきか否かを判断しようとし、結果として「伝えるべきである」と「伝えるべきではない」の両方の結論が出てしまい、矛盾が生じます。まるでロボットが頭痛を起こしているような状態です。

著者たちは、彼らの「レフェリー」手法がこれを即座に解決することを示しています。彼らはルールを制約として設定します。

• 制約1：もし行かないならば、母親に伝えてはならない。
• 制約2：もし行くならば、母親に伝えなければならない。

コンピュータが「あなたは行かなかった（事実4）」という事実を見たとき、制約をチェックします。まず、制約2（「もし行くならば」というルール）は条件が満たされていないため適用されないことを確認します。次に、制約1を見ます。あなたは行かなかったので、ルールは「伝えないこと」となります。コンピュータは、「行かず、かつ母親に伝えなかった」という有効な世界を容易に見つけ出します。矛盾も頭痛もありません。「パラドックス」は、ルールが互いに戦う硬直したコマンドではなく、条件が満たされたときにのみ適用される柔軟な制約として扱われているために消滅するのです。

なぜこれが重要なのか

著者たちは単一のパズルを解いただけではありません。彼らは、この手法が「フォレスターのパラドックス」や「サルトルのジレンマ」を含む、一連の論理的問題を解決できることを示しています。彼らは、**回答集合プログラミング（ASP）**が持つ「もしも」のシナリオや「例外」を扱う能力を利用することで、複雑な倫理的・法的システムを以前よりもずっと自然にモデル化できることを証明しています。

また、これがどのように「二次的義務」を扱うかも示しています。例えば、友人の車を借りたとします。あなたにはメインのルール「車を返す」があります。しかし、そこには二次的なルールもあります。「正午前に返す」、「バッテリーを満タンにして返す」などです。もしあなたが車を壊した場合（メインルールの違反）、二次的なルールは変化したり消失したりする可能性があります。著者たちは、彼らのシステムがいかにこれらのルールを自動的に「先取り（preempt）」できるかを示しています。もし車が壊れていれば、「正午前に返す」という制約は、（返すべき車が存在するという）条件がなくなったためにドロップされます。コンピュータは混乱することなく、単に有効な世界のリストを更新するのです。

結論

この論文は、倫理や法律のあらゆる問題を解決したと主張しているわけではありません。むしろ、ルールを理解するシステムを構築するための、クリーンでエレガントなツールキットを提供しています。義務を「現実を変えるためのコマンド」としてではなく、**「可能な世界に対する制約」**として扱うことで、人間と同じように、柔軟に、例外を認め、論理的なループに陥ることなくルールについて推論できるコンピュータを構築できることを証明しています。著者たちは、このアプローチが、複雑な新しい数学や「制裁（罰則）」を必要とした従来の手法よりも、より単純で直接的であることを示唆しています。回答集合プログラミングに備わっている既存のツールを活用することで、人間のようなルールを理解するための道は、私たちが考えていたよりも短く、真っ直ぐなものであることを彼らは示したのです。