Documentation

Incompleteness.Arith.D1

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

LO.FirstOrder.Derivation2 T Δ

Equations

d.cast h = h ▸ d

Instances For

noncomputable 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 Γ = ∑ φ ∈ Γ, exp ⌜φ⌝

Instances For

noncomputable 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)) :

⌜Γ⌝ = ∑ φ ∈ Γ, exp ⌜φ⌝

@[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} [L.DecidableEq] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {Γ : Finset (LO.FirstOrder.SyntacticFormula L)} {φ : LO.FirstOrder.SyntacticFormula L} :

⌜φ⌝ ∈ ⌜Γ⌝ ↔ φ ∈ Γ

theorem LO.FirstOrder.Derivation2.Sequent.quote_inj {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [L.DecidableEq] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {Γ Δ : 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} [L.DecidableEq] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {Γ Δ : 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)] [L.DecidableEq] (φ : LO.FirstOrder.SyntacticFormula L) :

⌜{φ}⌝ = {⌜φ⌝}

@[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)] [L.DecidableEq] (Γ : Finset (LO.FirstOrder.SyntacticFormula L)) (φ : LO.FirstOrder.SyntacticFormula L) :

⌜insert φ Γ⌝ = insert ⌜φ⌝ ⌜Γ⌝

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} [L.DecidableEq] {Γ : Finset (LO.FirstOrder.SyntacticFormula L)} (hx : x ∈ ⌜Γ⌝) :

∃ φ ∈ Γ, x = ⌜φ⌝

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

x ∈ ⌜Γ⌝ ↔ ∃ φ ∈ Γ, x = ⌜φ⌝

theorem LO.FirstOrder.Derivation2.setShift_quote {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [L.DecidableEq] [(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.Rewriting.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} [L.DecidableEq] {Γ : Finset (LO.FirstOrder.SyntacticFormula L)} :

LO.FirstOrder.Derivation2 T Γ → V

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)

Instances For

instance LO.FirstOrder.Derivation2.instGoedelQuote_incompleteness (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [L.DecidableEq] [(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} [L.DecidableEq] [(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} [L.DecidableEq] [(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] [L.DecidableEq] (Γ : Finset (LO.FirstOrder.SyntacticFormula L)) :

(L.codeIn V).setShift ⌜Γ⌝ = ⌜Finset.image LO.FirstOrder.Rewriting.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] [L.DecidableEq] {Γ : 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] {φ : LO.FirstOrder.SyntacticFormula L} :

T ⊢! φ → (LO.FirstOrder.Theory.codeIn V T).Provable ⌜φ⌝

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] {φ : LO.FirstOrder.SyntacticFormula L} :

T ⊢! φ → LO.FirstOrder.Theory.tCodeIn V T ⊢! ⌜φ⌝

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} [L.DecidableEq] [(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} [L.DecidableEq] [(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.Derivable2 T Γ

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

LO.FirstOrder.Derivable2SingleConseq T φ

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

T ⊢! φ

theorem LO.Arith.Language.Theory.Provable.sound₀ {L : LO.FirstOrder.Language} [L.DecidableEq] [(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} [L.DecidableEq] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {T : LO.FirstOrder.Theory L} [T.Delta1Definable] {φ : LO.FirstOrder.SyntacticFormula L} :

LO.FirstOrder.Theory.tCodeIn ℕ T ⊢! ⌜φ⌝ ↔ T ⊢! φ