refactor

Logic/FirstOrder/Incompleteness/Derivability/FirstIncompleteness.lean

@@ -1,7 +1,8 @@
+import Logic.Logic.HilbertStyle
 import Logic.FirstOrder.Incompleteness.Derivability.Theory
 import Logic.FirstOrder.Incompleteness.Derivability.Conditions
 
-open LO.System
+open LO.System LO.System.Intuitionistic
 
 namespace LO.FirstOrder.Arith.Incompleteness
 
@@ -19,14 +20,14 @@ variable (hG : IsGoedelSentence T₀ T G)
 open HasProvablePred.Derivability1
 
 lemma GoedelSentenceUnprovablility [hConsis : Theory.Consistent T] : T ⊬! G := by
-  by_contra hP;
+  by_contra hP; simp at hP;
   have h₁ : T ⊢! (Pr[T] ⸢G⸣) := hD1.D1' hP;
   have h₂ : T ⊢! (Pr[T] ⸢G⸣) ⟶ ~G := by simpa using weakening $ iff_mpr $ iff_contra hG;
   have hR : T ⊢! ~G := weakening (MP h₂ h₁);
   exact hConsis.consistent.false (NC hP hR).some;
 
 lemma GoedelSentenceUnrefutability [hSound : SigmaOneSound T] : T ⊬! ~G := by
