add(FirstOrder): Independence of Yablo Sentences

[SnO2WMaN]

基本的にはCieśliński, Urbaniakの証明に沿う．
次を示す．

1. For $n \in \omega$, $T \nvdash Y(n)$ and $T \nvdash \lnot Y(n)$
2. $T \vdash \forall x. \lbrack Y(n) \leftrightarrow \mathrm{Con}_T \rbrack$
3. $T \vdash \forall x, y. \lbrack Y(n) \leftrightarrow Y(m) \rbrack$

[SnO2WMaN]

2が証明できれば3は明らかだが，量化子の入った形式的証明の書き方がよくわかってない．どこを参照すればよいとかあるだろうか？

[iehality]

2が証明できれば3は明らかだが，量化子の入った形式的証明の書き方がよくわかってない．どこを参照すればよいとかあるだろうか？

量化子があると代入や等号が面倒なので，できるだけ直接形式的証明は書かずモデルで議論することにしている．例は

Foundation/Foundation/ProvabilityLogic/GL/Completeness.lean

Line 496 in eda8e3a

oRing_provable₀_of _ _ fun (V : Type) _ _ ↦ by

などがある．

[SnO2WMaN]

InfoViewでは通っているが証明のコンパイルが重すぎて出来ていない気がする．

[iehality]

証明を見る限りだとモデル論的議論と証明論的議論を行ったり来たりしているようだが，最初からすべてモデル論的議論でやってしまえば軽くなるかもしれない（おそらく問題点は sentence の whnf に時間がかかっていることなので）．

[SnO2WMaN]

おそらく一番根幹となる yablo_diagonal_modeled ですら重すぎてコンパイル出来ておらず，モデル論的議論単体でやったとしてもそもそも重すぎている．simpのwhnfを長く取れば良いかもしれないが多分それでは解決しなさそう．

[iehality]

この例に関しては これらのエラーは simp に Matrix.comp_vecCons' が足りてないだけな気がする．

[SnO2WMaN]

すべての問題はこれで解決した．ありがとう．

[SnO2WMaN]

なかなか終わらないので，1のYablo文はすべて独立，という事実のみをこのPRでは扱うことにする．コメントを外せば証明は一応通るはずだが重すぎるのでこれからリファクタリングする…