diff --git a/Cslib.lean b/Cslib.lean
index 6e70be7b9..168124fc1 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -71,6 +71,14 @@ public import Cslib.Foundations.Data.StackTape
 public import Cslib.Foundations.Lint.Basic
 public import Cslib.Foundations.Logic.InferenceSystem
 public import Cslib.Foundations.Logic.LogicalEquivalence
+public import Cslib.Foundations.Logic.Operators.And
+public import Cslib.Foundations.Logic.Operators.Box
+public import Cslib.Foundations.Logic.Operators.Diamond
+public import Cslib.Foundations.Logic.Operators.Iff
+public import Cslib.Foundations.Logic.Operators.Impl
+public import Cslib.Foundations.Logic.Operators.Not
+public import Cslib.Foundations.Logic.Operators.Or
+public import Cslib.Foundations.Logic.Operators.Tensor
 public import Cslib.Foundations.Relation.Attr
 public import Cslib.Foundations.Relation.Confluence
 public import Cslib.Foundations.Relation.Defs
diff --git a/Cslib/Foundations/Logic/LogicalEquivalence.lean b/Cslib/Foundations/Logic/LogicalEquivalence.lean
index 7f6c0d332..f4dbc06d9 100644
--- a/Cslib/Foundations/Logic/LogicalEquivalence.lean
+++ b/Cslib/Foundations/Logic/LogicalEquivalence.lean
@@ -8,6 +8,7 @@ module
 
 public import Cslib.Foundations.Syntax.Context
 public import Cslib.Foundations.Syntax.Congruence
+public import Cslib.Foundations.Logic.InferenceSystem
 
 /-! Typeclass and notation for logical equivalence. -/
 
@@ -15,21 +16,33 @@ public import Cslib.Foundations.Syntax.Congruence
 
 namespace Cslib.Logic
 
+open scoped InferenceSystem
+
 /-- A logical equivalence for a given type of `Judgement`s is a congruence on propositions that
 preserves validity of judgements under any judgemental context. -/
-class LogicalEquivalence
+class LogicalEquivalence S
     (Proposition : Type u) [HasContext Proposition]
     (Judgement : Type v) [HasHContext Judgement Proposition]
-    (Valid : Judgement → Sort w) where
-  /-- The logical equivalence relation. -/
+    [InferenceSystem S Judgement] where
+  /-- `a ≡[S] b` means that `a` and `b` are logically equivalent in the inference system `S`. -/
   eqv (a b : Proposition) : Prop
   /-- Proof that `eqv` is a congruence. -/
   [congruence : Congruence Proposition eqv]
   /-- Validity is preserved for any judgemental context. -/
   eqvFillValid (heqv : eqv a b) (c : HasHContext.Context Judgement Proposition)
-    (h : Valid (c<[a])) : Valid (c<[b])
+    (h : S⇓(c<[a])) : S⇓(c<[b])
 
 @[inherit_doc]
-scoped infix:29 " ≡ " => LogicalEquivalence.eqv
+scoped notation a " ≡[" S "]" b => LogicalEquivalence.eqv S a b
+
+/-- Class for types (`α`) that have a canonical logical equivalence (under a canonical, default
+inference system). -/
+abbrev HasLogicalEquivalence (Proposition : Type u) [HasContext Proposition]
+    (Judgement : Type v) [HasHContext Judgement Proposition]
+    [HasInferenceSystem Judgement] :=
+  LogicalEquivalence InferenceSystem.Default Proposition Judgement
+
+/-- `a ≡ b` means that `a` and `b` are logically equivalent. -/
+scoped infix:29 " ≡ " => LogicalEquivalence.eqv InferenceSystem.Default
 
 end Cslib.Logic
