計算形而上学入門

An Introduction to Computational Metaphysics

First published Sun Dec 13 00:03:45 2015 +0900 ; substantive revision Mon Apr 2 00:43:50 2018 +0900 ; Authored by nolze (submitted for Buho Magazine, Theoretical Science Group, 2015)

Tags : 哲学形而上学計算形而上学

　この記事は第66回駒場祭で頒布された東京大学理論科学グループ (TSG) の部報に掲載したものです。

　この記事はTSG Advent Calendar 2015の12日目です。7日目はTeXで簡単プログラミング♪ - ０番染色体でした。13日目はpCICについて - Sis puella magica!です。

[…] このことが成されたならば、何か論争が生じても、二人の哲学者の間で議論することに、二人の計算者 Computistas の間で議論すること以上の必要はなくなる。ただペンを手に取って計算台 abacus に向かって座り（望むなら、友も呼びだしておいて）こう言うのだ—「計算しよう」、と。

—ライプニッツ草稿 (Gerhardt ed. 1890)

本稿では Fitelson & Zalta の論文「『計算形而上学』への歩み Steps Toward a Computational Metaphysics」(2007) を紹介します。

著者の一人で取り組みの中心人物である哲学者のザルタ E. Zalta はスタンフォード哲学百科事典 (SEP) の創設者で、今も主席編集者を務めているので哲学や論理学に関心のある人なら一度は名前を目にしたことがあるかもしれません。「計算形而上学 Computational Metaphysics (以下CM)」のプロジェクトを簡潔に説明すると、彼が考案した抽象的対象論¹ Theory of Abstract Objects の枠組みでさまざまな形而上学的主張を公理化し (曰く「公理的形而上学」) 自動定理証明系に投げることで、主張の一貫性をチェックしたり帰結を見たりしようという研究の試みです。

Zaltaの抽象的対象論

対象論とは

「対象論」は、端的に言えば、存在するかどうかを問わずに「対象」を認める立場の理論です。今日「マイノング主義」と呼ばれる思潮の直接の源流は、名前の通り19世紀末の哲学者で心理学者としても知られるマイノング A. Meinong に遡ることができます。マイノングは、ブレンターノ F. Brentano の「志向性」の理論に影響を受けつつ、心的な次元から出発して独自の対象論 Gegenstandtheorie を確立しました。マイノング主義においては、よく挙げられる例として「黄金の山」や「丸い四角」が「存在しない対象」として認められることになります。彼の後を継いだのがマリー E. Mally で、彼はマイノングの対象論を精緻化するとともに、その論理学的な分析によっても成果を残しました。マイノング-マリーの対象論を特徴づける原理として、以下の二つがあります。

対象の「かくあること Sosein」は、その対象の「存在しないこと Nichtsein」に依存しない (独立性の原理)
対象の「存在すること Sein」か「存在しないこと」のどちらかが対象について成り立っているが、存在は対象に本質的には関与しない (無差別性の原理)

とはいえ、そのようなよくわからないものを何でも—「丸い四角」のような矛盾したものは特に—どんな形であれ認めたりするのは「素朴に」やばい感じもします。ラッセル B. Russell はマイノングに批判的な立場を取るようになった一人で、Russell (1905) における強力な確定記述の理論の確立はマイノング主義に対する反論として大きな影響力を持ち、以後マイノング主義は有名どころだけでも Quine (1948) で隠喩的に叩かれる、「対象論は […] 死に、埋葬され、復活することはないだろう」(Ryle 1973) と書かれるなどあまり評価されてこなかったようです。

しかしながら、こうした情勢にあって Parsons、Routley、Castañeda、Rapaport などなどの論者の尽力で徐々にマイノング主義の再評価と (分析哲学界隈で戦えるような) 論理学的な形式化が進みます。Zaltaの抽象的対象論もこの流れの中で (直接的には Parsons の影響で) 登場した理論のひとつです。他の理論に関しては、最近は日本でも Priest (2005) の邦訳が出たりしています。

