Craig's trick

The Craig companion of a recursively enumerable theory is moreover primitive recursive.

theorem FFL.FirstOrder.Semiformula.weight_succ {L : Language} {ξ : Type u_1} {n : ℕ} (k : ℕ) : weight (k + 1) = ⊤ ⋏ weight k

theorem FFL.FirstOrder.Semiformula.encode_weight_succ {L : Language} {ξ : Type u_1} {n : ℕ} [L.Encodable] [Encodable ξ] (k : ℕ) : Encodable.encode (weight (k + 1)) = Nat.pair 4 (Nat.pair (Encodable.encode ⊤) (Encodable.encode (weight k))) + 1

theorem FFL.FirstOrder.Semiformula.le_encode_weight {L : Language} {ξ : Type u_1} {n : ℕ} [L.Encodable] [Encodable ξ] (k : ℕ) : k ≤ Encodable.encode (weight k)

theorem FFL.FirstOrder.Semiformula.encode_padding {L : Language} {ξ : Type u_1} {n : ℕ} [L.Encodable] [Encodable ξ] (φ : Semiformula L ξ n) (k : ℕ) : Encodable.encode (φ.padding k) = Nat.pair 4 (Nat.pair (Encodable.encode φ) (Encodable.encode (weight k))) + 1

theorem FFL.FirstOrder.Semiformula.encode_lt_encode_padding {L : Language} {ξ : Type u_1} {n : ℕ} [L.Encodable] [Encodable ξ] (φ : Semiformula L ξ n) (k : ℕ) : Encodable.encode φ < Encodable.encode (φ.padding k)

theorem FFL.FirstOrder.Semiformula.lt_encode_padding {L : Language} {ξ : Type u_1} {n : ℕ} [L.Encodable] [Encodable ξ] (φ : Semiformula L ξ n) (k : ℕ) : k < Encodable.encode (φ.padding k)

theorem FFL.FirstOrder.Semiformula.primrec_encode_weight {L : Language} {ξ : Type u_1} {n : ℕ} [L.Encodable] [Encodable ξ] : Primrec fun (k : ℕ) => Encodable.encode (weight k)

noncomputable def FFL.FirstOrder.Theory.reCh {L : Language} [L.Encodable] [L.Primcodable] (T : Theory L) [T.RE] : 𝚺₁.Semisentence 1

Equations

• T.reCh = FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkSigma (FFL.FirstOrder.Arithmetic.codeOfREPred (Encodable.encode '' T)) ⋯

noncomputable def FFL.FirstOrder.Theory.reWitness {L : Language} [L.Encodable] [L.Primcodable] (T : Theory L) [T.RE] : 𝚺₀.Semisentence 2

Equations

• T.reWitness = ⋯.choose

