def LO.FirstOrder.Derivation2.cast : {L : LO.FirstOrder.Language} → {T : LO.FirstOrder.Theory L} → {Γ Δ : Finset (LO.FirstOrder.SyntacticFormula L)} → LO.FirstOrder.Derivation2 T Γ → Γ = Δ → LO.FirstOrder.Derivation2 T Δ

Equations

• d.cast h = h ▸ d

def LO.FirstOrder.Derivation2.Sequent.codeIn (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] (Γ : Finset (LO.FirstOrder.SyntacticFormula L)) : V

Equations

• LO.FirstOrder.Derivation2.Sequent.codeIn V Γ = ∑ p ∈ Γ, exp ⌜p⌝

instance LO.FirstOrder.Derivation2.instGoedelQuoteFinsetSyntacticFormula_incompleteness (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] : LO.GoedelQuote (Finset (LO.FirstOrder.SyntacticFormula L)) V

Equations

• LO.FirstOrder.Derivation2.instGoedelQuoteFinsetSyntacticFormula_incompleteness V = { quote := LO.FirstOrder.Derivation2.Sequent.codeIn V }

theorem LO.FirstOrder.Derivation2.Sequent.codeIn_def (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] (Γ : Finset (LO.FirstOrder.SyntacticFormula L)) : ⌜Γ⌝ = ∑ p ∈ Γ, exp ⌜p⌝

@[simp]

theorem LO.FirstOrder.Derivation2.Sequent.codeIn_empty {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] : ⌜∅⌝ = ∅

theorem LO.FirstOrder.Derivation2.Sequent.mem_codeIn_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {Γ : Finset (LO.FirstOrder.SyntacticFormula L)} {p : LO.FirstOrder.SyntacticFormula L} : ⌜p⌝ ∈ ⌜Γ⌝ ↔ p ∈ Γ