diff --git a/Cslib/Foundations/Logic/Operators/And.lean b/Cslib/Foundations/Logic/Operators/And.lean
new file mode 100644
index 000000000..f562e919c
--- /dev/null
+++ b/Cslib/Foundations/Logic/Operators/And.lean
@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+module
+
+public import Cslib.Init
+
+/-! # And connective (∧) -/
+
+@[expose] public section
+
+namespace Cslib.Logic
+
+/-- The type `α` has an and connective (`∧`). -/
+class HasAnd (α : Type*) where
+  /-- `a ∧ b` is the conjunction of `a` and `b`. -/
+  and (a b : α) : α
+
+@[inherit_doc] scoped infixr:36 " ∧ " => HasAnd.and
+
+end Cslib.Logic
diff --git a/Cslib/Foundations/Logic/Operators/Box.lean b/Cslib/Foundations/Logic/Operators/Box.lean
new file mode 100644
index 000000000..19421c8d4
--- /dev/null
+++ b/Cslib/Foundations/Logic/Operators/Box.lean
@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+module
+
+public import Cslib.Init
+
+/-! # Box modality (□) -/
+
+@[expose] public section
+
+namespace Cslib.Logic
+
+/-- The type `α` has a box modality (`□`). -/
+class HasBox (α : Type*) where
+  /-- `a` is valid in all immediately reachable states. -/
+  box (a : α) : α
+
+@[inherit_doc] scoped prefix:40 "□" => HasBox.box
+
+end Cslib.Logic
diff --git a/Cslib/Foundations/Logic/Operators/Diamond.lean b/Cslib/Foundations/Logic/Operators/Diamond.lean
new file mode 100644
index 000000000..d15741fb5
--- /dev/null
+++ b/Cslib/Foundations/Logic/Operators/Diamond.lean
@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+module
+
+public import Cslib.Init
+
+/-! # Diamond modality (◇) -/
+
+@[expose] public section
+
+namespace Cslib.Logic
+
+/-- The type `α` has a diamond modality (`◇`). -/
+class HasDiamond (α : Type*) where
+  /-- `a` is valid in a reachable state. -/
+  diamond (a : α) : α
+
+@[inherit_doc] scoped prefix:40 "◇" => HasDiamond.diamond
+
+end Cslib.Logic
diff --git a/Cslib/Foundations/Logic/Operators/Iff.lean b/Cslib/Foundations/Logic/Operators/Iff.lean
new file mode 100644
index 000000000..7617b9e35
--- /dev/null
+++ b/Cslib/Foundations/Logic/Operators/Iff.lean
@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi, Thomas Waring
+-/
+
+module
+
+public import Cslib.Init
+
+/-! # Iff connective (↔) -/
+
+@[expose] public section
+
+namespace Cslib.Logic
+
+/-- The type `α` has a bi-implication connective (`↔`). -/
+class HasIff (α : Type*) where
+  /-- `a ↔ b` denotes `a` implies `b` and vice-versa. -/
+  iff (a b : α) : α
+
+@[inherit_doc] scoped infixr:20 " ↔ " => HasIff.iff
+
+end Cslib.Logic
diff --git a/Cslib/Foundations/Logic/Operators/Impl.lean b/Cslib/Foundations/Logic/Operators/Impl.lean
new file mode 100644
index 000000000..5ef62666e
--- /dev/null
+++ b/Cslib/Foundations/Logic/Operators/Impl.lean
@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi, Thomas Waring
+-/
+
+module
+
+public import Cslib.Init
+
+/-! # Impl connective (→) -/
+
+@[expose] public section
+
+namespace Cslib.Logic
+
+/-- The type `α` has an implication connective (`→`). -/
+class HasImpl (α : Type*) where
+  /-- `a → b` denotes `a` implies `b`. -/
+  impl (a b : α) : α
+
+@[inherit_doc] scoped infixr:25 " → " => HasImpl.impl
+
+end Cslib.Logic
diff --git a/Cslib/Foundations/Logic/Operators/Not.lean b/Cslib/Foundations/Logic/Operators/Not.lean
new file mode 100644
index 000000000..76489f4a1
--- /dev/null
+++ b/Cslib/Foundations/Logic/Operators/Not.lean
@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+module
+
+public import Cslib.Init
+
+/-! # Negation connective (¬) -/
+
+@[expose] public section
+
+namespace Cslib.Logic
+
+/-- The type `α` has a negation connective (`¬`). -/
+class HasNot (α : Type*) where
+  /-- `¬a` is the negation of `a`. -/
+  not (a : α) : α
+
+@[inherit_doc] scoped notation:max "¬" p:40 => HasNot.not p
+
+end Cslib.Logic
diff --git a/Cslib/Foundations/Logic/Operators/Or.lean b/Cslib/Foundations/Logic/Operators/Or.lean
new file mode 100644
index 000000000..1f1aadab0
--- /dev/null
+++ b/Cslib/Foundations/Logic/Operators/Or.lean
@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi, Thomas Waring
+-/
+
+module
+
+public import Cslib.Init
+
+/-! # Or connective (∨) -/
+
+@[expose] public section
+
+namespace Cslib.Logic
+
+/-- The type `α` has an or connective (`∨`). -/
+class HasOr (α : Type*) where
+  /-- `a ∨ b` is the disjunction of `a` and `b`. -/
+  or (a b : α) : α
+
+@[inherit_doc] scoped infixr:30 " ∨ " => HasOr.or
+
+end Cslib.Logic
diff --git a/Cslib/Foundations/Logic/Operators/Tensor.lean b/Cslib/Foundations/Logic/Operators/Tensor.lean
new file mode 100644
index 000000000..45f66174c
--- /dev/null
+++ b/Cslib/Foundations/Logic/Operators/Tensor.lean
@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+module
+
+public import Cslib.Init
+
+/-! # Tensor connective (⊗) -/
+
+@[expose] public section
+
+namespace Cslib.Logic
+
+/-- The type `α` has a tensor connective (⊗). -/
+class HasTensor (α : Type*) where
+  /-- `a ⊗ b` is the multiplicative conjunction of `a` and `b`. -/
+  tensor (a b : α) : α
+
+@[inherit_doc] scoped infixr:35 " ⊗ " => HasTensor.tensor
+
+end Cslib.Logic
diff --git a/Cslib/Logics/LinearLogic/CLL/Basic.lean b/Cslib/Logics/LinearLogic/CLL/Basic.lean
index c331ae2ae..ce8db29a4 100644
--- a/Cslib/Logics/LinearLogic/CLL/Basic.lean
+++ b/Cslib/Logics/LinearLogic/CLL/Basic.lean
@@ -650,7 +650,7 @@ instance : Congruence (Proposition Atom) Proposition.Equiv where
     intro ctx a b hab
     induction ctx <;> grind [= Context.fill]
 
