2023.09.16
https://gyazo.com/0559af8664938731b65a4656df8777ca
いいね
https://nicothumb2img.vercel.app/image/sm38238565#.png https://nico.ms/sm38238565
観た
感想は上記記事で書く。
メモ
memo:
$ \sf LPに負の内省公理を入れて拡張する$ \sf JS5と算術との対応が上手く出来ない． Simpsonという人物の方法に沿って様相論理GLの直観主義バージョンを考える $ \sf GL_{circ}が$ \sf GLのTait計算$ \sf GL_{seq}と証明能力が等しくなる すなわち$ \sf GL, K4は片方を循環証明体系に拡張することで証明能力が同じになる． 2023.11.11メモ: 読んだバージョンに依るのかもしれないがこの事実はあまり明確には書いてない． すなわち$ \mathsf{R} + Uが無矛盾となる任意の理論$ Uは決定不可能である．
知った
思った
本質的遺伝的本質的決定不能性というのはあるのだろうか？
すなわち，任意の理論$ Uについて$ T+Uが無矛盾なら$ Uは本質的決定不能となるような理論$ T Diagonalizable algebraとも言われるが多分古いとおもう．
メモ
読んだ
メモ
プログラムを用いて$ \Delta_0,\Sigma_1を説明する
決定可能$ \Delta_0とは大雑把にはこういうプログラムである． code:delta_0
for(nat i = 0; i < L; i++){
if(isFoo(i)) return true;
}
return false; // L回のループを回りきったらここに辿り着く．
for(nat i = 0; i < L; i++){}という形式のfor文が使えるプログラムであると考えて良い．
このプログラムはtrueかfalseのどちらかを必ず有限時間で返すので決定可能である． code:sigma_1
nat i = 0;
while(true) {
if(isFoo(i)) return true;
}
return false; // ここには辿り着けない．
このプログラムはisFoo(args)によっては永遠にreturn falseに辿り着くことは出来ない．
ただしisFoo(x)は$ \Delta_0，すなわちisFooの計算自体が永遠に終わらないということはないものとする．
今，算術の命題$ Sを自然数にエンコードした結果がsであるとする．
また，算術の命題の列$ \mathcal{P} \coloneqq \lang p_1,p_2,p_3,\dots,p_n\rangの自然数へのエンコードをpとする．
このとき，$ \mathcal{P}は$ Sの有効な証明であるということを計算するisProof(x, p)は決定可能/$ \Delta_0であるように構成出来る．以下スケッチ．
toSentences(p) = [p1, p2, ..., pn, pm]となるようにtoSentences(x)を構成する．
有効でないならnullを返してもよいとする．
isImpliable(x, y)を構成する．
先程toSentences(p)で得たリストに対しisImpliable(p1, p2) && isImpliable(p2, p3) && ... && isImpliable(pn, pm)を返せば良い．
なお内々の処理でnullが出たらその時点で計算を打ち切ってfalseを返せば良い．
isProof(x, p)となるpを探し続けるisProvable(x)は$ \Sigma_1である．
code:isProvable
isProvable(x: nat){
nat i = 0;
while(true) {
if(isProof(x, i)) return true;
}
return false;
}