もちろん、Zaltaの抽象的対象論も含め対象論が存在を説明する唯一の理論であるというわけではなく、内在的な問題 (特に種々のパラドックス) がいろいろと指摘されているほか、マイノング主義を前提せずにこのような「対象」を説明できるとする Lewis (1978) のような議論もあります。

Zaltaの抽象的対象論については、スタンフォード大学言語・情報研究センターの「形而上学研究室」のWebサイト²に情報が集約されています。書籍の Zalta (1983) が最も丁寧な文献ですが、形式的な内容についてはWebサイト内の Principia Metaphysica というドラフトに網羅的にまとまっています。

言語

対象変数と対象定数 : $x,y,z,…;a,b,c,…$
関係変数と関係定数³ : $P^n,Q^n,R^n,…;$ $n = 0$ のとき $p,q,r,…;$ $n = 1$ のとき $P,Q,R,…$
特別な1項関係 : $E!$ (読みは「具体的 concrete」)
原子論理式 :
- 例化 : $F^{n} x_{1}…x_{n}$
- エンコーディング : $xF$
複合論理式 : $(\lnot\varphi)…$
複合項 :
- 確定記述 : $\iota x \varphi$
- λ式 : $[\lambda x_1…x_n \varphi]$
通常 ordinary : $O! =_{df} [\lambda x \Diamond E!x]$
抽象的 abstract : $A! =_{df} [\lambda x \neg \Diamond E!x]$
同一性 : $x = y =_{df} x =_{E} y \lor (A!x \mathop \& A!y \mathop \& \Box \forall F (xF \equiv yF))$
関係の同一性 : $F = G =_{df} \Box \forall{x}(xF \equiv xG)$

0項関係は命題、1項関係は性質 property と呼ばれます。例化 exemplify とエンコード encode は区別される「叙述の様態」で、$Fx$は「xはF (という性質) を例化する」というおなじみの叙述であるのに対し $xF$ は「xはF (という性質) をエンコードする」と読みます。対象論的なのは後者であって、これは性質が対象を「決定する determinieren」というマリーの言い回しをZalta流に解釈したものです。後述の理論の公理から、抽象的対象だけが性質を「エンコードする」というあり方をします。よって例えば、「丸い四角」があるということは「丸さ」を$R$、「四角さ」を$S$として次のように書くことができます :

\[\exists{x} (A!x \mathop\& \forall{F} (xF \equiv F=R \lor F=S) )\]

論理

基本的には様相論理の体系 S5 な定領域の二階様相述語論理です。後で使うので、様相に関する公理だけ提示しておきます。

公理K : $\Box(\varphi \to \phi) \to (\Box\varphi \to \Box\phi)$
公理T : $\Box\varphi \to \varphi$
公理5 : $\Diamond\varphi \to \Box\Diamond\varphi$

これにエンコーディング・λ式・確定記述に関する公理が追加されます。

エンコーディングの論理 : $\Diamond x F \to \Box x F$
同一性の論理 : $\alpha = \beta \to [\phi(\alpha,\alpha) \equiv \phi(\alpha,\beta)]$
λ式の論理 : β簡約・η/α変換
確定記述の論理 : $\psi_z^{\iota x \varphi} \equiv \exists{x}(\varphi \mathop\& \forall{y}(\varphi_x^y \to y = x) \mathop\& \psi_z^x)$

理論の公理

通常対象の公理 : $O!x \to \Box \neg{\exists{F}(xF)}$
抽象的対象の公理 : $\exists{x} (A!x \mathop\& \forall{F} (xF \equiv \phi) )$ ($\phi$は自由変項を含まない式)

ハンズオン : イデアの計算理論

CMの取り組みの実例として、Fitelson & Zalta (2007) でも触れられている「プラトンのイデアの計算理論」⁴を取り上げます。この取り組みの直接の元ネタは、 Meinwald (1992) に即していわゆる「第三の人間」論を取り上げる Pelletier & Zalta (2000) であるものの、公理的形而上学としてのイデア論については Zalta (1983) に既にまとまっています。自動定理証明器に対する入力はCMのWebページで Fitelson & Zalta (2007) に載っていないものも含め公開されていますが、以下ではなるべく抽象的対象論に忠実な形になるよう若干異なった定式化の仕方をしている場合があるので参照する際は注意してください。

