Function calculates Gödel number of negated sentence

[SnO2WMaN]

問題意識としては https://github.com/FormalizedFormalLogic/Foundation/issues/108 も参照

文 σ に対して ⌜∼σ⌝ = neg ⌜σ⌝ となる関数 neg の構成と，その利用として “x. ¬!𝔅.prov (neg x)”: $\lnot \mathrm{Pr}(\dot{\lnot}(x))$ のような論理式を考えたいのだが，どう定義すればいいのかよくわからなかった．良い案はあるだろうか？

[iehality]

形式化された否定なら https://github.com/FormalizedFormalLogic/Arithmetization/blob/3d99d24b572f61cb362e8f40f81697343e3562a6/Arithmetization/ISigmaOne/Metamath/Coding.lean#L477 のように定義してあるのでそれを使えばよいと思う．