Fully Evaluated Left-Sequential Logics

あなたが複雑な料理を準備するシェフだと想像してください。コンピュータ論理の世界では、「材料」は事実（真または偽）であり、「レシピ」はそれらを組み合わせる方法に関する指示です。この論文は、**完全評価左順次論理（FELs）**と呼ばれる調理スタイルの一族を導入します。

核心となる考え方はシンプルです：料理が完成するかどうかを判断する前に、左から右へ、すべての材料を順番に一つずつ味わわなければなりません。 ステップを飛ばすことはできず、最初の材料がまずかったからといって途中で止めることもできません。

以下は、日常的なアナロジーを用いて、著者が探求する異なる「調理スタイル」（論理）の解説です。

1. 基本ルール：「左順次」

これらの論理では、順序が重要です。レシピが「A なら B」という場合、あなたは必ず最初に A を味わわなければなりません。

• ドット: 著者はこのことを示すために、特別なドット（∧• のようなもの）を使用します。これは「左側をまず味わう。それが終わったら、右側を味わう」と意味します。
• 違い: 通常の論理（標準的な真理値表など）では、最初の部分が「偽」であれば、全体がすでに偽であるためそこで止めるかもしれません。しかし、これらの論理では、続けなければなりません。二番目の部分もとにかく味わいます。これを「完全評価」と呼びます。

2. 「調理スタイル」の 4 つのレベル

この論文は、最も混沌としたものから最も厳格なものまで、4 つの論理の階層を提示します。これらを異なるレベルの厨房の規律だと考えてください。

レベル 1：自由 FEL（FFEL） – 「混沌とした味見係」

• 雰囲気: これは最も基本的で「自由」なスタイルです。
• ルール: すべてを順番に味わいます。ただし、同じ材料を二度味わう場合（例えば A、そして再び A）、二度目は一度目が厨房を変えてしまったため、味が異なるかもしれません。
• アナロジー: レモンを味わうと想像してください。最初は酸っぱいです。しかし、絞った直後に再び味わうと、今はただの濡れた皮かもしれません。FFEL では、最初の A が「副作用」（環境の変化など）を持っていた可能性があるため、A と A は必ずしも同じではありません。
• 主要な特徴: 材料が変化しないと約束する場合にのみ、副作用に対して免疫を持ちます。最も予測不可能性を許容するため、最も「弱い」論理です。

レベル 2：記憶 FEL（MFEL） – 「メモを取るシェフ」

• 雰囲気: このシェフは整理整頓されています。
• ルール: 材料（例えば A）を味わったら、それをノートに書き留めます。後でレシピの中で A に再び出会ったら、ノートを見るだけです。二度と味わいません。
• アナロジー: 身分証をチェックする警備員を想像してください。彼が入口であなたの身分証をチェックしたら、裏口でもチェックする必要はありません。彼はあなたを覚えているからです。
• 主要な特徴: これにより「副作用」がなくなります。一度原子（材料）が評価されると、その値はプロセスの残りの間固定されます。これにより、論理はより強力で予測可能になります。

レベル 3：条件付き FEL（CℓFEL） – 「柔軟なチーム」

• 雰囲気: このチームは入れ替わることができます。
• ルール: MFEL のように（味わったものを覚えますが）、異なる材料であれば順序を入れ替えることができます。A なら B は B なら A と同じように扱われます。
• アナロジー: ピザと寿司のどちらにするか決める友人グループを想像してください。アリスとボブがどちらを先に話すかは関係ありません。最終的な決定は同じです。
• 主要な特徴: この論理は、ボチャールの論理と呼ばれる有名な 3 値論理と同等です。「未定義」の材料（割れた卵など）を扱い、その場合、料理全体を即座に「壊れた（未定義）」として扱います。

レベル 4：静的 FEL（SFEL） – 「厳格な会計士」

• 雰囲気: 最も厳格で伝統的なスタイルです。
• ルール: これは単に標準的な命題論理（高校の数学など）ですが、それでもすべてを順番に味わうというルールが付いています。
• アナロジー: これは「ゴールドスタンダード」です。「卵が悪ければ、ケーキも悪い」というレシピがあれば、この論理はそれに同意します。すべての混沌を吸収します。
• 主要な特徴: 非常に厳格であるため、「未定義」の材料を扱うことができません。「未定義」と「偽」を混ぜようとすると、数学が破綻します（なぜなら「未定義」が「偽」になるため、矛盾が生じるからです）。

3. 「未定義」の材料（U）

著者はまた、材料が未定義（U）である場合に何が起こるかも探求します。

• 「自由」および「記憶」スタイルでは: 未定義の材料を味わうと、プロセス全体が停止するか、未定義になります。「謎の粉」でケーキを焼こうとするようなものです。結果は「謎のケーキ」になります。
• 「吸収」ルール: 最も強力な 3 値バージョン（条件付き FEL）では、未定義の材料は「吸収的」です。未定義 を何かと混ぜると、結果は 未定義 になります。それはレシピの中のブラックホールのようなものです。

4. 論理の「木」

ルールが機能することを証明するために、著者は評価木を使用します。

• 家系図を想像してください:
  • 頂点は主な質問です。
  • 枝は「左（真）」と「右（偽）」の経路です。
  • 底の葉は最終的な答え（真または偽）です。
• 革新性: これらの論理では、木はあなたがたどった正確な経路を示します。A を味わい、次に B を味わった場合、木はその特定の旅を示します。「記憶」論理では、同じ材料を二度味わうことを示さないため、木はよりクリーンになります。

論文の成果のまとめ

著者はこれらの調理スタイルを単に記述しただけではなく、それぞれに**規則書（公理系）**を書き上げました。

1. 材料を組み合わせる方法を正確に定義しました（方程式）。
2. これらの規則書が完全（すべての可能なシナリオを網羅している）かつ独立（どの規則も冗長ではなく、システムを壊さずに削除することはできない）であることを証明しました。
3. 人間の誤りが混入しないよう、コンピュータツール（Prover9 および Mace4）を使用して数学を二重チェックしました。

要約すると: この論文は、すべての材料を順番に味わうことを強制される論理システムのスペクトルを地図化しています。それは、材料が変化する可能性のある混沌としたシステムから始まり、味わったものを覚えるシステムへと移り、次に順序が重要でなくなるシステムへと進み、最後に標準的な数学のように振る舞う厳格なシステムに至ります。彼らは、各スタイルに対する正確な数学的法則を提供しています。