-noncomputable instance : LogicalEquivalence (Proposition Atom) (Sequent Atom) Proof where
+noncomputable instance : HasLogicalEquivalence (Proposition Atom) (Sequent Atom) where
   eqv := Proposition.Equiv
   eqvFillValid {a b : Proposition Atom} (heqv : a.Equiv b)
       (c : HasHContext.Context (Sequent Atom) (Proposition Atom))
diff --git a/Cslib/Logics/Modal/Basic.lean b/Cslib/Logics/Modal/Basic.lean
index fda217a1c..0d08da3d5 100644
--- a/Cslib/Logics/Modal/Basic.lean
+++ b/Cslib/Logics/Modal/Basic.lean
@@ -6,7 +6,13 @@ Authors: Fabrizio Montesi, Marianna Girlando
 
 module
 
-public import Cslib.Init
+public import Cslib.Foundations.Logic.Operators.And
+public import Cslib.Foundations.Logic.Operators.Or
+public import Cslib.Foundations.Logic.Operators.Impl
+public import Cslib.Foundations.Logic.Operators.Not
+public import Cslib.Foundations.Logic.Operators.Box
+public import Cslib.Foundations.Logic.Operators.Diamond
+public import Cslib.Foundations.Logic.Operators.Iff
 public import Cslib.Foundations.Logic.InferenceSystem
 public import Mathlib.Data.Set.Basic
 public import Mathlib.Order.Defs.Unbundled
@@ -47,29 +53,51 @@ inductive Proposition (Atom : Type u) : Type u where
   /-- Possibility. -/
   | diamond (φ : Proposition Atom)
 
-@[inherit_doc] scoped prefix:40 "¬" => Proposition.not
-@[inherit_doc] scoped infix:36 " ∧ " => Proposition.and
-@[inherit_doc] scoped prefix:40 "◇" => Proposition.diamond
+instance : HasNot (Proposition Atom) := {not := Proposition.not}
+instance : HasAnd (Proposition Atom) := {and := Proposition.and}
+instance : HasDiamond (Proposition Atom) := {diamond := Proposition.diamond}
+
+@[scoped grind =]
+lemma Proposition.not_def (φ : Proposition Atom) : φ.not = ¬φ := rfl
+
+@[scoped grind =]
+lemma Proposition.and_def (φ₁ φ₂ : Proposition Atom) : φ₁.and φ₂ = (φ₁ ∧ φ₂) := rfl
+
+@[scoped grind =]
+lemma Proposition.diamond_def (φ : Proposition Atom) : φ.diamond = (◇φ) := rfl
 
 /-- Disjunction. -/
 def Proposition.or (φ₁ φ₂ : Proposition Atom) : Proposition Atom := ¬(¬φ₁ ∧ ¬φ₂)
 
