述語関数論理

数理論理学において、述語関数論理（PFL）は、一階述語論理（述語論理とも呼ばれる）を純粋に代数的な手段、すなわち量化変数なしで表現する方法の1つです。PFLは、項に作用して項を生成する述語関数（または述語修飾子）^[1]と呼ばれる少数の代数的装置を使用します。PFLは主に、論理学者で哲学者の ウィラード・クワインの発明です。

このセクションとこのエントリの大部分の出典は、Quine (1976) です。Quine は、ブール代数が命題論理を代数化するのと類似した方法で、一階論理を代数化する方法として PFL を提案しました。彼は、PFL が、同一性を持つ一階論理とまったく同じ表現力を持つように設計しました。したがって、 PFLのメタ数学は、解釈された述語文字のない一階論理のメタ数学とまったく同じです。つまり、どちらの論理も健全で、完全で、決定不可能です。Quine が生涯の最後の 30 年間に発表した論理と数学に関するほとんどの研究は、何らかの形で PFL に触れています。^[要出典]

クワインは、哲学と数理論理学で初めて「関手」を使用した友人ルドルフ・カルナップの著作から「関手」を引用し、次のように定義しました。

「関数子という語は、意味は文法的だが、その生息環境は論理的である...与えられた文法種類の 1 つ以上の表現に付加されて、与えられた文法種類の表現を生成する記号である。」(Quine 1982: 129)

PFL 以外の一階論理を代数化する方法としては、次のものがあります。

• アルフレッド・タルスキと彼のアメリカ人学生による円筒代数。バーネイズ (1959) で提案された簡略化された円筒代数により、クワインは「述語関数」という語句を初めて使用した論文を執筆した。
• Paul Halmosの多項式代数。この代数は、その経済的なプリミティブと公理のおかげで、PFL に最も似ています。
• 関係代数は、3つ以上の量指定子のスコープ内に原子式を持たない式からなる一階述語論理のフラグメントを代数化する。しかし、そのフラグメントはペアノ算術と公理的集合論ZFCには十分である。したがって、関係代数は、PFLとは異なり、不完全である。1920年頃からの関係代数に関する研究のほとんどは、タルスキと彼のアメリカ人学生によるものである。関係代数の威力は、PFLに関連する3つの重要な論文、すなわちベーコン（1985）、クーン（1983）、クワイン（1976）の後に出版されたモノグラフ、タルスキとギヴァント（1987）まで明らかではなかった。
• 組み合わせ論理は、コンビネータ、つまりドメインが別のコンビネータまたは関数であり、値域がさらに別のコンビネータである高階関数に基づいて構築されます。したがって、組み合わせ論理は集合論の表現力を持つことによって一階論理を超えており、これにより組み合わせ論理はパラドックスに対して脆弱になります。一方、述語関数子は、述語（項とも呼ばれる）を述語に単純にマッピングします。

PFL はおそらくこれらの形式主義の中で最も単純ですが、最も記述が少ない形式主義でもあります。

クワインは生涯にわたって組合せ論理に興味を持っていた。これは、ロシアの論理学者モーゼス・シェーンフィンケルが組合せ論理を創始した論文の翻訳をヴァン・ヘイエノールト (1967) で紹介したことからも明らかである。クワインが PFL に本格的に取り組み始めた 1959 年当時、組合せ論理は次のような理由から失敗作であると一般に考えられていた。

• 1960 年代後半にダナ・スコットが組合せ論理のモデル理論について書き始めるまで、その論理に取り組んでいたのはハスケル・カリー、彼の学生、そしてベルギーのロバート・フェイズだけだった。
• 組合せ論理の満足のいく公理的定式化はゆっくりと進みました。1930 年代には、組合せ論理のいくつかの定式化に矛盾があることが判明しました。カリーは、組合せ論理特有のカリーのパラドックスも発見しました。
• ラムダ計算は、組合せ論理と同じ表現力を持ち、優れた形式論であると考えられていました。

このセクションで説明されているPFL構文、プリミティブ、公理は、主にSteven Kuhn (1983) のものです。関数のセマンティクスは Quine (1982) のものです。このエントリの残りの部分には、Bacon (1985) の用語がいくつか組み込まれています。

原子項は、 IとS を除く大文字のラテン文字に、次数と呼ばれる上付き数字、または連結された小文字の変数（総称して引数リスト）が続きます。項の次数は、述語文字に続く変数の数と同じ情報を伝えます。次数 0 の原子項は、ブール変数または真理値を表します。Iの次数は必ず 2 なので示されません。

