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.

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\)
という具合です

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

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

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

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

順序対を表現するのに掛け算を使うが掛け算、というか関数の表現に順序対をつかってループしてるんだよな

集合論で算術を再現して、その算術でバシク行列を再現ってのも二度手間だし、将来のこと考えると直接集合論でバシク行列を再現したほうがいいかもしれないが、2階算術との関係を証明するうえで

いっぺんにやらないで別々にすすめてもいいが

x_1のシングルトンがx_2={x_1}
\(∀x_3(x_3∈x_2→x_3=x_1)\)

x_1とx_2の和集合がx_3=x_1∪x_2
\(∀x_4(x_4∈x_3\leftrightarrow (x_4∈x_1∨x_4∈x_2))\)

後者 s(x_1)=x_2
\(x_2=x_1∪{x_1}\)

算術なら順序対は掛け算と素数で定義するのがすじでは

こんな具合に1階算術をやっていくのは昔やってたが、実際に計算機モデルを適当な形式言語で再現するところから

Inductionの階層の厳密性を証明する必要

[x](0)(1)(1)...(1)
はΣ_1-Inductionで証明論的順序数でω^ω