feat(ProvabilityLogic): Arithmetical Completeness of GL Part.1

[SnO2WMaN]

適当な条件を満たすような算術の文(Solovay sentences)が構成可能だと仮定すると、𝐆𝐋の算術的完全性が言えるという事実を形式化する。Part.2では実際にSolovay Sentencesが構成可能であることを形式化する予定。

余談: とりあえず和書では新井の『数学基礎論』増補版の3章後半を参考してほしいが、Solovay sentencesは原始的再帰関数に関する再帰定理から構成出来る。この定理に対応する形式化はあるだろうか？

[iehality]

見る限り単なる原始再帰的関数ではなく算術の内部で形式化した原始再帰的関数を用いているように見えるが，これは形式化していないし，するならかなり大変だと思う．一つの案として，https://formalizedformallogic.github.io/Book/first_order/isigma1.html#fixpoint の改変を使えばできそうな気がする．
また，しっかり証明を追ったわけではないので誤っているかもしれないが，ある種の対角化補題を使って示せないだろうか．
確か
$$\phi_i \leftrightarrow \theta_i(\ulcorner \phi_0 \urcorner, ..., \ulcorner \phi_k \urcorner)$$ (for all $$i < k$$)
を満たす不動点 $$\phi_i$$ が $$\theta_i$$ について存在する（と思う．間違っていたら申し訳ない）ので，これを用いる．

つまり
$$H(p_1, ..., p_k, 0) := 0, H(p_1, ..., p_k, n + 1) := z (\text{if } H(p, n) \prec z \land Prov(n, \hat{\lnot} p_z)) := H(p_1, ..., p_k, n) (\text{o.w.})$$ を満たす $$H$$は $$\mathsf{I}\Sigma_1$$ で定義可能である． $$\Phi_i(p_1, ..., p_k) := (\exists m)(\forall n \ge m)[H(p_1, ..., p_k) = i]$$ を対角化すれば $$L(i) \leftrightarrow (\exists m)(\forall n \ge m)[H(\ulcorner L(0) \urcorner, ..., \ulcorner L(k) \urcorner, n) = i]$$ を満たす．

[SnO2WMaN]

再帰定理ではなく不動点補題を用いてsolovay sentencesを構成する方法もあったはず（証明は忘れました）なので一旦こちらで行けるか検証してみます。検討ありがとう。

[iehality]

また，しっかり証明を追ったわけではないので誤っているかもしれないが，ある種の対角化補題を使って示せないだろうか．

この一般化した不動点補題を示した．

Incompleteness/Incompleteness/Arith/Second.lean

Lines 126 to 127 in 7f9d87b

	theorem multidiagonal (θ : Fin k → Semisentence ℒₒᵣ k) :
	T ⊢!. multifixpoint θ i ⭤ (Rew.substs fun j ↦ ⌜multifixpoint θ j⌝).hom (θ i) :=