Prover9/Mace4のインストール

論文やWebページにならって、本稿でも自動定理証明器Prover9とモデル探索器 Mace4 を使うことにします。公式ページ⁵からLinux/Mac OS X向けのソースコードとWindows向けのバイナリがダウンロードできます。コマンドライン版 (LADR) と GUI版がありますが、以下ではコマンドライン版を前提します。

抽象的対象論の定式化

導出原理を基盤とするProver9で直接扱えるのは一階述語古典論理に限られるため、Object(x)やProperty(x)といった述語を導入することで抽象的対象論の二階述語論理を多ソートな many-sorted 一階述語論理に書き換えるのが基本的な方針になります。

様相に関しても relational translation というテク (Ohlbach 1993, Manzano 1996) でKripkeモデルをソートによって表わします⁶。

公理T : $\Box\varphi \to \varphi$

% AXIOM T, FROM OBJECT THEORY
Point(W).

$Point(w)$ は、直感的には「現実世界Wから世界wへ到達可能である」と読むことができます⁷。残るはλ式の処理で、今回は使わないので割愛しますが、論文にある通りこれも別のテクで表現できます。

同一性の定義は具体的対象の同一性と抽象的対象の同一性の選言ですが、後で必要になる抽象的対象の同一性だけ定式化します。

同一性 : $x = y =_{df} x =_{E} y \lor (A!x \mathop \& A!y \mathop \& \Box \forall F (xF \equiv yF))$

% ABSTRACT IDENTITY, FROM OBJECT THEORY
all x all y ((Object(x) & Object(y) & Ex1(A,x,W) & Ex1(A,y,W)) ->
  (x=y <-> (all F all w ((Property(F) & Point(w)) -> (MEnc(x,F,w) <-> MEnc(y,F,w)))))).

エンコーディングの論理 : $\Diamond x F \to \Box x F$

% LOGIC OF ENCODING, FROM OBJECT THEORY
all x all F ((Object(x) & Property(F)) ->
  ((exists w (Point(w) & MEnc(x,F,w))) -> (all w (Point(w) -> MEnc(x,F,w))))).

また論文やWebページの略記に合わせてEnc(x,F)をMEnc(x,F,W)として定義しておきます。

% ENCODING ABBR., FROM OBJECT THEORY
all x all F ((Object(x) & Property(F)) -> (Enc(x,F) <-> MEnc(x,F,W))).

イデア論の定式化

原理

Pelletier & Zalta (2000) では、抽象的対象論における「$x$は抽象的である」を「$x$はイデア的である」に読み替えて⁸、以下の原理を設定しています。

イデア的対象の原理 :
- 内包原理 : $\exists{x} (A!x \mathop\& \forall{F} (xF \equiv \phi) )$ ($\phi$は自由変項を含まない式)
- 同一性原理 : $A!x \mathop\& A!y \mathop\& \forall{F} (xF \equiv yF) \to x = y$

内包原理は抽象的対象の公理と同じです。次の定義から内包原理の帰結に関する具体的な例が定式化できます。

(必然的) 帰結 entailment : $G \Rightarrow F =_{df} \Box \forall x (Gx \to Fx)$

% ENTAILMENT, FROM THEORY OF FORMS
all F all G ((Property(F) & Property(G)) ->
  (Implies(F,G) <-> (all x all w ((Object(x) & Point(w)) -> (Ex1(F,x,w) -> Ex1(G,x,w)))))).

帰結による内包 : $\forall G \exists x (A!x \mathop\& xF \equiv G \Rightarrow F)$

% ENTAILMENT INSTANCE OF COMPR. PR., FROM THEORY OF FORMS
all G (Property(G) ->
  (exists x (Object(x) & Ex1(A,x,W)
    & (all F (Property(F) -> (Enc(x,F) <-> Implies(G,F))))))).

