類似性、命題、高次射

コンピュータッドとか雑多に色々考えてみる、ほんと雑多 - 檜山正幸のキマイラ飼育記 メモ編で類似性という概念に触れた。次のことが言えると思う。

• すべての命題は類似性の主張である。
• すべてのメタ命題は存在命題である。
• すべての証明は構成的である。

高次圏を固定して、Morⁿをn-射の集合とする。Idⁿ, Invⁿをそれぞれ、n-恒等射の集合、n-可逆射の集合とする。可逆性は、on-the-noseで定義可能： α;β = id_{dom α}, β;α = id_{dom β} 。

イコールは厳密な類似性、同型はタイトな類似性、その他はラックスな類似性とする。a, bをn-射＝n-対象として：

• a = b ⇔ ∃α∈Idⁿ⁺¹.α:a→b
• a b ⇔ ∃α∈Invⁿ⁺¹.α:a→b
• a > b ⇔ ∃α∈Morⁿ⁺¹.α:a→b

類似性の類似度（厳密、タイト、ラックス）は色々あれど、類似性の証拠は1次元高い射になる。したがって、類似性の証明とは、1次元高い適切な射を見つけることになる。見つけるとは結局は具体的に構成することだから、「証明＝射の構成」となる。

コンピュータッドとか雑多に色々考えてみる、ほんと雑多 - 檜山正幸のキマイラ飼育記 メモ編で提示した疑問

• 描画と証明の関係（なぜ、描画が証明なのか）

は、この考え方である程度は了解できるだろう。

論理系とは、上記の高次圏のことで、高次圏の選び方により様々な論理が展開できる。