モナド述語計算

論理学において、モナド述語計算（モナド一階述語論理とも呼ばれる）は、シグネチャ内のすべての関係記号がモナド的（つまり、引数を1つしか取らない）であり、関数記号が存在しない一階述語論理の一部である。したがって、すべての原子式は という形式をとる。ここでは関係記号、は変数である。 ${\displaystyle P(x)}$ ${\displaystyle P}$ ${\displaystyle x}$

モナディック述語計算は、2 つ以上の引数を取る関係シンボルを許可するポリアディック述語計算とは対照的です。

表現力

モナド述語計算では、多項式関係記号が存在しないために表現できる内容が著しく制限される。この計算は非常に弱いため、完全な述語計算とは異なり、 決定可能である。つまり、与えられたモナド述語計算の式が論理的に妥当であるかどうか（すべての空でない領域において真であるかどうか）を決定する決定手続きが存在する。 ^{[ 1 ] [ 2 ]}しかし、モナド論理に2項関係記号を1つ追加すると、決定不可能な論理となる。

項論理との関係

モナド論理を超える必要性は、19世紀にオーガスタス・ド・モーガンとチャールズ・サンダース・パースが関係論理について、そして1879年にフレーゲが『三段論法』で著した研究によって初めて認識されました。これら3人の研究以前は、形式的な演繹推論には項論理（三段論法）が適切であると広く考えられていました。

項論理における推論はすべてモナド述語論理で表現できる。例えば、

犬はすべて哺乳類です。

哺乳類の中には鳥類は存在しません。

したがって、犬は鳥ではありません。

これは、モナド述語計算の言語では次のように表記できる。

${\displaystyle [(\forall x\,D(x)\Rightarrow M(x))\land \neg (\exists y\,M(y)\land B(y))]\Rightarrow \neg (\exists z\,D(z)\land B(z))}$

ここで、、はそれぞれ犬、哺乳類、鳥類であることの述語を表します。 ${\displaystyle D}$ ${\displaystyle M}$ ${\displaystyle B}$

逆に、モナド述語計算は項論理よりも表現力が著しく優れているわけではない。モナド述語計算の各式は、量指定子が次の形式の閉じた部分式にのみ現れる 式と等価である。

${\displaystyle \forall x\,P_{1}(x)\lor \cdots \lor P_{n}(x)\lor \neg P'_{1}(x)\lor \cdots \lor \neg P'_{m}(x)}$

または

${\displaystyle \exists x\,\neg P_{1}(x)\land \cdots \land \neg P_{n}(x)\land P'_{1}(x)\land \cdots \land P'_{m}(x),}$

これらの式は、項論理で考慮される基本的な判断を若干一般化しています。例えば、この形式では「すべての哺乳類は草食動物か肉食動物（あるいはその両方）である」といった命題が許容されます。しかし、このような命題に関する推論は、19の古典的なアリストテレス三段論法だけでは対応できないものの、項論理の枠組みの中で扱うことができます。 ${\displaystyle \forall x\,M(x)\Rightarrow (H(x)\lor C(x))}$

命題論理を所与とすると、モナド述語計算におけるあらゆる式は、項論理においても同様に定式化できる何かを表現する。一方、伝統論理における多重一般性の問題に対する現代的な見解は、束縛変数を関連付ける多項述語がなければ、量化子は有効に入れ子にすることができないという結論に至る。

変種

上記の形式体系は、純粋モナド述語計算と呼ばれることもあります。ここで「純粋」とは、関数記号が存在しないことを意味します。モナド関数記号を許容しても論理は表面的にしか変化しませんが、2項関数記号を1つでも許容すると、決定不能な論理になってしまいます。

モナドの 2 階論理では、式内でより高次の述語を使用できますが、2 階の量化は単項述語に制限されます。つまり、許可される 2 階変数はサブセット変数のみです。

脚注

1. Heinrich Behmann、 Beiträge zur Algebra der Logik、insbesondere zum Entscheidungsproblem、 Mathematische Annalen (1922)
2. Löwenheim, L. (1915) "Über Möglichkeiten im Relativkalkül"、 Mathematische Annalen 76: 447-470。 Jean van Heijenoort、1967 年に「親戚の微積分における可能性について」として翻訳。数学的論理のソースブック、1879 ～ 1931 年。ハーバード大学プレス: 228-51。