diff --git a/Incompleteness/Arith/D1.lean b/Incompleteness/Arith/D1.lean
index d7852d6..a254126 100644
--- a/Incompleteness/Arith/D1.lean
+++ b/Incompleteness/Arith/D1.lean
@@ -351,7 +351,7 @@ lemma Language.Theory.Derivation.sound {d : ℕ} (h : (T.codeIn ℕ).Derivation
     have : Δ₁ = (p ⫽ Γ) := Sequent.quote_inj (V := ℕ) <| by simp [hΔ₁, h₁]
     rcases this
     rcases ih d₂ (by simp) dd₂ with ⟨Δ₂, hΔ₂, ⟨b₂⟩⟩
-    have : Δ₂ = (~p ⫽ Γ) := Sequent.quote_inj (V := ℕ) <| by simp [hΔ₂, h₂]
+    have : Δ₂ = (∼p ⫽ Γ) := Sequent.quote_inj (V := ℕ) <| by simp [hΔ₂, h₂]
     rcases this
     refine ⟨Derivation2.cut b₁ b₂⟩
   · rcases by simpa using hΓ
diff --git a/Incompleteness/Arith/First.lean b/Incompleteness/Arith/First.lean
index 2ec8fd9..a13d8ca 100644
--- a/Incompleteness/Arith/First.lean
+++ b/Incompleteness/Arith/First.lean
@@ -19,7 +19,7 @@ lemma re_iff_sigma1 {P : ℕ → Prop} : RePred P ↔ 𝚺₁-Predicate P := by
 variable (T : Theory ℒₒᵣ) [𝐑₀ ≼ T] [Sigma1Sound T] [T.Delta1Definable]
 
 theorem incomplete : ¬System.Complete T  := by
-  let D : ℕ → Prop := fun n : ℕ ↦ ∃ p : SyntacticSemiformula ℒₒᵣ 1, n = ⌜p⌝ ∧ T ⊢! ~p/[⌜p⌝]
+  let D : ℕ → Prop := fun n : ℕ ↦ ∃ p : SyntacticSemiformula ℒₒᵣ 1, n = ⌜p⌝ ∧ T ⊢! ∼p/[⌜p⌝]
   have D_re : RePred D := by
     have : 𝚺₁-Predicate fun p : ℕ ↦
       ⌜ℒₒᵣ⌝.IsSemiformula 1 p ∧ (T.codeIn ℕ).Provable (⌜ℒₒᵣ⌝.neg <| ⌜ℒₒᵣ⌝.substs ?[numeral p] p) := by definability
@@ -34,12 +34,12 @@ theorem incomplete : ¬System.Complete T  := by
   let ρ : SyntacticFormula ℒₒᵣ := σ/[⌜σ⌝]
   have : ∀ n : ℕ, D n ↔ T ⊢! σ/[‘↑n’] := fun n ↦ by
     simpa [Semiformula.coe_substs_eq_substs_coe₁] using re_complete (T := T) (D_re) (x := n)
-  have : T ⊢! ~ρ ↔ T ⊢! ρ := by
+  have : T ⊢! ∼ρ ↔ T ⊢! ρ := by
     simpa [D, goedelNumber'_def, quote_eq_encode] using this ⌜σ⌝
   have con : System.Consistent T := consistent_of_sigma1Sound T
   refine LO.System.incomplete_iff_exists_undecidable.mpr ⟨↑ρ, ?_, ?_⟩
   · intro h
-    have : T ⊢! ~↑ρ := by simpa [provable₀_iff] using this.mpr h
+    have : T ⊢! ∼↑ρ := by simpa [provable₀_iff] using this.mpr h
     exact LO.System.not_consistent_iff_inconsistent.mpr (inconsistent_of_provable_of_unprovable h this) inferInstance
   · intro h
     have : T ⊢! ↑ρ := this.mp (by simpa [provable₀_iff] using h)
diff --git a/Incompleteness/Arith/FormalizedArithmetic.lean b/Incompleteness/Arith/FormalizedArithmetic.lean
index e8c7a65..c8815c5 100644
--- a/Incompleteness/Arith/FormalizedArithmetic.lean
+++ b/Incompleteness/Arith/FormalizedArithmetic.lean
@@ -35,11 +35,11 @@ variable {V}
 
 class R₀Theory (T : LOR.TTheory (V := V)) where
   refl : T ⊢ (#'0 =' #'0).all
-  replace (p : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) : T ⊢ (#'1 =' #'0 ⟶ p^/[(#'1).sing] ⟶ p^/[(#'0).sing]).all.all
+  replace (p : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) : T ⊢ (#'1 =' #'0 ➝ p^/[(#'1).sing] ➝ p^/[(#'0).sing]).all.all
   add (n m : V) : T ⊢ (n + m : ⌜ℒₒᵣ⌝[V].Semiterm 0) =' ↑(n + m)
   mul (n m : V) : T ⊢ (n * m : ⌜ℒₒᵣ⌝[V].Semiterm 0) =' ↑(n * m)
   ne {n m : V} : n ≠ m → T ⊢ ↑n ≠' ↑m
-  ltNumeral (n : V) : T ⊢ (#'0 <' ↑n ⟷ (tSubstItr (#'0).sing (#'1 =' #'0) n).disj).all
+  ltNumeral (n : V) : T ⊢ (#'0 <' ↑n ⭤ (tSubstItr (#'0).sing (#'1 =' #'0) n).disj).all
 
 abbrev oneAbbrev {n} : ⌜ℒₒᵣ⌝[V].Semiterm n := (1 : V)
 
@@ -71,74 +71,74 @@ def eqRefl (t : ⌜ℒₒᵣ⌝.Term) : T ⊢ t =' t := by
 lemma eq_refl! (t : ⌜ℒₒᵣ⌝.Term) : T ⊢! t =' t := ⟨eqRefl T t⟩
 
 noncomputable def replace (p : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (t u : ⌜ℒₒᵣ⌝.Term) :
-    T ⊢ t =' u ⟶ p^/[t.sing] ⟶ p^/[u.sing] := by
-  have : T ⊢ (#'1 =' #'0 ⟶ p^/[(#'1).sing] ⟶ p^/[(#'0).sing]).all.all := R₀Theory.replace p
+    T ⊢ t =' u ➝ p^/[t.sing] ➝ p^/[u.sing] := by
+  have : T ⊢ (#'1 =' #'0 ➝ p^/[(#'1).sing] ➝ p^/[(#'0).sing]).all.all := R₀Theory.replace p
   have := by simpa using specialize this t
   simpa [Language.SemitermVec.q_of_pos, Language.Semiformula.substs₁,
     Language.TSemifromula.substs_substs] using specialize this u
 
-lemma replace! (p : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (t u : ⌜ℒₒᵣ⌝.Term) : T ⊢! t =' u ⟶ p^/[t.sing] ⟶ p^/[u.sing] := ⟨replace T p t u⟩
+lemma replace! (p : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (t u : ⌜ℒₒᵣ⌝.Term) : T ⊢! t =' u ➝ p^/[t.sing] ➝ p^/[u.sing] := ⟨replace T p t u⟩
 
-def eqSymm (t₁ t₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢ t₁ =' t₂ ⟶ t₂ =' t₁ := by
+def eqSymm (t₁ t₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢ t₁ =' t₂ ➝ t₂ =' t₁ := by
   apply deduct'
   let Γ := [t₁ =' t₂]
   have e₁ : Γ ⊢[T] t₁ =' t₂ := FiniteContext.byAxm (by simp [Γ])
   have e₂ : Γ ⊢[T] t₁ =' t₁ := of <| eqRefl T t₁
-  have : Γ ⊢[T] t₁ =' t₂ ⟶ t₁ =' t₁ ⟶ t₂ =' t₁ := of <| by
+  have : Γ ⊢[T] t₁ =' t₂ ➝ t₁ =' t₁ ➝ t₂ =' t₁ := of <| by
     simpa using replace T (#'0 =' t₁.bShift) t₁ t₂
   exact this ⨀ e₁ ⨀ e₂
 
-lemma eq_symm! (t₁ t₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢! t₁ =' t₂ ⟶ t₂ =' t₁ := ⟨eqSymm T t₁ t₂⟩
+lemma eq_symm! (t₁ t₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢! t₁ =' t₂ ➝ t₂ =' t₁ := ⟨eqSymm T t₁ t₂⟩
 
 lemma eq_symm'! {t₁ t₂ : ⌜ℒₒᵣ⌝.Term} (h : T ⊢! t₁ =' t₂) : T ⊢! t₂ =' t₁ := eq_symm! T t₁ t₂ ⨀ h
 
-def eqTrans (t₁ t₂ t₃ : ⌜ℒₒᵣ⌝.Term) : T ⊢ t₁ =' t₂ ⟶ t₂ =' t₃ ⟶ t₁ =' t₃ := by
+def eqTrans (t₁ t₂ t₃ : ⌜ℒₒᵣ⌝.Term) : T ⊢ t₁ =' t₂ ➝ t₂ =' t₃ ➝ t₁ =' t₃ := by
   apply deduct'
   apply deduct
   let Γ := [t₂ =' t₃, t₁ =' t₂]
   have e₁ : Γ ⊢[T] t₁ =' t₂ := FiniteContext.byAxm (by simp [Γ])
   have e₂ : Γ ⊢[T] t₂ =' t₃ := FiniteContext.byAxm (by simp [Γ])
-  have : Γ ⊢[T] t₂ =' t₃ ⟶ t₁ =' t₂ ⟶ t₁ =' t₃ := of <| by
+  have : Γ ⊢[T] t₂ =' t₃ ➝ t₁ =' t₂ ➝ t₁ =' t₃ := of <| by
     simpa using replace T (t₁.bShift =' #'0) t₂ t₃
   exact this ⨀ e₂ ⨀ e₁
 
-lemma eq_trans! (t₁ t₂ t₃ : ⌜ℒₒᵣ⌝.Term) : T ⊢! t₁ =' t₂ ⟶ t₂ =' t₃ ⟶ t₁ =' t₃ := ⟨eqTrans T t₁ t₂ t₃⟩
+lemma eq_trans! (t₁ t₂ t₃ : ⌜ℒₒᵣ⌝.Term) : T ⊢! t₁ =' t₂ ➝ t₂ =' t₃ ➝ t₁ =' t₃ := ⟨eqTrans T t₁ t₂ t₃⟩
 
-noncomputable def addExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢ t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ (t₁ + u₁) =' (t₂ + u₂) := by
+noncomputable def addExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢ t₁ =' t₂ ➝ u₁ =' u₂ ➝ (t₁ + u₁) =' (t₂ + u₂) := by
   apply deduct'
   apply deduct
   let Γ := [u₁ =' u₂, t₁ =' t₂]
   have bt : Γ ⊢[T] t₁ =' t₂ := FiniteContext.byAxm <| by simp [Γ]
   have bu : Γ ⊢[T] u₁ =' u₂ := FiniteContext.byAxm <| by simp [Γ]
-  have : T ⊢ t₁ =' t₂ ⟶ (t₁ + u₁) =' (t₁ + u₁) ⟶ (t₁ + u₁) =' (t₂ + u₁) := by
+  have : T ⊢ t₁ =' t₂ ➝ (t₁ + u₁) =' (t₁ + u₁) ➝ (t₁ + u₁) =' (t₂ + u₁) := by
     have := replace T ((t₁.bShift + u₁.bShift) =' (#'0 + u₁.bShift)) t₁ t₂
     simpa using this
   have b : Γ ⊢[T] (t₁ + u₁) =' (t₂ + u₁) := of (Γ := Γ) this ⨀ bt ⨀ of (eqRefl _ _)
-  have : T ⊢ u₁ =' u₂ ⟶ (t₁ + u₁) =' (t₂ + u₁) ⟶ (t₁ + u₁) =' (t₂ + u₂) := by
+  have : T ⊢ u₁ =' u₂ ➝ (t₁ + u₁) =' (t₂ + u₁) ➝ (t₁ + u₁) =' (t₂ + u₂) := by
     have := replace T ((t₁.bShift + u₁.bShift) =' (t₂.bShift + #'0)) u₁ u₂
     simpa using this
   exact of (Γ := Γ) this ⨀ bu ⨀ b
 
-lemma add_ext! (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢! t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ (t₁ + u₁) =' (t₂ + u₂) := ⟨addExt T t₁ t₂ u₁ u₂⟩
+lemma add_ext! (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢! t₁ =' t₂ ➝ u₁ =' u₂ ➝ (t₁ + u₁) =' (t₂ + u₂) := ⟨addExt T t₁ t₂ u₁ u₂⟩
 
-noncomputable def mulExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢ t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ (t₁ * u₁) =' (t₂ * u₂) := by
+noncomputable def mulExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢ t₁ =' t₂ ➝ u₁ =' u₂ ➝ (t₁ * u₁) =' (t₂ * u₂) := by
   apply deduct'
   apply deduct
   let Γ := [u₁ =' u₂, t₁ =' t₂]
   have bt : Γ ⊢[T] t₁ =' t₂ := FiniteContext.byAxm <| by simp [Γ]
   have bu : Γ ⊢[T] u₁ =' u₂ := FiniteContext.byAxm <| by simp [Γ]
-  have : T ⊢ t₁ =' t₂ ⟶ (t₁ * u₁) =' (t₁ * u₁) ⟶ (t₁ * u₁) =' (t₂ * u₁) := by
+  have : T ⊢ t₁ =' t₂ ➝ (t₁ * u₁) =' (t₁ * u₁) ➝ (t₁ * u₁) =' (t₂ * u₁) := by
     have := replace T ((t₁.bShift * u₁.bShift) =' (#'0 * u₁.bShift)) t₁ t₂
     simpa using this
   have b : Γ ⊢[T] (t₁ * u₁) =' (t₂ * u₁) := of (Γ := Γ) this ⨀ bt ⨀ of (eqRefl _ _)
-  have : T ⊢ u₁ =' u₂ ⟶ (t₁ * u₁) =' (t₂ * u₁) ⟶ (t₁ * u₁) =' (t₂ * u₂) := by
+  have : T ⊢ u₁ =' u₂ ➝ (t₁ * u₁) =' (t₂ * u₁) ➝ (t₁ * u₁) =' (t₂ * u₂) := by
     have := replace T ((t₁.bShift * u₁.bShift) =' (t₂.bShift * #'0)) u₁ u₂
     simpa using this
   exact of (Γ := Γ) this ⨀ bu ⨀ b
 
-lemma mul_ext! (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢! t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ (t₁ * u₁) =' (t₂ * u₂) := ⟨mulExt T t₁ t₂ u₁ u₂⟩
+lemma mul_ext! (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢! t₁ =' t₂ ➝ u₁ =' u₂ ➝ (t₁ * u₁) =' (t₂ * u₂) := ⟨mulExt T t₁ t₂ u₁ u₂⟩
 
-noncomputable def eqExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢ t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ t₁ =' u₁ ⟶ t₂ =' u₂ := by
+noncomputable def eqExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢ t₁ =' t₂ ➝ u₁ =' u₂ ➝ t₁ =' u₁ ➝ t₂ =' u₂ := by
   apply deduct'
   apply deduct
   apply deduct
@@ -149,10 +149,10 @@ noncomputable def eqExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢ t
   have e3 : Γ ⊢[T] u₁ =' u₂ := FiniteContext.byAxm (by simp [Γ])
   exact (of <| eqTrans T t₂ u₁ u₂) ⨀ ((of <| eqTrans T t₂ t₁ u₁) ⨀ e1 ⨀ e2) ⨀ e3
 
-lemma eq_ext (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢! t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ t₁ =' u₁ ⟶ t₂ =' u₂ :=
+lemma eq_ext (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢! t₁ =' t₂ ➝ u₁ =' u₂ ➝ t₁ =' u₁ ➝ t₂ =' u₂ :=
   ⟨eqExt T t₁ t₂ u₁ u₂⟩
 
-noncomputable def neExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢ t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ t₁ ≠' u₁ ⟶ t₂ ≠' u₂ := by
+noncomputable def neExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢ t₁ =' t₂ ➝ u₁ =' u₂ ➝ t₁ ≠' u₁ ➝ t₂ ≠' u₂ := by
   apply deduct'
   apply deduct
   apply deduct
@@ -160,18 +160,18 @@ noncomputable def neExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢ t
   have bt : Γ ⊢[T] t₁ =' t₂ := FiniteContext.byAxm <| by simp [Γ]
   have bu : Γ ⊢[T] u₁ =' u₂ := FiniteContext.byAxm <| by simp [Γ]
   have bl : Γ ⊢[T] t₁ ≠' u₁ := FiniteContext.byAxm <| by simp [Γ]
-  have : T ⊢ t₁ =' t₂ ⟶ t₁ ≠' u₁ ⟶ t₂ ≠' u₁ := by
+  have : T ⊢ t₁ =' t₂ ➝ t₁ ≠' u₁ ➝ t₂ ≠' u₁ := by
     have := replace T (#'0 ≠' u₁.bShift) t₁ t₂
     simpa using this
   have b : Γ ⊢[T] t₂ ≠' u₁ := of (Γ := Γ) this ⨀ bt ⨀ bl
-  have : T ⊢ u₁ =' u₂ ⟶ t₂ ≠' u₁ ⟶ t₂ ≠' u₂ := by
+  have : T ⊢ u₁ =' u₂ ➝ t₂ ≠' u₁ ➝ t₂ ≠' u₂ := by
     simpa using replace T (t₂.bShift ≠' #'0) u₁ u₂
   exact of (Γ := Γ) this ⨀ bu ⨀ b
 
-lemma ne_ext (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢! t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ t₁ ≠' u₁ ⟶ t₂ ≠' u₂ :=
+lemma ne_ext (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢! t₁ =' t₂ ➝ u₁ =' u₂ ➝ t₁ ≠' u₁ ➝ t₂ ≠' u₂ :=
   ⟨neExt T t₁ t₂ u₁ u₂⟩
 
-noncomputable def ltExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢ t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ t₁ <' u₁ ⟶ t₂ <' u₂ := by
+noncomputable def ltExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢ t₁ =' t₂ ➝ u₁ =' u₂ ➝ t₁ <' u₁ ➝ t₂ <' u₂ := by
   apply deduct'
   apply deduct
   apply deduct
@@ -179,18 +179,18 @@ noncomputable def ltExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢ t
   have bt : Γ ⊢[T] t₁ =' t₂ := FiniteContext.byAxm <| by simp [Γ]
   have bu : Γ ⊢[T] u₁ =' u₂ := FiniteContext.byAxm <| by simp [Γ]
   have bl : Γ ⊢[T] t₁ <' u₁ := FiniteContext.byAxm <| by simp [Γ]
-  have : T ⊢ t₁ =' t₂ ⟶ t₁ <' u₁ ⟶ t₂ <' u₁ := by
+  have : T ⊢ t₁ =' t₂ ➝ t₁ <' u₁ ➝ t₂ <' u₁ := by
     have := replace T (#'0 <' u₁.bShift) t₁ t₂
     simpa using this
   have b : Γ ⊢[T] t₂ <' u₁ := of (Γ := Γ) this ⨀ bt ⨀ bl
-  have : T ⊢ u₁ =' u₂ ⟶ t₂ <' u₁ ⟶ t₂ <' u₂ := by
+  have : T ⊢ u₁ =' u₂ ➝ t₂ <' u₁ ➝ t₂ <' u₂ := by
     have := replace T (t₂.bShift <' #'0) u₁ u₂
     simpa using this
   exact of (Γ := Γ) this ⨀ bu ⨀ b
 
-lemma lt_ext! (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢! t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ t₁ <' u₁ ⟶ t₂ <' u₂ := ⟨ltExt T t₁ t₂ u₁ u₂⟩
+lemma lt_ext! (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢! t₁ =' t₂ ➝ u₁ =' u₂ ➝ t₁ <' u₁ ➝ t₂ <' u₂ := ⟨ltExt T t₁ t₂ u₁ u₂⟩
 
-noncomputable def nltExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢ t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ t₁ ≮' u₁ ⟶ t₂ ≮' u₂ := by
+noncomputable def nltExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢ t₁ =' t₂ ➝ u₁ =' u₂ ➝ t₁ ≮' u₁ ➝ t₂ ≮' u₂ := by
   apply deduct'
   apply deduct
   apply deduct
@@ -198,30 +198,30 @@ noncomputable def nltExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢ t
   have bt : Γ ⊢[T] t₁ =' t₂ := FiniteContext.byAxm <| by simp [Γ]
   have bu : Γ ⊢[T] u₁ =' u₂ := FiniteContext.byAxm <| by simp [Γ]
   have bl : Γ ⊢[T] t₁ ≮' u₁ := FiniteContext.byAxm <| by simp [Γ]
-  have : T ⊢ t₁ =' t₂ ⟶ t₁ ≮' u₁ ⟶ t₂ ≮' u₁ := by
+  have : T ⊢ t₁ =' t₂ ➝ t₁ ≮' u₁ ➝ t₂ ≮' u₁ := by
     have := replace T (#'0 ≮' u₁.bShift) t₁ t₂
     simpa using this
   have b : Γ ⊢[T] t₂ ≮' u₁ := of (Γ := Γ) this ⨀ bt ⨀ bl
-  have : T ⊢ u₁ =' u₂ ⟶ t₂ ≮' u₁ ⟶ t₂ ≮' u₂ := by
+  have : T ⊢ u₁ =' u₂ ➝ t₂ ≮' u₁ ➝ t₂ ≮' u₂ := by
     have := replace T (t₂.bShift ≮' #'0) u₁ u₂
     simpa using this
   exact of (Γ := Γ) this ⨀ bu ⨀ b
 
-lemma nlt_ext (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢! t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ t₁ ≮' u₁ ⟶ t₂ ≮' u₂ := ⟨nltExt T t₁ t₂ u₁ u₂⟩
+lemma nlt_ext (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢! t₁ =' t₂ ➝ u₁ =' u₂ ➝ t₁ ≮' u₁ ➝ t₂ ≮' u₂ := ⟨nltExt T t₁ t₂ u₁ u₂⟩
 
 noncomputable def ballReplace (p : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (t u : ⌜ℒₒᵣ⌝.Term) :
-    T ⊢ t =' u ⟶ p.ball t ⟶ p.ball u := by
+    T ⊢ t =' u ➝ p.ball t ➝ p.ball u := by
   simpa [Language.TSemifromula.substs_substs] using replace T ((p^/[(#'0).sing]).ball #'0) t u
 
 lemma ball_replace! (p : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (t u : ⌜ℒₒᵣ⌝.Term) :
-    T ⊢! t =' u ⟶ p.ball t ⟶ p.ball u := ⟨ballReplace T p t u⟩
+    T ⊢! t =' u ➝ p.ball t ➝ p.ball u := ⟨ballReplace T p t u⟩
 
 noncomputable def bexReplace (p : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (t u : ⌜ℒₒᵣ⌝.Term) :
-    T ⊢ t =' u ⟶ p.bex t ⟶ p.bex u := by
+    T ⊢ t =' u ➝ p.bex t ➝ p.bex u := by
   simpa [Language.TSemifromula.substs_substs] using replace T ((p^/[(#'0).sing]).bex #'0) t u
 
 lemma bex_replace! (p : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (t u : ⌜ℒₒᵣ⌝.Term) :
-    T ⊢! t =' u ⟶ p.bex t ⟶ p.bex u := ⟨bexReplace T p t u⟩
+    T ⊢! t =' u ➝ p.bex t ➝ p.bex u := ⟨bexReplace T p t u⟩
 
 def eqComplete {n m : V} (h : n = m) : T ⊢ ↑n =' ↑m := by
   rcases h; exact eqRefl T _
@@ -240,15 +240,15 @@ def neComplete {n m : V} (h : n ≠ m) : T ⊢ ↑n ≠' ↑m := R₀Theory.ne h
 
 lemma ne_complete! {n m : V} (h : n ≠ m) : T ⊢! ↑n ≠' ↑m := ⟨neComplete T h⟩
 
-def ltNumeral (t : ⌜ℒₒᵣ⌝.Term) (n : V) : T ⊢ t <' ↑n ⟷ (tSubstItr t.sing (#'1 =' #'0) n).disj := by
-  have : T ⊢ (#'0 <' ↑n ⟷ (tSubstItr (#'0).sing (#'1 =' #'0) n).disj).all := R₀Theory.ltNumeral n
+def ltNumeral (t : ⌜ℒₒᵣ⌝.Term) (n : V) : T ⊢ t <' ↑n ⭤ (tSubstItr t.sing (#'1 =' #'0) n).disj := by
+  have : T ⊢ (#'0 <' ↑n ⭤ (tSubstItr (#'0).sing (#'1 =' #'0) n).disj).all := R₀Theory.ltNumeral n
   simpa [Language.SemitermVec.q_of_pos, Language.Semiformula.substs₁] using specialize this t
 
-noncomputable def nltNumeral (t : ⌜ℒₒᵣ⌝.Term) (n : V) : T ⊢ t ≮' ↑n ⟷ (tSubstItr t.sing (#'1 ≠' #'0) n).conj := by
+noncomputable def nltNumeral (t : ⌜ℒₒᵣ⌝.Term) (n : V) : T ⊢ t ≮' ↑n ⭤ (tSubstItr t.sing (#'1 ≠' #'0) n).conj := by
   simpa using negReplaceIff' <| ltNumeral T t n
 
 def ltComplete {n m : V} (h : n < m) : T ⊢ ↑n <' ↑m := by
-  have : T ⊢ ↑n <' ↑m ⟷ _ := ltNumeral T n m
+  have : T ⊢ ↑n <' ↑m ⭤ _ := ltNumeral T n m
   apply andRight this ⨀ ?_
   apply disj (i := m - (n + 1)) _ (by simpa using sub_succ_lt_self (by simp [h]))
   simpa [nth_tSubstItr', h] using eqRefl T ↑n
@@ -256,7 +256,7 @@ def ltComplete {n m : V} (h : n < m) : T ⊢ ↑n <' ↑m := by
 lemma lt_complete! {n m : V} (h : n < m) : T ⊢! ↑n <' ↑m := ⟨ltComplete T h⟩
 
 noncomputable def nltComplete {n m : V} (h : m ≤ n) : T ⊢ ↑n ≮' ↑m := by
-  have : T ⊢ ↑n ≮' ↑m ⟷ (tSubstItr (↑n : ⌜ℒₒᵣ⌝.Term).sing (#'1 ≠' #'0) m).conj := by
+  have : T ⊢ ↑n ≮' ↑m ⭤ (tSubstItr (↑n : ⌜ℒₒᵣ⌝.Term).sing (#'1 ≠' #'0) m).conj := by
     simpa using negReplaceIff' <| ltNumeral T n m
   refine andRight this ⨀ ?_
   apply conj'
diff --git a/Incompleteness/Arith/Second.lean b/Incompleteness/Arith/Second.lean
index d0877c1..b4fa1e3 100644
--- a/Incompleteness/Arith/Second.lean
+++ b/Incompleteness/Arith/Second.lean
@@ -60,7 +60,7 @@ lemma fixpoint_eq (θ : Semisentence ℒₒᵣ 1) :
   simp [fixpoint, substs_diag]
 
 theorem diagonal (θ : Semisentence ℒₒᵣ 1) :
-    T ⊢!. fixpoint θ ⟷ θ/[⌜fixpoint θ⌝] :=
+    T ⊢!. fixpoint θ ⭤ θ/[⌜fixpoint θ⌝] :=
   haveI : 𝐄𝐐 ≼ T := System.Subtheory.comp (𝓣 := 𝐈𝚺₁) inferInstance inferInstance
   complete (T := T) <| oRing_consequence_of _ _ fun (V : Type) _ _ ↦ by
     haveI : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V 𝐈𝚺₁ T inferInstance inferInstance
@@ -79,9 +79,9 @@ variable (U : Theory ℒₒᵣ) [U.Delta1Definable]
 
 abbrev _root_.LO.FirstOrder.Theory.bewₐ (σ : Sentence ℒₒᵣ) : Sentence ℒₒᵣ := U.provableₐ/[⌜σ⌝]
 
-abbrev _root_.LO.FirstOrder.Theory.consistentₐ : Sentence ℒₒᵣ := ~U.bewₐ ⊥
+abbrev _root_.LO.FirstOrder.Theory.consistentₐ : Sentence ℒₒᵣ := ∼U.bewₐ ⊥
 
-def _root_.LO.FirstOrder.Theory.goedelₐ : Sentence ℒₒᵣ := fixpoint (~U.provableₐ)
+def _root_.LO.FirstOrder.Theory.goedelₐ : Sentence ℒₒᵣ := fixpoint (∼U.provableₐ)
 
 end
 
@@ -96,7 +96,7 @@ theorem provableₐ_D1 {σ} : U ⊢!. σ → T ⊢!. U.bewₐ σ := by
     haveI : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V _ T inferInstance inferInstance
     simpa [models_iff] using provableₐ_of_provable (T := U) (V := V) h
 
-theorem provableₐ_D2 {σ π} : T ⊢!. U.bewₐ (σ ⟶ π) ⟶ U.bewₐ σ ⟶ U.bewₐ π :=
+theorem provableₐ_D2 {σ π} : T ⊢!. U.bewₐ (σ ➝ π) ➝ U.bewₐ σ ➝ U.bewₐ π :=
   haveI : 𝐄𝐐 ≼ T := System.Subtheory.comp (𝓣 := 𝐈𝚺₁) inferInstance inferInstance
   complete (T := T) <| oRing_consequence_of _ _ fun (V : Type) _ _ ↦ by
     haveI : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V _ T inferInstance inferInstance
@@ -105,21 +105,21 @@ theorem provableₐ_D2 {σ π} : T ⊢!. U.bewₐ (σ ⟶ π) ⟶ U.bewₐ σ 
     exact provableₐ_iff.mpr <| (by simpa using provableₐ_iff.mp hσπ) ⨀ provableₐ_iff.mp hσ
 
 lemma provableₐ_sigma₁_complete {σ : Sentence ℒₒᵣ} (hσ : Hierarchy 𝚺 1 σ) :
-    T ⊢!. σ ⟶ U.bewₐ σ :=
+    T ⊢!. σ ➝ U.bewₐ σ :=
   haveI : 𝐄𝐐 ≼ T := System.Subtheory.comp (𝓣 := 𝐈𝚺₁) inferInstance inferInstance
   complete (T := T) <| oRing_consequence_of _ _ fun (V : Type) _ _ ↦ by
     haveI : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V _ T inferInstance inferInstance
     simpa [models_iff] using sigma₁_complete (T := U) (V := V) hσ
 
 theorem provableₐ_D3 {σ : Sentence ℒₒᵣ} :
-    T ⊢!. U.bewₐ σ ⟶ U.bewₐ (U.bewₐ σ) := provableₐ_sigma₁_complete (by simp)
+    T ⊢!. U.bewₐ σ ➝ U.bewₐ (U.bewₐ σ) := provableₐ_sigma₁_complete (by simp)
 
-lemma goedel_iff_unprovable_goedel : T ⊢!. U.goedelₐ ⟷ ~U.bewₐ U.goedelₐ := by
-  simpa [Theory.goedelₐ, Theory.bewₐ] using diagonal (~U.provableₐ)
+lemma goedel_iff_unprovable_goedel : T ⊢!. U.goedelₐ ⭤ ∼U.bewₐ U.goedelₐ := by
+  simpa [Theory.goedelₐ, Theory.bewₐ] using diagonal (∼U.provableₐ)
 
 open LO.System LO.System.FiniteContext
 
-lemma provableₐ_D2_context {Γ σ π} (hσπ : Γ ⊢[T.alt]! (U.bewₐ (σ ⟶ π))) (hσ : Γ ⊢[T.alt]! U.bewₐ σ) :
+lemma provableₐ_D2_context {Γ σ π} (hσπ : Γ ⊢[T.alt]! (U.bewₐ (σ ➝ π))) (hσ : Γ ⊢[T.alt]! U.bewₐ σ) :
     Γ ⊢[T.alt]! U.bewₐ π := of'! provableₐ_D2 ⨀ hσπ ⨀ hσ
 
 lemma provableₐ_D3_context {Γ σ} (hσπ : Γ ⊢[T.alt]! U.bewₐ σ) : Γ ⊢[T.alt]! U.bewₐ (U.bewₐ σ) := of'! provableₐ_D3 ⨀ hσπ
@@ -146,40 +146,40 @@ local notation "𝗖𝗼𝗻" => T.consistentₐ
 
 local prefix:max "□" => T.bewₐ
 
-lemma goedel_unprovable [System.Consistent T] : T ⊬! ↑𝗚 := by
+lemma goedel_unprovable [System.Consistent T] : T ⊬ ↑𝗚 := by
   intro h
   have hp : T ⊢! ↑□𝗚 := provableₐ_D1 h
-  have hn : T ⊢! ~↑□𝗚 := by simpa [provable₀_iff] using and_left! goedel_iff_unprovable_goedel ⨀ h
+  have hn : T ⊢! ∼↑□𝗚 := by simpa [provable₀_iff] using and_left! goedel_iff_unprovable_goedel ⨀ h
   exact not_consistent_iff_inconsistent.mpr (inconsistent_of_provable_of_unprovable hp hn) inferInstance
 
-lemma not_goedel_unprovable [ℕ ⊧ₘ* T] : T ⊬! ~↑𝗚 := fun h ↦ by
+lemma not_goedel_unprovable [ℕ ⊧ₘ* T] : T ⊬ ∼↑𝗚 := fun h ↦ by
   haveI : 𝐑₀ ≼ T := System.Subtheory.comp (𝓣 := 𝐈𝚺₁) inferInstance inferInstance
   have : T ⊢!. □𝗚 := System.contra₂'! (and_right! goedel_iff_unprovable_goedel) ⨀ (by simpa [provable₀_iff] using h)
   have : T ⊢! ↑𝗚 := provableₐ_sound this
   exact not_consistent_iff_inconsistent.mpr (inconsistent_of_provable_of_unprovable this h)
     (Sound.consistent_of_satisfiable ⟨_, (inferInstance : ℕ ⊧ₘ* T)⟩)
 
-lemma consistent_iff_goedel : T ⊢! ↑𝗖𝗼𝗻 ⟷ ↑𝗚 := by
+lemma consistent_iff_goedel : T ⊢! ↑𝗖𝗼𝗻 ⭤ ↑𝗚 := by
   apply iff_intro!
-  · have bew_G : [~𝗚] ⊢[T.alt]! □𝗚 := deductInv'! <| contra₂'! <| and_right! goedel_iff_unprovable_goedel
-    have bew_not_bew_G : [~𝗚] ⊢[T.alt]! □(~□𝗚) := by
-      have : T ⊢!. □(𝗚 ⟶ ~□𝗚) := provableₐ_D1 <| and_left! goedel_iff_unprovable_goedel
+  · have bew_G : [∼𝗚] ⊢[T.alt]! □𝗚 := deductInv'! <| contra₂'! <| and_right! goedel_iff_unprovable_goedel
+    have bew_not_bew_G : [∼𝗚] ⊢[T.alt]! □(∼□𝗚) := by
+      have : T ⊢!. □(𝗚 ➝ ∼□𝗚) := provableₐ_D1 <| and_left! goedel_iff_unprovable_goedel
       exact provableₐ_D2_context (of'! this) bew_G
-    have bew_bew_G : [~𝗚] ⊢[T.alt]! □□𝗚 := provableₐ_D3_context bew_G
-    have : [~𝗚] ⊢[T.alt]! □⊥ :=
+    have bew_bew_G : [∼𝗚] ⊢[T.alt]! □□𝗚 := provableₐ_D3_context bew_G
+    have : [∼𝗚] ⊢[T.alt]! □⊥ :=
       provableₐ_D2_context (provableₐ_D2_context (of'! <| provableₐ_D1 <| efq_imply_not₁!) bew_not_bew_G) bew_bew_G
     simpa [provable₀_iff] using contra₂'! (deduct'! this)
   · have : [□⊥] ⊢[T.alt]! □𝗚 := by
-      have : T ⊢!. □(⊥ ⟶ 𝗚) := provableₐ_D1 efq!
+      have : T ⊢!. □(⊥ ➝ 𝗚) := provableₐ_D1 efq!
       exact provableₐ_D2_context (of'! this) (by simp)
-    have : [□⊥] ⊢[T.alt]! ~𝗚 :=
+    have : [□⊥] ⊢[T.alt]! ∼𝗚 :=
       of'! (contra₁'! <| and_left! <| goedel_iff_unprovable_goedel) ⨀ this
     simpa [provable₀_iff] using  contra₁'! (deduct'! this)
 
-lemma consistent_unprovable [System.Consistent T] : T ⊬! ↑𝗖𝗼𝗻 := fun h ↦
+lemma consistent_unprovable [System.Consistent T] : T ⊬ ↑𝗖𝗼𝗻 := fun h ↦
   goedel_unprovable <| and_left! consistent_iff_goedel ⨀ h
 
-lemma inconsistent_unprovable [ℕ ⊧ₘ* T] : T ⊬! ~↑𝗖𝗼𝗻 := fun h ↦
+lemma inconsistent_unprovable [ℕ ⊧ₘ* T] : T ⊬ ∼↑𝗖𝗼𝗻 := fun h ↦
   not_goedel_unprovable <| contra₀'! (and_right! (consistent_iff_goedel (T := T))) ⨀ h
 
 end
diff --git a/Incompleteness/Arith/Theory.lean b/Incompleteness/Arith/Theory.lean
index a4f58df..a289a3d 100644
--- a/Incompleteness/Arith/Theory.lean
+++ b/Incompleteness/Arith/Theory.lean
@@ -578,7 +578,7 @@ def eqRefl.proof : ⌜𝐑₀'⌝[V] ⊢ (#'0 =' #'0).all := Language.Theory.TPr
   simp [qqAll, nat_cast_pair, qqEQ, qqRel, cons_absolute, qqBvar]
 
 def replace.proof (p : ⌜ℒₒᵣ⌝[V].Semiformula (0 + 1)) :
-    ⌜𝐑₀'⌝[V] ⊢ (#'1 =' #'0 ⟶ p^/[(#'1).sing] ⟶ p^/[(#'0).sing]).all.all := Language.Theory.TProof.byAxm <| by
+    ⌜𝐑₀'⌝[V] ⊢ (#'1 =' #'0 ➝ p^/[(#'1).sing] ➝ p^/[(#'0).sing]).all.all := Language.Theory.TProof.byAxm <| by
   apply FirstOrder.Semiformula.curve_mem_right
   apply FirstOrder.Semiformula.curve_mem_left
   unfold replace
@@ -631,7 +631,7 @@ def Ω₃.proof {n m : V} (ne : n ≠ m) : ⌜𝐑₀'⌝[V] ⊢ ↑n ≠' ↑m
   · exact lt_of_le_of_lt (by simp) (lt_qqNEQ_left _ _)
   · exact lt_of_le_of_lt (by simp) (lt_qqNEQ_right _ _)
 
-def Ω₄.proof (n : V): ⌜𝐑₀'⌝[V] ⊢ (#'0 <' ↑n ⟷ (tSubstItr (#'0).sing (#'1 =' #'0) n).disj).all := Language.Theory.TProof.byAxm <| by
+def Ω₄.proof (n : V): ⌜𝐑₀'⌝[V] ⊢ (#'0 <' ↑n ⭤ (tSubstItr (#'0).sing (#'1 =' #'0) n).disj).all := Language.Theory.TProof.byAxm <| by
   apply FirstOrder.Semiformula.curve_mem_right
   apply FirstOrder.Semiformula.curve_mem_right
   apply FirstOrder.Semiformula.curve_mem_right
diff --git a/Incompleteness/DC/Basic.lean b/Incompleteness/DC/Basic.lean
index dc25579..4b01879 100644
--- a/Incompleteness/DC/Basic.lean
+++ b/Incompleteness/DC/Basic.lean
@@ -29,34 +29,34 @@ variable {T₀ T : Theory L}
 def pr (𝔅 : ProvabilityPredicate T₀ T) (σ : Sentence L) : Sentence L := 𝔅.prov/[⌜σ⌝]
 instance : CoeFun (ProvabilityPredicate T₀ T) (fun _ => Sentence L → Sentence L) := ⟨pr⟩
 
-def con (𝔅 : ProvabilityPredicate T₀ T) : Sentence L := ~(𝔅 ⊥)
+def con (𝔅 : ProvabilityPredicate T₀ T) : Sentence L := ∼(𝔅 ⊥)
 
 end ProvabilityPredicate
 
 class Diagonalization (T : Theory L) where
   fixpoint : Semisentence L 1 → Sentence L
-  diag (θ) : T ⊢!. fixpoint θ ⟷ θ/[⌜fixpoint θ⌝]
+  diag (θ) : T ⊢!. fixpoint θ ⭤ θ/[⌜fixpoint θ⌝]
 
 namespace ProvabilityPredicate
 
 variable {T₀ T : Theory L}
 
 class HBL2 (𝔅 : ProvabilityPredicate T₀ T) where
-  D2 {σ τ : Sentence L} : T₀ ⊢!. 𝔅 (σ ⟶ τ) ⟶ (𝔅 σ) ⟶ (𝔅 τ)
+  D2 {σ τ : Sentence L} : T₀ ⊢!. 𝔅 (σ ➝ τ) ➝ (𝔅 σ) ➝ (𝔅 τ)
 
 class HBL3 (𝔅 : ProvabilityPredicate T₀ T) where
-  D3 {σ : Sentence L} : T₀ ⊢!. (𝔅 σ) ⟶ 𝔅 (𝔅 σ)
+  D3 {σ : Sentence L} : T₀ ⊢!. (𝔅 σ) ➝ 𝔅 (𝔅 σ)
 
 class HBL (𝔅 : ProvabilityPredicate T₀ T) extends 𝔅.HBL2, 𝔅.HBL3
 
 class Loeb (𝔅 : ProvabilityPredicate T₀ T) where
-  LT {σ : Sentence L} : T ⊢!. (𝔅 σ) ⟶ σ → T ⊢!. σ
+  LT {σ : Sentence L} : T ⊢!. (𝔅 σ) ➝ σ → T ⊢!. σ
 
 class FormalizedLoeb (𝔅 : ProvabilityPredicate T₀ T) where
-  FLT {σ : Sentence L} : T₀ ⊢!. 𝔅 ((𝔅 σ) ⟶ σ) ⟶ (𝔅 σ)
+  FLT {σ : Sentence L} : T₀ ⊢!. 𝔅 ((𝔅 σ) ➝ σ) ➝ (𝔅 σ)
 
 class Rosser (𝔅 : ProvabilityPredicate T₀ T) where
-  Ro {σ : Sentence L} : T ⊢!. ~σ → T₀ ⊢!. ~(𝔅 σ)
+  Ro {σ : Sentence L} : T ⊢!. ∼σ → T₀ ⊢!. ∼(𝔅 σ)
 
 section
 
@@ -79,39 +79,39 @@ def D1_shift : T ⊢!. σ → T ⊢!. (𝔅 σ) := by
   apply System.Subtheory.prf! (𝓢 := T₀);
   apply D1 h;
 
-def D2_shift [𝔅.HBL2] : T ⊢!. 𝔅 (σ ⟶ τ) ⟶ (𝔅 σ) ⟶ (𝔅 τ) := by
+def D2_shift [𝔅.HBL2] : T ⊢!. 𝔅 (σ ➝ τ) ➝ (𝔅 σ) ➝ (𝔅 τ) := by
   apply System.Subtheory.prf! (𝓢 := T₀);
   apply D2;
 
-def D3_shift [𝔅.HBL3] : T ⊢!. (𝔅 σ) ⟶ 𝔅 (𝔅 σ) := by
+def D3_shift [𝔅.HBL3] : T ⊢!. (𝔅 σ) ➝ 𝔅 (𝔅 σ) := by
   apply System.Subtheory.prf! (𝓢 := T₀);
   apply D3;
 
-def FLT_shift [𝔅.FormalizedLoeb] : T ⊢!. 𝔅 ((𝔅 σ) ⟶ σ) ⟶ (𝔅 σ) := by
+def FLT_shift [𝔅.FormalizedLoeb] : T ⊢!. 𝔅 ((𝔅 σ) ➝ σ) ➝ (𝔅 σ) := by
   apply System.Subtheory.prf! (𝓢 := T₀);
   apply 𝔅.FLT;
 
-def D2' [𝔅.HBL2] [System.ModusPonens T] : T₀ ⊢!. 𝔅 (σ ⟶ τ) → T₀ ⊢!. (𝔅 σ) ⟶ (𝔅 τ) := by
+def D2' [𝔅.HBL2] [System.ModusPonens T] : T₀ ⊢!. 𝔅 (σ ➝ τ) → T₀ ⊢!. (𝔅 σ) ➝ (𝔅 τ) := by
   intro h;
   exact D2 ⨀ h;
 
-def prov_distribute_imply (h : T ⊢!. σ ⟶ τ) : T₀ ⊢!. (𝔅 σ) ⟶ (𝔅 τ) := D2' $ D1 h
+def prov_distribute_imply (h : T ⊢!. σ ➝ τ) : T₀ ⊢!. (𝔅 σ) ➝ (𝔅 τ) := D2' $ D1 h
 
-def prov_distribute_iff (h : T ⊢!. σ ⟷ τ) : T₀ ⊢!. (𝔅 σ) ⟷ (𝔅 τ) := by
+def prov_distribute_iff (h : T ⊢!. σ ⭤ τ) : T₀ ⊢!. (𝔅 σ) ⭤ (𝔅 τ) := by
   apply iff_intro!;
   . exact prov_distribute_imply $ and₁'! h;
   . exact prov_distribute_imply $ and₂'! h;
 
-def prov_distribute_and : T₀ ⊢!. 𝔅 (σ ⋏ τ) ⟶ (𝔅 σ) ⋏ (𝔅 τ) := by
-  have h₁ : T₀ ⊢!. 𝔅 (σ ⋏ τ) ⟶ (𝔅 σ) := D2' <| D1 and₁!;
-  have h₂ : T₀ ⊢!. 𝔅 (σ ⋏ τ) ⟶ (𝔅 τ) := D2' <| D1 and₂!;
+def prov_distribute_and : T₀ ⊢!. 𝔅 (σ ⋏ τ) ➝ (𝔅 σ) ⋏ (𝔅 τ) := by
+  have h₁ : T₀ ⊢!. 𝔅 (σ ⋏ τ) ➝ (𝔅 σ) := D2' <| D1 and₁!;
+  have h₂ : T₀ ⊢!. 𝔅 (σ ⋏ τ) ➝ (𝔅 τ) := D2' <| D1 and₂!;
   exact imply_right_and! h₁ h₂;
 
 def prov_distribute_and' : T₀ ⊢!. 𝔅 (σ ⋏ τ) → T₀ ⊢!. (𝔅 σ) ⋏ (𝔅 τ) := λ h => prov_distribute_and ⨀ h
 
-def prov_collect_and : T₀ ⊢!. (𝔅 σ) ⋏ (𝔅 τ) ⟶ 𝔅 (σ ⋏ τ) := by
-  have h₁ : T₀ ⊢!. (𝔅 σ) ⟶ 𝔅 (τ ⟶ σ ⋏ τ) := prov_distribute_imply $ and₃!;
-  have h₂ : T₀ ⊢!. 𝔅 (τ ⟶ σ ⋏ τ) ⟶ (𝔅 τ) ⟶ 𝔅 (σ ⋏ τ) := D2;
+def prov_collect_and : T₀ ⊢!. (𝔅 σ) ⋏ (𝔅 τ) ➝ 𝔅 (σ ⋏ τ) := by
+  have h₁ : T₀ ⊢!. (𝔅 σ) ➝ 𝔅 (τ ➝ σ ⋏ τ) := prov_distribute_imply $ and₃!;
+  have h₂ : T₀ ⊢!. 𝔅 (τ ➝ σ ⋏ τ) ➝ (𝔅 τ) ➝ 𝔅 (σ ⋏ τ) := D2;
   apply and_imply_iff_imply_imply'!.mpr;
   exact imp_trans''! h₁ h₂;
 
@@ -136,14 +136,14 @@ local notation "γ" => goedel T₀ T 𝔅
 
 section GoedelSentence
 
-lemma goedel_spec : T₀ ⊢!. γ ⟷ ~𝔅 γ := by
+lemma goedel_spec : T₀ ⊢!. γ ⭤ ∼𝔅 γ := by
   convert (diag (T := T₀) “x. ¬!𝔅.prov x”);
   simp [goedel, ←Rew.hom_comp_app, Rew.substs_comp_substs];
   rfl;
 
-private lemma goedel_specAux₁ : T ⊢!. γ ⟷ ~𝔅 γ := Subtheory.prf! (𝓢 := T₀) goedel_spec
+private lemma goedel_specAux₁ : T ⊢!. γ ⭤ ∼𝔅 γ := Subtheory.prf! (𝓢 := T₀) goedel_spec
 
-private lemma goedel_specAux₂ : T ⊢!. ~γ ⟶ 𝔅 γ := contra₂'! $ and₂'! goedel_specAux₁
+private lemma goedel_specAux₂ : T ⊢!. ∼γ ➝ 𝔅 γ := contra₂'! $ and₂'! goedel_specAux₁
 
 end GoedelSentence
 
@@ -157,16 +157,16 @@ section First
 
 variable [System.Consistent T]
 
-theorem unprovable_goedel : T ⊬!. γ := by
+theorem unprovable_goedel : T ⊬. γ := by
   intro h;
   have h₁ : T ⊢!. 𝔅 γ := D1_shift h;
-  have h₂ : T ⊢!. ~𝔅 γ := (and₁'! goedel_specAux₁) ⨀ h;
+  have h₂ : T ⊢!. ∼𝔅 γ := (and₁'! goedel_specAux₁) ⨀ h;
   have : T ⊢!. ⊥ := (neg_equiv'!.mp h₂) ⨀ h₁;
   have : ¬Consistent T := not_consistent_iff_inconsistent.mpr <|
     inconsistent_iff_provable_bot.mpr (by simpa [provable₀_iff] using this)
   contradiction;
 
-theorem unrefutable_goedel [𝔅.GoedelSound] : T ⊬!. ~γ := by
+theorem unrefutable_goedel [𝔅.GoedelSound] : T ⊬. ∼γ := by
   intro h₂;
   have h₁ : T ⊢!. γ := γ_sound $ goedel_specAux₂ ⨀ h₂;
   have : T ⊢!. ⊥ := (neg_equiv'!.mp h₂) ⨀ h₁;
@@ -175,7 +175,7 @@ theorem unrefutable_goedel [𝔅.GoedelSound] : T ⊬!. ~γ := by
   contradiction;
 
 theorem goedel_independent [𝔅.GoedelSound] : System.Undecidable T ↑γ := by
-  suffices T ⊬!. γ ∧ T ⊬!. ~γ by simpa [System.Undecidable, not_or, unprovable₀_iff] using this
+  suffices T ⊬. γ ∧ T ⊬. ∼γ by simpa [System.Undecidable, not_or, unprovable₀_iff] using this
   constructor
   . apply unprovable_goedel
   . apply unrefutable_goedel
@@ -190,45 +190,45 @@ section Second
 
 variable [Diagonalization T] [𝔅.HBL]
 
-lemma formalized_consistent_of_existance_unprovable : T₀ ⊢!. ~(𝔅 σ) ⟶ 𝔅.con := contra₀'! $ 𝔅.D2 ⨀ (D1 efq!)
+lemma formalized_consistent_of_existance_unprovable : T₀ ⊢!. ∼(𝔅 σ) ➝ 𝔅.con := contra₀'! $ 𝔅.D2 ⨀ (D1 efq!)
 
-private lemma consistency_lemma_1 [T₀ ≼ U] [𝔅.HBL] : (U ⊢!. 𝔅.con ⟶ ~(𝔅 σ)) ↔ (U ⊢!. (𝔅 σ) ⟶ 𝔅 (~σ)) := by
+private lemma consistency_lemma_1 [T₀ ≼ U] [𝔅.HBL] : (U ⊢!. 𝔅.con ➝ ∼(𝔅 σ)) ↔ (U ⊢!. (𝔅 σ) ➝ 𝔅 (∼σ)) := by
   constructor;
   . intro H;
     exact contra₃'! $ imp_trans''! (Subtheory.prf! (𝓢 := T₀) formalized_consistent_of_existance_unprovable) H;
   . intro H
     apply contra₀'!
-    have : T₀ ⊢!. (𝔅 σ) ⋏ 𝔅 (~σ) ⟶ 𝔅 ⊥ := imp_trans''! prov_collect_and $ prov_distribute_imply lac!;
-    have : U ⊢!. (𝔅 σ) ⟶ 𝔅 (~σ) ⟶ 𝔅 ⊥ := Subtheory.prf! $ and_imply_iff_imply_imply'!.mp $ this;
+    have : T₀ ⊢!. (𝔅 σ) ⋏ 𝔅 (∼σ) ➝ 𝔅 ⊥ := imp_trans''! prov_collect_and $ prov_distribute_imply lac!;
+    have : U ⊢!. (𝔅 σ) ➝ 𝔅 (∼σ) ➝ 𝔅 ⊥ := Subtheory.prf! $ and_imply_iff_imply_imply'!.mp $ this;
     exact this ⨀₁ H;
 
-private lemma consistency_lemma_2 : T₀ ⊢!. ((𝔅 σ) ⟶ 𝔅 (~σ)) ⟶ (𝔅 σ) ⟶ 𝔅 ⊥ := by
-  have : T ⊢!. σ ⟶ ~σ ⟶ ⊥ := and_imply_iff_imply_imply'!.mp lac!
-  have : T₀ ⊢!. (𝔅 σ) ⟶ 𝔅 (~σ ⟶ ⊥)  := prov_distribute_imply this;
-  have : T₀ ⊢!. (𝔅 σ) ⟶ (𝔅 (~σ) ⟶ 𝔅 ⊥) := imp_trans''! this D2;
+private lemma consistency_lemma_2 : T₀ ⊢!. ((𝔅 σ) ➝ 𝔅 (∼σ)) ➝ (𝔅 σ) ➝ 𝔅 ⊥ := by
+  have : T ⊢!. σ ➝ ∼σ ➝ ⊥ := and_imply_iff_imply_imply'!.mp lac!
+  have : T₀ ⊢!. (𝔅 σ) ➝ 𝔅 (∼σ ➝ ⊥)  := prov_distribute_imply this;
+  have : T₀ ⊢!. (𝔅 σ) ➝ (𝔅 (∼σ) ➝ 𝔅 ⊥) := imp_trans''! this D2;
 
   -- TODO: more simple proof
   apply FiniteContext.deduct'!;
   apply FiniteContext.deduct!;
-  have d₁ : [(𝔅 σ), (𝔅 σ) ⟶ 𝔅 (~σ)] ⊢[T₀.alt]! (𝔅 σ) := FiniteContext.by_axm!;
-  have d₂ : [(𝔅 σ), (𝔅 σ) ⟶ 𝔅 (~σ)] ⊢[T₀.alt]! (𝔅 σ) ⟶ 𝔅 (~σ) := FiniteContext.by_axm!;
-  have d₃ : [(𝔅 σ), (𝔅 σ) ⟶ 𝔅 (~σ)] ⊢[T₀.alt]! 𝔅 (~σ) := d₂ ⨀ d₁;
+  have d₁ : [(𝔅 σ), (𝔅 σ) ➝ 𝔅 (∼σ)] ⊢[T₀.alt]! (𝔅 σ) := FiniteContext.by_axm!;
+  have d₂ : [(𝔅 σ), (𝔅 σ) ➝ 𝔅 (∼σ)] ⊢[T₀.alt]! (𝔅 σ) ➝ 𝔅 (∼σ) := FiniteContext.by_axm!;
+  have d₃ : [(𝔅 σ), (𝔅 σ) ➝ 𝔅 (∼σ)] ⊢[T₀.alt]! 𝔅 (∼σ) := d₂ ⨀ d₁;
   exact ((FiniteContext.of'! this) ⨀ d₁) ⨀ d₃;
 
 /-- Formalized First Incompleteness Theorem -/
-theorem formalized_unprovable_goedel : T ⊢!. 𝔅.con ⟶ ~𝔅 γ := by
-  have h₁ : T₀ ⊢!. 𝔅 γ ⟶ 𝔅 (𝔅 γ) := D3;
-  have h₂ : T ⊢!. 𝔅 γ ⟶ ~γ := Subtheory.prf! $ contra₁'! $ and₁'! goedel_spec;
-  have h₃ : T₀ ⊢!. 𝔅 (𝔅 γ) ⟶ 𝔅 (~γ) := prov_distribute_imply h₂;
+theorem formalized_unprovable_goedel : T ⊢!. 𝔅.con ➝ ∼𝔅 γ := by
+  have h₁ : T₀ ⊢!. 𝔅 γ ➝ 𝔅 (𝔅 γ) := D3;
+  have h₂ : T ⊢!. 𝔅 γ ➝ ∼γ := Subtheory.prf! $ contra₁'! $ and₁'! goedel_spec;
+  have h₃ : T₀ ⊢!. 𝔅 (𝔅 γ) ➝ 𝔅 (∼γ) := prov_distribute_imply h₂;
   exact Subtheory.prf! $ contra₀'! $ consistency_lemma_2 ⨀ (imp_trans''! h₁ h₃);
 
-theorem iff_goedel_consistency : T ⊢!. γ ⟷ 𝔅.con
+theorem iff_goedel_consistency : T ⊢!. γ ⭤ 𝔅.con
   := iff_trans''! goedel_specAux₁ $ iff_intro! (Subtheory.prf! (𝓢 := T₀) formalized_consistent_of_existance_unprovable) formalized_unprovable_goedel
 
-theorem unprovable_consistency [System.Consistent T] : T ⊬!. 𝔅.con
+theorem unprovable_consistency [System.Consistent T] : T ⊬. 𝔅.con
   := unprovable_iff! iff_goedel_consistency |>.mp $ unprovable_goedel
 
-theorem unrefutable_consistency [System.Consistent T] [𝔅.GoedelSound] : T ⊬!. ~𝔅.con
+theorem unrefutable_consistency [System.Consistent T] [𝔅.GoedelSound] : T ⊬. ∼𝔅.con
   := unprovable_iff! (neg_replace_iff'! $ iff_goedel_consistency) |>.mp $ unrefutable_goedel
 
 end Second
@@ -246,29 +246,29 @@ section KrieselSentence
 
 variable [𝔅.HBL]
 
-lemma kreisel_spec (σ : Sentence L) : T₀ ⊢!. κ(σ) ⟷ (𝔅 (κ(σ)) ⟶ σ) := by
+lemma kreisel_spec (σ : Sentence L) : T₀ ⊢!. κ(σ) ⭤ (𝔅 (κ(σ)) ➝ σ) := by
   convert (diag (T := T₀) “x. !𝔅.prov x → !σ”);
   simp [kreisel, ←Rew.hom_comp_app, Rew.substs_comp_substs];
   rfl;
 
-private lemma kreisel_specAux₁ (σ : Sentence L) : T₀ ⊢!. 𝔅 κ(σ) ⟶ (𝔅 σ) := (imp_trans''! (D2 ⨀ (D1 (Subtheory.prf! $ and₁'! (kreisel_spec σ)))) D2) ⨀₁ D3
+private lemma kreisel_specAux₁ (σ : Sentence L) : T₀ ⊢!. 𝔅 κ(σ) ➝ (𝔅 σ) := (imp_trans''! (D2 ⨀ (D1 (Subtheory.prf! $ and₁'! (kreisel_spec σ)))) D2) ⨀₁ D3
 
-private lemma kreisel_specAux₂ (σ : Sentence L) : T₀ ⊢!. (𝔅 κ(σ) ⟶ σ) ⟶ κ(σ) := and₂'! (kreisel_spec σ)
+private lemma kreisel_specAux₂ (σ : Sentence L) : T₀ ⊢!. (𝔅 κ(σ) ➝ σ) ➝ κ(σ) := and₂'! (kreisel_spec σ)
 
 end KrieselSentence
 
-theorem loeb_theorm [𝔅.HBL] (H : T ⊢!. (𝔅 σ) ⟶ σ) : T ⊢!. σ := by
-  have d₁ : T ⊢!. 𝔅 κ(σ) ⟶ σ := imp_trans''! (Subtheory.prf! (kreisel_specAux₁ σ)) H;
+theorem loeb_theorm [𝔅.HBL] (H : T ⊢!. (𝔅 σ) ➝ σ) : T ⊢!. σ := by
+  have d₁ : T ⊢!. 𝔅 κ(σ) ➝ σ := imp_trans''! (Subtheory.prf! (kreisel_specAux₁ σ)) H;
   have d₂ : T ⊢!. 𝔅 κ(σ)     := Subtheory.prf! (𝓢 := T₀) (D1 $ Subtheory.prf! (kreisel_specAux₂ σ) ⨀ d₁);
   exact d₁ ⨀ d₂;
 
 instance [𝔅.HBL] : 𝔅.Loeb := ⟨loeb_theorm (T := T)⟩
 
 
-theorem formalized_loeb_theorem [𝔅.HBL] : T₀ ⊢!. 𝔅 ((𝔅 σ) ⟶ σ) ⟶ (𝔅 σ) := by
-  have hκ₁ : T₀ ⊢!. 𝔅 (κ(σ)) ⟶ (𝔅 σ) := kreisel_specAux₁ σ;
-  have : T₀ ⊢!. ((𝔅 σ) ⟶ σ) ⟶ (𝔅 κ(σ) ⟶ σ) := replace_imply_left! hκ₁;
-  have : T ⊢!. ((𝔅 σ) ⟶ σ) ⟶ κ(σ) := Subtheory.prf! (𝓢 := T₀) $ imp_trans''! this (kreisel_specAux₂ σ);
+theorem formalized_loeb_theorem [𝔅.HBL] : T₀ ⊢!. 𝔅 ((𝔅 σ) ➝ σ) ➝ (𝔅 σ) := by
+  have hκ₁ : T₀ ⊢!. 𝔅 (κ(σ)) ➝ (𝔅 σ) := kreisel_specAux₁ σ;
+  have : T₀ ⊢!. ((𝔅 σ) ➝ σ) ➝ (𝔅 κ(σ) ➝ σ) := replace_imply_left! hκ₁;
+  have : T ⊢!. ((𝔅 σ) ➝ σ) ➝ κ(σ) := Subtheory.prf! (𝓢 := T₀) $ imp_trans''! this (kreisel_specAux₂ σ);
   exact imp_trans''! (D2 ⨀ (D1 this)) hκ₁;
 
 instance [𝔅.HBL] : 𝔅.FormalizedLoeb := ⟨formalized_loeb_theorem (T := T)⟩
@@ -276,24 +276,24 @@ instance [𝔅.HBL] : 𝔅.FormalizedLoeb := ⟨formalized_loeb_theorem (T := T)
 
 variable [System.Consistent T]
 
-lemma unprovable_consistency_via_loeb [𝔅.Loeb] : T ⊬!. 𝔅.con := by
+lemma unprovable_consistency_via_loeb [𝔅.Loeb] : T ⊬. 𝔅.con := by
   by_contra hC;
   have : T ⊢!. ⊥ := Loeb.LT $ neg_equiv'!.mp hC;
   have : ¬Consistent T := not_consistent_iff_inconsistent.mpr $ inconsistent_iff_provable_bot.mpr (by simpa [provable₀_iff] using this)
   contradiction
 
 lemma formalized_unprovable_not_consistency [𝔅.HBL] [𝔅.GoedelSound]
-  : T ⊬!. 𝔅.con ⟶ ~𝔅 (~𝔅.con) := by
+  : T ⊬. 𝔅.con ➝ ∼𝔅 (∼𝔅.con) := by
   by_contra hC;
-  have : T ⊢!. ~𝔅.con := Loeb.LT $ contra₁'! hC;
-  have : T ⊬!. ~𝔅.con := unrefutable_consistency;
+  have : T ⊢!. ∼𝔅.con := Loeb.LT $ contra₁'! hC;
+  have : T ⊬. ∼𝔅.con := unrefutable_consistency;
   contradiction;
 
 lemma formalized_unrefutable_goedel [𝔅.HBL] [𝔅.GoedelSound]
-  : T ⊬!. 𝔅.con ⟶ ~𝔅 (~γ) := by
+  : T ⊬. 𝔅.con ➝ ∼𝔅 (∼γ) := by
   by_contra hC;
-  have : T ⊬!. 𝔅.con ⟶ ~𝔅 (~𝔅.con)  := formalized_unprovable_not_consistency;
-  have : T ⊢!. 𝔅.con ⟶ ~𝔅 (~𝔅.con) := imp_trans''! hC $ Subtheory.prf! $ and₁'! $ neg_replace_iff'! $ prov_distribute_iff $ neg_replace_iff'! $ iff_goedel_consistency;
+  have : T ⊬. 𝔅.con ➝ ∼𝔅 (∼𝔅.con)  := formalized_unprovable_not_consistency;
+  have : T ⊢!. 𝔅.con ➝ ∼𝔅 (∼𝔅.con) := imp_trans''! hC $ Subtheory.prf! $ and₁'! $ neg_replace_iff'! $ prov_distribute_iff $ neg_replace_iff'! $ iff_goedel_consistency;
   contradiction;
 
 end Loeb
@@ -309,9 +309,9 @@ section RosserSentence
 
 variable [𝔅.Rosser]
 
-lemma rosser_spec : T₀ ⊢!. ρ ⟷ ~(𝔅 ρ) := goedel_spec
+lemma rosser_spec : T₀ ⊢!. ρ ⭤ ∼(𝔅 ρ) := goedel_spec
 
-private lemma rosser_specAux₁ : T ⊢!. ρ ⟷ ~(𝔅 ρ) := goedel_specAux₁
+private lemma rosser_specAux₁ : T ⊢!. ρ ⭤ ∼(𝔅 ρ) := goedel_specAux₁
 
 end RosserSentence
 
@@ -319,9 +319,9 @@ section
 
 variable [System.Consistent T] [𝔅.Rosser]
 
-lemma unprovable_rosser : T ⊬!. ρ := unprovable_goedel
+lemma unprovable_rosser : T ⊬. ρ := unprovable_goedel
 
-theorem unrefutable_rosser : T ⊬!. ~ρ := by
+theorem unrefutable_rosser : T ⊬. ∼ρ := by
   intro hnρ;
   have hρ : T ⊢!. ρ := Subtheory.prf! $ (and₂'! rosser_spec) ⨀ (Ro hnρ);
   have : ¬Consistent T := not_consistent_iff_inconsistent.mpr $ inconsistent_iff_provable_bot.mpr <|
@@ -329,7 +329,7 @@ theorem unrefutable_rosser : T ⊬!. ~ρ := by
   contradiction
 
 theorem rosser_independent : System.Undecidable T ↑ρ := by
-  suffices T ⊬!. ρ ∧ T ⊬!. ~ρ by simpa [System.Undecidable, not_or, unprovable₀_iff] using this;
+  suffices T ⊬. ρ ∧ T ⊬. ∼ρ by simpa [System.Undecidable, not_or, unprovable₀_iff] using this;
   constructor
   . apply unprovable_rosser
   . apply unrefutable_rosser
@@ -339,7 +339,7 @@ theorem rosser_first_incompleteness : ¬System.Complete T
 
 /-- If `𝔅` satisfies Rosser provability condition, then `𝔅.con` is provable in `T`. -/
 theorem kriesel_remark : T ⊢!. 𝔅.con := by
-  have : T₀ ⊢!. ~𝔅 ⊥ := Ro (neg_equiv'!.mpr (by simp));
+  have : T₀ ⊢!. ∼𝔅 ⊥ := Ro (neg_equiv'!.mpr (by simp));
   exact Subtheory.prf! $ this;
 
 end
diff --git a/Incompleteness/ProvabilityLogic/Basic.lean b/Incompleteness/ProvabilityLogic/Basic.lean
index 1102f1e..4bbacf3 100644
--- a/Incompleteness/ProvabilityLogic/Basic.lean
+++ b/Incompleteness/ProvabilityLogic/Basic.lean
@@ -24,7 +24,7 @@ def Realization.interpret
   | .atom a => f a
   | □p => 𝔅 (f.interpret 𝔅 p)
   | ⊥ => ⊥
-  | p ⟶ q => (f.interpret 𝔅 p) ⟶ (f.interpret 𝔅 q)
+  | p ➝ q => (f.interpret 𝔅 p) ➝ (f.interpret 𝔅 q)
 
 variable [Semiterm.Operator.GoedelNumber L (Sentence L)]
 
diff --git a/lake-manifest.json b/lake-manifest.json
index 0958a00..a87b733 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -75,17 +75,17 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "24006582e25395fb5fa3da38181905cff44d0f36",
+   "rev": "c14a269c27ee9ef7936bcbb84fc7c51056480479",
    "name": "logic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
-   "inherited": false,
+   "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/FormalizedFormalLogic/Arithmetization",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "1805c5a19a4fa5987d02b0d47b006c7cc6d810b6",
+   "rev": "1bfdc1b5a1c5912433564e2aa0fb94efee0278d1",
    "name": "arithmetization",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
diff --git a/lakefile.lean b/lakefile.lean
index b3d3935..d36d312 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -8,8 +8,6 @@ package «Incompleteness» where
   ]
   -- add any additional package configuration options here
 
-require «logic» from git "https://github.com/FormalizedFormalLogic/Foundation" @ "master"
-
 require arithmetization from git "https://github.com/FormalizedFormalLogic/Arithmetization" @ "master"
 
 require proofwidgets from git "https://github.com/leanprover-community/ProofWidgets4"@"v0.0.39"