refactor(Propositional): Redesign Hilbert Systems

[SnO2WMaN]

論理式の集合 Logic が意味論に対して健全・完全というのをやっぱり止めて，Hilbert流証明体系が健全・完全という方向性に変える．その他細々とした修正．

メモ：規則から全く異なるHilbert流体系をHilbertWFやHilbertFとして導入しないとならないので命名はゴチャゴチャになる可能性はある．

[SnO2WMaN]

@iehality

意見として訊きたいのだが，現状の実装の Logic α をmembershipによってEntailmentとして扱う方針ってどうなのだろうか？（Logicと言ったときには集合的なものとして今後も扱いたい．このPRではstructureとして再実装している）

instance : Entailment (Logic α) (Formula α) := ⟨fun L φ ↦ PLift (φ ∈ L)⟩

正直これに関してはProofとProvableの違いが何もないので微妙に思える．Entailment.SoundやEntailment.Completeなどの定義が流用できるのはよいが…Logic側で同じようなものを定義するのもそれほどコストはかからないとは思う．

[iehality]

@iehality

意見として訊きたいのだが，現状の実装の Logic α をmembershipによってEntailmentとして扱う方針ってどうなのだろうか？（Logicと言ったときには集合的なものとして今後も扱いたい．このPRではstructureとして再実装している）

instance : Entailment (Logic α) (Formula α) := ⟨fun L φ ↦ PLift (φ ∈ L)⟩

正直これに関してはProofとProvableの違いが何もないので微妙に思える．Entailment.SoundやEntailment.Completeなどの定義が流用できるのはよいが…Logic側で同じようなものを定義するのもそれほどコストはかからないとは思う．

微妙なのはそう．これによる利益は Sound, Complete, また Propositional.Hilbert 下の証明を再利用できるということしかない．いくつかの対応策がある．

1. Logic 下で上の定義を実装する： Propositional, Modal などには役に立つと思うが，述語論理では自由変数を含む文の意味論は図式的に良い性質を満たさない（Sematics.Tarski でない）ので普遍的な解決策ではない．
2. そもそも Entailment を関係として定義してしまう：

  class Entailment (S : Type*) (F : outParam Type*) where
    Prf : S → F → Prop

これはそんなに悪くない（わたしが何か見落としていなければ）．Sound や Complete など主要な性質は証明可能性だけで十分記述できるし，Propositional.Hilbert 下の証明も，その証明の具体的な内容が必要になることはおそらくないだろう（あったとしたらそれは Propositional.Hilbert を使用すべきでない）．ただ大工事になる．