同一性原理は抽象的対象論における同一性の定義から導出できます。

formulas(assumptions).
  % AXIOM T, FROM OBJECT THEORY
  Point(W).
  % ABSTRACT IDENTITY, FROM OBJECT THEORY
  all x all y ((Object(x) & Object(y) & Ex1(A,x,W) & Ex1(A,y,W)) ->
    (x = y <-> (all F all w ((Property(F) & Point(w)) -> (MEnc(x,F,w) <-> MEnc(y,F,w)))))).
  % LOGIC OF ENCODING, FROM OBJECT THEORY
  all x all F ((Object(x) & Property(F)) ->
    ((exists w (Point(w) & MEnc(x,F,w))) -> (all w (Point(w) -> MEnc(x,F,w))))).
  % ENCODING ABBR., FROM OBJECT THEORY
  all x all F ((Object(x) & Property(F)) ->
    (Enc(x,F) <-> all w (Point(w) -> MEnc(x,F,w)))).
end_of_list.

formulas(goals).
  % IDENTITY, FROM THEORY OF FORMS
  all x all y ((Object(x) & Object(y) & Ex1(A,x,W) & Ex1(A,y,W)) ->
    ((all F (Property(F) -> (Enc(x,F) <-> Enc(y,F)))) ->  x = y)).
end_of_list.

イデア

次にイデアまわりを定義します。

「xはGのイデアである」 : $Form(x,G) =_{df} A!x \mathop \& \forall F (xF \equiv F \Rightarrow G)$

% A FORM, FROM THEORY OF FORMS
all x all G (IsAFormOf(x,G) -> Object(x) & Property(G)).
all x all G ((Object(x) & Property(G)) ->
  (IsAFormOf(x,G) <-> (Ex1(A,x,W) & (all F (Property(F) -> (Enc(x,F) <-> Implies(G,F))))))).

Gのイデア : $\Phi_F =_{df} \iota x (Form(x,G))$

先述の理由からProver9では確定記述を直接表現できないので、次のように変形します。

Gのイデア : $\forall x \forall G (\Phi_F \equiv A!x \mathop \& \forall y (Form(y,G) \to x = y))$

% THE FORM, FROM THEORY OF FORMS
all x all G (IsTheFormOf(x,G) -> Object(x) & Property(G)).
all x all G ((Object(x) & Property(G)) ->
  (IsTheFormOf(x,G) <-> (IsAFormOf(x,G)  & (all y (IsAFormOf(y,G) -> y=x))))). 

いわゆるイデアの「分有」は「第三の人間」の議論を取り上げる上での中心テーマであり、 Meinwald (1991) で提出された「他のものとの関係において pros ta alla (PTA) 」と「自分自身との関係において pros heauto (PH) 」の区別が取り入れられています。Pelletier & Zalta (2000) の説明を補って簡単に述べると、ある述語 (関係) $F$ に関して、前者は「ある性質F」についてそれを持っているという普通の個物における分有を、後者は性質Fをその本質として持っているというイデアにおける分有を意味します。ここではこの両者をそれぞれ$Fx$と$xF$に関連させて以下のように定義します。

PTA型の分有 : $Participates_{PTA}(y,x) \equiv \exists{F}(x = \Phi_F \mathop\& Fy)$

% PTA-PARTICIPATION, FROM THEORY OF FORMS
all y all x all w ((Object(x) & Object(y) & Point(w)) ->
  (PartPTA(y,x,w) <-> (exists F (Property(F) & IsTheFormOf(x,F) & Ex1(F,y,w))))).

PH型の分有 : $Participates_{PTA}(y,x) \equiv \exists{F}(x = \Phi_F \mathop\& yF)$

% PH-PARTICIPATION, FROM THEORY OF FORMS
all y all x ((Object(x) & Object(y)) ->
  (PartPH(y,x) <-> (exists F (Property(F) & IsTheFormOf(x,F) & Enc(y,F))))).

イデア論の定理

定理1 (イデアの存在と唯一性) : $\forall G \exists! x Form(x,G)$

