Is Sigma1 of hierarchy
LO.FirstOrder.Arithmetic.isSigma1_of_hierarchy
Plain-language statement
(⟸) Every 𝚺₁ formula has a 𝚺₁-recognized code. By sigma₁_induction'.
Exact Lean statement
lemma isSigma1_of_hierarchy {n : ℕ} {ψ : _root_.LO.FirstOrder.ArithmeticSemiformula ℕ n} (h : Hierarchy 𝚺 1 ψ) :
IsSigma1 (⌜ψ⌝ : ℕ)Formal artifact
Lean source
lemma isSigma1_of_hierarchy {n : ℕ} {ψ : _root_.LO.FirstOrder.ArithmeticSemiformula ℕ n} (h : Hierarchy 𝚺 1 ψ) : IsSigma1 (⌜ψ⌝ : ℕ) := by refine sigma₁_induction' h (P := fun n φ => IsSigma1 (⌜φ⌝ : ℕ)) ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ · intro n; simp · intro n; simp · intro n t₁ t₂; simp [Semiformula.quote_rel] · intro n t₁ t₂; simp [Semiformula.quote_nrel] · intro n t₁ t₂; simp [Semiformula.quote_rel] · intro n t₁ t₂; simp [Semiformula.quote_nrel] · intro n φ ψ hφ hψ ihφ ihψ; simpa [Semiformula.quote_and] using ⟨ihφ, ihψ⟩ · intro n φ ψ hφ hψ ihφ ihψ; simpa [Semiformula.quote_or] using ⟨ihφ, ihψ⟩ · intro n t φ hφ ihφ rw [quote_ball] refine IsSigma1.mk (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr ⟨termBShift ℒₒᵣ (⌜t⌝ : ℕ), (⌜φ⌝ : ℕ), ⟨(⌜t⌝ : ℕ), ?_, rfl⟩, ihφ, rfl⟩))))))) simp [Semiterm.quote_def] · intro n φ hφ ihφ; simpa [Semiformula.quote_ex] using ihφ- Project
- Foundation
- License
- Apache-2.0
- Commit
- 8dcdb3196454
- Source
- Foundation/FirstOrder/Incompleteness/InductionSchemeDelta1.lean:1154-1171
Reuse this declaration
Bring the exact result into your workflow
The import identifies the source module. Your project still needs the pinned package dependency shown on this page.
What this badge means
This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.
Continue in this project
Related declarations
Computable Pred iff decoded pred
ComputablePred.iff_decoded_pred
Plain-language statement
Computability of a predicate on a Primcodable type is equivalent to the computability of the corresponding predicate on ℕ obtained by decoding.
Source project: Foundation
Person-level attribution pending.
Bv quote fixitr
LO.FirstOrder.Arithmetic.Bootstrapping.bv_quote_fixitr
Plain-language statement
bv-pin bridge (over ℕ): bv ⌜fixitr 0 (fvSup χ) ▹ χ⌝ = fvSup χ. - ≤ is immediate from quote_univCl_eq + bv_qqAlls (closing fvSup quantifiers reaches a sentence, whose bv is 0). - ≥ is by level-factoring: were the body an IsSemiformula j for some j < fvSup, IsSemiformula.sound + castLE-invariance would re-express χ as `γ ⇜ ![...
Source project: Foundation
Person-level attribution pending.
Conj
LO.FirstOrder.Arithmetic.Bootstrapping.Derivable.conj
Plain-language statement
Crucial inducion for formalized -completeness.
Source project: Foundation
Person-level attribution pending.