-@[inherit_doc] scoped infix:35 " ∨ " => Proposition.or
+instance : HasOr (Proposition Atom) := {or := Proposition.or}
+
+@[scoped grind =]
+lemma Proposition.or_def (φ₁ φ₂ : Proposition Atom) : φ₁.or φ₂ = (φ₁ ∨ φ₂) := rfl
 
 /-- Implication. -/
 def Proposition.impl (φ₁ φ₂ : Proposition Atom) : Proposition Atom := ¬φ₁ ∨ φ₂
 
-@[inherit_doc] scoped infix:30 " → " => Proposition.impl
+instance : HasImpl (Proposition Atom) := {impl := Proposition.impl}
+
+@[scoped grind =]
+lemma Proposition.impl_def (φ₁ φ₂ : Proposition Atom) : φ₁.impl φ₂ = (φ₁ → φ₂) := rfl
 
 /-- Bi-implication. -/
 def Proposition.iff (φ₁ φ₂ : Proposition Atom) : Proposition Atom := (φ₁ → φ₂) ∧ (φ₂ → φ₁)
 
-@[inherit_doc] scoped infix:30 " ↔ " => Proposition.iff
+instance : HasIff (Proposition Atom) := {iff := Proposition.iff}
+
+@[scoped grind =]
+lemma Proposition.iff_def (φ₁ φ₂ : Proposition Atom) :
+    φ₁.iff φ₂ = (φ₁ ↔ φ₂) := rfl
 
 /-- Necessity. -/
 def Proposition.box (φ : Proposition Atom) : Proposition Atom := ¬◇¬φ
 
-@[inherit_doc] scoped prefix:40 "□" => Proposition.box
+instance : HasBox (Proposition Atom) := {box := Proposition.box}
+
+@[scoped grind =]
+lemma Proposition.box_def (φ : Proposition Atom) : φ.box = (□φ) := rfl
 
 /-- Satisfaction relation. `Satisfies m w φ` means that, in the model `m`, the world `w` satisfies
 the proposition `φ`. -/