左右方向の含意でふたつの定理に分けて証明します。公理はすべて前提に入れても差し支えないのですが、見やすさと紙幅の都合からCMのWebページにある入力を参考に証明が成り立つ範囲で適当に前提を省いています。

定理1a (イデアの存在) : $\forall G \exists x Form(x,G)$

formulas(assumptions).
  % ENTAILMENT INSTANCE OF COMPR. PR., FROM THEORY OF FORMS
  all G (Property(G) ->
    (exists x (Object(x) & Ex1(A,x,W)
      & (all F (Property(F) -> (Enc(x,F) <-> Implies(G,F))))))).
  % A FORM, FROM THEORY OF FORMS
  all x all G (IsAFormOf(x,G) -> Object(x) & Property(G)).
  all x all G ((Object(x) & Property(G)) ->
    (IsAFormOf(x,G) <-> (Ex1(A,x,W) & (all F (Property(F) -> (Enc(x,F) <-> Implies(G,F))))))).
end_of_list.

formulas(goals).
  % THEOREM 1A
  all G (Property(G) -> (exists x (Object(x) & IsAFormOf(x,G)))).
end_of_list.

証明器に投げてみましょう。

$./LADR-2009-11A/bin/prover9 < theorem1a.in
...
============================== PROOF =================================

% Proof 1 at 0.02 (+ 0.01) seconds.
% Length of proof is 33.
% Level of proof is 8.
% Maximum clause weight is 25.000.
% Given clauses 25.

1 (all G (Property(G) -> (exists x (Object(x) & Ex1(A,x,W) & 
  (all F (Property(F) -> (Enc(x,F) <-> Implies(G,F)))))))) # label(non_clause).  [assumption].
2
...
105 Implies(c1,f2(f1(c1),c1)). 
[resolve(103,a,71,d),unit_del(a,34),unit_del(b,58)].
109 $F.  [ur(75,a,34,a,b,58,a,d,103,a),unit_del(a,105)].

============================== end of proof ==========================
...

THEOREM PROVED
...

証明が見つかりました。同様にして以下の定理も証明できます。

定理1b (イデアの唯一性) : $\forall G \forall x \forall y (Form(x,G) \& Form (y,G)) \to x = y)$

formulas(assumptions).
  % A FORM, FROM THEORY OF FORMS
  all x all G (IsAFormOf(x,G) -> Object(x) & Property(G)).
  all x all G ((Object(x) & Property(G)) ->
    (IsAFormOf(x,G) <-> (Ex1(A,x,W) & (all F (Property(F) -> (Enc(x,F) <-> Implies(G,F))))))).
  % IDENTITY, FROM THEORY OF FORMS
  all x all y ((Object(x) & Object(y) & Ex1(A,x,W) & Ex1(A,y,W)) ->
    ((all F (Property(F) -> (Enc(x,F) <-> Enc(y,F)))) ->  x=y)).
end_of_list.

formulas(goals).
  % THEOREM 1B
  all G (Property(G) -> (all x all y ((IsAFormOf(x,G) & IsAFormOf(y,G)) -> x=y))).
end_of_list.

以上から定理1が証明できました。この「イデアの計算理論」からは、どのような性質Gについてもイデアがただひとつ存在するという基本的なテーゼが問題なく導けます。

定理3 (PTA型の分有) : $Fx \equiv Participates_{PTA}(x,\Phi_F)$

PTA型の分有は例化を使って定義されましたが、より直裁的に例化との同値関係も満たします。

