2026.07.22
https://gyazo.com/4a253300d4b979d8cccbb801be22ec44
やった
https://gyazo.com/6f2b5cffb6373df3013fe0781e23a116
$ \mathsf{Z}_\inftyへの埋め込み：$ \mathsf{PA} \vdash \Gammaのとき$ \mathsf{Z}_\infty \vdash^\alpha_0 \Gamma（カットフリー証明可能）
偽リテラルの削除：$ \mathsf{Z}_\infty \vdash^\alpha_c \bot, \Gammaなら$ \mathsf{Z}_\infty \vdash^\alpha_c \Gamma
よって$ \mathsf{PA} \vdash \botと仮定すると$ \mathsf{Z}_\infty \vdash \emptyset．しかしそれはおかしいから，$ \mathsf{PA} \nvdash \bot．
が．．$ \N \models \mathsf{PA}なので無矛盾，というのは述べていて，proof irrevalenceなのでこの形式化はただ証明としてはあまり意味がない．はず
もっと精緻な解析がいる．のだけど証明論や順序数解析周りの話について全く分からないので．．．．．．．．．． メモ
思った