@@ -107,8 +135,15 @@ theorem derivation_def {m : Model World Atom} {w : World} {φ : Proposition Atom
 
 /-- A world satisfies a proposition iff it does not satisfy the negation of the proposition. -/
 @[scoped grind =]
-theorem not_satisfies : ⇓Modal[m,w ⊨ ¬φ] ↔ ¬⇓Modal[m,w ⊨ φ] := by
-  induction φ generalizing w <;> grind
+theorem Satisfies.not_iff_not : ⇓Modal[m,w ⊨ ¬φ] ↔ ¬⇓Modal[m,w ⊨ φ] := by rfl
+
+@[scoped grind =]
+theorem Satisfies.and_iff_and {m : Model World Atom} :
+    ⇓Modal[m,w ⊨ φ₁ ∧ φ₂] ↔ ⇓Modal[m,w ⊨ φ₁] ∧ ⇓Modal[m,w ⊨ φ₂] := by rfl
+
+@[scoped grind =]
+theorem Satisfies.diamond_iff_exists {m : Model World Atom} :
+    ⇓Modal[m,w ⊨ ◇φ] ↔ ∃ w', m.r w w' ∧ ⇓Modal[m,w' ⊨ φ] := by rfl
 
 /-- Characterisation of the `∨` connective.
 
@@ -116,7 +151,8 @@ Disjunction is defined in terms of the more primitive connectives given in `Prop
 This result proves that the definition is correct. -/
 @[scoped grind =]
 theorem Satisfies.or_iff_or {m : Model World Atom} :
-    ⇓Modal[m,w ⊨ φ₁ ∨ φ₂] ↔ ⇓Modal[m,w ⊨ φ₁] ∨ ⇓Modal[m,w ⊨ φ₂] := by grind [Proposition.or]
+    ⇓Modal[m,w ⊨ φ₁ ∨ φ₂] ↔ ⇓Modal[m,w ⊨ φ₁] ∨ ⇓Modal[m,w ⊨ φ₂] := by
+  grind [=_ Proposition.or_def, Proposition.or]
 
 /-- Characterisation of the `→` connective.
 
@@ -125,7 +161,8 @@ This result proves that the definition is correct.
 -/
 @[scoped grind =]
 theorem Satisfies.impl_iff_impl {m : Model World Atom} :
-    ⇓Modal[m,w ⊨ φ₁ → φ₂] ↔ (⇓Modal[m,w ⊨ φ₁] → ⇓Modal[m,w ⊨ φ₂]) := by grind [Proposition.impl]
+    ⇓Modal[m,w ⊨ φ₁ → φ₂] ↔ (⇓Modal[m,w ⊨ φ₁] → ⇓Modal[m,w ⊨ φ₂]) := by
+  grind [=_ Proposition.impl_def, Proposition.impl]
 
 /-- Characterisation of the `↔` connective.
 
@@ -134,7 +171,7 @@ This result proves that the definition is correct. -/
 @[scoped grind =]
 theorem Satisfies.iff_iff_iff {m : Model World Atom} :
     ⇓Modal[m,w ⊨ φ₁ ↔ φ₂] ↔ (⇓Modal[m,w ⊨ φ₁] ↔ ⇓Modal[m,w ⊨ φ₂]) := by
-  simp only [Proposition.iff]
+  simp only [HasIff.iff, Proposition.iff]
   grind [= derivation_def]
 
 /-- Characterisation of the `□` modality.
@@ -143,7 +180,8 @@ Necessity is defined in terms of the more primitive connectives given in `Propos
 This result proves that the definition is correct. -/
 @[scoped grind =]
 theorem Satisfies.box_iff_forall {m : Model World Atom} :
-    ⇓Modal[m,w ⊨ □φ] ↔ ∀ w', m.r w w' → ⇓Modal[m,w' ⊨ φ] := by grind [Proposition.box]
+    ⇓Modal[m,w ⊨ □φ] ↔ ∀ w', m.r w w' → ⇓Modal[m,w' ⊨ φ] := by
+  grind [=_ Proposition.box_def, Proposition.box]
 
 /-- The theory of a world in a model is the set of all propositions that it satifies. -/
 abbrev theory (m : Model World Atom) (w : World) : Set (Proposition Atom) :=
@@ -162,7 +200,7 @@ theorem satisfies_theory (h : Satisfies m w φ) : φ ∈ theory m w := by grind
 
 /-- If two worlds are not theory equivalent, there exists a distinguishing proposition. -/
 lemma not_theoryEq_satisfies (h : ¬TheoryEq m w₁ w₂) :
-    ∃ φ, (⇓Modal[m,w₁ ⊨ φ] ∧ ¬⇓Modal[m,w₂ ⊨ φ]) := by grind [=_ not_satisfies]
+    ∃ φ, (⇓Modal[m,w₁ ⊨ φ] ∧ ¬⇓Modal[m,w₂ ⊨ φ]) := by grind [=_ Satisfies.not_iff_not]
 
 /-- If two worlds are theory equivalent and the former satisfies a proposition, the latter does as
 well. -/
@@ -174,11 +212,13 @@ theorem theoryEq_satisfies {m : Model World Atom} (h : TheoryEq m w₁ w₂)
 /-- The K axiom, valid for all models. -/
 theorem Satisfies.k : ⇓Modal[m,w ⊨ □(φ₁ → φ₂) → (□φ₁ → □φ₂)] := by grind
 
-set_option linter.tacticAnalysis.verifyGrindOnly false in
 /-- The dual axiom, valid for all models. -/
 theorem Satisfies.dual : ⇓Modal[m,w ⊨ ◇φ ↔ ¬□¬φ] := by
-  grind only [Satisfies.iff_iff_iff.mpr, → satisfies_theory, usr Set.mem_setOf_eq, = impl_iff_impl,
-    =_ derivation_def, = not_satisfies, Satisfies, = box_iff_forall, = Set.setOf_true]
+  constructor
+  · grind
+  · grind
+    --  only [→ satisfies_theory, usr Set.mem_setOf_eq, = impl_iff_impl, = derivation_def,
+    -- = not_satisfies, Satisfies, = box_iff_forall, = Set.setOf_true]
 
 /-- The T axiom, valid for all reflexive models. -/
 theorem Satisfies.t {m : Model World Atom} [instRefl : Std.Refl m.r] {w : World}
diff --git a/Cslib/Logics/Modal/Denotation.lean b/Cslib/Logics/Modal/Denotation.lean
index b74e8f3f1..4b3415b33 100644
--- a/Cslib/Logics/Modal/Denotation.lean
+++ b/Cslib/Logics/Modal/Denotation.lean
@@ -18,7 +18,7 @@ A denotational semantics for modal logic, inspired by the one for Hennessy-Milne
 
 namespace Cslib.Logic.Modal
 
-open scoped Proposition InferenceSystem
+open scoped Proposition InferenceSystem Satisfies
 
 /-- Denotation of a proposition. -/
 @[simp, scoped grind =]
diff --git a/Cslib/Logics/Modal/LogicalEquivalence.lean b/Cslib/Logics/Modal/LogicalEquivalence.lean
index 0fc089e4e..0f34ad0e5 100644
--- a/Cslib/Logics/Modal/LogicalEquivalence.lean
+++ b/Cslib/Logics/Modal/LogicalEquivalence.lean
@@ -122,8 +122,8 @@ lemma Satisfies.Context.fill_def {c : Satisfies.Context World Atom} :
 open scoped Satisfies.Context
 
 /-- Logical equivalence for Modal Logic K. That is, no assumptions on models are made. -/
-instance : LogicalEquivalence
-    (Proposition Atom) (Judgement World Atom) Satisfies.Bundled where
+instance : HasLogicalEquivalence
+    (Proposition Atom) (Judgement World Atom) where
   eqv := Proposition.Equiv Set.univ
   eqvFillValid heqv c h := by
     specialize heqv c.m
diff --git a/Cslib/Logics/Propositional/Defs.lean b/Cslib/Logics/Propositional/Defs.lean
index e9c603d91..d76539323 100644
--- a/Cslib/Logics/Propositional/Defs.lean
+++ b/Cslib/Logics/Propositional/Defs.lean
@@ -6,6 +6,10 @@ Authors: Thomas Waring
 
 module
 
+public import Cslib.Foundations.Logic.Operators.And
+public import Cslib.Foundations.Logic.Operators.Or
+public import Cslib.Foundations.Logic.Operators.Impl
+public import Cslib.Foundations.Logic.Operators.Not
 public import Cslib.Foundations.Logic.InferenceSystem
 public import Mathlib.Data.FunLike.Basic
 public import Mathlib.Data.Set.Image
@@ -30,8 +34,10 @@ theory.
 
 ## Notation
 
-We introduce notation for the logical connectives: `⊥ ⊤ ∧ ∨ → ¬` for, respectively, falsum, verum,
-conjunction, disjunction, implication and negation.
+We instantiate the notation classes `HasAnd`, `HasOr`, `HasImpl` and `HasNot` for `Proposition Atom`
+to give access to, respectively, the notations `∧, ∨, →` and `¬` for propositional connectives.
+In the case that `Atom` has a bottom element (respectively, is inhabited) we give instances
+`HasBot (Proposition Atom)` and (respectively, `HasTop (Proposition Atom)`).
 -/
 
 @[expose] public section
@@ -67,10 +73,14 @@ instance instTopProposition [Inhabited Atom] : Top (Proposition Atom) := ⟨.top
 
 example [Bot Atom] : (⊤ : Proposition Atom) = Proposition.impl ⊥ ⊥ := rfl
 
-@[inherit_doc] scoped infix:36 " ∧ " => Proposition.and
-@[inherit_doc] scoped infix:35 " ∨ " => Proposition.or
-@[inherit_doc] scoped infix:30 " → " => Proposition.impl
-@[inherit_doc] scoped prefix:40 " ¬ " => Proposition.neg
+instance : HasAnd (Proposition Atom) := {and := Proposition.and}
+instance : HasOr (Proposition Atom) := {or := Proposition.or}
+instance : HasImpl (Proposition Atom) := {impl := Proposition.impl}
+instance [Bot Atom] : HasNot (Proposition Atom) := {not := Proposition.neg}
+
+omit [DecidableEq Atom] in
+@[grind =]
+lemma not_eq [Bot Atom] (A : Proposition Atom) : (A → ⊥) = ¬ A := rfl
 
 /-- Substitute each atom in a proposition for a proposition, possibly changing the atomic
 language. -/