formulas(assumptions).
  % AXIOM T, FROM OBJECT THEORY
  Point(W).
  % ENTAILMENT, FROM THEORY OF FORMS
  all F all G ((Property(F) & Property(G)) ->
    (Implies(F,G) <-> (all x all w ((Object(x) & Point(w)) -> (Ex1(F,x,w) -> Ex1(G,x,w)))))).
  % A FORM, FROM THEORY OF FORMS
  all x all G (IsAFormOf(x,G) -> Object(x) & Property(G)).
  all x all G ((Object(x) & Property(G)) ->
    (IsAFormOf(x,G) <-> (Ex1(A,x,W) & (all F (Property(F) -> (Enc(x,F) <-> Implies(G,F))))))).
  % THE FORM, FROM THEORY OF FORMS
  all x all G (IsTheFormOf(x,G) -> Object(x) & Property(G)).
  all x all G ((Object(x) & Property(G)) ->
    (IsTheFormOf(x,G) <-> (IsAFormOf(x,G)  & (all y (IsAFormOf(y,G) -> y = x))))).
  % PTA-PARTICIPATION, FROM THEORY OF FORMS
  all y all x all w ((Object(x) & Object(y) & Point(w)) ->
    (PartPTA(y,x,w) <-> (exists F (Property(F) & IsTheFormOf(x,F) & Ex1(F,y,w))))).
end_of_list.

formulas(goals).
  % THEOREM 3
  all x all y all G ((Object(x) & Object(y) & Property(G)) ->
    (IsTheFormOf(x,G) -> (Ex1(G,y,W) <-> PartPTA(y,x,W)))).
end_of_list.

「定理」4 (PH型の分有) : $xF \equiv Participates_{PH}(x,\Phi_F)$

PH型はどうでしょうか。この定理については、Pelletier & Zalta (2000) では左から右方向の証明が与えられ、右から左方向は「読者への課題」となっています。怠惰な読者の代わりにProver9にやってもらいましょう。

formulas(assumptions).
  % TRIVIAL PREMISES
  Property(A).
  all x (Point(x) -> -Property(x)).
  % AXIOM T, FROM OBJECT THEORY
  Point(W).
  % ENTAILMENT, FROM THEORY OF FORMS
  all F all G ((Property(F) & Property(G)) ->
    (Implies(F,G) <-> (all x all w ((Object(x) & Point(w)) -> (Ex1(F,x,w) -> Ex1(G,x,w)))))).
  % A FORM, FROM THEORY OF FORMS
  all x all G (IsAFormOf(x,G) -> Object(x) & Property(G)).
  all x all G ((Object(x) & Property(G)) ->
    (IsAFormOf(x,G) <-> (Ex1(A,x,W) & (all F (Property(F) -> (Enc(x,F) <-> Implies(G,F))))))).
  % THE FORM, FROM THEORY OF FORMS
  all x all G (IsTheFormOf(x,G) -> Object(x) & Property(G)).
  all x all G ((Object(x) & Property(G)) ->
    (IsTheFormOf(x,G) <-> (IsAFormOf(x,G)  & (all y (IsAFormOf(y,G) -> y = x))))).
  % PH-PARTICIPATION, FROM THEORY OF FORMS
  all y all x ((Object(x) & Object(y)) ->
    (PartPH(y,x) <-> (exists F (Property(F) & IsTheFormOf(x,F) & Enc(y,F))))).
end_of_list.

formulas(goals).
  % THEOREM 4
  all x all y all G ((Object(x) & Object(y) & Property(G)) ->
    (IsTheFormOf(x,G) -> (PartPH(y,x) -> Enc(y,G)))).
end_of_list.

なぜか証明が見つからなかったと思います。驚くべきことに(？)実は Pelletier & Zalta (2000) が間違っていたのでした。同じ入力を Mace4 に投げると反例モデルを見つけてくれるので、それを手がかりに具体的な反例を構成することができます。

Fitelson & Zalta (2007) では左から右方向の証明をProver9で確認して「定理」4を次のように弱めています。証明を試してみてください。

定理4* : $xF \to Participates_{PH}(x,\Phi_F)$

おわりに

CMのWebページには他にも、可能世界の定式化や、アンセルムスやライプニッツの形而上学に関する取り組みが掲載されています。自動定理証明器に対する入力には、本稿では参考文献での参照のしやすさと人間による読みやすさを重視してProver9固有のシンタックスを採用しましたが、汎用のものとしてはTPTPシンタックスが普及しています。新しく出たより高速な証明器を利用することができるなどのメリットがあるので、CMの最近のプロジェクトはこのシンタックスを採用しているようです。