theorem LO.FirstOrder.Derivation2.Sequent.quote_inj {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {Γ : Finset (LO.FirstOrder.SyntacticFormula L)} {Δ : Finset (LO.FirstOrder.SyntacticFormula L)} : ⌜Γ⌝ = ⌜Δ⌝ → Γ = Δ

theorem LO.FirstOrder.Derivation2.Sequent.subset_of_quote_subset_quote {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {Γ : Finset (LO.FirstOrder.SyntacticFormula L)} {Δ : Finset (LO.FirstOrder.SyntacticFormula L)} : ⌜Γ⌝ ⊆ ⌜Δ⌝ → Γ ⊆ Δ

@[simp]

theorem LO.FirstOrder.Derivation2.Sequent.codeIn_singleton {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] (p : LO.FirstOrder.SyntacticFormula L) : ⌜{p}⌝ = {⌜p⌝}

@[simp]

theorem LO.FirstOrder.Derivation2.Sequent.codeIn_insert {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] (Γ : Finset (LO.FirstOrder.SyntacticFormula L)) (p : LO.FirstOrder.SyntacticFormula L) : ⌜insert p Γ⌝ = insert ⌜p⌝ ⌜Γ⌝

theorem LO.FirstOrder.Derivation2.Sequent.mem_codeIn {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {x : V} {Γ : Finset (LO.FirstOrder.SyntacticFormula L)} (hx : x ∈ ⌜Γ⌝) : ∃ p ∈ Γ, x = ⌜p⌝

theorem LO.FirstOrder.Derivation2.Sequent.mem_codeIn_iff' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {x : V} {Γ : Finset (LO.FirstOrder.SyntacticFormula L)} : x ∈ ⌜Γ⌝ ↔ ∃ p ∈ Γ, x = ⌜p⌝

theorem LO.FirstOrder.Derivation2.setShift_quote {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] (Γ : Finset (LO.FirstOrder.SyntacticFormula L)) : (L.codeIn V).setShift ⌜Γ⌝ = ⌜Finset.image (⇑(LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.shift)) Γ⌝

def LO.FirstOrder.Derivation2.codeIn (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {T : LO.FirstOrder.Theory L} {Γ : Finset (LO.FirstOrder.SyntacticFormula L)} : LO.FirstOrder.Derivation2 T Γ → V

Equations

• LO.FirstOrder.Derivation2.codeIn V (LO.FirstOrder.Derivation2.closed x p a a_1) = LO.Arith.axL ⌜x⌝ ⌜p⌝
• LO.FirstOrder.Derivation2.codeIn V (LO.FirstOrder.Derivation2.root p a a_1) = LO.Arith.root ⌜x⌝ ⌜p⌝
• LO.FirstOrder.Derivation2.codeIn V (LO.FirstOrder.Derivation2.verum a) = LO.Arith.verumIntro ⌜x⌝
• LO.FirstOrder.Derivation2.codeIn V (LO.FirstOrder.Derivation2.and a bp bq) = LO.Arith.andIntro ⌜x⌝ ⌜p⌝ ⌜q⌝ (LO.FirstOrder.Derivation2.codeIn V bp) (LO.FirstOrder.Derivation2.codeIn V bq)
• LO.FirstOrder.Derivation2.codeIn V (LO.FirstOrder.Derivation2.or a d) = LO.Arith.orIntro ⌜x⌝ ⌜p⌝ ⌜q⌝ (LO.FirstOrder.Derivation2.codeIn V d)
• LO.FirstOrder.Derivation2.codeIn V (LO.FirstOrder.Derivation2.all a d) = LO.Arith.allIntro ⌜x⌝ ⌜p⌝ (LO.FirstOrder.Derivation2.codeIn V d)
• LO.FirstOrder.Derivation2.codeIn V (LO.FirstOrder.Derivation2.ex a t d) = LO.Arith.exIntro ⌜x⌝ ⌜p⌝ ⌜t⌝ (LO.FirstOrder.Derivation2.codeIn V d)
• LO.FirstOrder.Derivation2.codeIn V (d.wk a) = LO.Arith.wkRule ⌜x⌝ (LO.FirstOrder.Derivation2.codeIn V d)
• LO.FirstOrder.Derivation2.codeIn V d.shift = LO.Arith.shiftRule ⌜Finset.image (⇑(LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.shift)) Δ⌝ (LO.FirstOrder.Derivation2.codeIn V d)
• LO.FirstOrder.Derivation2.codeIn V (d.cut dn) = LO.Arith.cutRule ⌜x⌝ ⌜p⌝ (LO.FirstOrder.Derivation2.codeIn V d) (LO.FirstOrder.Derivation2.codeIn V dn)

instance LO.FirstOrder.Derivation2.instGoedelQuote_incompleteness (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {T : LO.FirstOrder.Theory L} (Γ : Finset (LO.FirstOrder.SyntacticFormula L)) : LO.GoedelQuote (LO.FirstOrder.Derivation2 T Γ) V

Equations

• LO.FirstOrder.Derivation2.instGoedelQuote_incompleteness V Γ = { quote := LO.FirstOrder.Derivation2.codeIn V }

theorem LO.FirstOrder.Derivation2.quote_derivation_def (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {T : LO.FirstOrder.Theory L} {Γ : Finset (LO.FirstOrder.SyntacticFormula L)} (d : LO.FirstOrder.Derivation2 T Γ) : ⌜d⌝ = LO.FirstOrder.Derivation2.codeIn V d

@[simp]

theorem LO.FirstOrder.Derivation2.fstidx_quote (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {T : LO.FirstOrder.Theory L} {Γ : Finset (LO.FirstOrder.SyntacticFormula L)} (d : LO.FirstOrder.Derivation2 T Γ) : LO.Arith.fstIdx ⌜d⌝ = ⌜Γ⌝

@[simp]

theorem LO.Arith.formulaSet_codeIn_finset {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] (Γ : Finset (LO.FirstOrder.SyntacticFormula L)) : (L.codeIn V).IsFormulaSet ⌜Γ⌝

theorem LO.Arith.quote_image_shift {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] (Γ : Finset (LO.FirstOrder.SyntacticFormula L)) : (L.codeIn V).setShift ⌜Γ⌝ = ⌜Finset.image (⇑(LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.shift)) Γ⌝

@[simp]

theorem LO.Arith.derivation_quote {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {T : LO.FirstOrder.Theory L} [T.Delta1Definable] {Γ : Finset (LO.FirstOrder.SyntacticFormula L)} (d : LO.FirstOrder.Derivation2 T Γ) : (LO.FirstOrder.Theory.codeIn V T).Derivation ⌜d⌝

@[simp]

theorem LO.Arith.derivationOf_quote {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {T : LO.FirstOrder.Theory L} [T.Delta1Definable] {Γ : Finset (LO.FirstOrder.SyntacticFormula L)} (d : LO.FirstOrder.Derivation2 T Γ) : (LO.FirstOrder.Theory.codeIn V T).DerivationOf ⌜d⌝ ⌜Γ⌝

theorem LO.Arith.derivable_of_quote {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {T : LO.FirstOrder.Theory L} [T.Delta1Definable] {Γ : Finset (LO.FirstOrder.SyntacticFormula L)} (d : LO.FirstOrder.Derivation2 T Γ) : (LO.FirstOrder.Theory.codeIn V T).Derivable ⌜Γ⌝

theorem LO.Arith.provable_of_provable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {T : LO.FirstOrder.Theory L} [T.Delta1Definable] {p : LO.FirstOrder.SyntacticFormula L} : T ⊢! p → (LO.FirstOrder.Theory.codeIn V T).Provable ⌜p⌝

theorem LO.Arith.tprovable_of_provable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {T : LO.FirstOrder.Theory L} [T.Delta1Definable] {p : LO.FirstOrder.SyntacticFormula L} : T ⊢! p → LO.FirstOrder.Theory.tCodeIn V T ⊢! ⌜p⌝

Hilbert–Bernays provability condition D1

theorem LO.Arith.provableₐ_of_provable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {T : LO.FirstOrder.Theory ℒₒᵣ} [T.Delta1Definable] {σ : LO.FirstOrder.SyntacticFormula ℒₒᵣ} : T ⊢! σ → T.Provableₐ ⌜σ⌝

theorem Nat.double_add_one_div_of_double (n : ℕ) (m : ℕ) : (2 * n + 1) / (2 * m) = n / m

theorem Nat.mem_bitIndices_iff {x : ℕ} {s : ℕ} : x ∈ s.bitIndices ↔ Odd (s / 2 ^ x)

theorem LO.Arith.isFormulaSet_sound {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {s : ℕ} : (L.codeIn ℕ).IsFormulaSet s → ∃ (S : Finset (LO.FirstOrder.SyntacticFormula L)), ⌜S⌝ = s

theorem LO.Arith.Language.Theory.Derivation.sound {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {T : LO.FirstOrder.Theory L} [T.Delta1Definable] {d : ℕ} (h : (LO.FirstOrder.Theory.codeIn ℕ T).Derivation d) : ∃ (Γ : Finset (LO.FirstOrder.SyntacticFormula L)), ⌜Γ⌝ = LO.Arith.fstIdx d ∧ LO.FirstOrder.Derivable3 T Γ

theorem LO.Arith.Language.Theory.Provable.sound2 {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {T : LO.FirstOrder.Theory L} [T.Delta1Definable] {p : LO.FirstOrder.SyntacticFormula L} (h : (LO.FirstOrder.Theory.codeIn ℕ T).Provable ⌜p⌝) : LO.FirstOrder.Derivable3SingleConseq T p

theorem LO.Arith.Language.Theory.Provable.sound {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {T : LO.FirstOrder.Theory L} [T.Delta1Definable] {p : LO.FirstOrder.SyntacticFormula L} (h : (LO.FirstOrder.Theory.codeIn ℕ T).Provable ⌜p⌝) : T ⊢! p

theorem LO.Arith.Language.Theory.Provable.sound₀ {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {T : LO.FirstOrder.Theory L} [T.Delta1Definable] {σ : LO.FirstOrder.Sentence L} (h : (LO.FirstOrder.Theory.codeIn ℕ T).Provable ⌜σ⌝) : T ⊢! ↑σ

theorem LO.Arith.Language.Theory.Provable.complete {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {T : LO.FirstOrder.Theory L} [T.Delta1Definable] {p : LO.FirstOrder.SyntacticFormula L} : LO.FirstOrder.Theory.tCodeIn ℕ T ⊢! ⌜p⌝ ↔ T ⊢! p