Skip to content

Commit

Permalink
feat(FirstOrder): Finite theory (#204)
Browse files Browse the repository at this point in the history 
* WeakerThan

* `System` ↦ `Entailment`

* remove

* feat(FirstOrder): add some `WeakerThan` facts

* consistency

* feat(FirstOrder): finiteness
  • Loading branch information
@iehality
iehality authored Feb 14, 2025
1 parent dd1982c commit a668f38
Show file tree
Hide file tree
Showing 6 changed files with 252 additions and 62 deletions.
10 changes: 5 additions & 5 deletions Foundation/FirstOrder/Arith/Model.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -137,12 +137,12 @@ instance [M ⊧ₘ* 𝐈open] : M ⊧ₘ* 𝐏𝐀⁻ := ModelsTheory.of_add_lef
instance [M ⊧ₘ* 𝐈open] : M ⊧ₘ* Theory.indScheme ℒₒᵣ Semiformula.Open :=
ModelsTheory.of_add_right M 𝐏𝐀⁻ (Theory.indScheme _ Semiformula.Open)

def models_PAMinus_of_models_indH (Γ n) [M ⊧ₘ* 𝐈𝐍𝐃 Γ n] : M ⊧ₘ* 𝐏𝐀⁻ := ModelsTheory.of_add_left M 𝐏𝐀⁻ (Theory.indScheme _ (Arith.Hierarchy Γ n))
def models_PeanoMinus_of_models_indH (Γ n) [M ⊧ₘ* 𝐈𝐍𝐃 Γ n] : M ⊧ₘ* 𝐏𝐀⁻ := ModelsTheory.of_add_left M 𝐏𝐀⁻ (Theory.indScheme _ (Arith.Hierarchy Γ n))

def models_indScheme_of_models_indH (Γ n) [M ⊧ₘ* 𝐈𝐍𝐃 Γ n] : M ⊧ₘ* Theory.indScheme ℒₒᵣ (Arith.Hierarchy Γ n) :=
ModelsTheory.of_add_right M 𝐏𝐀⁻ (Theory.indScheme _ (Arith.Hierarchy Γ n))

instance models_PAMinus_of_models_peano [M ⊧ₘ* 𝐏𝐀] : M ⊧ₘ* 𝐏𝐀⁻ := ModelsTheory.of_add_left M 𝐏𝐀⁻ (Theory.indScheme _ Set.univ)
instance models_PeanoMinus_of_models_peano [M ⊧ₘ* 𝐏𝐀] : M ⊧ₘ* 𝐏𝐀⁻ := ModelsTheory.of_add_left M 𝐏𝐀⁻ (Theory.indScheme _ Set.univ)

end

Expand All @@ -161,7 +161,7 @@ instance models_CobhamR0 : ℕ ⊧ₘ* 𝐑₀ := ⟨by
case Ω₃ h =>
simpa [models_def, ←le_iff_eq_or_lt] using h⟩

instance models_PAMinus : ℕ ⊧ₘ* 𝐏𝐀⁻ := ⟨by
instance models_PeanoMinus : ℕ ⊧ₘ* 𝐏𝐀⁻ := ⟨by
intro σ h
rcases h <;> simp [models_def, ←le_iff_eq_or_lt]
case addAssoc => intro f; exact add_assoc _ _ _
Expand All @@ -186,14 +186,14 @@ lemma models_succInd (φ : Semiformula ℒₒᵣ ℕ 1) : ℕ ⊧ₘ succInd φ
· exact hsucc x ih

instance models_iSigma (Γ k) : ℕ ⊧ₘ* 𝐈𝐍𝐃Γ k := by
simp [Theory.indScheme, models_PAMinus]; rintro _ φ _ rfl; simp [models_succInd]
simp [Theory.indScheme, models_PeanoMinus]; rintro _ φ _ rfl; simp [models_succInd]

instance models_iSigmaZero : ℕ ⊧ₘ* 𝐈𝚺₀ := inferInstance

instance models_iSigmaOne : ℕ ⊧ₘ* 𝐈𝚺₁ := inferInstance

instance models_peano : ℕ ⊧ₘ* 𝐏𝐀 := by
simp [Theory.peano, Theory.indScheme, models_PAMinus]; rintro _ φ _ rfl; simp [models_succInd]
simp [Theory.peano, Theory.indScheme, models_PeanoMinus]; rintro _ φ _ rfl; simp [models_succInd]

end Standard

Expand Down
2 changes: 1 addition & 1 deletion Foundation/FirstOrder/Arith/Nonstandard.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -80,7 +80,7 @@ instance trueArith : ℕ⋆ ⊧ₘ* 𝐓𝐀 := ⟨by
exact e ▸ this⟩

instance : ℕ⋆ ⊧ₘ* 𝐏𝐀⁻ :=
ModelsTheory.of_ss (U := 𝐓𝐀) inferInstance (Structure.subset_of_models.mpr $ Arith.Standard.models_PAMinus)
ModelsTheory.of_ss (U := 𝐓𝐀) inferInstance (Structure.subset_of_models.mpr $ Arith.Standard.models_PeanoMinus)

open LO.Arith

Expand Down
40 changes: 20 additions & 20 deletions Foundation/FirstOrder/Arith/PeanoMinus.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,55 +21,55 @@ lemma le_def {x y : M} : x ≤ y ↔ x = y ∨ x < y := iff_of_eq rfl
variable [M ⊧ₘ* 𝐏𝐀⁻]

protected lemma add_zero (x : M) : x + 0 = x := by
simpa[models_iff] using ModelsTheory.models M Theory.PAMinus.addZero (fun _ ↦ x)
simpa[models_iff] using ModelsTheory.models M Theory.PeanoMinus.addZero (fun _ ↦ x)

protected lemma add_assoc (x y z : M) : (x + y) + z = x + (y + z) := by
simpa[models_iff] using ModelsTheory.models M Theory.PAMinus.addAssoc (x :>ₙ y :>ₙ fun _ ↦ z)
simpa[models_iff] using ModelsTheory.models M Theory.PeanoMinus.addAssoc (x :>ₙ y :>ₙ fun _ ↦ z)

protected lemma add_comm (x y : M) : x + y = y + x := by
simpa[models_iff] using ModelsTheory.models M Theory.PAMinus.addComm (x :>ₙ fun _ ↦ y)
simpa[models_iff] using ModelsTheory.models M Theory.PeanoMinus.addComm (x :>ₙ fun _ ↦ y)

lemma add_eq_of_lt (x y : M) : x < y → ∃ z, x + z = y := by
simpa[models_iff] using ModelsTheory.models M Theory.PAMinus.addEqOfLt (x :>ₙ fun _ ↦ y)
simpa[models_iff] using ModelsTheory.models M Theory.PeanoMinus.addEqOfLt (x :>ₙ fun _ ↦ y)

@[simp] lemma zero_le (x : M) : 0 ≤ x := by
simpa[models_iff, Structure.le_iff_of_eq_of_lt] using ModelsTheory.models M Theory.PAMinus.zeroLe (fun _ ↦ x)
simpa[models_iff, Structure.le_iff_of_eq_of_lt] using ModelsTheory.models M Theory.PeanoMinus.zeroLe (fun _ ↦ x)

lemma zero_lt_one : (0 : M) < 1 := by
simpa[models_iff] using ModelsTheory.models M Theory.PAMinus.zeroLtOne
simpa[models_iff] using ModelsTheory.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 ModelsTheory.models M Theory.PAMinus.oneLeOfZeroLt (fun _ ↦ x)
simpa[models_iff, Structure.le_iff_of_eq_of_lt] using ModelsTheory.models M Theory.PeanoMinus.oneLeOfZeroLt (fun _ ↦ x)

lemma add_lt_add (x y z : M) : x < y → x + z < y + z := by
simpa[models_iff] using ModelsTheory.models M Theory.PAMinus.addLtAdd (x :>ₙ y :>ₙ fun _ ↦ z)
simpa[models_iff] using ModelsTheory.models M Theory.PeanoMinus.addLtAdd (x :>ₙ y :>ₙ fun _ ↦ z)

protected lemma mul_zero (x : M) : x * 0 = 0 := by
simpa[models_iff] using ModelsTheory.models M Theory.PAMinus.mulZero (fun _ ↦ x)
simpa[models_iff] using ModelsTheory.models M Theory.PeanoMinus.mulZero (fun _ ↦ x)

protected lemma mul_one (x : M) : x * 1 = x := by
simpa[models_iff] using ModelsTheory.models M Theory.PAMinus.mulOne (fun _ ↦ x)
simpa[models_iff] using ModelsTheory.models M Theory.PeanoMinus.mulOne (fun _ ↦ x)

protected lemma mul_assoc (x y z : M) : (x * y) * z = x * (y * z) := by
simpa[models_iff] using ModelsTheory.models M Theory.PAMinus.mulAssoc (x :>ₙ y :>ₙ fun _ ↦ z)
simpa[models_iff] using ModelsTheory.models M Theory.PeanoMinus.mulAssoc (x :>ₙ y :>ₙ fun _ ↦ z)

protected lemma mul_comm (x y : M) : x * y = y * x := by
simpa[models_iff] using ModelsTheory.models M Theory.PAMinus.mulComm (x :>ₙ fun _ ↦ y)
simpa[models_iff] using ModelsTheory.models M Theory.PeanoMinus.mulComm (x :>ₙ fun _ ↦ y)

lemma mul_lt_mul (x y z : M) : x < y → 0 < z → x * z < y * z := by
simpa[models_iff] using ModelsTheory.models M Theory.PAMinus.mulLtMul (x :>ₙ y :>ₙ fun _ ↦ z)
simpa[models_iff] using ModelsTheory.models M Theory.PeanoMinus.mulLtMul (x :>ₙ y :>ₙ fun _ ↦ z)

lemma distr (x y z : M) : x * (y + z) = x * y + x * z := by
simpa[models_iff] using ModelsTheory.models M Theory.PAMinus.distr (x :>ₙ y :>ₙ fun _ ↦ z)
simpa[models_iff] using ModelsTheory.models M Theory.PeanoMinus.distr (x :>ₙ y :>ₙ fun _ ↦ z)

lemma lt_irrefl (x : M) : ¬x < x := by
simpa[models_iff] using ModelsTheory.models M Theory.PAMinus.ltIrrefl (fun _ ↦ x)
simpa[models_iff] using ModelsTheory.models M Theory.PeanoMinus.ltIrrefl (fun _ ↦ x)

protected lemma lt_trans (x y z : M) : x < y → y < z → x < z := by
simpa[models_iff] using ModelsTheory.models M Theory.PAMinus.ltTrans (x :>ₙ y :>ₙ fun _ ↦ z)
simpa[models_iff] using ModelsTheory.models M Theory.PeanoMinus.ltTrans (x :>ₙ y :>ₙ fun _ ↦ z)

lemma lt_tri (x y : M) : x < y ∨ x = y ∨ y < x := by
simpa[models_iff] using ModelsTheory.models M Theory.PAMinus.ltTri (x :>ₙ fun _ ↦ y)
simpa[models_iff] using ModelsTheory.models M Theory.PeanoMinus.ltTri (x :>ₙ fun _ ↦ y)

scoped instance : AddCommMonoid M where
add_assoc := Arith.add_assoc
Expand Down Expand Up @@ -175,11 +175,11 @@ open LO.Arith

variable {T : Theory ℒₒᵣ} [𝐏𝐀⁻ ⪯ T]

instance CobhamR0.subTheoryPAMinus : 𝐑₀ ⪯ 𝐏𝐀⁻ := Entailment.WeakerThan.ofAxm! <| by
instance CobhamR0.subTheoryPeanoMinus : 𝐑₀ ⪯ 𝐏𝐀⁻ := Entailment.WeakerThan.ofAxm! <| by
intro φ h
rcases h
case equal h =>
exact Entailment.by_axm _ (Theory.PAMinus.equal _ h)
exact Entailment.by_axm _ (Theory.PeanoMinus.equal _ h)
case Ω₁ n m =>
apply complete <| oRing_consequence_of.{0} _ _ <| fun M _ _ => by simp [models_iff, numeral_eq_natCast]
case Ω₂ n m =>
Expand All @@ -196,7 +196,7 @@ instance CobhamR0.subTheoryPAMinus : 𝐑₀ ⪯ 𝐏𝐀⁻ := Entailment.Weake
instance : 𝐑₀ ⪱ 𝐏𝐀⁻ :=
Entailment.StrictlyWeakerThan.of_unprovable_provable
R₀_unprovable_add_zero
(Entailment.by_axm _ Theory.PAMinus.addZero)
(Entailment.by_axm _ Theory.PeanoMinus.addZero)

end FirstOrder.Arith

Expand Down
146 changes: 124 additions & 22 deletions Foundation/FirstOrder/Arith/Theory.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,27 +27,49 @@ inductive CobhamR0 : Theory ℒₒᵣ

notation "𝐑₀" => CobhamR0

inductive PAMinus : Theory ℒₒᵣ
| equal : ∀ φ ∈ 𝐄𝐐, PAMinus φ
| addZero : PAMinus “x | x + 0 = x”
| addAssoc : PAMinus “x y z | (x + y) + z = x + (y + z)”
| addComm : PAMinus “x y | x + y = y + x”
| addEqOfLt : PAMinus “x y | x < y → ∃ z, x + z = y”
| zeroLe : PAMinus “x | 0 ≤ x”
| zeroLtOne : PAMinus “0 < 1”
| oneLeOfZeroLt : PAMinus “x | 0 < x → 1 ≤ x”
| addLtAdd : PAMinus “x y z | x < y → x + z < y + z”
| mulZero : PAMinus “x | x * 0 = 0”
| mulOne : PAMinus “x | x * 1 = x”
| mulAssoc : PAMinus “x y z | (x * y) * z = x * (y * z)”
| mulComm : PAMinus “x y | x * y = y * x”
| mulLtMul : PAMinus “x y z | x < y ∧ 0 < z → x * z < y * z”
| distr : PAMinus “x y z | x * (y + z) = x * y + x * z”
| ltIrrefl : PAMinus “x | x ≮ x”
| ltTrans : PAMinus “x y z | x < y ∧ y < z → x < z”
| ltTri : PAMinus “x y | x < y ∨ x = y ∨ x > y”

notation "𝐏𝐀⁻" => PAMinus
variable {L}

abbrev Arith.addZero : SyntacticFormula L := “x | x + 0 = x”
abbrev Arith.addAssoc : SyntacticFormula L := “x y z | (x + y) + z = x + (y + z)”
abbrev Arith.addComm : SyntacticFormula L := “x y | x + y = y + x”
abbrev Arith.addEqOfLt : SyntacticFormula L := “x y | x < y → ∃ z, x + z = y”
abbrev Arith.zeroLe : SyntacticFormula L := “x | 0 ≤ x”
abbrev Arith.zeroLtOne : SyntacticFormula L := “0 < 1”
abbrev Arith.oneLeOfZeroLt : SyntacticFormula L := “x | 0 < x → 1 ≤ x”
abbrev Arith.addLtAdd : SyntacticFormula L := “x y z | x < y → x + z < y + z”
abbrev Arith.mulZero : SyntacticFormula L := “x | x * 0 = 0”
abbrev Arith.mulOne : SyntacticFormula L := “x | x * 1 = x”
abbrev Arith.mulAssoc : SyntacticFormula L := “x y z | (x * y) * z = x * (y * z)”
abbrev Arith.mulComm : SyntacticFormula L := “x y | x * y = y * x”
abbrev Arith.mulLtMul : SyntacticFormula L := “x y z | x < y ∧ 0 < z → x * z < y * z”
abbrev Arith.distr : SyntacticFormula L := “x y z | x * (y + z) = x * y + x * z”
abbrev Arith.ltIrrefl : SyntacticFormula L := “x | x ≮ x”
abbrev Arith.ltTrans : SyntacticFormula L := “x y z | x < y ∧ y < z → x < z”
abbrev Arith.ltTri : SyntacticFormula L := “x y | x < y ∨ x = y ∨ x > y”

inductive PeanoMinus : Theory ℒₒᵣ
| equal : ∀ φ ∈ 𝐄𝐐, PeanoMinus φ
| addZero : PeanoMinus Arith.addZero
| addAssoc : PeanoMinus Arith.addAssoc
| addComm : PeanoMinus Arith.addComm
| addEqOfLt : PeanoMinus Arith.addEqOfLt
| zeroLe : PeanoMinus Arith.zeroLe
| zeroLtOne : PeanoMinus Arith.zeroLtOne
| oneLeOfZeroLt : PeanoMinus Arith.oneLeOfZeroLt
| addLtAdd : PeanoMinus Arith.addLtAdd
| mulZero : PeanoMinus Arith.mulZero
| mulOne : PeanoMinus Arith.mulOne
| mulAssoc : PeanoMinus Arith.mulAssoc
| mulComm : PeanoMinus Arith.mulComm
| mulLtMul : PeanoMinus Arith.mulLtMul
| distr : PeanoMinus Arith.distr
| ltIrrefl : PeanoMinus Arith.ltIrrefl
| ltTrans : PeanoMinus Arith.ltTrans
| ltTri : PeanoMinus Arith.ltTri

notation "𝐏𝐀⁻" => PeanoMinus

variable (L)

def indScheme (Γ : Semiformula L ℕ 1 → Prop) : Theory L :=
{ ψ | ∃ φ : Semiformula L ℕ 1, Γ φ ∧ ψ = succInd φ }
Expand Down Expand Up @@ -98,7 +120,7 @@ instance : 𝐏𝐀⁻ ⪯ 𝐈𝐍𝐃Γ n := Entailment.WeakerThan.ofSubset (b

instance : 𝐄𝐐 ⪯ 𝐑₀ := Entailment.WeakerThan.ofSubset <| fun φ hp ↦ CobhamR0.equal φ hp

instance : 𝐄𝐐 ⪯ 𝐏𝐀⁻ := Entailment.WeakerThan.ofSubset <| fun φ hp ↦ PAMinus.equal φ hp
instance : 𝐄𝐐 ⪯ 𝐏𝐀⁻ := Entailment.WeakerThan.ofSubset <| fun φ hp ↦ PeanoMinus.equal φ hp

instance : 𝐄𝐐 ⪯ 𝐈𝐍𝐃Γ n := Entailment.WeakerThan.trans (inferInstanceAs (𝐄𝐐 ⪯ 𝐏𝐀⁻)) inferInstance

Expand All @@ -116,6 +138,86 @@ instance : 𝐈𝚺₀ ⪯ 𝐈𝚺₁ :=
instance (i) : 𝐈𝚺i ⪯ 𝐏𝐀 :=
Entailment.WeakerThan.ofSubset <| Set.union_subset_union_right _ <| indScheme_subset (by intros; trivial)

example (a b : ℕ) : Set.Finite {a, b} := by simp only [Set.finite_singleton, Set.Finite.insert]

@[simp] lemma PeanoMinus.finite : Set.Finite 𝐏𝐀⁻ := by
have : 𝐏𝐀⁻ =
𝐄𝐐 ∪
{ Arith.addZero,
Arith.addAssoc,
Arith.addComm,
Arith.addEqOfLt,
Arith.zeroLe,
Arith.zeroLtOne,
Arith.oneLeOfZeroLt,
Arith.addLtAdd,
Arith.mulZero,
Arith.mulOne,
Arith.mulAssoc,
Arith.mulComm,
Arith.mulLtMul,
Arith.distr,
Arith.ltIrrefl,
Arith.ltTrans,
Arith.ltTri } := by
ext φ; constructor
· rintro ⟨⟩
case equal => left; assumption
case addZero => tauto
case addAssoc => tauto
case addComm => tauto
case addEqOfLt => tauto
case zeroLe => tauto
case zeroLtOne => tauto
case oneLeOfZeroLt => tauto
case addLtAdd => tauto
case mulZero => tauto
case mulOne => tauto
case mulAssoc => tauto
case mulComm => tauto
case mulLtMul => tauto
case distr => tauto
case ltIrrefl => tauto
case ltTrans => tauto
case ltTri => tauto
· rintro (h | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl)
· exact equal _ h
· exact addZero
· exact addAssoc
· exact addComm
· exact addEqOfLt
· exact zeroLe
· exact zeroLtOne
· exact oneLeOfZeroLt
· exact addLtAdd
· exact mulZero
· exact mulOne
· exact mulAssoc
· exact mulComm
· exact mulLtMul
· exact distr
· exact ltIrrefl
· exact ltTrans
· exact ltTri
rw [this]; simp only [Set.finite_union, EqAxiom.finite, true_and]
apply Set.Finite.insert
apply Set.Finite.insert
apply Set.Finite.insert
apply Set.Finite.insert
apply Set.Finite.insert
apply Set.Finite.insert
apply Set.Finite.insert
apply Set.Finite.insert
apply Set.Finite.insert
apply Set.Finite.insert
apply Set.Finite.insert
apply Set.Finite.insert
apply Set.Finite.insert
apply Set.Finite.insert
apply Set.Finite.insert
apply Set.Finite.insert
apply Set.finite_singleton

end Theory

end FirstOrder
Loading

0 comments on commit a668f38

Please sign in to comment.