単純階型理論

ウィキペディア小見出し辞書

単純階型理論（Simple Theory of Types）

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/09/16 08:53 UTC 版)

「型理論」の記事における「単純階型理論（Simple Theory of Types）」の解説

ここでは、Mendelson (1997, 289-293）の体系 ST を解説する。量化の議論領域は型の階層に分けられ、個体要素（individuals）には型が割り当てられる。基盤となる論理は一階述語論理であり、量化変数の範囲は型によって限定される。ST は『数学原理』の型理論に比べて単純であり、任意の関係の議論領域は全て同じ型でなければならない。 階層中、最も低い型では、個体要素にはメンバーはなく、それらは2番目に低い型のメンバーとなる。最下層の型の個体要素は、ある集合論の原要素（Ur-elements）に対応する。それぞれの型にはより高位の型があり、ペアノの公理の後者関数（successor function）の記法にも似ている。ST では最高位の型があるかどうかは規定していない。超限数個の型があってもなんら不都合は生じない。このようにペアノの公理と似た性質であるため、各型に自然数を割り当てることが容易で、最下層の型に 0 を割り当てる。ただし、型理論そのものは自然数の定義を前提とはしていない。 ST に固有な記号として、プライム付きの変数と接中辞 ∈ がある。論理式において、プライムのない変数は全て同じ型に属し、プライム付き変数（x' )はその1つ上の型に属する。ST の原子論理式は、x=y （恒等式）か y∈x ’ という形式である。接中辞記号 ∈ は、集合の所属関係を示唆している。 以下にあげる公理に使われている変数は、全て2つの連続する型のいずれかに属する。プライムなしの変数は低位の型の変数であり、'∈' の左辺にのみ出現する（プライムつきは逆）。ST での一階述語論理では、型をまたいだ量化ができない。従って、ある型とそれに隣接する型ごとに外延性と内包性の公理を定義する必要が出てくるが、下記の外延性と内包性の公理を型をまたいで成り立つ公理型（axiom schema）とすればよい。 同一性: x=y ↔ ∀z’ [x∈z’ ↔ y∈z’] 外延性: ∀x[x∈y’ ↔ x∈z’] → y’=z’ ここで、自由変項 x を含む任意の一階述語論理式を Φ(x) で表すものとする。 内包性: ∃z’∀x[x∈z’ ↔ Φ(x)] 注意: 同じ型の要素を集めたものは次のレベルの型のオブジェクトを形成する。内包性は型に関する公理というだけでなく、Φ(x) の公理でもある。 無限性: 最下層の型の個体要素間についての空でない二項関係 R で以下を満たすものが存在。 狭義の全順序（非反射的で推移的で、強連結 (∀x, y[x ≠ y↔[xRy ∨ yRx]])）で有り、極小元以外の任意の要素はそれより大きい要素を持つ（余定義域は定義域の部分領域で有る）。 注意: 無限性 は純粋に数学的な ST 固有の公理である。これは R が全順序関係であることを意味している。最下層の型に 0 を割り当てたとき、R の型は 3 となる。無限性 が成り立つのは R の議論領域が無限のときだけであり、結果として無限集合の存在を前提としている。関係を順序対で定義する場合、この公理の前に順序対を定義する必要が生じる。これは ST に Kuratowski の定義を導入することで実現する。ZFCのような他の集合論の無限集合の公理が何故 ST で採用されなかったのかは書籍にも書かれていない。 ST は型理論が公理的集合論と似ていることを明らかにした。さらに、ZFC などの従来の集合論よりも単純な存在論に基づく "iterative conception of set" と呼ばれる ST のより精巧な存在論がもっと簡単な公理（公理型）を構成している。型理論の出発点は集合論だが、その公理、存在論、用語は異なる。型理論には他にも New Foundations や Scott-Potter set theory がある。