D1

@[implicit_reducible]

noncomputable def LO.FirstOrder.instDecidableEqOfClassical (α : Sort u_1) : DecidableEq α

Local classical decidable equality instance used by imported proofs.

Equations

• LO.FirstOrder.instDecidableEqOfClassical α = Classical.decEq α

def LO.FirstOrder.Derivation2.cast {L : Language} [L.DecidableEq] {Γ Δ : Finset (SyntacticFormula L)} {T : Theory L} (d : Derivation2 T Γ) (h : Γ = Δ) : Derivation2 T Δ

Imported declaration from the Incompleteness formalization.

Equations

• d.cast h = h ▸ d

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

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

Equations

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

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

@[simp]

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Derivation2.codeIn V (LO.FirstOrder.Derivation2.closed x✝ φ a a_1) = LO.Arith.axL ⌜x✝⌝ ⌜φ⌝
• LO.FirstOrder.Derivation2.codeIn V (LO.FirstOrder.Derivation2.root φ a a_1) = LO.Arith.root ⌜x✝⌝ ⌜φ⌝
• 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✝⌝ ⌜φ⌝ ⌜ψ⌝ (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✝⌝ ⌜φ⌝ ⌜ψ⌝ (LO.FirstOrder.Derivation2.codeIn V d)
• LO.FirstOrder.Derivation2.codeIn V (LO.FirstOrder.Derivation2.all a d) = LO.Arith.allIntro ⌜x✝⌝ ⌜φ⌝ (LO.FirstOrder.Derivation2.codeIn V d)
• LO.FirstOrder.Derivation2.codeIn V (LO.FirstOrder.Derivation2.ex a t d) = LO.Arith.exIntro ⌜x✝⌝ ⌜φ⌝ ⌜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.Rewriting.shift Δ⌝ (LO.FirstOrder.Derivation2.codeIn V d)
• LO.FirstOrder.Derivation2.codeIn V (d.cut dn) = LO.Arith.cutRule ⌜x✝⌝ ⌜φ⌝ (LO.FirstOrder.Derivation2.codeIn V d) (LO.FirstOrder.Derivation2.codeIn V dn)

@[implicit_reducible]

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

Equations

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

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

@[simp]

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

@[implicit_reducible]

noncomputable def LO.Arith.instDecidableEqOfClassical₂ (α : Sort u_1) : DecidableEq α

Local classical decidable equality instance used by imported proofs.

Equations

• LO.Arith.instDecidableEqOfClassical₂ α = Classical.decEq α

@[simp]

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

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

@[simp]

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

@[simp]

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

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

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

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

Hilbert–Bernays provability condition D1

theorem LO.Arith.provableₐ_of_provable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {T : FirstOrder.Theory ℒₒᵣ} [T.Delta1Definable] {σ : 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 : FirstOrder.Language} [L.DecidableEq] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [DefinableLanguage L] {s : ℕ} : (L.codeIn ℕ).IsFormulaSet s → ∃ (S : Finset (FirstOrder.SyntacticFormula L)), ⌜S⌝ = s

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

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

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

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

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

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

@[simp]

theorem LO.Arith.provableₐ_iff_provable₀ {T : FirstOrder.Theory ℒₒᵣ} [T.Delta1Definable] [𝐑₀ wkn T] {σ : FirstOrder.Sentence ℒₒᵣ} : T.Provableₐ ⌜σ⌝ ↔ T ⊢! ↑σ