「組み合わせ」（この言葉はクワインの）述語関数はすべてモナド的で PFL に特有であり、Inv、inv、∃、+、およびpです。項はアトミック項、または次の再帰規則によって構築されます。 τ が項である場合、Inv τ、inv τ、∃ τ、+ τ、およびp τ は項です。上付き文字n（nは 1より大きい自然数）の付いた関数は、その関数のn回の連続した適用（反復）を表します。

式は項であるか、または再帰規則によって定義されます。α と β が式である場合、αβ と ~(α) も同様に式です。したがって、「~」は別のモナド関数であり、連結は唯一の二項述語関数です。Quine はこれらの関数を「alethic」と呼びました。「~」の自然な解釈は否定です。連結の自然な解釈は、否定と組み合わせると機能的に完全な接続子セットを形成する接続子です。Quine が好んだ機能的に完全なセットは、連言と否定でした。したがって、連結された項は結合されていると見なされます。表記+は Bacon (1985) の表記であり、他の表記はすべて Quine (1976; 1982) の表記です。PFL の alethic 部分は、Quine (1982) のブール項スキーマと同一です。

よく知られているように、2 つの alethic 関数は、次の構文と意味を持つ単一の 2 項関数に置き換えることができます。α と β が式である場合、(αβ) は意味が「(α および/または β) ではない」という式です ( NANDとNOR を参照)。

クワインは PFL の公理化も証明手順も示していない。クワイン (1983) で提案された 2 つの PFL 公理化のうちの 1 つである次の公理化は簡潔で記述しやすいが、自由変数を多用しているため PFL の精神を十分に反映していない。クーンは自由変数を使わない別の公理化を提示しているが、これは記述が難しく、定義された関数を多用している。クーンは PFL 公理化の両方が健全かつ完全であることを証明した。

このセクションは、プリミティブ述語関数といくつかの定義済み関数を中心に構築されています。 論理的述語関数は、プリミティブが否定と ∧ または ∨ のいずれかである文論理の公理の任意のセットによって公理化できます。 同様に、文論理のすべてのトートロジーは公理として扱うことができます。

クワイン（1982）の各述語関数の意味論は、抽象化（集合構築記法）の観点で以下に述べられており、その後にクーン（1983）の関連する公理、またはクワイン（1976）の定義が続く。この記法は、原子式を満たすn組の集合を表す。${\displaystyle \{x_{1}\cdots x_{n}:Fx_{1}\cdots x_{n}\}}$${\displaystyle Fx_{1}\cdots x_{n}.}$

• アイデンティティIは次のように定義されます。

${\displaystyle IFx_{1}x_{2}\cdots x_{n}\leftrightarrow (Fx_{1}x_{1}\cdots x_{n}\leftrightarrow Fx_{2}x_{2}\cdots x_{n}){\text{.}}}$

恒等式は反射的( Ixx )、対称的( Ixy → Iyx )、推移的( ( Ixy ∧ Iyz ) → Ixz ) であり、置換特性に従います。

${\displaystyle (Fx_{1}\cdots x_{n}\land Ix_{1}y)\rightarrow Fyx_{2}\cdots x_{n}.}$

• パディング( + ) は、任意の引数リストの左側に変数を追加します。

${\displaystyle \ +F^{n}\ {\overset {\underset {\mathrm {def} }{}}{=}}\ \{x_{0}x_{1}\cdots x_{n}:F^{n}x_{1}\cdots x_{n}\}.}$

${\displaystyle +Fx_{1}\cdots x_{n}\leftrightarrow Fx_{2}\cdots x_{n}.}$

• 切り取り、∃、は引数リストの一番左の変数を消去します。

${\displaystyle \exists F^{n}\ {\overset {\underset {\mathrm {def} }{}}{=}}\ \{x_{2}\cdots x_{n}:\exists x_{1}F^{n}x_{1}\cdots x_{n}\}.}$

${\displaystyle Fx_{1}\cdots x_{n}\rightarrow \exists Fx_{2}\cdots x_{n}.}$

クロッピングにより、 2 つの便利な定義済み関数が有効になります。

• 反射、S：

${\displaystyle SF^{n}\ {\overset {\underset {\mathrm {def} }{}}{=}}\ \{x_{2}\cdots x_{n}:F^{n}x_{2}x_{2}\cdots x_{n}\}.}$

