言葉づかい、態度 3: 焦点

computational, computationally, computable を単に「計算的」で修飾するかも知れない。

• 計算的圏＝計算可能圏
• 計算的集合＝計算的圏の対象
• 計算的関数＝計算的圏の射＝計算可能関数

計算的圏は、高々加算な付点集合の圏に埋め込める。さらに、高々加算集合の圏にも埋め込める。

• Cptbl → PtSet_≦ω → Set_≦ω

PtSet_≦ωとSet_≦ωの中間的存在として、PtSet^nons_≦ωは、non-strict mapを許した圏。nons は allow non-strict の意味。

計算的集合の部分集合は、計算可能なものに限定すべき。計算可能＝計算的部分集合は、帰納的加算集合と一致すべき。よって、計算的部分集合＝帰納的加算集合。

計算的集合に、計算的部分集合の束を対応させると、計算的論理の計算的ハイパードクトリンになるだろう。ローヴェアの言葉で言うなら、計算的部分集合が計算的属性代数〈computational attribute algebra〉で統制されればよい。属性代数は、真偽値の代数の一般化。

計算的論理とはあらずもがなな言い方で、通常の論理は暗黙に計算的だろう。暗黙の前提をハッキリさせて、計算的論理と超越的論理の差を見る。

computational/computableの意味でΓを添えることにすると：

• Pow_Γ(X)⊆Pow(X)
• Pow(X) ⊆ Pow_Γ(X) とは限らない。
• Map_Γ(X, Y)⊆Map(X, Y)
• Map(X, Y)⊆Map_Γ(X, Y) とは限らない。

ここで、Map(-, -) = Hom_Set(-, -) = Set(X, Y), Map_Γ(-, -) = Hom_Cptbl(-, -) = Cptbl(X, Y)。