theorem FFL.FirstOrder.Theory.reWitness_spec {L : Language} [L.Encodable] [L.Primcodable] (T : Theory L) [T.RE] (V : Type u_1) [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (e : Fin 1 → V) : (Semiformula.Evalb e) ↑T.reCh ↔ ∃ (w : V), (Semiformula.Evalb (w :> e)) ↑T.reWitness

@[simp]

theorem FFL.FirstOrder.Theory.rePred_codes_of_RE {L : Language} [L.Encodable] [L.Primcodable] (T : Theory L) [T.RE] : REPred (Encodable.encode '' T)

theorem FFL.FirstOrder.Theory.exists_mem_of_reCh {L : Language} [L.Encodable] [L.Primcodable] (T : Theory L) [T.RE] [L.LORDefinable] (φ : Proposition L) (h : (Semiformula.Evalb ![⌜φ⌝]) ↑T.reCh) : ∃ σ ∈ T, φ = Rewriting.emb σ

theorem FFL.FirstOrder.Theory.mem_of_reCh {L : Language} [L.Encodable] [L.Primcodable] (T : Theory L) [T.RE] [L.LORDefinable] (σ : Sentence L) (h : (Semiformula.Evalb ![⌜σ⌝]) ↑T.reCh) : σ ∈ T

theorem FFL.FirstOrder.Theory.reCh_of_mem {L : Language} [L.Encodable] [L.Primcodable] (T : Theory L) [T.RE] [L.LORDefinable] (σ : Sentence L) (hσ : σ ∈ T) : (Semiformula.Evalb ![⌜σ⌝]) ↑T.reCh

def FFL.FirstOrder.Theory.craig {L : Language} [L.Encodable] [L.Primcodable] (T : Theory L) [T.RE] [L.LORDefinable] : Theory L

Equations

• One or more equations did not get rendered due to their size.

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.quote_eq_qqAnd_iff {L : Language} [L.Encodable] [L.LORDefinable] {φ : Proposition L} {p q : ℕ} : ⌜φ⌝ = qqAnd p q ↔ ∃ (φ₁ : Proposition L) (φ₂ : Proposition L), φ = φ₁ ⋏ φ₂ ∧ p = ⌜φ₁⌝ ∧ q = ⌜φ₂⌝

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.quote_weight {L : Language} [L.Encodable] [L.LORDefinable] {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (k : ℕ) : ⌜Semiformula.weight k⌝ = qqVerums ↑k

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.quote_padding {L : Language} [L.Encodable] [L.LORDefinable] {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (φ : Proposition L) (k : ℕ) : ⌜Semiformula.padding φ k⌝ = qqAnd ⌜φ⌝ (qqVerums ↑k)

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.Sentence.quote_padding {L : Language} [L.Encodable] [L.LORDefinable] {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (σ : Sentence L) (k : ℕ) : ⌜Semiformula.padding σ k⌝ = qqAnd ⌜σ⌝ (qqVerums ↑k)

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.quote_eq_qqVerums {L : Language} [L.Encodable] [L.LORDefinable] {χ : Proposition L} {s : ℕ} : ⌜χ⌝ = qqVerums s → χ = Semiformula.weight s

def FFL.FirstOrder.Theory.IsCraigAxiom {L : Language} [L.Encodable] {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] [L.Primcodable] (T : Theory L) [T.RE] : V → Prop

Equations

• One or more equations did not get rendered due to their size.

noncomputable def FFL.FirstOrder.Theory.craigCh {L : Language} [L.Encodable] [L.Primcodable] (T : Theory L) [T.RE] : 𝚫₁.Semisentence 1

Equations

• One or more equations did not get rendered due to their size.

instance FFL.FirstOrder.Arithmetic.Bootstrapping.Theory.IsCraigAxiom.defined {L : Language} [L.Encodable] {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] [L.Primcodable] {T : Theory L} [T.RE] : 𝚫₁-Predicate T.IsCraigAxiom via T.craigCh

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.Theory.isCraigAxiom_quote_iff {L : Language} [L.Encodable] [L.LORDefinable] [L.Primcodable] {T : Theory L} [T.RE] (φ : Proposition L) : T.IsCraigAxiom ⌜φ⌝ ↔ ∃ ρ ∈ T.craig, φ = Rewriting.emb ρ

theorem FFL.FirstOrder.Theory.mem_craig_codes_iff {L : Language} [L.Encodable] [L.LORDefinable] [L.Primcodable] {T : Theory L} [T.RE] (n : ℕ) : n ∈ Encodable.encode '' T.craig ↔ ∃ s < n, ∃ m < n, (Encodable.decode₂ (Sentence L) m).isSome = true ∧ n = Nat.pair 4 (Nat.pair m (Encodable.encode (Semiformula.weight s))) + 1 ∧ (Semiformula.Evalb ![s, m]) ↑T.reWitness

theorem FFL.FirstOrder.Theory.primrecPred_craig_core {L : Language} [L.Encodable] [L.Primcodable] {T : Theory L} [T.RE] : PrimrecPred fun (p : ℕ × ℕ × ℕ) => (Encodable.decode₂ (Sentence L) p.1).isSome = true ∧ p.2.1 = Nat.pair 4 (Nat.pair p.1 (Encodable.encode (Semiformula.weight p.2.2))) + 1 ∧ (Semiformula.Evalb ![p.2.2, p.1]) ↑T.reWitness

theorem FFL.FirstOrder.Theory.primrecPred_craig_codes {L : Language} [L.Encodable] [L.LORDefinable] [L.Primcodable] {T : Theory L} [T.RE] : PrimrecPred fun (x : ℕ) => x ∈ Encodable.encode '' T.craig

instance FFL.FirstOrder.Theory.instPrimrecCraig {L : Language} [L.Encodable] [L.LORDefinable] [L.Primcodable] {T : Theory L} [T.RE] : T.craig.Primrec

@[instance_reducible]

noncomputable instance FFL.FirstOrder.Theory.instΔ₁Craig {L : Language} [L.Encodable] [L.LORDefinable] [L.Primcodable] {T : Theory L} [T.RE] : T.craig.Δ₁

Equations

• FFL.FirstOrder.Theory.instΔ₁Craig = { ch := T.craigCh, mem_iff := ⋯, isDelta1 := ⋯ }

instance FFL.FirstOrder.Theory.instWeakerThanSentenceCraig {L : Language} [L.Encodable] [L.LORDefinable] [L.Primcodable] {T : Theory L} [T.RE] [L.DecidableEq] : T.craig ⪯ T

instance FFL.FirstOrder.Theory.instWeakerThanSentenceCraig_1 {L : Language} [L.Encodable] [L.LORDefinable] [L.Primcodable] {T : Theory L} [T.RE] [L.DecidableEq] : T ⪯ T.craig

instance FFL.FirstOrder.Theory.instEquivSentenceCraig {L : Language} [L.Encodable] [L.LORDefinable] [L.Primcodable] {T : Theory L} [T.RE] [L.DecidableEq] : T ≊ T.craig

instance FFL.FirstOrder.Theory.instConsistentSentenceCraig {L : Language} [L.Encodable] [L.LORDefinable] [L.Primcodable] {T : Theory L} [T.RE] [L.DecidableEq] [Entailment.Consistent T] : Entailment.Consistent T.craig