${\displaystyle SF^{n}\leftrightarrow \exists IF^{n}.}$

S は、反射性の概念を 2 より大きい任意の有限次数のすべての項に一般化します。注意: S を、組み合わせ論理のプリミティブ コンビネータ Sと混同しないでください。

• デカルト積、;${\displaystyle \times }$

${\displaystyle F^{m}\times G^{n}\leftrightarrow F^{m}\exists ^{m}G^{n}.}$

ここでのみ、クワインは中置記法を採用しました。これは、デカルト積に対する中置記法が数学で非常によく確立されているためです。デカルト積により、連言を次のように言い換えることができます。

${\displaystyle F^{m}x_{1}\cdots x_{m}G^{n}x_{1}\cdots x_{n}\leftrightarrow (F^{m}\times G^{n})x_{1}\cdots x_{m}x_{1}\cdots x_{n}.}$

連結された引数リストを並べ替えて、重複する変数のペアを左端にシフトし、S を呼び出して重複を排除します。これを必要な回数繰り返すと、長さ max( m , n )の引数リストが生成されます。

次の 3 つの関数により、引数リストを自由に並べ替えることができます。

• 主要な反転Inv は、引数リスト内の変数を右に回転し、最後の変数が最初の変数になるようにします。

${\displaystyle \operatorname {Inv} F^{n}\ {\overset {\underset {\mathrm {def} }{}}{=}}\ \{x_{1}\cdots x_{n}:F^{n}x_{n}x_{1}\cdots x_{n-1}\}.}$

${\displaystyle \operatorname {Inv} Fx_{1}\cdots x_{n}\leftrightarrow Fx_{n}x_{1}\cdots x_{n-1}.}$

• マイナー反転inv は、引数リストの最初の 2 つの変数を交換します。

${\displaystyle \operatorname {inv} F^{n}\ {\overset {\underset {\mathrm {def} }{}}{=}}\ \{x_{1}\cdots x_{n}:F^{n}x_{2}x_{1}\cdots x_{n}\}.}$

${\displaystyle \operatorname {inv} Fx_{1}\cdots x_{n}\leftrightarrow Fx_{2}x_{1}\cdots x_{n}.}$

• 順列pは、引数リスト内の 2 番目から最後の変数を左に回転し、2 番目の変数が最後になるようにします。

${\displaystyle \ pF^{n}\ {\overset {\underset {\mathrm {def} }{}}{=}}\ \{x_{1}\cdots x_{n}:F^{n}x_{1}x_{3}\cdots x_{n}x_{2}\}.}$

${\displaystyle pFx_{1}\cdots x_{n}\leftrightarrow \operatorname {Inv} \operatorname {inv} Fx_{1}x_{3}\cdots x_{n}x_{2}.}$

n 個の変数からなる引数リストが与えられた場合、p は暗黙的に最後のn −1 個の変数を自転車のチェーンのように扱い、各変数がチェーン内のリンクを構成します。pを 1 回適用すると、チェーンは 1 つのリンクだけ進みます。pをF ⁿにk回連続して適用すると、k +1 個の変数がF内の 2 番目の引数の位置に移動します。

n =2の場合、 Invとinv は単にx ₁とx ₂を入れ替えるだけです。n =1 の場合、効果はありません。 したがって、n < 3 の場合、 p は効果がありません。

Kuhn (1983) は、 Major inversionとMinor inversion をプリミティブとして採用しています。Kuhn の表記p はinvに対応します。Kuhn にはPermutationとの類似点がないため、それに対する公理はありません。Quine (1976) に従ってp をプリミティブとして採用すると、Invとinv は、 +、∃、および反復されたpの非自明な組み合わせとして定義できます。

次の表は、関数が引数の次数にどのように影響するかをまとめたものです。

述語文字のすべてのインスタンスは、有効性に影響を与えることなく、同じ程度の別の述語文字に置き換えることができます。ルールは次のとおりです。

• モーダスポネンス;
• αとβ を、が出現しないPFL 式とします。 がPFL 定理である場合、 も同様に PFL 定理です。${\displaystyle x_{1}}$${\displaystyle (\alpha \land Fx_{1}...x_{n})\rightarrow \beta }$${\displaystyle (\alpha \land \exists Fx_{2}...x_{n})\rightarrow \beta }$

Quine (1976) は、PFL を公理化する代わりに、候補公理として次の推測を提案しました。

${\displaystyle \exists I}$

pをn −1回連続して繰り返すと、元の状態に戻ります。

