feat(Modal): Arithmetical Soundness of 𝐆𝐋
#69
Conversation
SnO2WMaN
force-pushed
the
GL-interpretation
branch
from
8f49efe to
9773263
Compare
|
|
||
| section | ||
|
|
||
| variable (T₀ T : Theory L) [T₀ ≼ T] [System.Classical T₀] [System.Classical T] [HilbertBernays β T₀ T] |
There was a problem hiding this comment.
System.Classical TはLogic/HilbertStyle/Gentzenで証明されているのでそれをインポートすれば良いと思う．
There was a problem hiding this comment.
NegationEquiv Tも常に証明できるはず．Logic/HilbertStyle/Gentzenを参考に証明が書けると思う．
|
レビューを受け修正． |
| private lemma loeb_fixpoint | ||
| (β : ProvabilityPredicate L L) [β.HilbertBernays T₀ T] | ||
| (σ : Sentence L) : ∃ (θ : Sentence L), T₀ ⊢! ⦍β⦎θ ⟶ ⦍β⦎σ ∧ T₀ ⊢! (⦍β⦎θ ⟶ σ) ⟶ θ := by | ||
| have hθ := diag (T := T₀) “x | !β.prov x → !σ”; | ||
| generalize (fixpoint T₀ “x | !β.prov x → !σ”) = θ at hθ; | ||
|
|
||
| have eθ : θ ⟷ (β.prov/[#0] ⟶ σ/[])/[⸢θ⸣] = θ ⟷ (⦍β⦎θ ⟶ σ) := by | ||
| simp [←Rew.hom_comp_app, Rew.substs_comp_substs]; rfl; | ||
| replace hθ : T₀ ⊢! θ ⟷ (⦍β⦎θ ⟶ σ) := by simpa [←eθ] using hθ; | ||
|
|
||
| existsi θ; | ||
| constructor; | ||
| . exact (imp_trans! (D2 ⨀ (D1 (Subtheory.prf! $ conj₁'! hθ))) D2) ⨀₁ D3; | ||
| . exact conj₂'! hθ; | ||
|
|
There was a problem hiding this comment.
Löbの定理で使う不動点の構成，出来ている以上はおそらく合っていると思うのだが書き換えシステムなどに慣れていないので正しいのかわからない．一応チェックしてもらえると助かる．
There was a problem hiding this comment.
だいたい良いと思うが，構成的に示せるならば∃ (θ : Sentence L) ...の形ではなく具体的にwitnessを示したほうが良いと思う．
ただ“x | !β.prov x → !σ”でなく“x | !β.prov x → !!σ”の表記のほうが扱いやすいかもしれない（前者は空の列をσに代入しているが，後者はσを直接用いる）
There was a problem hiding this comment.
“x | !β.prov x → !!σ”にした場合，σがSemisentence L 1でないという理由で型チェックが通らない．（望ましい挙動なのかはよくわからない）．
具体的にwitnessを示すというのがどういったことを指すのかよくわかっていない．例えば下記のよう定義してkreisel_specみたいなものを補題として用意する，という意味だろうか？
def kriesel (β : ProvabilityPredicate L L) [β.HilbertBernays T₀ T] (σ : Sentence L) := fixpoint T₀ “x | !β.prov x → !σ”
There was a problem hiding this comment.
なるほど，勘違いしていた．witnessについては，具体的にKreisel文を定義するということで間違いない．
|
気になる点がなければマージする． |
related: #1