KurohaKafka is a user on googoldon.net. You can follow them or interact with them if you have an account anywhere in the fediverse. If you don't, you can sign up here.

訂正

 長さの定義の例

$\text{Length}(A)=m\leftrightarrow\text{Col}(m,A)=Φ∧∀n(\text{Col}(n,A)=Φ→m\leq n)$

数列は大文字、自然数は小文字

空列の公理

$∃X∀Y(Y\not∈X)$

 空列をΦと表す

(数列の)外延性の公理

$∀X∀Y∀n(\text{Col}(n,X)=\text{Col}(n,Y)\leftrightarrow X=Y)$

 等号記号=は自然数と共有する

連結の公理

$∀X∀Y∃Z(X\frown Y=Z)$

長さの公理 任意の数列は自然数の長さをもつ

$∀X∃n(\text{Length}(X)=n)$

 長さの定義の例

$\text{Length}(A)=m\leftrightarrow\text{Col}(n,A)=Φ∧∀n(\text{Col}(n,A)=Φ→m\leq n)$

単列の公理

$∃X(\text{Col}(0,X)=X)$

内容の公理

$∀X∃n(\text{Col}(0,X)=X→\text{Content}(X)=n)$

 「内容」よりもふさわしい言い方があるかもしれないが、暫定的に

単純に考えれば全域真理値割り当てなんだけど、形式的に厳密に考えるとその全域性がなにによって保証されるのか。なにかしらのドメインを示したうえで全域性を示すことができたとして、じゃあ新たに記号を追加された言語による拡張されたドメインにおいても全域性が保証されているのか? これは超準モデルの存在的に形式主義の限界ではないか。

完全性を証明するだけなら同値類で纏めればいいし、ドメインの拡張まで考えなくていいんだけど

素因数分解以外にやり方があればこの限りではない

あと算術によるコーディングは素因数分解の一意性が示せないとだめだけど、これけっこう強いのな。
とりあえずロビンソン算術では無理かな

命題論理のモデルについてはまだいろいろ思うところあって踏ん切りがついてない

2階算術基準で考えて真理値割り当てをメタ自然数の集合とした。

あらかじめ真理値割り当てが関数として記号と公理が用意されている1階算術で考えるのもよし

うまいことやってΔ_1-CA_0で済むかな

この算術の2階部分としての真理値割り当てのすべての要素とすべての命題変数をうまいこと組み合わせて命題論理のモデルとする

最初から1階述語論理でやったがいい気もする

論理演算子の優先順位的にとして括弧を付けなければ
$\langle\langle5,\lceilφ\rceil,\lceilψ\rceil\rangle,1\rangle∈\cal{I}\leftrightarrow(\langle\lceilφ\rceil,1\rangle∈\cal{I}→\langle\lceilψ\rceil,1\rangle∈\cal{I})\\
)$

$\langle\langle4,\lceilφ\rceil,\lceilψ\rceil\rangle,1\rangle∈\cal{I}\leftrightarrow(\langle\lceilφ\rceil,1\rangle∈\cal{I}∨\langle\lceilψ\rceil,1\rangle∈\cal{I})∧$
$\langle\langle5,\lceilφ\rceil,\lceilψ\rceil\rangle,1\rangle∈\cal{I}\leftrightarrow\langle\lceilφ\rceil,1\rangle∈\cal{I}→\langle\lceilψ\rceil,1\rangle∈\cal{I}∧$

$∀\lceilφ\rceil,\lceilψ\rceil∈\text{Fml\(^L\)}($
$\langle\lceilφ\rceil,0\rangle∈\cal{I}\leftrightarrow\langle\lceilφ\rceil,1\rangle\not∈\cal{I}∧$
$\langle\lceilφ\rceil,0\rangle∈\cal{I}\leftrightarrow\langle\langle2,\lceilφ\rceil\rangle,1\rangle∈\cal{I}∧$
$\langle\langle3,\lceilφ\rceil,\lceilψ\rceil\rangle,1\rangle∈\cal{I}\leftrightarrow\langle\lceilφ\rceil,1\rangle∈\cal{I}∧\langle\lceilψ\rceil,1\rangle∈\cal{I}∧$

訂正
(0,0,0)(1,1,1)(2,1,1)(3,1,1)(3,1,0)(4,2,0)=$ψ_{χ_0(0)}(ψ_{χ_{ε_{M+1}}(0)}(0))$

@koteitan
そんなところですね。
数列ではありませんがloader.cではPair関数で2分木を表してる感じです、ヘッダに当たる部分が0か1か2か・・・で依存型かλ式か適用か変数か・・・にわかれるんだったか

@koteitan
二つの異なる素数p,qをして、たとえば<2,3>なら
\(p^2\cdot q^3=p\cdot p\cdot q\cdot q\cdot q\)
という具合です

ここでいう算術はメタなほう

最初の内は算術から初めて、あとから集合論に翻訳でもいいな

集合論からはじめるとして、集合論における順序対を定義→掛け算を定義→算術における順序対を定義

でもいいけどこれだけの手間をかける意味は?