Skip to content

Commit fd11f33

Browse files
SnO2WMaNSnO2WMaN
authored
refactor: Replace symbol ➝ to 🡒 and ⭤ to 🡘 (#811)
1 parent e014827 commit fd11f33

211 files changed

Lines changed: 2325 additions & 2325 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎Foundation/FirstOrder/Arithmetic/Basic/Hierarchy.lean‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -164,7 +164,7 @@ lemma neg {φ : Semiformula L ξ n} : Hierarchy Γ s φ → Hierarchy Γ.alt s (
164164
@[simp] lemma neg_iff {φ : Semiformula L ξ n} : Hierarchy Γ s (∼φ) ↔ Hierarchy Γ.alt s φ :=
165165
⟨fun h => by simpa using neg h, fun h => by simpa using neg h⟩
166166

167-
@[simp] lemma imp_iff {φ ψ : Semiformula L ξ n} : Hierarchy Γ s (φ ➝ ψ) ↔ (Hierarchy Γ.alt s φ ∧ Hierarchy Γ s ψ) := by simp [Semiformula.imp_eq]
167+
@[simp] lemma imp_iff {φ ψ : Semiformula L ξ n} : Hierarchy Γ s (φ 🡒 ψ) ↔ (Hierarchy Γ.alt s φ ∧ Hierarchy Γ s ψ) := by simp [Semiformula.imp_eq]
168168

169169
set_option linter.flexible false in
170170
@[simp] lemma ball_iff {Γ s n} {φ : Semiformula L ξ (n + 1)} {t : Semiterm L ξ (n + 1)} (ht : t.Positive) :
@@ -336,11 +336,11 @@ lemma of_open {φ : Semiformula L ξ n} : φ.Open → Hierarchy Γ s φ := by
336336
variable {L : Language} [L.ORing]
337337

338338
lemma iff_iff {φ ψ : Semiformula L ξ n} :
339-
Hierarchy b s (φ ⭤ ψ) ↔ (Hierarchy b s φ ∧ Hierarchy b.alt s φ ∧ Hierarchy b s ψ ∧ Hierarchy b.alt s ψ) := by
339+
Hierarchy b s (φ 🡘 ψ) ↔ (Hierarchy b s φ ∧ Hierarchy b.alt s φ ∧ Hierarchy b s ψ ∧ Hierarchy b.alt s ψ) := by
340340
simp [Semiformula.iff_eq]; tauto
341341

342342
@[simp] lemma iff_iff₀ {φ ψ : Semiformula L ξ n} :
343-
Hierarchy b 0 (φ ⭤ ψ) ↔ (Hierarchy b 0 φ ∧ Hierarchy b 0 ψ) := by
343+
Hierarchy b 0 (φ 🡘 ψ) ↔ (Hierarchy b 0 φ ∧ Hierarchy b 0 ψ) := by
344344
simp [Semiformula.iff_eq]; tauto
345345

346346
@[simp] lemma matrix_conj_iff {b s n} {φ : Fin m → Semiformula L ξ n} :

‎Foundation/FirstOrder/Arithmetic/Basic/Misc.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -65,7 +65,7 @@ def Semiformula.toStringORing : ∀ {n}, Semiformula ℒₒᵣ ξ n → String
6565
| _, nrel Language.LT.lt v => (v 0).toStringORing ++ " \\not < " ++ (v 1).toStringORing
6666
| _, φ ⋏ ψ => "[" ++ φ.toStringORing ++ "]" ++ " \\land " ++ "[" ++ ψ.toStringORing ++ "]"
6767
| _, φ ⋎ ψ => "[" ++ φ.toStringORing ++ "]" ++ " \\lor " ++ "[" ++ ψ.toStringORing ++ "]"
68-
| n, ∀⁰ (rel Language.LT.lt v ➝ φ) => "(\\forall x_{" ++ toString n ++ "} < " ++ (v 1).toStringORing ++ ") " ++ "[" ++ φ.toStringORing ++ "]"
68+
| n, ∀⁰ (rel Language.LT.lt v 🡒 φ) => "(\\forall x_{" ++ toString n ++ "} < " ++ (v 1).toStringORing ++ ") " ++ "[" ++ φ.toStringORing ++ "]"
6969
| n, ∃⁰ (rel Language.LT.lt v ⋏ φ) => "(\\exists x_{" ++ toString n ++ "} < " ++ (v 1).toStringORing ++ ") " ++ "[" ++ φ.toStringORing ++ "]"
7070
| n, ∀⁰ φ => "(\\forall x_{" ++ toString n ++ "}) " ++ "[" ++ φ.toStringORing ++ "]"
7171
| n, ∃⁰ φ => "(\\exists x_{" ++ toString n ++ "}) " ++ "[" ++ φ.toStringORing ++ "]"

‎Foundation/FirstOrder/Arithmetic/Definability/Definable.lean‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -789,13 +789,13 @@ lemma ball_lt {Γ} {P : (Fin k → V) → V → Prop} {f : (Fin k → V) → V}
789789
⟨ .mkSigma (∃⁰ (bf.val ⋏ (∀⁰[“#0 < #1”] φ.val ⇜ (#0 :> (#·.succ.succ))))) (by simp),
790790
by intro v; simp [hbf.df.iff, hp.df.iff] ⟩
791791
| 𝚷 => exact
792-
⟨ .mkPi (∀⁰ (bf.val ➝ (∀⁰[“#0 < #1”] φ.val ⇜ (#0 :> (#·.succ.succ))))) (by simp),
792+
⟨ .mkPi (∀⁰ (bf.val 🡒 (∀⁰[“#0 < #1”] φ.val ⇜ (#0 :> (#·.succ.succ))))) (by simp),
793793
by intro v; simp [hbf.df.iff, hp.df.iff] ⟩
794794
| 𝚫 =>
795795
exact .of_sigma_of_pi
796796
⟨ .mkSigma (∃⁰ (bf.val ⋏ (∀⁰[“#0 < #1”] φ.sigma.val ⇜ (#0 :> (#·.succ.succ))))) (by simp),
797797
by intro v; simp [hbf.df.iff, hp.df.iff, HierarchySymbol.Semiformula.val_sigma] ⟩
798-
⟨ .mkPi (∀⁰ (bf.val ➝ (∀⁰[“#0 < #1”] φ.pi.val ⇜ (#0 :> (#·.succ.succ))))) (by simp),
798+
⟨ .mkPi (∀⁰ (bf.val 🡒 (∀⁰[“#0 < #1”] φ.pi.val ⇜ (#0 :> (#·.succ.succ))))) (by simp),
799799
by intro v; simp [hbf.df.iff, hp.df.iff, hp.proper.iff'] ⟩
800800

801801
lemma bexs_lt {Γ} {P : (Fin k → V) → V → Prop} {f : (Fin k → V) → V}
@@ -808,13 +808,13 @@ lemma bexs_lt {Γ} {P : (Fin k → V) → V → Prop} {f : (Fin k → V) → V}
808808
⟨ .mkSigma (∃⁰ (bf.val ⋏ (∃⁰[“#0 < #1”] φ.val ⇜ (#0 :> (#·.succ.succ))))) (by simp),
809809
by intro v; simp [hbf.df.iff, hp.df.iff] ⟩
810810
| 𝚷 => exact
811-
⟨ .mkPi (∀⁰ (bf.val ➝ (∃⁰[“#0 < #1”] φ.val ⇜ (#0 :> (#·.succ.succ))))) (by simp),
811+
⟨ .mkPi (∀⁰ (bf.val 🡒 (∃⁰[“#0 < #1”] φ.val ⇜ (#0 :> (#·.succ.succ))))) (by simp),
812812
by intro v; simp [hbf.df.iff, hp.df.iff] ⟩
813813
| 𝚫 =>
814814
exact .of_sigma_of_pi
815815
⟨ .mkSigma (∃⁰ (bf.val ⋏ (∃⁰[“#0 < #1”] φ.sigma.val ⇜ (#0 :> (#·.succ.succ))))) (by simp),
816816
by intro v; simp [hbf.df.iff, hp.df.iff, HierarchySymbol.Semiformula.val_sigma] ⟩
817-
⟨ .mkPi (∀⁰ (bf.val ➝ (∃⁰[“#0 < #1”] φ.pi.val ⇜ (#0 :> (#·.succ.succ))))) (by simp),
817+
⟨ .mkPi (∀⁰ (bf.val 🡒 (∃⁰[“#0 < #1”] φ.pi.val ⇜ (#0 :> (#·.succ.succ))))) (by simp),
818818
by intro v; simp [hbf.df.iff, hp.df.iff, hp.proper.iff'] ⟩
819819

820820
lemma ball_le [V ⊧ₘ* 𝗣𝗔⁻] {Γ} {P : (Fin k → V) → V → Prop} {f : (Fin k → V) → V}

‎Foundation/FirstOrder/Basic/BinderNotation.lean‎

Lines changed: 18 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -23,13 +23,13 @@ variable {L : Language} {ξ : Type*}
2323

2424
def nestFormulae (φ : Semiformula L ξ n) (Ψ : Fin n → Semiformula L ξ (m + 1)) : Semiformula L ξ m :=
2525
let σ : Semiformula L ξ (m + n) :=
26-
(Matrix.conj fun i : Fin n ↦ Rewriting.subst (Ψ i) (#(i.addCast m) :> fun j ↦ #(j.addNat n))) ➝
26+
(Matrix.conj fun i : Fin n ↦ Rewriting.subst (Ψ i) (#(i.addCast m) :> fun j ↦ #(j.addNat n))) 🡒
2727
Rewriting.subst φ fun i ↦ #(i.addCast m)
2828
∀⁰^[n] σ
2929

3030
def nestFormulaeFunc (φ : Semiformula L ξ (n + 1)) (Ψ : Fin n → Semiformula L ξ (m + 1)) : Semiformula L ξ (m + 1) :=
3131
let σ : Semiformula L ξ ((m + 1) + n) :=
32-
(Matrix.conj fun i : Fin n ↦ Rewriting.subst (Ψ i) (#(i.addCast m.succ) :> fun j ↦ #(j.succ.addNat n))) ➝
32+
(Matrix.conj fun i : Fin n ↦ Rewriting.subst (Ψ i) (#(i.addCast m.succ) :> fun j ↦ #(j.succ.addNat n))) 🡒
3333
Rewriting.subst φ (#((0 : Fin (m + 1)).addNat n) :> fun i ↦ #(i.addCast m.succ))
3434
∀⁰^[n] σ
3535

@@ -375,8 +375,8 @@ macro_rules
375375
| `(⤫formula($type)[ $binders* | $fbinders* | $φ ∧ $ψ ]) => `(⤫formula($type)[ $binders* | $fbinders* | $φ ] ⋏ ⤫formula($type)[ $binders* | $fbinders* | $ψ ])
376376
| `(⤫formula($type)[ $binders* | $fbinders* | $φ ∨ $ψ ]) => `(⤫formula($type)[ $binders* | $fbinders* | $φ ] ⋎ ⤫formula($type)[ $binders* | $fbinders* | $ψ ])
377377
| `(⤫formula($type)[ $binders* | $fbinders* | ¬$φ ]) => `(∼⤫formula($type)[ $binders* | $fbinders* | $φ ])
378-
| `(⤫formula($type)[ $binders* | $fbinders* | $φ → $ψ ]) => `(⤫formula($type)[ $binders* | $fbinders* | $φ ] ➝ ⤫formula($type)[ $binders* | $fbinders* | $ψ ])
379-
| `(⤫formula($type)[ $binders* | $fbinders* | $φ ↔ $ψ ]) => `(⤫formula($type)[ $binders* | $fbinders* | $φ ] ⭤ ⤫formula($type)[ $binders* | $fbinders* | $ψ ])
378+
| `(⤫formula($type)[ $binders* | $fbinders* | $φ → $ψ ]) => `(⤫formula($type)[ $binders* | $fbinders* | $φ ] 🡒 ⤫formula($type)[ $binders* | $fbinders* | $ψ ])
379+
| `(⤫formula($type)[ $binders* | $fbinders* | $φ ↔ $ψ ]) => `(⤫formula($type)[ $binders* | $fbinders* | $φ ] 🡘 ⤫formula($type)[ $binders* | $fbinders* | $ψ ])
380380
| `(⤫formula($type)[ $binders* | $fbinders* | ⋀ $i, $φ ]) => `(Matrix.conj fun $i ↦ ⤫formula($type)[ $binders* | $fbinders* | $φ ])
381381
| `(⤫formula($type)[ $binders* | $fbinders* | ⋁ $i, $φ ]) => `(Matrix.disj fun $i ↦ ⤫formula($type)[ $binders* | $fbinders* | $φ ])
382382
| `(⤫formula($type)[ $binders* | $fbinders* | ⋀ $i < $t, $φ ]) => `(conjLt (fun $i ↦ ⤫formula($type)[ $binders* | $fbinders* | $φ ]) $t)
@@ -718,61 +718,61 @@ macro_rules
718718
| `(⤫formula(faf)[ $binders* | $fbinders* | $t:first_order_term = $u:first_order_term ]) => do
719719
let x₁ : TSyntax `ident ← TSyntax.freshIdent
720720
let x₂ : TSyntax `ident ← TSyntax.freshIdent
721-
`(∀⁰ (⤫term(faf)[ $x₁ $binders* | $fbinders* | $t ] ➝ ∀⁰ (⤫term(faf)[ $x₁ $x₂ $binders* | $fbinders* | $u ] ➝ “#1 = #0”)))
721+
`(∀⁰ (⤫term(faf)[ $x₁ $binders* | $fbinders* | $t ] 🡒 ∀⁰ (⤫term(faf)[ $x₁ $x₂ $binders* | $fbinders* | $u ] 🡒 “#1 = #0”)))
722722
| `(⤫formula(faf)[ $binders* | $fbinders* | $t:first_order_term ≠ $u:first_order_term ]) => do
723723
let x₁ : TSyntax `ident ← TSyntax.freshIdent
724724
let x₂ : TSyntax `ident ← TSyntax.freshIdent
725-
`(∀⁰ (⤫term(faf)[ $x₁ $binders* | $fbinders* | $t ] ➝ ∀⁰ (⤫term(faf)[ $x₁ $x₂ $binders* | $fbinders* | $u ] ➝ “#1 ≠ #0”)))
725+
`(∀⁰ (⤫term(faf)[ $x₁ $binders* | $fbinders* | $t ] 🡒 ∀⁰ (⤫term(faf)[ $x₁ $x₂ $binders* | $fbinders* | $u ] 🡒 “#1 ≠ #0”)))
726726
| `(⤫formula(faf)[ $binders* | $fbinders* | $t:first_order_term < $u:first_order_term ]) => do
727727
let x₁ : TSyntax `ident ← TSyntax.freshIdent
728728
let x₂ : TSyntax `ident ← TSyntax.freshIdent
729-
`(∀⁰ (⤫term(faf)[ $x₁ $binders* | $fbinders* | $t ] ➝ ∀⁰ (⤫term(faf)[ $x₁ $x₂ $binders* | $fbinders* | $u ] ➝ “#1 < #0”)))
729+
`(∀⁰ (⤫term(faf)[ $x₁ $binders* | $fbinders* | $t ] 🡒 ∀⁰ (⤫term(faf)[ $x₁ $x₂ $binders* | $fbinders* | $u ] 🡒 “#1 < #0”)))
730730
| `(⤫formula(faf)[ $binders* | $fbinders* | $t:first_order_term ≮ $u:first_order_term ]) => do
731731
let x₁ : TSyntax `ident ← TSyntax.freshIdent
732732
let x₂ : TSyntax `ident ← TSyntax.freshIdent
733-
`(∀⁰ (⤫term(faf)[ $x₁ $binders* | $fbinders* | $t ] ➝ ∀⁰ (⤫term(faf)[ $x₁ $x₂ $binders* | $fbinders* | $u ] ➝ “#1 ≮ #0”)))
733+
`(∀⁰ (⤫term(faf)[ $x₁ $binders* | $fbinders* | $t ] 🡒 ∀⁰ (⤫term(faf)[ $x₁ $x₂ $binders* | $fbinders* | $u ] 🡒 “#1 ≮ #0”)))
734734
| `(⤫formula(faf)[ $binders* | $fbinders* | $t:first_order_term ≤ $u:first_order_term ]) => do
735735
let x₁ : TSyntax `ident ← TSyntax.freshIdent
736736
let x₂ : TSyntax `ident ← TSyntax.freshIdent
737-
`(∀⁰ (⤫term(faf)[ $x₁ $binders* | $fbinders* | $t ] ➝ ∀⁰ (⤫term(faf)[ $x₁ $x₂ $binders* | $fbinders* | $u ] ➝ “#1 ≤ #0”)))
737+
`(∀⁰ (⤫term(faf)[ $x₁ $binders* | $fbinders* | $t ] 🡒 ∀⁰ (⤫term(faf)[ $x₁ $x₂ $binders* | $fbinders* | $u ] 🡒 “#1 ≤ #0”)))
738738
| `(⤫formula(faf)[ $binders* | $fbinders* | $t:first_order_term ≰ $u:first_order_term ]) => do
739739
let x₁ : TSyntax `ident ← TSyntax.freshIdent
740740
let x₂ : TSyntax `ident ← TSyntax.freshIdent
741-
`(∀⁰ (⤫term(faf)[ $x₁ $binders* | $fbinders* | $t ] ➝ ∀⁰ (⤫term(faf)[ $x₁ $x₂ $binders* | $fbinders* | $u ] ➝ “#1 ≰ #0”)))
741+
`(∀⁰ (⤫term(faf)[ $x₁ $binders* | $fbinders* | $t ] 🡒 ∀⁰ (⤫term(faf)[ $x₁ $x₂ $binders* | $fbinders* | $u ] 🡒 “#1 ≰ #0”)))
742742
| `(⤫formula(faf)[ $binders* | $fbinders* | $t:first_order_term ∈ $u:first_order_term ]) => do
743743
let x₁ : TSyntax `ident ← TSyntax.freshIdent
744744
let x₂ : TSyntax `ident ← TSyntax.freshIdent
745-
`(∀⁰ (⤫term(faf)[ $x₁ $binders* | $fbinders* | $t ] ➝ ∀⁰ (⤫term(faf)[ $x₁ $x₂ $binders* | $fbinders* | $u ] ➝ “#1 ∈ #0”)))
745+
`(∀⁰ (⤫term(faf)[ $x₁ $binders* | $fbinders* | $t ] 🡒 ∀⁰ (⤫term(faf)[ $x₁ $x₂ $binders* | $fbinders* | $u ] 🡒 “#1 ∈ #0”)))
746746
| `(⤫formula(faf)[ $binders* | $fbinders* | $t:first_order_term ∉ $u:first_order_term ]) => do
747747
let x₁ : TSyntax `ident ← TSyntax.freshIdent
748748
let x₂ : TSyntax `ident ← TSyntax.freshIdent
749-
`(∀⁰ (⤫term(faf)[ $x₁ $binders* | $fbinders* | $t ] ➝ ∀⁰ (⤫term(faf)[ $x₁ $x₂ $binders* | $fbinders* | $u ] ➝ “#1 ∉ #0”)))
749+
`(∀⁰ (⤫term(faf)[ $x₁ $binders* | $fbinders* | $t ] 🡒 ∀⁰ (⤫term(faf)[ $x₁ $x₂ $binders* | $fbinders* | $u ] 🡒 “#1 ∉ #0”)))
750750

751751
macro_rules
752752
| `(⤫formula(faf)[ $binders* | $fbinders* | ∀ $x < $t, $φ ]) => do
753753
if binders.elem x then Macro.throwErrorAt x "error: variable is duplicated." else
754754
let vt : TSyntax `ident ← TSyntax.freshIdent
755-
`(∀⁰ (⤫term(faf)[ $vt $binders* | $fbinders* | $t ] ➝ Semiformula.ballLT #0 ⤫formula(faf)[ $x $vt $binders* | $fbinders* | $φ ]))
755+
`(∀⁰ (⤫term(faf)[ $vt $binders* | $fbinders* | $t ] 🡒 Semiformula.ballLT #0 ⤫formula(faf)[ $x $vt $binders* | $fbinders* | $φ ]))
756756
| `(⤫formula(faf)[ $binders* | $fbinders* | ∀ $x ≤ $t, $φ ]) => do
757757
if binders.elem x then Macro.throwErrorAt x "error: variable is duplicated." else
758758
let vt : TSyntax `ident ← TSyntax.freshIdent
759-
`(∀⁰ (⤫term(faf)[ $vt $binders* | $fbinders* | $t ] ➝ Semiformula.ballLE #0 ⤫formula(faf)[ $x $binders* | $fbinders* | $φ ]))
759+
`(∀⁰ (⤫term(faf)[ $vt $binders* | $fbinders* | $t ] 🡒 Semiformula.ballLE #0 ⤫formula(faf)[ $x $binders* | $fbinders* | $φ ]))
760760
| `(⤫formula(faf)[ $binders* | $fbinders* | ∀ $x ∈ $t, $φ ]) => do
761761
if binders.elem x then Macro.throwErrorAt x "error: variable is duplicated." else
762762
let vt : TSyntax `ident ← TSyntax.freshIdent
763-
`(∀⁰ (⤫term(faf)[ $vt $binders* | $fbinders* | $t ] ➝ Semiformula.ballMem #0 ⤫formula(faf)[ $x $vt $binders* | $fbinders* | $φ ]))
763+
`(∀⁰ (⤫term(faf)[ $vt $binders* | $fbinders* | $t ] 🡒 Semiformula.ballMem #0 ⤫formula(faf)[ $x $vt $binders* | $fbinders* | $φ ]))
764764
| `(⤫formula(faf)[ $binders* | $fbinders* | ∃ $x < $t, $φ ]) => do
765765
if binders.elem x then Macro.throwErrorAt x "error: variable is duplicated." else
766766
let vt : TSyntax `ident ← TSyntax.freshIdent
767-
`(∀⁰ (⤫term(faf)[ $vt $binders* | $fbinders* | $t ] ➝ Semiformula.bexsLT #0 ⤫formula(faf)[ $x $vt $binders* | $fbinders* | $φ ]))
767+
`(∀⁰ (⤫term(faf)[ $vt $binders* | $fbinders* | $t ] 🡒 Semiformula.bexsLT #0 ⤫formula(faf)[ $x $vt $binders* | $fbinders* | $φ ]))
768768
| `(⤫formula(faf)[ $binders* | $fbinders* | ∃ $x ≤ $t, $φ ]) => do
769769
if binders.elem x then Macro.throwErrorAt x "error: variable is duplicated." else
770770
let vt : TSyntax `ident ← TSyntax.freshIdent
771-
`(∀⁰ (⤫term(faf)[ $vt $binders* | $fbinders* | $t ] ➝ Semiformula.bexsLE #0 ⤫formula(faf)[ $x $vt $binders* | $fbinders* | $φ ]))
771+
`(∀⁰ (⤫term(faf)[ $vt $binders* | $fbinders* | $t ] 🡒 Semiformula.bexsLE #0 ⤫formula(faf)[ $x $vt $binders* | $fbinders* | $φ ]))
772772
| `(⤫formula(faf)[ $binders* | $fbinders* | ∃ $x ∈ $t, $φ ]) => do
773773
if binders.elem x then Macro.throwErrorAt x "error: variable is duplicated." else
774774
let vt : TSyntax `ident ← TSyntax.freshIdent
775-
`(∀⁰ (⤫term(faf)[ $vt $binders* | $fbinders* | $t ] ➝ Semiformula.bexsMem #0 ⤫formula(faf)[ $x $vt $binders* | $fbinders* | $φ ]))
775+
`(∀⁰ (⤫term(faf)[ $vt $binders* | $fbinders* | $t ] 🡒 Semiformula.bexsMem #0 ⤫formula(faf)[ $x $vt $binders* | $fbinders* | $φ ]))
776776

777777
syntax "f‘" first_order_term:0 "’" : term
778778
syntax "f‘" ident* "| " first_order_term:0 "’" : term

‎Foundation/FirstOrder/Basic/Calculus.lean‎

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -475,11 +475,11 @@ instance {𝓢 U : Schema L} : 𝓢 ⪯ 𝓢 ∪ U := Entailment.Axiomatized.wea
475475

476476
instance {𝓢 U : Schema L} : U ⪯ 𝓢 ∪ U := Entailment.Axiomatized.weakerThanOfSubset (by simp)
477477

478-
def deduction [L.DecidableEq] {𝓢 : Schema L} {φ ψ} (b : insert φ 𝓢 ⊢! ψ) : 𝓢 ⊢! φ.univCl' ➝ ψ :=
478+
def deduction [L.DecidableEq] {𝓢 : Schema L} {φ ψ} (b : insert φ 𝓢 ⊢! ψ) : 𝓢 ⊢! φ.univCl' 🡒 ψ :=
479479
have : 𝓢 ⟹ [∼φ.univCl', ψ] := Derivation.deduction b
480480
(Tait.or this).cast (by simp; rfl)
481481

482-
theorem deduction! [L.DecidableEq] {𝓢 : Schema L} {φ ψ} (b : insert φ 𝓢 ⊢ ψ) : 𝓢 ⊢ φ.univCl' ➝ ψ :=
482+
theorem deduction! [L.DecidableEq] {𝓢 : Schema L} {φ ψ} (b : insert φ 𝓢 ⊢ ψ) : 𝓢 ⊢ φ.univCl' 🡒 ψ :=
483483
⟨deduction b.get⟩
484484

485485
lemma close!_iff [L.DecidableEq] {𝓢 : Schema L} {φ} : 𝓢 ⊢ φ.univCl' ↔ 𝓢 ⊢ φ := by
@@ -515,14 +515,14 @@ instance : Axiomatized (Theory L) where
515515
prfAxm {T} σ h := ofSyntacticProof <| Axiomatized.prfAxm (by simpa using h)
516516
weakening {σ T B} h b := ofSyntacticProof <| Axiomatized.weakening (by simpa using h) b
517517

518-
def deduction [L.DecidableEq] {T : Theory L} {σ τ} (b : insert σ T ⊢! τ) : T ⊢! σ ➝ τ :=
518+
def deduction [L.DecidableEq] {T : Theory L} {σ τ} (b : insert σ T ⊢! τ) : T ⊢! σ 🡒 τ :=
519519
have : insert ↑σ T.toSchema ⊢! ↑τ := by simpa using toSyntacticProof b
520520
(Schema.deduction this).cast (by simp)
521521

522522
instance [L.DecidableEq] : Entailment.Deduction (Theory L) where
523523
ofInsert := Theory.deduction
524524
inv {σ τ T} b :=
525-
have : adjoin σ T ⊢! σ ➝ τ := Axiomatized.weakening (by simp) b
525+
have : adjoin σ T ⊢! σ 🡒 τ := Axiomatized.weakening (by simp) b
526526
this ⨀ (Axiomatized.adjoin _ _)
527527

528528
def compact! [L.DecidableEq] {T : Theory L} {φ : Sentence L} :
@@ -571,7 +571,7 @@ instance : Entailment.StrongCut (Theory L) (Theory L) where
571571
(toSyntacticProof d)
572572

573573
lemma compact' [L.DecidableEq] {T : Theory L} {φ : Sentence L}
574-
(b : T ⊢ φ) : ∃ (s : { s : Finset (Sentence L) // ↑s ⊆ T}), (∅ : Theory L) ⊢ s.val.conj ➝ φ := by
574+
(b : T ⊢ φ) : ∃ (s : { s : Finset (Sentence L) // ↑s ⊆ T}), (∅ : Theory L) ⊢ s.val.conj 🡒 φ := by
575575
let ⟨s, b⟩ := compact b
576576
let bc : ({s.val.conj} : Theory L) ⊢ s.val.conj := Axiomatized.provable_axm _ (by simp)
577577
have : {s.val.conj} ⊢ φ := StrongCut.cut! (fun {ψ} hψ ↦ Entailment.left_Fconj!_intro (by simpa) ⨀ bc) b
@@ -656,23 +656,23 @@ namespace Schema
656656

657657
variable {𝓢 : Schema L}
658658

659-
def specialize! (φ : SyntacticSemiformula L 1) (t : SyntacticTerm L) : 𝓢 ⊢! ∀⁰ φ ➝ φ/[t] :=
659+
def specialize! (φ : SyntacticSemiformula L 1) (t : SyntacticTerm L) : 𝓢 ⊢! ∀⁰ φ 🡒 φ/[t] :=
660660
have : 𝓢 ⟹ [(∼φ)/[t], φ/[t]] := Derivation.em (φ := φ/[t]) (by simp) (by simp)
661661
have : 𝓢 ⟹ [∃⁰ ∼φ, φ/[t]] := this.exs t
662662
this.or.cast (by simp [Semiformula.imp_eq])
663663

664-
lemma specialize (φ : SyntacticSemiformula L 1) (t : SyntacticTerm L) : 𝓢 ⊢ ∀⁰ φ ➝ φ/[t] := ⟨specialize! φ t⟩
664+
lemma specialize (φ : SyntacticSemiformula L 1) (t : SyntacticTerm L) : 𝓢 ⊢ ∀⁰ φ 🡒 φ/[t] := ⟨specialize! φ t⟩
665665

666666
end Schema
667667

668668
namespace Theory
669669

670670
variable {T : Theory L}
671671

672-
def specialize! (φ : Semisentence L 1) (t) : T ⊢! ∀⁰ φ ➝ φ/[t] := ofSyntacticProof <| by
672+
def specialize! (φ : Semisentence L 1) (t) : T ⊢! ∀⁰ φ 🡒 φ/[t] := ofSyntacticProof <| by
673673
simpa [Semiformula.coe_subst_eq_subst_coe₁] using (Schema.specialize! (𝓢 := T) φ (t : SyntacticTerm L))
674674

675-
lemma specialize (φ : Semisentence L 1) (t) : T ⊢ ∀⁰ φ ➝ φ/[t] := ⟨specialize! φ t⟩
675+
lemma specialize (φ : Semisentence L 1) (t) : T ⊢ ∀⁰ φ 🡒 φ/[t] := ⟨specialize! φ t⟩
676676

677677
end Theory
678678

‎Foundation/FirstOrder/Basic/Definability.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -219,7 +219,7 @@ lemma of_iff {P Q : (Fin k → M) → Prop} (H : L.Definable Q) (h : ∀ x, P x
219219
L.Definable fun v : Fin k → M ↦ R v → S v := by
220220
rcases hR with ⟨φ, hR⟩
221221
rcases hS with ⟨ψ, hS⟩
222-
exact ⟨φ ➝ ψ, by intro _; simp [hR.iff, hS.iff]⟩
222+
exact ⟨φ 🡒 ψ, by intro _; simp [hR.iff, hS.iff]⟩
223223

224224
@[grind .] lemma not {R : (Fin k → M) → Prop} (hR : L.Definable R) :
225225
L.Definable fun v : Fin k → M ↦ ¬R v := by
@@ -230,7 +230,7 @@ lemma of_iff {P Q : (Fin k → M) → Prop} (H : L.Definable Q) (h : ∀ x, P x
230230
L.Definable fun v : Fin k → M ↦ R v ↔ S v := by
231231
rcases hR with ⟨φ, hR⟩
232232
rcases hS with ⟨ψ, hS⟩
233-
exact ⟨φ ⭤ ψ, by intro _; simp [hR.iff, hS.iff]⟩
233+
exact ⟨φ 🡘 ψ, by intro _; simp [hR.iff, hS.iff]⟩
234234

235235
lemma all {R : (Fin k → M) → M → Prop} (hR : L.Definable fun w ↦ R (w ·.succ) (w 0)) :
236236
L.Definable fun v : Fin k → M ↦ ∀ x, R v x := by

0 commit comments

Comments
 (0)