chore(FirstOrder/Arith): rename

Logic.lean

@@ -55,11 +55,15 @@ import Logic.FirstOrder.Completeness.Completeness
 
 import Logic.FirstOrder.Order.Le
 
+import Logic.FirstOrder.Arith.Basic
 import Logic.FirstOrder.Arith.Hierarchy
 import Logic.FirstOrder.Arith.StrictHierarchy
 import Logic.FirstOrder.Arith.Theory
 import Logic.FirstOrder.Arith.Model
+import Logic.FirstOrder.Arith.PeanoMinus
+import Logic.FirstOrder.Arith.Representation
 import Logic.FirstOrder.Arith.Nonstandard
+
 import Logic.FirstOrder.Arith.EA.Basic
 
 import Logic.FirstOrder.Incompleteness.FirstIncompleteness

Logic/FirstOrder/Arith/EA/Basic.lean

@@ -26,17 +26,17 @@ namespace Theory
 
 variable (L)
 
-notation "𝐈open(exp)" => IOpen ℒₒᵣ(exp)
+notation "𝐈open(exp)" => iOpen ℒₒᵣ(exp)
 
-notation "𝐈𝚫₀(exp)" => ISigma ℒₒᵣ(exp) 0
+notation "𝐈𝚫₀(exp)" => iSigma ℒₒᵣ(exp) 0
 
 inductive Exponential : Theory L
   | zero : Exponential “exp 0 = 1”
   | succ : Exponential “∀ exp (#0 + 1) = 2 * exp #0”
 
 notation "𝐄𝐗𝐏" => Exponential ℒₒᵣ(exp)
 
-abbrev ElementaryArithmetic : Theory L := Semiformula.lMap Language.oringEmb '' 𝐏𝐀⁻ + Exponential L + ISigma L 0
+abbrev ElementaryArithmetic : Theory L := Semiformula.lMap Language.oringEmb '' 𝐏𝐀⁻ + Exponential L + iSigma L 0
 
 notation "𝐄𝐀" => ElementaryArithmetic ℒₒᵣ(exp)
 
@@ -112,8 +112,8 @@ lemma modelsSuccInd_exp (p : Semiformula ℒₒᵣ(exp) ℕ 1) : ℕ ⊧ₘ (∀
   · exact hsucc x ih
 
 lemma modelsTheoryElementaryArithmetic : ℕ ⊧ₘ* 𝐄𝐀 := by
-  simp [Theory.ElementaryArithmetic, Theory.add_def, Theory.ISigma, Theory.IndScheme]
-  exact ⟨⟨by intro σ hσ; simpa [models_iff] using modelsTheoryPAminus hσ, modelsTheoryExponential⟩,
+  simp [Theory.ElementaryArithmetic, Theory.add_def, Theory.iSigma, Theory.indScheme]
+  exact ⟨⟨by intro σ hσ; simpa [models_iff] using modelsTheoryPeanoMinus hσ, modelsTheoryExponential⟩,
     by rintro σ p _ rfl; exact modelsSuccInd_exp p⟩
 
 end Standard
@@ -139,12 +139,12 @@ instance : 𝐄𝐗𝐏.Mod M := Theory.Mod.of_add_left_right M (Semiformula.lMa
 
 instance : 𝐈𝚫₀(exp).Mod M := Theory.Mod.of_add_right M (Semiformula.lMap Language.oringEmb '' 𝐏𝐀⁻ + 𝐄𝐗𝐏) 𝐈𝚫₀(exp)
 
-lemma ISigma₀_subset_IDelta₀Exp : (𝐈𝚺₀ : Theory ℒₒᵣ(exp)) ⊆ 𝐈𝚫₀(exp) :=
-  Theory.coe_IHierarchy_subset_IHierarchy
+lemma iSigma₀_subset_IDelta₀Exp : (𝐈𝚺₀ : Theory ℒₒᵣ(exp)) ⊆ 𝐈𝚫₀(exp) :=
+  Theory.coe_iHierarchy_subset_iHierarchy
 
 instance : 𝐈𝚺₀.Mod M := ⟨by
   intro σ hσ
-  have : (𝐈𝚺₀ : Theory ℒₒᵣ(exp)) ⊆ 𝐈𝚫₀(exp) := Theory.coe_IHierarchy_subset_IHierarchy
+  have : (𝐈𝚺₀ : Theory ℒₒᵣ(exp)) ⊆ 𝐈𝚫₀(exp) := Theory.coe_iHierarchy_subset_iHierarchy
   have : M ⊧ₘ (σ : Sentence ℒₒᵣ(exp)) :=
     Theory.Mod.models M (show (σ : Sentence ℒₒᵣ(exp)) ∈ 𝐈𝚫₀(exp) from this (Set.mem_image_of_mem _ hσ))
   simpa [models_iff] using this⟩

Logic/FirstOrder/Arith/Model.lean

@@ -139,7 +139,7 @@ namespace Standard
 
 variable {μ : Type v} (e : Fin n → ℕ) (ε : μ → ℕ)
 
-lemma modelsTheoryPAminus : ℕ ⊧ₘ* 𝐏𝐀⁻ := by
+lemma modelsTheoryPeanoMinus : ℕ ⊧ₘ* 𝐏𝐀⁻ := by
   intro σ h
   rcases h <;> simp [models_def, ←le_iff_eq_or_lt]
   case addAssoc => intro l m n; exact add_assoc l m n
@@ -161,11 +161,11 @@ lemma modelsSuccInd (p : Semiformula ℒₒᵣ ℕ 1) : ℕ ⊧ₘ (∀ᶠ* succ
   · exact hsucc x ih
 
 lemma modelsPeano : ℕ ⊧ₘ* 𝐏𝐀 ∪ 𝐏𝐀⁻ ∪ 𝐄𝐪 := by
-  simp [Theory.Peano, Theory.IndScheme, modelsTheoryPAminus]; rintro _ p _ rfl; simp [modelsSuccInd]
+  simp [Theory.peano, Theory.indScheme, modelsTheoryPeanoMinus]; rintro _ p _ rfl; simp [modelsSuccInd]
 
 end Standard
 
-theorem Peano.Consistent : System.Consistent (𝐏𝐀 ∪ 𝐏𝐀⁻ ∪ 𝐄𝐪) :=
+theorem peano_consistent : System.Consistent (𝐏𝐀 ∪ 𝐏𝐀⁻ ∪ 𝐄𝐪) :=
   Sound.consistent_of_model Standard.modelsPeano
 
 section

Logic/FirstOrder/Arith/Nonstandard.lean

@@ -1,5 +1,5 @@
 import Logic.FirstOrder.Arith.Model
-import Logic.FirstOrder.Arith.PAminus
+import Logic.FirstOrder.Arith.PeanoMinus
 
 namespace LO
 
@@ -83,7 +83,7 @@ lemma trueArith : ℕ⋆ ⊧ₘ* 𝐓𝐀 := by
 instance : Theory.Mod ℕ⋆ 𝐓𝐀 := ⟨trueArith⟩
 
 instance : Theory.Mod ℕ⋆ 𝐏𝐀⁻ :=
-  Theory.Mod.of_ss (T₁ := 𝐓𝐀) _ (Structure.subset_of_models.mpr $ Arith.Standard.modelsTheoryPAminus)
+  Theory.Mod.of_ss (T₁ := 𝐓𝐀) _ (Structure.subset_of_models.mpr $ Arith.Standard.modelsTheoryPeanoMinus)
 
 lemma star_unbounded (n : ℕ) : n < ⋆ := by
   have : ℕ⋆ ⊧ₘ (“!!(Semiterm.Operator.numeral ℒₒᵣ⋆ n) < ⋆” : Sentence ℒₒᵣ⋆) :=

Logic/FirstOrder/Arith/PAminus.lean → Logic/FirstOrder/Arith/PeanoMinus.lean

@@ -2,7 +2,6 @@ import Logic.FirstOrder.Arith.Model
 import Logic.Vorspiel.ExistsUnique
 import Mathlib.Algebra.Order.Monoid.Canonical.Defs
 import Mathlib.Algebra.Associated
---import Logic.FirstOrder.Principia.Meta
 
 namespace LO
 
@@ -23,55 +22,55 @@ instance : LE M := ⟨fun x y => x = y ∨ x < y⟩
 lemma le_def {x y : M} : x ≤ y ↔ x = y ∨ x < y := iff_of_eq rfl
 
 protected lemma add_zero : ∀ x : M, x + 0 = x := by
-  simpa[models_iff] using Theory.Mod.models M Theory.PAminus.addZero
+  simpa[models_iff] using Theory.Mod.models M Theory.peanoMinus.addZero
 
 protected lemma add_assoc : ∀ x y z : M, (x + y) + z = x + (y + z) := by
-  simpa[models_iff] using Theory.Mod.models M Theory.PAminus.addAssoc
+  simpa[models_iff] using Theory.Mod.models M Theory.peanoMinus.addAssoc
 
 protected lemma add_comm : ∀ x y : M, x + y = y + x := by
-  simpa[models_iff] using Theory.Mod.models M Theory.PAminus.addComm
+  simpa[models_iff] using Theory.Mod.models M Theory.peanoMinus.addComm
 
 lemma add_eq_of_lt : ∀ x y : M, x < y → ∃ z, x + z = y := by
-  simpa[models_iff] using Theory.Mod.models M Theory.PAminus.addEqOfLt
+  simpa[models_iff] using Theory.Mod.models M Theory.peanoMinus.addEqOfLt
 
 @[simp] lemma zero_le : ∀ x : M, 0 ≤ x := by
-  simpa[models_iff, Structure.le_iff_of_eq_of_lt] using Theory.Mod.models M Theory.PAminus.zeroLe
+  simpa[models_iff, Structure.le_iff_of_eq_of_lt] using Theory.Mod.models M Theory.peanoMinus.zeroLe
 
 lemma zero_lt_one : (0 : M) < 1 := by
-  simpa[models_iff] using Theory.Mod.models M Theory.PAminus.zeroLtOne
+  simpa[models_iff] using Theory.Mod.models M Theory.peanoMinus.zeroLtOne
 
 lemma one_le_of_zero_lt : ∀ x : M, 0 < x → 1 ≤ x := by
-  simpa[models_iff, Structure.le_iff_of_eq_of_lt] using Theory.Mod.models M Theory.PAminus.oneLeOfZeroLt
+  simpa[models_iff, Structure.le_iff_of_eq_of_lt] using Theory.Mod.models M Theory.peanoMinus.oneLeOfZeroLt
 
 lemma add_lt_add : ∀ x y z : M, x < y → x + z < y + z := by
-  simpa[models_iff] using Theory.Mod.models M Theory.PAminus.addLtAdd
+  simpa[models_iff] using Theory.Mod.models M Theory.peanoMinus.addLtAdd
 
 protected lemma mul_zero : ∀ x : M, x * 0 = 0 := by
-  simpa[models_iff] using Theory.Mod.models M Theory.PAminus.mulZero
+  simpa[models_iff] using Theory.Mod.models M Theory.peanoMinus.mulZero
 
 protected lemma mul_one : ∀ x : M, x * 1 = x := by
-  simpa[models_iff] using Theory.Mod.models M Theory.PAminus.mulOne
+  simpa[models_iff] using Theory.Mod.models M Theory.peanoMinus.mulOne
 
 protected lemma mul_assoc : ∀ x y z : M, (x * y) * z = x * (y * z) := by
-  simpa[models_iff] using Theory.Mod.models M Theory.PAminus.mulAssoc
+  simpa[models_iff] using Theory.Mod.models M Theory.peanoMinus.mulAssoc
 
 protected lemma mul_comm : ∀ x y : M, x * y = y * x := by
-  simpa[models_iff] using Theory.Mod.models M Theory.PAminus.mulComm
+  simpa[models_iff] using Theory.Mod.models M Theory.peanoMinus.mulComm
 
 lemma mul_lt_mul : ∀ x y z : M, x < y → 0 < z → x * z < y * z := by
-  simpa[models_iff] using Theory.Mod.models M Theory.PAminus.mulLtMul
+  simpa[models_iff] using Theory.Mod.models M Theory.peanoMinus.mulLtMul
 
 lemma distr : ∀ x y z : M, x * (y + z) = x * y + x * z := by
-  simpa[models_iff] using Theory.Mod.models M Theory.PAminus.distr
+  simpa[models_iff] using Theory.Mod.models M Theory.peanoMinus.distr
 
 lemma lt_irrefl : ∀ x : M, ¬x < x := by
-  simpa[models_iff] using Theory.Mod.models M Theory.PAminus.ltIrrefl
+  simpa[models_iff] using Theory.Mod.models M Theory.peanoMinus.ltIrrefl
 
 lemma lt_trans : ∀ x y z : M, x < y → y < z → x < z := by
-  simpa[models_iff] using Theory.Mod.models M Theory.PAminus.ltTrans
+  simpa[models_iff] using Theory.Mod.models M Theory.peanoMinus.ltTrans
 
 lemma lt_tri : ∀ x y : M, x < y ∨ x = y ∨ y < x := by
-  simpa[models_iff] using Theory.Mod.models M Theory.PAminus.ltTri
+  simpa[models_iff] using Theory.Mod.models M Theory.peanoMinus.ltTri
 
 instance : AddCommMonoid M where
   add_assoc := Model.add_assoc

Logic/FirstOrder/Arith/Representation.lean

@@ -1,4 +1,4 @@
-import Logic.FirstOrder.Arith.PAminus
+import Logic.FirstOrder.Arith.PeanoMinus
 import Logic.Vorspiel.Arith
 import Logic.FirstOrder.Computability.Calculus
 

Logic/FirstOrder/Arith/StrictHierarchy.lean

@@ -1,4 +1,4 @@
-import Logic.FirstOrder.Arith.PAminus
+import Logic.FirstOrder.Arith.PeanoMinus
 
 namespace LO
 

Logic/FirstOrder/Arith/Theory.lean

@@ -20,62 +20,62 @@ variable (L)
 
 namespace Theory
 
-inductive PAminus : Theory ℒₒᵣ
-  | addZero       : PAminus “∀ #0 + 0 = #0”
-  | addAssoc      : PAminus “∀ ∀ ∀ (#2 + #1) + #0 = #2 + (#1 + #0)”
-  | addComm       : PAminus “∀ ∀ #1 + #0 = #0 + #1”
-  | addEqOfLt     : PAminus “∀ ∀ (#1 < #0 → ∃ #2 + #0 = #1)”
-  | zeroLe        : PAminus “∀ (0 ≤ #0)”
-  | zeroLtOne     : PAminus “0 < 1”
-  | oneLeOfZeroLt : PAminus “∀ (0 < #0 → 1 ≤ #0)”
-  | addLtAdd      : PAminus “∀ ∀ ∀ (#2 < #1 → #2 + #0 < #1 + #0)”
-  | mulZero       : PAminus “∀ #0 * 0 = 0”
-  | mulOne        : PAminus “∀ #0 * 1 = #0”
-  | mulAssoc      : PAminus “∀ ∀ ∀ (#2 * #1) * #0 = #2 * (#1 * #0)”
-  | mulComm       : PAminus “∀ ∀ #1 * #0 = #0 * #1”
-  | mulLtMul      : PAminus “∀ ∀ ∀ (#2 < #1 ∧ 0 < #0 → #2 * #0 < #1 * #0)”
-  | distr         : PAminus “∀ ∀ ∀ #2 * (#1 + #0) = #2 * #1 + #2 * #0”
-  | ltIrrefl      : PAminus “∀ ¬#0 < #0”
-  | ltTrans       : PAminus “∀ ∀ ∀ (#2 < #1 ∧ #1 < #0 → #2 < #0)”
-  | ltTri         : PAminus “∀ ∀ (#1 < #0 ∨ #1 = #0 ∨ #0 < #1)”
-
-notation "𝐏𝐀⁻" => PAminus
+inductive peanoMinus : Theory ℒₒᵣ
+  | addZero       : peanoMinus “∀ #0 + 0 = #0”
+  | addAssoc      : peanoMinus “∀ ∀ ∀ (#2 + #1) + #0 = #2 + (#1 + #0)”
+  | addComm       : peanoMinus “∀ ∀ #1 + #0 = #0 + #1”
+  | addEqOfLt     : peanoMinus “∀ ∀ (#1 < #0 → ∃ #2 + #0 = #1)”
+  | zeroLe        : peanoMinus “∀ (0 ≤ #0)”
+  | zeroLtOne     : peanoMinus “0 < 1”
+  | oneLeOfZeroLt : peanoMinus “∀ (0 < #0 → 1 ≤ #0)”
+  | addLtAdd      : peanoMinus “∀ ∀ ∀ (#2 < #1 → #2 + #0 < #1 + #0)”
+  | mulZero       : peanoMinus “∀ #0 * 0 = 0”
+  | mulOne        : peanoMinus “∀ #0 * 1 = #0”
+  | mulAssoc      : peanoMinus “∀ ∀ ∀ (#2 * #1) * #0 = #2 * (#1 * #0)”
+  | mulComm       : peanoMinus “∀ ∀ #1 * #0 = #0 * #1”
+  | mulLtMul      : peanoMinus “∀ ∀ ∀ (#2 < #1 ∧ 0 < #0 → #2 * #0 < #1 * #0)”
+  | distr         : peanoMinus “∀ ∀ ∀ #2 * (#1 + #0) = #2 * #1 + #2 * #0”
+  | ltIrrefl      : peanoMinus “∀ ¬#0 < #0”
+  | ltTrans       : peanoMinus “∀ ∀ ∀ (#2 < #1 ∧ #1 < #0 → #2 < #0)”
+  | ltTri         : peanoMinus “∀ ∀ (#1 < #0 ∨ #1 = #0 ∨ #0 < #1)”
+
+notation "𝐏𝐀⁻" => peanoMinus
 
 variable {L}
 
-def IndScheme (Γ : Semiformula L ℕ 1 → Prop) : Theory L :=
+def indScheme (Γ : Semiformula L ℕ 1 → Prop) : Theory L :=
   { q | ∃ p : Semiformula L ℕ 1, Γ p ∧ q = ∀ᶠ* succInd p }
 
 variable (L)
 
-abbrev IOpen : Theory L := IndScheme Semiformula.Open
+abbrev iOpen : Theory L := indScheme Semiformula.Open
 
-notation "𝐈open" => IOpen ℒₒᵣ
+notation "𝐈open" => iOpen ℒₒᵣ
 
-abbrev IHierarchy (Γ : Polarity) (k : ℕ) : Theory L := IndScheme (Arith.Hierarchy Γ k)
+abbrev iHierarchy (Γ : Polarity) (k : ℕ) : Theory L := indScheme (Arith.Hierarchy Γ k)
 
-notation "𝐈𝐍𝐃" => IHierarchy ℒₒᵣ
+notation "𝐈𝐍𝐃" => iHierarchy ℒₒᵣ
 
-abbrev ISigma (k : ℕ) : Theory L := IndScheme (Arith.Hierarchy Σ k)
+abbrev iSigma (k : ℕ) : Theory L := indScheme (Arith.Hierarchy Σ k)
 
-prefix:max "𝐈𝚺" => ISigma ℒₒᵣ
+prefix:max "𝐈𝚺" => iSigma ℒₒᵣ
 
-notation "𝐈𝚺₀" => ISigma ℒₒᵣ 0
+notation "𝐈𝚺₀" => iSigma ℒₒᵣ 0
 
-abbrev IPi (k : ℕ) : Theory L := IndScheme (Arith.Hierarchy Π k)
+abbrev iPi (k : ℕ) : Theory L := indScheme (Arith.Hierarchy Π k)
 
-prefix:max "𝐈𝚷" => IPi ℒₒᵣ
+prefix:max "𝐈𝚷" => iPi ℒₒᵣ
 
-notation "𝐈𝚷₀" => IPi ℒₒᵣ 0
+notation "𝐈𝚷₀" => iPi ℒₒᵣ 0
 
-abbrev Peano : Theory L := IndScheme Set.univ
+abbrev peano : Theory L := indScheme Set.univ
 
-notation "𝐏𝐀" => Peano ℒₒᵣ
+notation "𝐏𝐀" => peano ℒₒᵣ
 
 variable {L}
 
-lemma coe_IHierarchy_subset_IHierarchy : (𝐈𝐍𝐃 Γ ν : Theory L) ⊆ IHierarchy L Γ ν := by
-  simp [Theory.IHierarchy, Theory.IndScheme]
+lemma coe_iHierarchy_subset_iHierarchy : (𝐈𝐍𝐃 Γ ν : Theory L) ⊆ iHierarchy L Γ ν := by
+  simp [Theory.iHierarchy, Theory.indScheme]
   rintro _ p Hp rfl
   exact ⟨Semiformula.lMap (Language.oringEmb : ℒₒᵣ →ᵥ L) p, Hierarchy.oringEmb Hp,
     by simp [Formula.lMap_fvUnivClosure, succInd, Semiformula.lMap_substs]⟩

README.md

@@ -129,10 +129,10 @@ $\mathbf{PA^-}$ is not to be included in $\mathbf{I\Sigma}_n$ or $\mathbf{PA}$ f
 | $(\rm Cut)\vdash_\mathrm{T} \Gamma$ | Derivation in Tait-Calculus + Cut              | [LO.FirstOrder.Derivation](https://iehality.github.io/lean4-logic/Logic/FirstOrder/Basic/Calculus.html#LO.FirstOrder.Derivation) | `⊢¹ Γ`   |
 | $M \models \sigma$                  | Tarski's truth definition condition            | [LO.FirstOrder.Models](https://iehality.github.io/lean4-logic/Logic/FirstOrder/Basic/Semantics/Semantics.html#LO.FirstOrder.Models) | `M ⊧ₘ σ` |
 | $\mathbf{Eq}$                       | Axiom of equality                              | [LO.FirstOrder.Theory.Eq](https://iehality.github.io/lean4-logic/Logic/FirstOrder/Basic/Eq.html#LO.FirstOrder.Theory.Eq) | `𝐄𝐪` |
-| $\mathbf{PA^-}$                     | Finitely axiomatized fragment of $\mathbf{PA}$ | [LO.FirstOrder.Arith.Theory.PAminus](https://iehality.github.io/lean4-logic/Logic/FirstOrder/Arith/Theory.html#LO.FirstOrder.Arith.Theory.PAminus) | `𝐏𝐀⁻` |
-| $\mathbf{I}_\mathrm{open}$          | Induction of open formula                      | [LO.FirstOrder.Arith.Theory.IOpen](https://iehality.github.io/lean4-logic/Logic/FirstOrder/Arith/Theory.html#LO.FirstOrder.Arith.Theory.IOpen) | `𝐈open` |
-| $\mathbf{I\Sigma}_n$                | Induction of $\Sigma_n$ formula                | [LO.FirstOrder.Arith.Theory.ISigma](https://iehality.github.io/lean4-logic/Logic/FirstOrder/Arith/Theory.html#LO.FirstOrder.Arith.Theory.ISigma) | `𝐈𝚺` |
-| $\mathbf{PA}$                       | Peano arithmetic                               | [LO.FirstOrder.Arith.Theory.Peano](https://iehality.github.io/lean4-logic/Logic/FirstOrder/Arith/Theory.html#LO.FirstOrder.Arith.Theory.Peano) | `𝐏𝐀` |
+| $\mathbf{PA^-}$                     | Finitely axiomatized fragment of $\mathbf{PA}$ | [LO.FirstOrder.Arith.Theory.peanoMinus](https://iehality.github.io/lean4-logic/Logic/FirstOrder/Arith/Theory.html#LO.FirstOrder.Arith.Theory.peanoMinus) | `𝐏𝐀⁻` |
+| $\mathbf{I}_\mathrm{open}$          | Induction of open formula                      | [LO.FirstOrder.Arith.Theory.iOpen](https://iehality.github.io/lean4-logic/Logic/FirstOrder/Arith/Theory.html#LO.FirstOrder.Arith.Theory.iOpen) | `𝐈open` |
+| $\mathbf{I\Sigma}_n$                | Induction of $\Sigma_n$ formula                | [LO.FirstOrder.Arith.Theory.iSigma](https://iehality.github.io/lean4-logic/Logic/FirstOrder/Arith/Theory.html#LO.FirstOrder.Arith.Theory.iSigma) | `𝐈𝚺` |
+| $\mathbf{PA}$                       | peano arithmetic                               | [LO.FirstOrder.Arith.Theory.peano](https://iehality.github.io/lean4-logic/Logic/FirstOrder/Arith/Theory.html#LO.FirstOrder.Arith.Theory.peano) | `𝐏𝐀` |
 
 ### Theorem
 
@@ -264,7 +264,7 @@ In this formalization, _(Modal) Logic_ means set of axioms.
 - J. Han, F. van Doorn, A formalization of forcing and the unprovability of the continuum hypothesis
 - W. Pohlers, Proof Theory: The First Step into Impredicativity
 - P. Hájek, P. Pudlák, Metamathematics of First-Order Arithmetic
-- R. Kaye, Models of Peano arithmetic
+- R. Kaye, Models of peano arithmetic
 - 田中 一之, ゲーデルと20世紀の論理学
 - 菊池 誠 (編者), 『数学における証明と真理 ─ 様相論理と数学基礎論』
 - P. Blackburn, M. de Rijke, Y. Venema, "Modal Logic"