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

State before:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
⊢ System.Undecidable T γ
Tactic:
have h : T ⊢! γ ↔ T ⊢! ~γ := by simpa using diagRefutation_spec T ρ
State after:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
h : T ⊢! γ ↔ T ⊢! ~γ
⊢ System.Undecidable T γ

State before:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
h : T ⊢! γ ↔ T ⊢! ~γ
⊢ System.Undecidable T γ
Tactic:
exact
  ⟨fun b ↦ (Gentzen.inconsistent_of_provable_and_refutable! b (h.mp b)).not_con (consistent_of_sigmaOneSound T),
   fun b ↦ (Gentzen.inconsistent_of_provable_and_refutable! (h.mpr b) b).not_con (consistent_of_sigmaOneSound T)⟩
State after:
no goals

State before:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
⊢ T ⊢! γ ↔ T ⊢! ~γ
Tactic:
simpa using diagRefutation_spec T ρ
State after:
no goals