diff --git a/library/init/algebra/classes.lean b/library/init/algebra/classes.lean
index 93e14146b3..378cca49f3 100644
--- a/library/init/algebra/classes.lean
+++ b/library/init/algebra/classes.lean
@@ -71,34 +71,49 @@ class is_idempotent (α : Type u) (f : α → α) : Prop :=
 (idempotent : ∀ a, f (f a) = f a)
 -/
 
+/-- `is_irrefl X r` means the binary relation `r` on `X` is irreflexive (that is, `r x x` never
+holds). -/
 @[algebra] class is_irrefl (α : Type u) (r : α → α → Prop) : Prop :=
 (irrefl : ∀ a, ¬ r a a)
 
+/-- `is_refl X r` means the binary relation `r` on `X` is reflexive. -/
 @[algebra] class is_refl (α : Type u) (r : α → α → Prop) : Prop :=
 (refl : ∀ a, r a a)
 
+/-- `is_symm X r` means the binary relation `r` on `X` is symmetric. -/
 @[algebra] class is_symm (α : Type u) (r : α → α → Prop) : Prop :=
 (symm : ∀ a b, r a b → r b a)
 
+/-- The opposite of a symmetric relation is symmetric. -/
 instance is_symm_op_of_is_symm (α : Type u) (r : α → α → Prop) [is_symm α r] : is_symm_op α Prop r :=
 {symm_op := λ a b, propext $ iff.intro (is_symm.symm a b) (is_symm.symm b a)}
 
+/-- `is_asymm X r` means that the binary relation `r` on `X` is asymmetric, that is,
+`r a b → ¬ r b a`. -/
 @[algebra] class is_asymm (α : Type u) (r : α → α → Prop) : Prop :=
 (asymm : ∀ a b, r a b → ¬ r b a)
 
+/-- `is_antisymm X r` means the binary relation `r` on `X` is antisymmetric. -/
 @[algebra] class is_antisymm (α : Type u) (r : α → α → Prop) : Prop :=
 (antisymm : ∀ a b, r a b → r b a → a = b)
 
+/-- `is_trans X r` means the binary relation `r` on `X` is transitive. -/
 @[algebra] class is_trans (α : Type u) (r : α → α → Prop) : Prop :=
 (trans  : ∀ a b c, r a b → r b c → r a c)
 
+/-- `is_total X r` means that the binary relation `r` on `X` is total, that is, that for any
+`x y : X` we have `r x y` or `r y x`.-/
 @[algebra] class is_total (α : Type u) (r : α → α → Prop) : Prop :=
 (total : ∀ a b, r a b ∨ r b a)
 
+/-- `is_preorder X r` means that the binary relation `r` on `X` is a pre-order, that is, reflexive
+and transitive. -/
 @[algebra] class is_preorder (α : Type u) (r : α → α → Prop) extends is_refl α r, is_trans α r : Prop.
 
+/-- `is_total_preorder X r` means that the binary relation `r` on `X` is total and a preorder. -/
 @[algebra] class is_total_preorder (α : Type u) (r : α → α → Prop) extends is_trans α r, is_total α r : Prop.
 
+/-- Every total pre-order is a pre-order. -/
 instance is_total_preorder_is_preorder (α : Type u) (r : α → α → Prop) [s : is_total_preorder α r] : is_preorder α r :=
 {trans := s.trans,
  refl  := λ a, or.elim (@is_total.total _ r _ a a) id id}
diff --git a/library/init/algebra/order.lean b/library/init/algebra/order.lean
index 3d96241fba..7637130967 100644
--- a/library/init/algebra/order.lean
+++ b/library/init/algebra/order.lean
@@ -30,9 +30,11 @@ class partial_order (α : Type u) extends preorder α :=
 class linear_order (α : Type u) extends partial_order α :=
 (le_total : ∀ a b : α, a ≤ b ∨ b ≤ a)
 
+/-- The relation `≤` on a preorder is reflexive. -/
 @[refl] lemma le_refl [preorder α] : ∀ a : α, a ≤ a :=
 preorder.le_refl
 
+/-- The relation `≤` on a preorder is transitive. -/
 @[trans] lemma le_trans [preorder α] : ∀ {a b c : α}, a ≤ b → b ≤ c → a ≤ c :=
 preorder.le_trans
 
diff --git a/library/init/core.lean b/library/init/core.lean
index d976742f6b..6722205484 100644
--- a/library/init/core.lean
+++ b/library/init/core.lean
@@ -10,7 +10,7 @@ prelude
 notation `Prop` := Sort 0
 notation f ` $ `:1 a:0 := f a
 
-/- Reserving notation. We do this sot that the precedence of all of the operators
+/- Reserving notation. We do this so that the precedence of all of the operators
 can be seen in one place and to prevent core notation being accidentally overloaded later.  -/
 
 /- Notation for logical operations and relations -/
@@ -142,6 +142,8 @@ inductive false : Prop
 
 inductive empty : Type
 
+/-- `not P`, with notation `¬ P`, is the `Prop` which is true if and only if `P` is false. It is
+internally represented as `P → false`. -/
 def not (a : Prop) := a → false
 prefix `¬` := not
 
@@ -183,6 +185,8 @@ structure prod (α : Type u) (β : Type v) :=
 structure pprod (α : Sort u) (β : Sort v) :=
 (fst : α) (snd : β)
 
+/-- `and P Q`, with notation `P ∧ Q`, is the `Prop` which is true precisely when `P` and `Q` are
+both true. -/
 structure and (a b : Prop) : Prop :=
 intro :: (left : a) (right : b)
 
@@ -246,6 +250,8 @@ inductive psum (α : Sort u) (β : Sort v)
 | inl (val : α) : psum
 | inr (val : β) : psum
 
+/-- `or P Q`, with notation `P ∨ Q`, is the proposition which is true if and only if `P` or `Q` is
+true. -/
 inductive or (a b : Prop) : Prop
 | inl (h : a) : or
 | inr (h : b) : or
diff --git a/library/init/logic.lean b/library/init/logic.lean
index 556e9fd340..32d6957684 100644
--- a/library/init/logic.lean
+++ b/library/init/logic.lean
@@ -20,6 +20,7 @@ def flip {α : Sort u} {β : Sort v} {φ : Sort w} (f : α → β → φ) : β 
 
 def implies (a b : Prop) := a → b
 
+/-- Implication `→` is transitive. If `P → Q` and `Q → R` then `P → R`. -/
 @[trans] lemma implies.trans {p q r : Prop} (h₁ : implies p q) (h₂ : implies q r) : implies p r :=
 assume hp, h₂ (h₁ hp)
 
@@ -32,7 +33,7 @@ false.rec b (h₂ h₁)
 lemma not.intro {a : Prop} (h : a → false) : ¬ a :=
 h
 
-/-- Modus tollens.-/
+/-- Modus tollens. If an implication is true, then so is its contrapositive. -/
 lemma mt {a b : Prop} (h₁ : a → b) (h₂ : ¬b) : ¬a := assume ha : a, h₂ (h₁ ha)
 
 /- not -/
@@ -221,7 +222,8 @@ def or.symm := @or.swap
 def xor (a b : Prop) := (a ∧ ¬ b) ∨ (b ∧ ¬ a)
 
 /- iff -/
-
+/-- `iff P Q`, with notation `P ↔ Q`, is the proposition asserting that `P` and `Q` are equivalent,
+that is, have the same truth value. -/
 structure iff (a b : Prop) : Prop :=
 intro :: (mp : a → b) (mpr : b → a)