${\displaystyle F^{n}\leftrightarrow p^{n-1}F^{n}}$

+と∃ は互いに打ち消し合う:

${\displaystyle {\begin{cases}F^{n}\rightarrow +\exists F^{n}\\F^{n}\leftrightarrow \exists +F^{n}\end{cases}}}$

否定は+、∃、pに分配されます。

${\displaystyle {\begin{cases}+\lnot F^{n}\leftrightarrow \lnot +F^{n}\\\lnot \exists F^{n}\rightarrow \exists \lnot F^{n}\\p\lnot F^{n}\leftrightarrow \lnot pF^{n}\end{cases}}}$

+とp は論理積で分配します。

${\displaystyle {\begin{cases}+(F^{n}G^{m})\leftrightarrow (+F^{n}+G^{m})\\p(F^{n}G^{m})\leftrightarrow (pF^{n}pG^{m})\end{cases}}}$

アイデンティティには興味深い意味合いがあります。

${\displaystyle IF^{n}\rightarrow p^{n-2}\exists p+F^{n}}$

クワインはまた、 αが PFL 定理であるならば、pα、+α、およびも PFL 定理であるという規則を推測しました。 ${\displaystyle \lnot \exists \lnot \alpha }$

Bacon (1985) は、条件、否定、同一性、パディング、およびメジャー反転とマイナー反転をプリミティブとして、クロッピングを定義どおりにとらえています。上記とは多少異なる用語と表記法を使用して、Bacon (1985) は PFL の 2 つの定式化を提示しています。

• フレデリック・フィッチ風の自然演繹定式。ベーコンは、この定式が健全かつ完全であることを詳細に証明しています。
• ベーコンが主張しているが証明していない公理的定式化。前述の公理と同等。これらの公理のいくつかは、ベーコンの表記法で言い直されたクワインの予想に過ぎません。

ベーコンはまた:

• PFL と Sommers (1982) の用語論理との関係について説明し、Lockwood が Sommers の付録で提案した構文を使用して PFL を書き直すと、PFL が「読みやすく、使いやすく、教えるのが簡単」になるはずだと主張します。
• Invとinvの群論的構造について触れます。
• 文論理、モナド述語論理、様相論理 S5 、および (非) 順列関係のブール論理はすべて PFL の断片であると述べています。

次のアルゴリズムはQuine (1976: 300–2) から引用したものです。一階述語論理の閉じた式が与えられた場合、まず次の操作を行います。

• 各述語文字に数字の下付き文字を付けて、その度合いを示します。
• すべての全称量指定子を存在量指定子と否定に変換します。
• x = y形式のすべての原子式をIxyとして書き直します。

ここで、前の結果に次のアルゴリズムを適用します。

PFLから一階述語論理への逆変換については、Quine（1976：302–4）で議論されています。

数学の標準的な基礎は公理的集合論であり、背景論理は恒等式を持つ一階述語論理で構成され、議論対象領域は完全に集合で構成される。集合のメンバーシップとして解釈される、次数2の述語文字が1つある。標準的な公理的集合論ZFCのPFL翻訳は難しくなく、ZFC公理は6つ以上の量化変数を必要としない。^[2]

• 代数論理

• ベーコン、ジョン、1985、「述語関数論理の完全性」、Journal of Symbolic Logic 50 : 903–26。
• Paul Bernays、1959 年、「Uber eine naturliche Erweiterung des Relationenkalkuls」、Heyting, A. 編、『数学における構成性』。北オランダ: 1–14。
• Kuhn, Steven T.、1983、「述語関数論理の公理化」、Notre Dame Journal of Formal Logic 24 : 233–41。
• ウィラード・クワイン、1976年、「代数論理と述語関数」、Ways of Paradox and Other Essays、改訂増補版。ハーバード大学出版局、283-307ページ。
• ウィラード・クワイン、1982年。『論理の方法』第4版。ハーバード大学出版局。第45章。
• ソマーズ、フレッド、1982年。『自然言語の論理』オックスフォード大学出版局。
• アルフレッド・タルスキ、スティーブン・ギヴァント（1987年）「変数のない集合論の形式化」AMS。
• Jean Van Heijenoort、1967年。『フレーゲからゲーデルまで：数学論理学の原典』ハーバード大学出版局。

• 述語関数論理入門 (ワンクリックダウンロード、PS ファイル)、著者: Mats Dahllöf (ウプサラ大学言語学部)