Arithmetic Hierarchy

This file defines Σ₁ formulas in arithmetic hierarchy and ω-consistency. Current we are not interested in defining the whole arithmetic hierarchy.

inductive FirstOrder.Language.peano.Sigma₁ {n : ℕ} : peano.Formula n → Prop

The set of Σ₁ formulas is closed under conjunction, disjunction, existential quantifier and bounded universal quantifier. This is a strict syntactic definition, mainly used to prove Hilbert-Bernays provability conditions.

• eq {n : ℕ} {t₁ t₂ : peano.Term n} : Sigma₁ (t₁ ≐ t₂)
• neq {n : ℕ} {t₁ t₂ : peano.Term n} : Sigma₁ (~ t₁ ≐ t₂)
• false {n : ℕ} : Sigma₁ ⊥
• true {n : ℕ} : Sigma₁ ⊤
• and {n : ℕ} {p q : peano.Formula n} : Sigma₁ p → Sigma₁ q → Sigma₁ (p ⩑ q)
• or {n : ℕ} {p q : peano.Formula n} : Sigma₁ p → Sigma₁ q → Sigma₁ (p ⩒ q)
• ex {n : ℕ} {p : peano.Formula (n + 1)} : Sigma₁ p → Sigma₁ (∃' p)
• bdall {n : ℕ} {p : peano.Formula (n + 1)} {t : peano.Term n} : Sigma₁ p → Sigma₁ (∀[≺ t] p)

theorem FirstOrder.Language.peano.Sigma₁.le {n✝ : ℕ} {t₁ t₂ : peano.Term n✝} : Sigma₁ (t₁ ⪯ t₂)

theorem FirstOrder.Language.peano.Sigma₁.lt {n✝ : ℕ} {t₁ t₂ : peano.Term n✝} : Sigma₁ (t₁ ≺ t₂)

theorem FirstOrder.Language.peano.Sigma₁.andN {n m : ℕ} {v : Vec (peano.Formula n) m} : (∀ (i : Fin m), Sigma₁ (v i)) → Sigma₁ (⋀ (i : Fin m), v i)

theorem FirstOrder.Language.peano.Sigma₁.orN {n m : ℕ} {v : Vec (peano.Formula n) m} : (∀ (i : Fin m), Sigma₁ (v i)) → Sigma₁ (⋁ (i : Fin m), v i)

theorem FirstOrder.Language.peano.Sigma.exN {n m : ℕ} {p : peano.Formula (n + m)} : Sigma₁ p → Sigma₁ (∃^[m] p)

theorem FirstOrder.Language.peano.Sigma.bdex {a✝ : ℕ} {p : peano.Formula (a✝ + 1)} {t : peano.Term a✝} : Sigma₁ p → Sigma₁ (∃[≺ t] p)

theorem FirstOrder.Language.peano.Sigma₁.subst {n m : ℕ} {p : peano.Formula n} {σ : peano.Subst n m} : Sigma₁ p → Sigma₁ p[σ]ₚ

def FirstOrder.Language.peano.OmegaConsistent (T : peano.Theory) : Prop

A theory is ω-consistent if it does not prove both ∃ x. p(x) and p(0), p(1), ⋯.

Equations

• FirstOrder.Language.peano.OmegaConsistent T = ∀ (p : FirstOrder.Language.peano.Formula (0 + 1)), ¬(T ⊢ ∃' p ∧ ∀ (n : ℕ), T ⊢ ~ p[↦ₛ FirstOrder.Language.peano.ofNat n]ₚ)

theorem FirstOrder.Language.peano.OmegaConsistent.consistent {T : peano.Theory} : OmegaConsistent T → Consistent T