定義的等号と命題的等号の区別が問題になるが、もっと問題なのは、宣言的所属関係と命題的所属関係だろう。宣言的＝合意形成的、命題的＝問題提示的
所属的所属関係も $`\in`$ で書かれる。$`:`$ も使うが、宣言的所属関係を $`:`$ で書くと、圏論のコロンの用法とコンフリクト〈バッティング〉する。$`:\in`$ を宣言的所属関係の記号とする。
宣言的所属関係は、束縛を伴う項・式のヘッド部に登場する。
- ラムダ記法の関数項・式のヘッド部、ラムダリスト＝仮引数リスト
- 集合の内包的記法のヘッド部
- 全称命題論理式のヘッド部
- 存在命題論理式のヘッド部
関数抽象〈ラムダ抽象〉とは、パラメーター付きインスタンス項〈値項 | 証明項〉から無名関数〈無名定理〉を作ること。関数抽象の結果は、（無名だが）関数〈定理〉で、関数としてのプロファイル〈関数空間型〉を居住地〈アビタ〉情報として持つ。
関数抽象の二項演算子記号として、関数アロー記号を認める。関数アロー記号は、関数空間型の型構成子とは違う。$`\mapsto`$ を使う。$`(x, y)\mapsto f(x, y)`$
左右逆にするには：
$`\newcommand{\leftmapsto}{ \mathrel{\style{display: inline-block; transform: rotate(180deg)}{\mapsto}} }
\newcommand{\Imp}{ \mathrel{=\!\!\triangleright} }
f(x, y) \leftmapsto (x, y)`$
\newcommand{\leftmapsto}{ \mathrel{\style{display: inline-block; transform: rotate(180deg)}{\mapsto}} } f(x, y) \leftmapsto (x, y)
例：
$`( (x, y) \mapsto x^2 + y^2 )`$
$`( x^2 + y^2 \leftmapsto (x, y) )`$
$`( x^2 + y^2 \leftmapsto (x:\in {\bf R}, y:\in {\bf R}) )`$
$`( x^2 + y^2 :\in {\bf R}\leftmapsto (x:\in {\bf R}, y:\in {\bf R}) )`$
構文的整形式性の正当性命題〈justification proposition〉は：
$`x\in {\bf R}\land y\in {\bf R} \Imp x^2 + y^2 \in {\bf R}`$
$`\lambda\, (x \mid x\ge 0). \varepsilon!\,(t).( t^2 = x \land t \ge 0)`$ の正当性命題は：
$`\forall x:\in {\bf R}.( x\ge 0 \Imp \exists! (t :\in {\bf R}).( t^2 = x \land t \ge 0) )`$
- 「Problem → Solve → Knowledge〈PSK〉」サイクルで数理科学的知識ベース〈MSKB〉が進化発展する。
- 定義的〈宣言的〉／背景的等号を $`=!`$ 、定義的／背景的論理同値を $`\equiv!`$ にして、ビックリなしを命題的等号、命題的論理同値とする。問題的・疑問的等号を $`=?`$ とする。
- 定義的〈宣言的〉／背景的伴意を $`\vdash!`$ として、ビックリなしを命題的伴意とする。問題的・疑問的等伴意を $`\vdash?`$ とする。
