Theorem: LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.godel_independent (Logic/FirstOrder/Incompleteness/SelfReference.lean)

State before:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
⊢ Undecidable T G
Tactic:
suffices ¬(T ⊢! G ∨ T ⊢! ~G) by
  simpa[System.Undecidable, not_or] using this
State after:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
⊢ ¬(T ⊢! G ∨ T ⊢! ~G)

State before:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
⊢ ¬(T ⊢! G ∨ T ⊢! ~G)
Tactic:
rintro (H | H)
State after:
case inl
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
H : T ⊢! G
⊢ False

case inr
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
H : T ⊢! ~G
⊢ False

State before:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
this : ¬(T ⊢! G ∨ T ⊢! ~G)
⊢ Undecidable T G
Tactic:
simpa[System.Undecidable, not_or] using this
State after:
no goals

State before:
case inl
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
H : T ⊢! G
⊢ False
Tactic:
have h₁ : T ⊢! ~(provableSentence T)/[⸢G⸣] := System.and_left! (goedel_spec T) ⨀ H
State after:
case inl
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
H : T ⊢! G
h₁ : T ⊢! ~[→ ⸢G⸣].hom (provableSentence T)
⊢ False

State before:
case inl
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
H : T ⊢! G
h₁ : T ⊢! ~[→ ⸢G⸣].hom (provableSentence T)
⊢ False
Tactic:
have h₂ : T ⊢! (provableSentence T)/[⸢G⸣]  := by simpa using (provableSentence_representation (L := ℒₒᵣ)).mpr H
State after:
case inl
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
H : T ⊢! G
h₁ : T ⊢! ~[→ ⸢G⸣].hom (provableSentence T)
h₂ : T ⊢! [→ ⸢G⸣].hom (provableSentence T)
⊢ False

State before:
case inl
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
H : T ⊢! G
h₁ : T ⊢! ~[→ ⸢G⸣].hom (provableSentence T)
h₂ : T ⊢! [→ ⸢G⸣].hom (provableSentence T)
⊢ False
Tactic:
exact (Gentzen.inconsistent_of_provable_and_refutable! h₂ h₁).not_con (consistent_of_sigmaOneSound T)
State after:
no goals

State before:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
H : T ⊢! G
h₁ : T ⊢! ~[→ ⸢G⸣].hom (provableSentence T)
⊢ T ⊢! [→ ⸢G⸣].hom (provableSentence T)
Tactic:
simpa using (provableSentence_representation (L := ℒₒᵣ)).mpr H
State after:
no goals

State before:
case inr
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
H : T ⊢! ~G
⊢ False
Tactic:
have : T ⊢! ~G ⟷ (provableSentence T)/[⸢G⸣] := Gentzen.not_contra! (goedel_spec T)
State after:
case inr
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
H : T ⊢! ~G
this : T ⊢! ~G ⟷ [→ ⸢G⸣].hom (provableSentence T)
⊢ False

State before:
case inr
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
H : T ⊢! ~G
this : T ⊢! ~G ⟷ [→ ⸢G⸣].hom (provableSentence T)
⊢ False
Tactic:
have : T ⊢! (provableSentence T)/[⸢G⸣] := System.and_left! this ⨀ H
State after:
case inr
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
H : T ⊢! ~G
this✝ : T ⊢! ~G ⟷ [→ ⸢G⸣].hom (provableSentence T)
this : T ⊢! [→ ⸢G⸣].hom (provableSentence T)
⊢ False

State before:
case inr
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
H : T ⊢! ~G
this✝ : T ⊢! ~G ⟷ [→ ⸢G⸣].hom (provableSentence T)
this : T ⊢! [→ ⸢G⸣].hom (provableSentence T)
⊢ False
Tactic:
have : T ⊢! G := (provableSentence_representation (L := ℒₒᵣ)).mp this
State after:
case inr
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
H : T ⊢! ~G
this✝¹ : T ⊢! ~G ⟷ [→ ⸢G⸣].hom (provableSentence T)
this✝ : T ⊢! [→ ⸢G⸣].hom (provableSentence T)
this : T ⊢! G
⊢ False

State before:
case inr
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
H : T ⊢! ~G
this✝¹ : T ⊢! ~G ⟷ [→ ⸢G⸣].hom (provableSentence T)
this✝ : T ⊢! [→ ⸢G⸣].hom (provableSentence T)
this : T ⊢! G
⊢ False
Tactic:
exact (Gentzen.inconsistent_of_provable_and_refutable! this H).not_con (consistent_of_sigmaOneSound T)
State after:
no goals