Rename `Hierarchy` and `StrictHierarchy`

[SnO2WMaN]

メモ：一般的にはこちらのほうが標準的な定義な気がして，むしろ今のhierarchyが[Buss98 p.85]の $\Sigma^+_n$ に相当するもののはず．そのうちリネームするべきか？

Originally posted by @SnO2WMaN in #920 (comment)

[SnO2WMaN]

これどっちに寄せる・名称をどうするべきだろうか，というのをそろそろ正式に決めないとそのうち支障が出ると思う．

ここではとりあえずややこしいので，Bussに合わせて今までの途中にbounded quantifierを挟むことを許容するhierarchyをbroad hierarchy $\Sigma^+_1$ とし，そうでない厳密な方をstrict hierarchy $\Sigma_1$ とかと書くこととする．

現実的な利用や数学的な慣習ないし，現状のGödelコーディングなどを考えるとLean側で 𝗜𝚺₁ と書いたときnotationとしては $\Sigma_1^+$ クラスによるinductionを意図した方が都合が良いあるいは便利なような気もする．
一方で $𝚺₁$-sentence といったなら strict hierarchy の方で解釈して $\exists x \varphi(x)$ の形を厳密にしててほしいなというジレンマもある．

なお，いずれにしても 𝚺₀.Sentence などは Semiformula.Boundedなどを使ってBoundedSentenceにしてもよいかなとは思う（他同様）．
https://github.com/FormalizedFormalLogic/Foundation/pull/949/changes#diff-3cd51b01c26e4dfd715ad136e14c2286d3dae7e9060e7cb19807f87d9321c638 部分参照
hierarchyの名称や取り扱いをどう変えてもおそらく独立な定義に出来るはず．

[iehality]

notation についてはそれで良いと思う．𝗜𝚺₁⁺ ⪯ 𝗜𝚺₁ が示されているなら仮定 V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁ から V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁⁺ が自動で infer される（ようにする）ので induction を使用する際も問題ないだろう．

[SnO2WMaN]

方針はこうでいいですか

• 原則としてこのプロジェクトでは算術的階層は緩い階層の方を指すことにする．
• 現状の 𝗜𝚺₁ は 𝗜𝚺₁ のまま．
• strict hierarchyのinductionによる理論は 𝗜𝚺₁ˢ のような添字付けるnotationで表す．

[iehality]

いや，むしろ意図していたのは次の方針だった．

• Schema は strict な定義を標準にし，必要なときにのみ broad version を用いる．
• 論理式については broad な定義を標準で用いる．strict なものが必要なときは prenex への翻訳を用いる．

後者を要求するのはそうでないと具体的な定義（expGraph, standard provability predicate, ... etc.）を扱うのがあまりにも大変だからという理由による．

[SnO2WMaN]

それならば #949 で作業中なのでOKです．