なぜより表現力のあるCoqなどの定理証明支援系ではなく自動定理証明系なのか？という点に関しては、冒頭のライプニッツからの引用に表れているような普遍学 scientia generalis の理念をZaltaは意識したようです。夢があっていいですね。

「計算形而上学」は、Zaltaの抽象的対象論で理論的には尽きていて「コンピュテーショナル」な部分が本質的な役割を担っているわけではないので、今日盛んに研究されている哲学と情報・計算の間の本質的な関係に迫る感じのやつを期待した人は若干がっかりしたかもしれませんが、期待されているポジションとしてはむしろ生物学に対するバイオインフォマティクスのそれに近いのかな？と思います。コンピュテーションが本質的でないというのは利点でもあって、なーにがエンコードじゃと思うならZaltaの抽象的対象論以外の理論を基盤にすることもできます。情報と哲学という組み合わせは一筋縄ではいかないところはありますが、踏み込んだ議論から一歩引いてもなお新しい発見のある領域なのではないかと思います。

[FOOTNOTES]

参考文献

Fitelson, B., & Zalta, E. N. (2007). Steps Toward a Computational Metaphysics. Journal of Philosophical Logic, 36(2), 227-247. URL=<https://mally.stanford.edu/Papers/computation.pdf>.
Leibniz, G. W. (1890). Die philosophischen Schriften von Gottfried Wilhelm Leibniz, hrsg. v. Carl Immanuel Gerhardt, Hildesheim, Olms, 7.
Lewis, D. (1978). Truth in fiction. American Philosophical Quarterly, 37-46.
Manzano, M. (1996). Extensions of first order logic (Vol. 19). Cambridge University Press.
Meinwald, C. C. (1991). Plato’s Parmenides.
Meinwald, C. (1992). Good-bye to the Third Man.
Ohlbach, H. J. (1993). Translation methods for non-classical logics: an overview. Logic Journal of IGPL, 1(1), 69-89.
Oppenheimer, P. E., & Zalta, E. N. (2010). Relations versus functions at the foundations of logic: Type-theoretic considerations. Journal of Logic and Computation, exq017.
Pelletier, F. J., & Zalta, E. N. (2000). How to say goodbye to the third man. Noûs, 34(2), 165-202.
Priest, G. (2005). Towards non-being: The logic and metaphysics of intentionality.
Quine, W. V. (1948). On what there is. The Review of Metaphysics, 2(1), 21-38.
Russell, B. (1905). On denoting. Mind, 479-493.
Ryle, G. (1973). Intentionality-theory and the nature of thinking. Revue internationale de philosophie, 255-265.
Zalta, E. (1983). Abstract objects: An introduction to axiomatic metaphysics (No. 160). Springer Science & Business Media.

単に対象論 Object Theory, Theory of Objects とも。他の「対象論」とのバランスから本稿では Zalta (1983) を背景に「抽象的対象論」で統一します。 ↩
https://mally.stanford.edu/ ↩
いわゆるn項述語ですが、述語に関しては Oppenheimer & Zalta (2010) で展開されているような微妙な背景がありそうなのでそのまま関係と訳します。 ↩
https://mally.stanford.edu/cm/forms/ ↩
http://www.cs.unm.edu/~mccune/mace4/ ↩
自動定理証明界隈ではこの辺の技術は発達しているようで、例えば同じく自動定理証明系である SPASS は様相を内部的に変換してくれるらしいです。 ↩
抽象的対象論では、可能世界もひとつの対象として（メタ言語に対する）対象言語で定義されるので、$Point$ というソートの導入はあくまで公理の形式的な変換として理解するのが正確なところです。 ↩
イデアの実在性を保持するため、Zalta (1983) はプラトニックな存在 Platonic Being $\overline{E}! =_{df} A!$ (！)を導入していますが、Pelletier & Zalta (2000) では実在性に直接言及しないで、読み替えによって通常の存在とプラトニックな存在の「差異を捉える」という戦略から出発しています。 ↩