add(Incompleteness): Add Jeroslow's Sentence and Formalized Law of Noncontradiction#700
add(Incompleteness): Add Jeroslow's Sentence and Formalized Law of Noncontradiction#700
Conversation
| lemma Refutable.quote_iff {σ : Sentence L} : T.Refutable (V := V) ⌜σ⌝ ↔ T.Provable (V := V) ⌜∼σ⌝ := by | ||
| simp [Refutable, Sentence.quote_def, Semiformula.quote_def] | ||
|
|
||
| noncomputable def refutable (T : Theory L) [T.Δ₁] : 𝚷-[2].Semisentence 1 := .mkPi |
There was a problem hiding this comment.
neg は
SnO2WMaN
changed the title
| dsimp [flon] at consis; | ||
| have : T ⊢ (safe 𝔅 ℜ)/[⌜𝐉⌝] := by | ||
| sorry; | ||
| have h₃ : T ⊢ ∼(𝔅 𝐉 ⋏ ℜ 𝐉) := by simpa [safe] using this; |
There was a problem hiding this comment.
とても初歩的な質問なのだが，T ⊢ ∀' (safe 𝔅 ℜ)/[#0] から T ⊢ (safe 𝔅 ℜ)/[⌜𝐉⌝] を出したい．つまり specialize がどこかにあると思うのだが，探してもどこにあるのかよくわからなかった．どうすればいいのだろうか？
There was a problem hiding this comment.
実質的に LO.FirstOrder.Derivation.specialize がそれだが，普通の証明可能性については示していないと思う．
|
|
||
| variable [L.ReferenceableBy L₀] {T₀ : Theory L₀} {T : Theory L} | ||
|
|
||
| @[coe] def rf (ℜ : Refutability T₀ T) (σ : Sentence L) : Sentence L₀ := ℜ.refu/[⌜σ⌝] |
There was a problem hiding this comment.
どうでもいいことだが，証明可能性を bewisbar の 𝔅 で書くなら，反証可能性は widerlegbar の 𝔚 で書くべきでは．
There was a problem hiding this comment.
これは思ったが，𝔅 をそもそも 𝔓 にしたほうが良いような気もする．
There was a problem hiding this comment.
抽象的な可証性述語を B で書くのは Eine Interpretation des intuitionistischen Aussagenkalküls からの慣例なのでそんなに悪くないと思う．
| namespace Derivation | ||
|
|
||
| variable {𝓢 : SyntacticFormulas L} {φ : SyntacticSemiformula L 1} | ||
|
|
||
| def specialize'! (t : SyntacticTerm L) (b : 𝓢 ⊢! ∀' φ) : 𝓢 ⊢! φ/[t] := by simpa using specialize (Γ := []) t b; | ||
|
|
||
| def specialize' (t : SyntacticTerm L) (b : 𝓢 ⊢ ∀' φ) : 𝓢 ⊢ φ/[t] := ⟨specialize'! t b.get⟩ | ||
|
|
||
| end Derivation | ||
|
|
||
|
|
||
| namespace Theory | ||
|
|
||
| variable {T : Theory L} {φ : Semisentence L 1} | ||
|
|
||
| def specialize! (t) (b : T ⊢! ∀' φ) : T ⊢! (φ/[t]) := by | ||
| apply ofSyntacticProof; | ||
| sorry; | ||
|
|
||
| def specialize (t) (b : T ⊢ ∀' φ) : T ⊢ (φ/[t]) := by | ||
| have := Derivation.specialize' t $ provable_def.mp b; | ||
| apply provable_def.mpr; | ||
| sorry; | ||
|
|
||
| end Theory |
There was a problem hiding this comment.
あっては欲しいのだが．Termの扱いがよくわからず頓挫している．
There was a problem hiding this comment.
2 participants
close #698