言葉づかい、態度
ほんとに深刻だよなー。
- 内容的な命題：人間が解釈し運用する命題
- 形式化された内容的命題： 記号化された内容的命題
- 符号化された命題： 形式化された内容的命題に脱符号化できるが、人間が解釈し運用することはない。
- データ化された命題： 符号化された命題だが、脱符号化を考えない。
ここで、符号化＝ゲーデル化、データは選ばれたデータ領域の要素のこと。
何を信頼し、何を疑うか？ で逆の態度を取ってしまうとアウトだ。
- 内容的な古典二値論理と内容的な証明を疑うわけではない。逆！ 古典二値論理と形式化された証明は徹底的に信じる。でないと、確実な拠り所がなくなり、何も信用しないという悪しき懐疑主義に陥る。
- 素朴集合論も同様に信じる。
- 特定の集合や写像に関する議論では、内容的な証明なしに予測や雰囲気で信じない。
- 特定の集合や写像に関する内容的命題は、古典的な証明があるなら信じる。
古典論理や素朴集合論を疑う方向に傾くと、ロクなことにならない。通常の、普通に行われている（形式化されてない）記述と証明の行為は徹底的に信じる。
風評・風説は、逆の方向（誤解）に誘導しているように思える。
言葉づかい、態度 2
ゲーデル化をどうするか？ その2 - 檜山正幸のキマイラ飼育記 で、「コード」を問題にしたが、「述語」も大問題。
- 基本〈原子 | 原始〉述語記号〈述語名〉
- 定義された述語記号〈述語名〉
- 幾つかの変数を持つ論理式
- 論理式をボディに持つラムダ関数式〈ラムダ抽象〉
- 意味領域側の、任意のブール値関数
- 意味領域側の、論理式で表現可能なブール値関数
多項式と多項式関数は違うのと同じように、まったく任意のブール値関数（部分集合と同義）と、論理式で定義される関数は違う。濃度からして違う。
区別するなら：
- 述語記号＝述語名
- n項の述語式＝論理式をボディに持つラムダ関数式
- 述語関数は、述語式で定義される関数
計算可能性に関して、
- 計算的集合〈computational set〉＝列挙付き集合〈enumerated set〉
幾つかの計算的集合と、計算的集合のあいだの幾つかの関数を、基本集合と基本関数として、計算可能圏〈computable category〉を作れる。計算可能圏の構成は、通常のデカルト圏構成以外に、再帰構成と計算的イプシロン記号〈computational epsilon〉を入れてよい。計算的イプシロン εx∈A.P は計算的集合〈データ領域〉A上の論理式Pに対して、P(a)が真であるaを返す手続き。aが存在しないなら⊥を返す。
再帰もイプシロンも、述語関数＝計算可能ブール値関数という概念が必要なので、ブール値集合と、基本述語関数は前もって指定しておく必要がある。
述語関数＝計算可能ブール値関数により、次の構成が可能となる。
- if文： if(p(x)) then f(x) else g(x)
- find文： find(x in D) p(x) ≡ for(x in D){if(p(x)) x}
付点集合を対象として、任意の写像を射とする圏を考えると、点を保つ写像の圏は、広い部分圏になる。この部分圏が通常の付点写像の圏で、部分写像の圏と同型。
具体的な計算可能圏は、付点写像の圏の部分圏であるが、充満部分圏ではない。
- fが計算可能 ⇒ fは付点写像（fはストリクト）
逆が成立しない。
非ストリクト関数は当然に計算可能ではない。計算可能の観点からの“超越関数”である。ここでの超越関数は、非代数的じゃなくて、非計算的の意味。
