>>590
つづき

(4)高階直観主義論理とトポス.この間の深い関係についてはLawvereによってつとに指摘されていたが,
完全性定理の形式で,しかもトポスと高階論理の本質的な同等性をはっきりと示したのはFourman(1974[6],[7])が最初である.
ここで2つの流派が生じる.われわれが対象とする論理は直観主義論理であり,それが解釈され
るトポスは,

(5)無限論理とGr0thendieck topos. Lawvereの意図したGrothendieck toposの完全なin
ternalizationは不可能であった. Joyal等はLawvereの捨象したGrothendieck toposの集合論
的外延的性質すなわちcompleteな性質を圏論と論理の中核に据える一そのかわリベキを捨象し
た一研究の方向を示した. 2.9はMakkai-Reyes[31]によるその方面の成果の素描である.以下
Grothendieck toposをGr-トポスと略称する.

(6)層の圏. §3の例はいずれも集合論的に定義されるものであるが参考書をあげるにとどめる.
とくにV(H)は竹内外史氏が来日中(1979)にひろめた数々のスローガン, ‘アーベル群(環)の直観
主義化はアーベル群(環)の層である.一変数関数論の直観主義化は多変数関数論である' (5)等を具現
するモデルであり,実例研究のたえざる出発点である([43]) .

(7)PartＩからみたトポス.トポスと高階論理が同値な概念であるとするならばどちらを出発
点にとるかは諸個人の趣味の問題であり,トポスはけっきょく一つのモードにすぎないといえるか
も知れない.けれども論理そのものが新たに圏論的表象を得たという点に新しいパラダイムの特徴
があるのであって,たとえば人はいつでも論理学の研究をsyntaxを経ることなく直接にトポス上
の図式から始めることができる.もっとも今のところトポス自身は‘aは対象である'‘fは射である'
を無定義述語とする言語で基礎づけられねばならぬけれども.
原理的には伝統的な枠の中で証明されえた筈の諸定理,4.一2(1),§5のOsiusの結果等がまずトポ
スにおいて明らかにされた背後には適切で簡潔な表現へと志向するトポスパラダイムが作用してい
たといえよう。

つづく