Collection in models, and 𝗕𝚺 (s + 1) below 𝗜𝚺 (s + 1)

Collection for a definable relation in a model of a collection scheme, the converse passage from collection to a model of the scheme, and the collection available in a model of 𝗜𝚺 (s + 1).

References

• [HP98]
• [Bus98]

theorem FFL.FirstOrder.Arithmetic.CollectionScheme.collection {V : Type u_1} [ORingStructure V] {C : ArithmeticSemiformula ℕ 2 → Prop} [V↓[ℒₒᵣ] ⊧* CollectionScheme C] {R : V → V → Prop} (hR : ∃ (e : ℕ → V) (φ : ArithmeticSemiformula ℕ 2), C φ ∧ ∀ (x y : V), R x y ↔ (Semiformula.Eval ![x, y] e) φ) (a : V) (h : ∀ x < a, ∃ (y : V), R x y) : ∃ (b : V), ∀ x < a, ∃ y < b, R x y

theorem FFL.FirstOrder.Arithmetic.CollectionScheme.models_of_collection {V : Type u_1} [ORingStructure V] {Γ : Polarity} {s : ℕ} (H : ∀ {R : V → V → Prop}, ({ Γ := Γ.coe, rank := s }-Relation R) → ∀ (a : V), (∀ x < a, ∃ (y : V), R x y) → ∃ (b : V), ∀ x < a, ∃ y < b, R x y) : V↓[ℒₒᵣ] ⊧* CollectionScheme (Hierarchy Γ s)

instance FFL.FirstOrder.Arithmetic.CollectionOnHierarchy.models_CollectionScheme {V : Type u_1} [ORingStructure V] (Γ : Polarity) (s : ℕ) [V↓[ℒₒᵣ] ⊧* 𝗕 Γ s] : V↓[ℒₒᵣ] ⊧* CollectionScheme (StrictHierarchy Γ s)

theorem FFL.FirstOrder.Arithmetic.CollectionOnHierarchy.collection {V : Type u_1} [ORingStructure V] {R : V → V → Prop} (Γ : Polarity) (s : ℕ) [V↓[ℒₒᵣ] ⊧* 𝗕 Γ s] (hR : StrictDefinableRel Γ s R) (a : V) (h : ∀ x < a, ∃ (y : V), R x y) : ∃ (b : V), ∀ x < a, ∃ y < b, R x y

The standard model

instance FFL.FirstOrder.Arithmetic.models_CollectionOnHierarchy (Γ : Polarity) (s : ℕ) : ℕ↓[ℒₒᵣ] ⊧* 𝗕 Γ s

instance FFL.FirstOrder.Arithmetic.instConsistentSentenceORingArithmeticTheoryCollectionOnHierarchy {Γ : Polarity} {s : ℕ} : Entailment.Consistent (𝗕 Γ s)

𝗕𝚺 (s + 1) below 𝗜𝚺 (s + 1)

theorem FFL.FirstOrder.Arithmetic.ISigma.collection {V : Type u_1} [ORingStructure V] {s : ℕ} [V↓[ℒₒᵣ] ⊧* 𝗜𝚺(s + 1)] {R : V → V → Prop} (hR : { Γ := 𝚺, rank := s + 1 }-Relation R) (a : V) (h : ∀ x < a, ∃ (y : V), R x y) : ∃ (b : V), ∀ x < a, ∃ y < b, R x y

instance FFL.FirstOrder.Arithmetic.ISigma.models_BSigma_succ {V : Type u_1} [ORingStructure V] {s : ℕ} [V↓[ℒₒᵣ] ⊧* 𝗜𝚺(s + 1)] : V↓[ℒₒᵣ] ⊧* 𝗕𝚺(s + 1)

instance FFL.FirstOrder.Arithmetic.BSigma_weakerThan_ISigma {s : ℕ} : 𝗕𝚺(s + 1) ⪯ 𝗜𝚺(s + 1)

instance FFL.FirstOrder.Arithmetic.BSigma_weakerThan_ISigma_succ {s : ℕ} : 𝗕𝚺s ⪯ 𝗜𝚺(s + 1)

instance FFL.FirstOrder.Arithmetic.BSigma_weakerThan_Peano {s : ℕ} : 𝗕𝚺s ⪯ 𝗣𝗔