Supporting results for pointwise provable equality.

Craig's trick

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

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

theorem PointwiseComposition.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 PointwiseComposition.FFL.FirstOrder.Semiformula.le_encode_weight {L : Language} {ξ : Type u_1} {n : ℕ} [L.Encodable] [Encodable ξ] (k : ℕ) : k ≤ Encodable.encode (weight k)

theorem PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.FFL.FirstOrder.Semiformula.primrec_encode_weight {L : Language} {ξ : Type u_1} {n : ℕ} [L.Encodable] [Encodable ξ] : Primrec fun (k : ℕ) => Encodable.encode (weight k)

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

The re Ch construction in FFL.FirstOrder.Theory.

Equations

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

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

The re Witness construction in FFL.FirstOrder.Theory.

Equations

• T.reWitness = ⋯.choose

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

@[simp]

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

theorem PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.FFL.FirstOrder.Theory.craig {L : Language} [L.Encodable] (T : Theory L) [L.LORDefinable] : Theory L

The craig construction in FFL.FirstOrder.Theory.

Equations

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

theorem PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.quote_eq_qqVerums {L : Language} [L.Encodable] [L.LORDefinable] {χ : Proposition L} {s : ℕ} : ⌜χ⌝ = qqVerums s → χ = Semiformula.weight s

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

The Is Craig Axiom construction in FFL.FirstOrder.Theory.

Equations

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

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

The craig Ch construction in FFL.FirstOrder.Theory.

Equations

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

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.Theory.IsCraigAxiom.defined {L : Language} [L.Encodable] {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {T : Theory L} : ∆₁-Predicate T.IsCraigAxiom via T.craigCh

theorem PointwiseComposition.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 PointwiseComposition.FFL.FirstOrder.Theory.mem_craig_codes_iff {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} (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 PointwiseComposition.FFL.FirstOrder.Theory.primrecPred_craig_core {L : Language} [L.Encodable] [L.Primcodable] {T : Theory L} : 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 PointwiseComposition.FFL.FirstOrder.Theory.primrecPred_craig_codes {L : Language} [L.Encodable] [L.LORDefinable] [L.Primcodable] {T : Theory L} : PrimrecPred fun (x : ℕ) => x ∈ Encodable.encode '' T.craig

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

@[instance_reducible]

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

Equations

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

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

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

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

instance PointwiseComposition.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