-  by_contra hR;
+  by_contra hR; simp at hR;
   have h₁ : T ⊢! ~G ⟶ Pr[T] ⸢G⸣ := by simpa [Subformula.neg_neg'] using weakening $ iff_mp $ iff_contra hG;
   have h₂ : T ⊢! Pr[T] ⸢G⸣ := MP h₁ hR; simp at h₂;
   have h₃ : ℕ ⊧ (Pr[T] ⸢G⸣) := hSound.sound (Hierarchy.rew _ hPredDef.definable) h₂;
@@ -38,7 +39,7 @@ theorem FirstIncompleteness [hSound : SigmaOneSound T] : Theory.Incomplete T :=
   have := Consistent_of_SigmaOneSound T;
   by_contra hCC; simp at hCC;
   cases (hCC.some.complete G) with
-  | inl h => exact (GoedelSentenceUnprovablility T₀ T hG) h;
-  | inr h => exact (GoedelSentenceUnrefutability T₀ T hG) h;
+  | inl h => simpa using (GoedelSentenceUnprovablility T₀ T hG);
+  | inr h => simpa using (GoedelSentenceUnrefutability T₀ T hG);
 
 end LO.FirstOrder.Arith.Incompleteness

Logic/FirstOrder/Incompleteness/Derivability/LoebWithIT2.lean

@@ -3,7 +3,7 @@ import Logic.FirstOrder.Incompleteness.Derivability.Conditions
 import Logic.FirstOrder.Incompleteness.Derivability.FirstIncompleteness
 import Logic.FirstOrder.Incompleteness.Derivability.SecondIncompleteness
 
-open LO.System
+open LO.System LO.System.Intuitionistic
 
 namespace LO.FirstOrder.Arith.Incompleteness
 
@@ -49,17 +49,19 @@ variable [hSound : SigmaOneSound T] [HasProvablePred (T ∪ {~~ConL[T]})] [Defin
 
 theorem FormalizedUnprovabilityConsistency : T ⊬! (ConL[T]) ⟶ ~(Pr[T] ⸢(~ConL[T])⸣) := by
   by_contra H;
-  -- have : SubTheorem
-  have h₁ : T ⊢! Pr[T] ⸢~ConL[T]⸣ ⟶ ~ConL[T] := by have := imply_contra₃ H; nth_rw 2 [LConsistenncy]; simpa;
+  have h₁ : T ⊢! Pr[T] ⸢~ConL[T]⸣ ⟶ ~ConL[T] := by
+    have := imply_contra₃ (by simpa using H);
+    nth_rw 2 [LConsistenncy];
+    simpa;
   have h₂ : T ⊢! ~ConL[T] := (LoebTheorem T₀ T (~ConL[T])).mpr h₁;
   exact (NotSigmaOneSoundness_of_LConsitencyRefutability T₀ T h₂).false hSound;
 
 theorem FormalizedUnrefutabilityGoedelSentence (hG : IsGoedelSentence T₀ T G)
   : T ⊬! ConL[T] ⟶ ~Pr[T] ⸢~G⸣ := by
   by_contra H;
+  suffices : T ⊬! ConL[T] ⟶ ~Pr[T] ⸢~G⸣; aesop;
   have h₁ : T ⊢! ~G ⟷ ~ConL[T] := iff_contra $ equality_GoedelSentence_Consistency T₀ T hG;
   have h₂ : T ⊢! ~Pr[T] ⸢~ConL[T]⸣ ⟷ ~Pr[T] ⸢~G⸣ := iff_contra' $ MP (weakening $ @D2_iff T₀ T _ _ _ _ _) (hD1.D1' h₁);
-  have h₃ : T ⊬! ConL[T] ⟶ ~Pr[T] ⸢~G⸣ := unprov_imp_right_iff (FormalizedUnprovabilityConsistency T₀ T) h₂;
-  exact h₃ H;
+  exact unprov_imp_right_iff (FormalizedUnprovabilityConsistency T₀ T) h₂;
 
 end LO.FirstOrder.Arith.Incompleteness

Logic/FirstOrder/Incompleteness/Derivability/LoebWithoutIT2.lean

@@ -2,7 +2,7 @@ import Logic.FirstOrder.Incompleteness.Derivability.Theory
 import Logic.FirstOrder.Incompleteness.Derivability.Conditions
 import Logic.FirstOrder.Incompleteness.Derivability.FirstIncompleteness
 
-open LO.System
+open LO.System LO.System.Intuitionistic
 
 namespace LO.FirstOrder.Arith.Incompleteness
 
@@ -28,17 +28,17 @@ theorem LoebTheorem (σ : Sentence ℒₒᵣ) : T ⊢! σ ↔ T ⊢! (Pr[T] ⸢
     have h₂ : T ⊢! Pr[T] ⸢K ⟶ (Pr[T] ⸢K⸣ ⟶ σ)⸣ := hD1.D1' (iff_mp $ weakening hK);
     have h₃ : T ⊢! Pr[T] ⸢K⸣ ⟶ Pr[T] ⸢Pr[T] ⸢K⸣ ⟶ σ⸣ := MP hD2.D2' h₂;
     have h₄ : T ⊢! Pr[T] ⸢Pr[T] ⸢K⸣ ⟶ σ⸣ ⟶ (Pr[T] ⸢Pr[T] ⸢K⸣⸣ ⟶ Pr[T] ⸢σ⸣) := hD2.D2';
-    have h₅ : T ⊢! Pr[T] ⸢K⸣ ⟶ (Pr[T] ⸢Pr[T] ⸢K⸣⸣ ⟶ Pr[T] ⸢σ⸣) := imply_trans h₃ h₄;
+    have h₅ : T ⊢! Pr[T] ⸢K⸣ ⟶ (Pr[T] ⸢Pr[T] ⸢K⸣⸣ ⟶ Pr[T] ⸢σ⸣) := imp_trans h₃ h₄;
     have h₆ : T ⊢! Pr[T] ⸢K⸣ ⟶ Pr[T] ⸢Pr[T] ⸢K⸣⸣ := weakening $ hD3.D3';
     have h₇ : T ⊢! Pr[T] ⸢K⸣ ⟶ Pr[T] ⸢σ⸣ := imply_dilemma h₅ h₆;
-    have h₈ : T ⊢! Pr[T] ⸢K⸣ ⟶ σ := imply_trans h₇ H;
+    have h₈ : T ⊢! Pr[T] ⸢K⸣ ⟶ σ := imp_trans h₇ H;
     have h₉ : T ⊢! K := MP (iff_mpr $ weakening hK) h₈;
     exact MP h₈ (hD1.D1' h₉);
 
 /-- 2nd Incompleteness Theorem via Löb's Theorem -/
 theorem LConsistencyUnprovablility : T ⊬! (ConL[T]) := by
   by_contra hC;
-  exact hConsis.consistent.false ((LoebTheorem T₀ T (⊥ : Sentence ℒₒᵣ)).mpr $ neg_imply_bot hC).some;
+  exact hConsis.consistent.false ((LoebTheorem T₀ T (⊥ : Sentence ℒₒᵣ)).mpr $ neg_imply_bot (by simpa using hC)).some;
 
 theorem HenkinSentenceProvability (hH : IsHenkinSentence T₀ T H) : T ⊢! H := (LoebTheorem T₀ T H).mpr (iff_mpr $ weakening $ hH)
 

Logic/FirstOrder/Incompleteness/Derivability/SecondIncompleteness.lean

@@ -2,7 +2,7 @@ import Logic.FirstOrder.Incompleteness.Derivability.Theory
 import Logic.FirstOrder.Incompleteness.Derivability.Conditions
 import Logic.FirstOrder.Incompleteness.Derivability.FirstIncompleteness
 
-open LO.System
+open LO.System LO.System.Intuitionistic
 
 namespace LO.FirstOrder.Arith.Incompleteness
 
@@ -27,7 +27,7 @@ private lemma extend {σ : Sentence ℒₒᵣ}
   : (U ⊢! ConL[T] ⟶ ~Pr[T] ⸢σ⸣) ↔ (U ⊢! (Pr[T] ⸢σ⸣) ⟶ (Pr[T] ⸢~σ⸣)) := by
   apply Iff.intro;
   . intro H;
-    exact imply_contra₃ $ imply_trans (weakening $ FormalizedConsistency T₀ T (~σ)) H;
+    exact imply_contra₃ $ imp_trans (weakening $ FormalizedConsistency T₀ T (~σ)) H;
   . intro H;
     exact imply_contra₀ $ elim_and_left_dilemma (by
       have : T₀ ⊢! (Pr[T] ⸢σ⸣ ⋏ Pr[T] ⸢~σ⸣) ⟶ (Pr[T] ⸢⊥⸣) := formalized_NC' σ;
@@ -40,7 +40,7 @@ lemma formalizedGoedelSentenceUnprovablility : T ⊢! ConL[T] ⟶ ~Pr[T] ⸢G⸣
   have h₁ : T ⊢! (Pr[T] ⸢G⸣) ⟶ (Pr[T] ⸢(Pr[T] ⸢G⸣)⸣) := hD3.D3';
   have h₂ : T ⊢! Pr[T] ⸢G⸣ ⟶ ~G := weakening $ imply_contra₁ $ iff_mp hG;
   have h₃ : T ⊢! Pr[T] ⸢Pr[T] ⸢G⸣⸣ ⟶ Pr[T] ⸢~G⸣ := weakening $ @formalized_imp_intro T₀ T _ _ _ _ _ h₂;
-  exact (extend T₀ T T).mpr $ imply_trans h₁ h₃;
+  exact (extend T₀ T T).mpr $ imp_trans h₁ h₃;
 
 lemma equality_GoedelSentence_Consistency : T ⊢! G ⟷ ConL[T] := by
   have h₄ : T ⊢! ConL[T] ⟶ ~Pr[T] ⸢G⸣ := formalizedGoedelSentenceUnprovablility T₀ T hG;
@@ -54,7 +54,8 @@ theorem LConsistencyUnprovablility [hConsis : Theory.Consistent T] : T ⊬! ConL
 lemma Inconsistent_of_LConsistencyProvability : T ⊢! ConL[T] → (Theory.Inconsistent T) := by
   intro hP;
   by_contra hConsis; simp at hConsis; have := hConsis.some;
-  exact (LConsistencyUnprovablility T₀ T) hP;
+  suffices : T ⊬! ConL[T]; aesop;
+  exact LConsistencyUnprovablility T₀ T;
 
 theorem LConsistencyUnrefutability [hSound : SigmaOneSound T] : T ⊬! ~ConL[T] := by
   have ⟨G, ⟨hG, _⟩⟩ := @existsGoedelSentence T₀ T _ _ 1 _ _;
@@ -63,6 +64,7 @@ theorem LConsistencyUnrefutability [hSound : SigmaOneSound T] : T ⊬! ~ConL[T]
 lemma NotSigmaOneSoundness_of_LConsitencyRefutability : T ⊢! ~ConL[T] → IsEmpty (SigmaOneSound T) := by
   intro H;
   by_contra C; simp at C; have := C.some;
-  exact (LConsistencyUnrefutability T₀ T).elim H;
+  suffices : T ⊬! ~ConL[T]; aesop;
+  exact LConsistencyUnrefutability T₀ T;
 
 end LO.FirstOrder.Arith.Incompleteness

Logic/FirstOrder/Incompleteness/Derivability/Theory.lean

@@ -23,17 +23,15 @@ abbrev Inconsistent := IsEmpty (Theory.Consistent T)
 
 section PropositionalCalculus
 
-open System.IntuitionisticNC
+open System.Intuitionistic
 
-variable {T : Theory L} [System.IntuitionisticNC (Sentence L)]
+variable {T : Theory L} [System.Intuitionistic (Sentence L)]
 
 instance : Subtheory T (T ∪ {σ}) where
   sub := by
     intro σ' h;
     exact weakening h (by simp)
 
-infixl:50 "⊕" => modusPonens
-
 @[simp]
 lemma weakening [hs : Subtheory T₀ T] : (T₀ ⊢! σ) → (T ⊢! σ) := by
   simp;
@@ -50,56 +48,27 @@ lemma consistent_or {T} {σ : Sentence L} : (Theory.Inconsistent (T ∪ {σ})) 
 @[simp]
 lemma axm : T ∪ {σ} ⊢! σ := by sorry
 
-lemma or_intro_left : T ⊢! σ → T ⊢! σ ⋎ π := by
-  intro H;
-  exact (disj₁ _ _ _) ⊕ H;
-
-lemma or_intro_right : T ⊢! π → T ⊢! σ ⋎ π := by
-  intro H;
-  exact (disj₂ _ _ _) ⊕ H;
-
 lemma or_intro : (T ⊢! σ ∨ T ⊢! π) → T ⊢! σ ⋎ π
-  | .inl h => or_intro_left h
-  | .inr h => or_intro_right h
+  | .inl h => or_left h
+  | .inr h => or_right h
 
-lemma or_comm : T ⊢! σ ⋎ π → T ⊢! π ⋎ σ := by
-  intro H;
-  have hl := disj₁ T π σ;
-  have hr := disj₂ T π σ;
-  exact (((disj₃ T _ _ _) ⊕ hr) ⊕ hl) ⊕ H;
+lemma or_comm : T ⊢! σ ⋎ π → T ⊢! π ⋎ σ := or_symm
 
 lemma and_intro : (T ⊢! σ) → (T ⊢! π) → (T ⊢! σ ⋏ π) := by
   intro H₁ H₂;
-  exact ((conj₃ T σ π) ⊕ H₁) ⊕ H₂;
+  exact ((conj₃ T σ π) ⨀ H₁) ⨀ H₂;
 
-lemma and_comm : (T ⊢! σ ⋏ π) → (T ⊢! π ⋏ σ) := by
-  intro H;
-  have hl := (conj₁ T _ _) ⊕ H;
-  have hr := (conj₂ T _ _) ⊕ H;
-  exact ((conj₃ T π σ) ⊕ hr) ⊕ hl;
-
-lemma and_left : (T ⊢! σ ⋏ π) → (T ⊢! σ) := by
-  intro H;
-  exact (conj₁ T σ π) ⊕ H;
-
-lemma and_right : (T ⊢! σ ⋏ π) → (T ⊢! π) := λ H => and_left $ and_comm H
-
-lemma imply_decomp : (T ⊢! σ ⟶ π) → (T ⊢! σ) → (T ⊢! π) := System.IntuitionisticNC.modusPonens
+lemma imply_decomp : (T ⊢! σ ⟶ π) → (T ⊢! σ) → (T ⊢! π) := System.Intuitionistic.modus_ponens
 
 alias MP := imply_decomp
 
-lemma imply_intro_trivial {σ π} : (T ⊢! π) → (T ⊢! σ ⟶ π) := λ H => or_intro_right H
+lemma imply_intro_trivial {σ π} : (T ⊢! π) → (T ⊢! σ ⟶ π) := λ H => or_right H
 
 lemma imply_intro {σ π} : (T ⊢! σ) → ((T ⊢! σ) → (T ⊢! π)) → (T ⊢! σ ⟶ π) := λ H₁ H₂ => imply_intro_trivial (H₂ H₁)
 
 @[simp]
 lemma imply_axm : T ⊢! σ ⟶ σ := deduction.mpr axm
 
-lemma imply_trans : (T ⊢! σ ⟶ π) → (T ⊢! π ⟶ ρ) → (T ⊢! σ ⟶ ρ) := by
-  intro H₁ H₂;
-  apply deduction.mpr;
-  exact MP (weakening H₂) (deduction.mp H₁);
-
 lemma imply_contra₀ : (T ⊢! σ ⟶ π) → (T ⊢! ~π ⟶ ~σ) := by
   simp only [imp_eq, neg_neg']; intro H; exact or_comm H;
 
@@ -112,47 +81,23 @@ lemma imply_contra₂ : (T ⊢! ~σ ⟶ π) → (T ⊢! ~π ⟶ σ) := by
 lemma imply_contra₃ : (T ⊢! ~σ ⟶ ~π) → (T ⊢! π ⟶ σ) := by
   intro H; simpa using (imply_contra₀ H);
 
-
-lemma iff_comm : (T ⊢! σ ⟷ π) → (T ⊢! π ⟷ σ) := λ H => and_intro (and_right H) (and_left H)
-
-lemma iff_mp : (T ⊢! σ ⟷ π) → (T ⊢! σ ⟶ π) := λ H => and_left H
-
-lemma iff_mpr : (T ⊢! σ ⟷ π) → (T ⊢! π ⟶ σ) := λ h => iff_mp $ iff_comm h
+lemma iff_comm : (T ⊢! σ ⟷ π) → (T ⊢! π ⟷ σ) := iff_symm
 
 lemma iff_intro : (T ⊢! σ ⟶ π) → (T ⊢! π ⟶ σ) → (T ⊢! σ ⟷ π) := λ H₁ H₂ => and_intro H₁ H₂
 
 lemma iff_contra : (T ⊢! σ ⟷ π) → (T ⊢! ~σ ⟷ ~π) := λ H => iff_intro (imply_contra₀ $ iff_mpr H) (imply_contra₀ $ iff_mp H)
 
 lemma iff_contra' : (T ⊢! σ ⟷ π) → (T ⊢! ~π ⟷ ~σ) := λ H => iff_comm $ iff_contra H
 
-lemma iff_trans : (T ⊢! σ ⟷ π) → (T ⊢! π ⟷ ρ) → (T ⊢! σ ⟷ ρ) := by
-  intro H₁ H₂;
-  exact iff_intro (imply_trans (iff_mp H₁) (iff_mp H₂)) (imply_trans (iff_mpr H₂) (iff_mpr H₁));
-
-lemma iff_unprov : (T ⊢! σ ⟷ π) → (T ⊬! σ) → (T ⊬! π) := by
-  intro H Hn;
-  by_contra HC;
-  exact Hn $ MP (iff_mpr H) HC;
-
-lemma unprov_imp_left_iff : (T ⊬! σ ⟶ π) → (T ⊢! σ ⟷ ρ) → (T ⊬! ρ ⟶ π) := by
-  intro H₁ H₂;
-  by_contra HC;
-  exact H₁ $ imply_trans (iff_mp H₂) HC;
-
-lemma unprov_imp_right_iff : (T ⊬! σ ⟶ π) → (T ⊢! π ⟷ ρ) → (T ⊬! σ ⟶ ρ) := by
-  intro H₁ H₂;
-  by_contra HC;
-  exact H₁ $ imply_trans HC $ iff_mpr H₂;
-
 lemma NC : (T ⊢! σ) → (T ⊢! ~σ) → (T ⊢! ⊥) := by
   intro H₁ H₂;
-  have h₁ := imply₁ T σ ⊤ ⊕ H₁;
-  have h₂ := imply₁ T (~σ) ⊤ ⊕ H₂;
-  exact (neg₁ T ⊤ σ ⊕ h₁) ⊕ h₂;
+  have h₁ := imply₁ T σ ⊤ ⨀ H₁;
+  have h₂ := imply₁ T (~σ) ⊤ ⨀ H₂;
+  exact (neg₁ T ⊤ σ ⨀ h₁) ⨀ h₂;
 
 lemma neg_imply_bot {σ} : (T ⊢! ~σ) → (T ⊢! σ ⟶ ⊥) := by
   intro H;
-  simpa [neg_neg'] using (neg₂ T (~σ) ⊥ ⊕ H);
+  simpa [neg_neg'] using (neg₂ T (~σ) ⊥ ⨀ H);
 
 lemma neg_neg : (T ⊢! σ) ↔ (T ⊢! ~~σ) := by simp;
 

Logic/Logic/HilbertStyle.lean

@@ -18,6 +18,8 @@ class Intuitionistic (F : Type u) [LogicSymbol F] [System F] where
   disj₃       (T : Set F) (p q r : F) : T ⊢! (p ⟶ r) ⟶ (q ⟶ r) ⟶ p ⋎ q ⟶ r
   neg₁        (T : Set F) (p q : F)   : T ⊢! (p ⟶ q) ⟶ (p ⟶ ~q) ⟶ ~p
   neg₂        (T : Set F) (p q : F)   : T ⊢! p ⟶ ~p ⟶ q
+  -- MEMO: `⊤ = ~⊥`であることを要請すれば`neg₂`から明らか
+  efq         (T : Set F) (p : F)     : T ⊢! ⊥ ⟶ p
 
 variable {Struc : Type w → Type v} [𝓢 : Semantics F Struc]
 
@@ -38,6 +40,7 @@ instance [LO.Complete F] : Intuitionistic F where
   disj₃  := fun T p q r => Complete.consequence_iff_provable.mp (fun _ _ _ _ => by simpa using Or.rec)
   neg₁   := fun T p q => Complete.consequence_iff_provable.mp (fun _ _ _ _ => by simp; exact fun a b c => (b c) (a c))
   neg₂   := fun T p q => Complete.consequence_iff_provable.mp (fun _ _ _ _ => by simp; exact fun a b => (b a).elim)
+  efq    := fun T p => Complete.consequence_iff_provable.mp (fun _ _ _ _ => by simp)
 
 namespace Intuitionistic
 
@@ -58,13 +61,40 @@ lemma and_left {p q : F} (h : T ⊢! p ⋏ q) : T ⊢! p := conj₁ T p q ⨀ h
 
 lemma and_right {p q : F} (h : T ⊢! p ⋏ q) : T ⊢! q := conj₂ T p q ⨀ h
 
+lemma and_symm {p q : F} (h : T ⊢! p ⋏ q) : T ⊢! q ⋏ p := and_split (and_right h) (and_left h)
+
+lemma or_left {p q : F} (h : T ⊢! p) : T ⊢! p ⋎ q := disj₁ T p q ⨀ h
+
+lemma or_right {p q : F} (h : T ⊢! q) : T ⊢! p ⋎ q := disj₂ T p q ⨀ h
+
+lemma or_symm {p q : F} (h : T ⊢! p ⋎ q) : T ⊢! q ⋎ p := (disj₃ T _ _ _) ⨀ (disj₂ _ _ _) ⨀ (disj₁ _ _ _) ⨀ h
+
 lemma iff_refl (p : F) : T ⊢! p ⟷ p := and_split (imp_id p) (imp_id p)
 
 lemma iff_symm {p q : F} (h : T ⊢! p ⟷ q) : T ⊢! q ⟷ p := and_split (and_right h) (and_left h)
 
 lemma iff_trans {p q r : F} (hp : T ⊢! p ⟷ q) (hq : T ⊢! q ⟷ r) : T ⊢! p ⟷ r :=
   and_split (imp_trans (and_left hp) (and_left hq)) (imp_trans (and_right hq) (and_right hp))
 
+lemma iff_mp {p q : F} (h : T ⊢! p ⟷ q) : T ⊢! p ⟶ q := and_left h
+
+lemma iff_mpr {p q : F} (h : T ⊢! p ⟷ q) : T ⊢! q ⟶ p := and_right h
+
+lemma iff_unprov {p q : F} (h₁ : T ⊢! p ⟷ q) (h₂ : T ⊬! p) : T ⊬! q := by
+  by_contra hC;
+  suffices : T ⊢! p; aesop;
+  exact (iff_mpr h₁) ⨀ (by simpa using hC);
+
+lemma unprov_imp_left_iff (h₁ : T ⊬! σ ⟶ π) (h₂ : T ⊢! σ ⟷ ρ): (T ⊬! ρ ⟶ π) := by
+  by_contra HC;
+  suffices : T ⊢! σ ⟶ π; simp_all only [not_isEmpty_of_nonempty];
+  exact imp_trans (iff_mp h₂) (by simpa using HC);
+
+lemma unprov_imp_right_iff (h₁ : T ⊬! σ ⟶ π) (h₂ : T ⊢! π ⟷ ρ): (T ⊬! σ ⟶ ρ) := by
+  by_contra HC;
+  suffices : T ⊢! σ ⟶ π; simp_all only [not_isEmpty_of_nonempty];
+  exact imp_trans (by simpa using HC) (iff_mpr h₂);
+
 end Intuitionistic
 
 end System

Logic/Logic/System.lean

@@ -42,6 +42,9 @@ abbrev Unprovable (T : Set F) (f : F) : Prop := IsEmpty (T ⊢ f)
 
 infix:45 " ⊬ " => System.Unprovable
 
+-- TODO: 互換性のために残している
+infix:45 " ⊬! " => System.Unprovable
+
 lemma unprovable_iff_not_provable {T : Set F} {f : F} : T ⊬ f ↔ ¬T ⊢! f := by simp[System.Unprovable]
 
 protected def Complete (T : Set F) : Prop := ∀ f, (T ⊢! f) ∨ (T ⊢! ~f)