def FirstOrder.Language.Term.varPR : Primrec 1

Equations

• FirstOrder.Language.Term.varPR = Primrec.mul.comp₂ (Primrec.const 2) (Primrec.proj 0)

theorem FirstOrder.Language.Term.varPR_eval {L : Language} [(n : ℕ) → Encodable (L.Func n)] {x n : ℕ} (h : x < n) : varPR.eval [x]ᵥ = Encodable.encode #⟨x, h⟩

def FirstOrder.Language.Term.funcPR : Primrec 3

Equations

• FirstOrder.Language.Term.funcPR = Primrec.succ.comp₁ (Primrec.mul.comp₂ (Primrec.const 2) (Primrec.pair.comp₂ (Primrec.proj 0) (Primrec.pair.comp₂ (Primrec.proj 1) (Primrec.proj 2))))

@[simp]

theorem FirstOrder.Language.Term.funcPR_eval {L : Language} [(n : ℕ) → Encodable (L.Func n)] {n m : ℕ} {f : L.Func m} {v : Vec (L.Term n) m} : funcPR.eval [m, Encodable.encode f, Encodable.encode v]ᵥ = Encodable.encode (f ⬝ᶠ v)

def FirstOrder.Language.Term.substPR : Primrec 2

Equations

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

theorem FirstOrder.Language.Term.substPR_eval {L : Language} [(n : ℕ) → Encodable (L.Func n)] {n m : ℕ} {t : L.Term n} {σ : L.Subst n m} : substPR.eval [Encodable.encode t, Encodable.encode σ]ᵥ = Encodable.encode t[σ]ₜ

def FirstOrder.Language.Subst.shiftPR : Primrec 1

Equations

• FirstOrder.Language.Subst.shiftPR = (Primrec.mul.comp₂ (Primrec.const 2) (Primrec.succ.comp₁ (Primrec.proj 0))).vmk

theorem FirstOrder.Language.Subst.shiftPR_eval {L : Language} [(n : ℕ) → Encodable (L.Func n)] {n : ℕ} : shiftPR.eval [n]ᵥ = Encodable.encode (shift 1)

def FirstOrder.Language.Term.shiftPR : Primrec 2

Equations

• FirstOrder.Language.Term.shiftPR = FirstOrder.Language.Term.substPR.comp₂ (Primrec.proj 1) (FirstOrder.Language.Subst.shiftPR.comp₁ (Primrec.proj 0))

theorem FirstOrder.Language.Term.shiftPR_eval {L : Language} [(n : ℕ) → Encodable (L.Func n)] {n : ℕ} {t : L.Term n} : shiftPR.eval [n, Encodable.encode t]ᵥ = Encodable.encode ↑ₜt

def FirstOrder.Language.Subst.liftPR : Primrec 3

Equations

• FirstOrder.Language.Subst.liftPR = Primrec.pair.comp₂ Primrec.zero (FirstOrder.Language.Term.shiftPR.swap.vmap.comp₃ (Primrec.proj 0) (Primrec.proj 2) (Primrec.proj 1))

theorem FirstOrder.Language.Subst.liftPR_eval {L : Language} [(n : ℕ) → Encodable (L.Func n)] {n m : ℕ} {σ : L.Subst n m} : liftPR.eval [n, m, Encodable.encode σ]ᵥ = Encodable.encode ⇑ₛσ

def FirstOrder.Language.Subst.liftNPR : Primrec 4

Equations

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

theorem FirstOrder.Language.Subst.liftNPR_eval {L : Language} [(n : ℕ) → Encodable (L.Func n)] {n m k : ℕ} {σ : L.Subst n m} : liftNPR.eval [k, n, m, Encodable.encode σ]ᵥ = Encodable.encode (⇑ₛ^[k] σ)

def FirstOrder.Language.Subst.singlePR : Primrec 2

Equations

• FirstOrder.Language.Subst.singlePR = Primrec.pair.comp₂ (Primrec.proj 1) ((Primrec.mul.comp₂ (Primrec.const 2) (Primrec.proj 0)).vmk.comp₁ (Primrec.proj 0))

theorem FirstOrder.Language.Subst.singlePR_eval {L : Language} [(n : ℕ) → Encodable (L.Func n)] {n : ℕ} {t : L.Term n} : singlePR.eval [n, Encodable.encode t]ᵥ = Encodable.encode (↦ₛ t)

def FirstOrder.Language.Subst.assignPR : Primrec 2

Equations

• FirstOrder.Language.Subst.assignPR = Primrec.pair.comp₂ (Primrec.proj 1) ((Primrec.mul.comp₂ (Primrec.const 2) (Primrec.succ.comp₁ (Primrec.proj 0))).vmk.comp₁ (Primrec.proj 0))

theorem FirstOrder.Language.Subst.assignPR_eval {L : Language} [(n : ℕ) → Encodable (L.Func n)] {n : ℕ} {t : L.Term (n + 1)} : assignPR.eval [n, Encodable.encode t]ᵥ = Encodable.encode (≔ₛ t)

def FirstOrder.Language.Formula.relPR : Primrec 3

Equations

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

@[simp]

theorem FirstOrder.Language.Formula.relPR_eval {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] {n m : ℕ} {r : L.Rel m} {v : Vec (L.Term n) m} : relPR.eval [m, Encodable.encode r, Encodable.encode v]ᵥ = Encodable.encode (r ⬝ʳ v)

def FirstOrder.Language.Formula.eqPR : Primrec 2

Equations

• FirstOrder.Language.Formula.eqPR = Primrec.add.comp₂ (Primrec.mul.comp₂ (Primrec.const 4) (Primrec.pair.comp₂ (Primrec.proj 0) (Primrec.proj 1))) (Primrec.const 2)

@[simp]

theorem FirstOrder.Language.Formula.eqPR_eval {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] {n : ℕ} {t₁ t₂ : L.Term n} : eqPR.eval [Encodable.encode t₁, Encodable.encode t₂]ᵥ = Encodable.encode (t₁ ≐ t₂)

def FirstOrder.Language.Formula.impPR : Primrec 2

Equations

• FirstOrder.Language.Formula.impPR = Primrec.add.comp₂ (Primrec.mul.comp₂ (Primrec.const 4) (Primrec.pair.comp₂ (Primrec.proj 0) (Primrec.proj 1))) (Primrec.const 3)

@[simp]

theorem FirstOrder.Language.Formula.impPR_eval {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] {n : ℕ} {p q : L.Formula n} : impPR.eval [Encodable.encode p, Encodable.encode q]ᵥ = Encodable.encode (p ⇒ q)

theorem FirstOrder.Language.Formula.eq_impPR_eval {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] {n a b : ℕ} {p : L.Formula n} : Encodable.encode p = impPR.eval [a, b]ᵥ → ∃ (q : L.Formula n) (r : L.Formula n), p = q ⇒ r ∧ a = Encodable.encode q ∧ b = Encodable.encode r

def FirstOrder.Language.Formula.isImpPR : Primrec 1

Equations

• FirstOrder.Language.Formula.isImpPR = (Primrec.mod.comp₂ (Primrec.proj 0) (Primrec.const 4)).eq (Primrec.const 3)

theorem FirstOrder.Language.Formula.isImpPR_eval_pos_iff {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] {n : ℕ} {p : L.Formula n} : 0 < isImpPR.eval [Encodable.encode p]ᵥ ↔ ∃ (q : L.Formula n) (r : L.Formula n), p = q ⇒ r

def FirstOrder.Language.Formula.impLeftPR : Primrec 1

Equations

• FirstOrder.Language.Formula.impLeftPR = Primrec.fst.comp₁ (Primrec.div.comp₂ (Primrec.proj 0) (Primrec.const 4))

@[simp]

theorem FirstOrder.Language.Formula.impLeftPR_eval {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] {n : ℕ} {p q : L.Formula n} : impLeftPR.eval [Encodable.encode (p ⇒ q)]ᵥ = Encodable.encode p

def FirstOrder.Language.Formula.impRightPR : Primrec 1

Equations

• FirstOrder.Language.Formula.impRightPR = Primrec.snd.comp₁ (Primrec.div.comp₂ (Primrec.proj 0) (Primrec.const 4))

@[simp]

theorem FirstOrder.Language.Formula.impRightPR_eval {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] {n : ℕ} {p q : L.Formula n} : impRightPR.eval [Encodable.encode (p ⇒ q)]ᵥ = Encodable.encode q

def FirstOrder.Language.Formula.negPR : Primrec 1

Equations

• FirstOrder.Language.Formula.negPR = FirstOrder.Language.Formula.impPR.comp₂ (Primrec.proj 0) Primrec.zero

@[simp]

theorem FirstOrder.Language.Formula.negPR_eval {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] {n : ℕ} {p : L.Formula n} : negPR.eval [Encodable.encode p]ᵥ = Encodable.encode (~ p)

def FirstOrder.Language.Formula.allPR : Primrec 1

Equations

• FirstOrder.Language.Formula.allPR = Primrec.add.comp₂ (Primrec.mul.comp₂ (Primrec.const 4) (Primrec.proj 0)) (Primrec.const 4)

@[simp]

theorem FirstOrder.Language.Formula.allPR_eval {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] {n : ℕ} {p : L.Formula (n + 1)} : allPR.eval [Encodable.encode p]ᵥ = Encodable.encode (∀' p)

def FirstOrder.Language.Formula.andPR : Primrec 2

Equations

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

@[simp]

theorem FirstOrder.Language.Formula.andPR_eval {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] {n : ℕ} {p q : L.Formula n} : andPR.eval [Encodable.encode p, Encodable.encode q]ᵥ = Encodable.encode (p ⩑ q)

def FirstOrder.Language.Formula.andNPR : Primrec 2

Equations

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

@[simp]

theorem FirstOrder.Language.Formula.andNPR_eval {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] {n m : ℕ} {v : Vec (L.Formula n) m} : andNPR.eval [m, Encodable.encode v]ᵥ = Encodable.encode (⋀ (i : Fin m), v i)

def FirstOrder.Language.Formula.allsPR : Primrec 2

Equations

• FirstOrder.Language.Formula.allsPR = FirstOrder.Language.Formula.allPR.iterate

@[simp]

theorem FirstOrder.Language.Formula.allsPR_eval {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] {n : ℕ} {p : L.Formula n} : allsPR.eval [n, Encodable.encode p]ᵥ = Encodable.encode (∀* p)

def FirstOrder.Language.Formula.depth {L : Language} {n : ℕ} : L.Formula n → ℕ

Equations

• (p.imp q).depth = max p.depth q.depth
• (∀' p).depth = p.depth + 1
• x✝.depth = 0

def FirstOrder.Language.Formula.depthPR : Primrec 1

Equations

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

theorem FirstOrder.Language.Formula.depthPR_eval {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] {n : ℕ} {p : L.Formula n} : depthPR.eval [Encodable.encode p]ᵥ = p.depth

def FirstOrder.Language.Formula.substPR : Primrec 4

Equations

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

theorem FirstOrder.Language.Formula.substPR_eval {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] {n m : ℕ} {p : L.Formula n} {σ : L.Subst n m} : substPR.eval [n, m, Encodable.encode p, Encodable.encode σ]ᵥ = Encodable.encode p[σ]ₚ

def FirstOrder.Language.Formula.shiftPR : Primrec 2

Equations

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

theorem FirstOrder.Language.Formula.shiftPR_eval {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] {n : ℕ} {p : L.Formula n} : shiftPR.eval [n, Encodable.encode p]ᵥ = Encodable.encode ↑ₚp

def FirstOrder.Language.Formula.substSinglePR : Primrec 3

Equations

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

theorem FirstOrder.Language.Formula.substSinglePR_eval {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] {n : ℕ} {p : L.Formula (n + 1)} {t : L.Term n} : substSinglePR.eval [n, Encodable.encode p, Encodable.encode t]ᵥ = Encodable.encode p[↦ₛ t]ₚ

def FirstOrder.Language.Formula.substAssignPR : Primrec 3

Equations

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

theorem FirstOrder.Language.Formula.substAssignPR_eval {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] {n : ℕ} {p : L.Formula (n + 1)} {t : L.Term (n + 1)} : substAssignPR.eval [n, Encodable.encode p, Encodable.encode t]ᵥ = Encodable.encode p[≔ₛ t]ₚ

class FirstOrder.Language.PrimCodable (L : Language) [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] : Type

• isFuncPR : Primrec 2
• isFuncPR_eval_pos_iff {n m : ℕ} : 0 < (isFuncPR L).eval [n, m]ᵥ ↔ ∃ (f : L.Func n), m = Encodable.encode f
• isRelPR : Primrec 2
• isRelPR_eval_pos_iff {n m : ℕ} : 0 < (isRelPR L).eval [n, m]ᵥ ↔ ∃ (r : L.Rel n), m = Encodable.encode r

def FirstOrder.Language.isTermPR (L : Language) [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] [L.PrimCodable] : Primrec 2

Equations

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

theorem FirstOrder.Language.isTermPR_eval_pos_iff (L : Language) [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] [L.PrimCodable] {n m : ℕ} : 0 < L.isTermPR.eval [n, m]ᵥ ↔ ∃ (t : L.Term n), m = Encodable.encode t

def FirstOrder.Language.isFormulaPR (L : Language) [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] [L.PrimCodable] : Primrec 2

Equations

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

theorem FirstOrder.Language.isFormulaPR_eval_pos_iff (L : Language) [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] [L.PrimCodable] {n m : ℕ} : 0 < L.isFormulaPR.eval [n, m]ᵥ ↔ ∃ (p : L.Formula n), m = Encodable.encode p

def FirstOrder.Language.isSentencePR (L : Language) [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] [L.PrimCodable] : Primrec 1

Equations

• L.isSentencePR = L.isFormulaPR.comp₂ (Primrec.const 0) (Primrec.proj 0)

theorem FirstOrder.Language.isSentencePR_eval_pos_iff (L : Language) [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] [L.PrimCodable] {k : ℕ} : 0 < L.isSentencePR.eval [k]ᵥ ↔ ∃ (p : L.Sentence), k = Encodable.encode p

def FirstOrder.Language.isAxiomPR (L : Language) [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] [L.PrimCodable] : Primrec 2

Equations

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

theorem FirstOrder.Language.isAxiomPR_eval_pos_iff (L : Language) [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] [L.PrimCodable] {n : ℕ} [L.HasConstEncodeZero] {p : L.Formula n} : 0 < L.isAxiomPR.eval [n, Encodable.encode p]ᵥ ↔ p ∈ L.Axiom

def FirstOrder.Language.isProofOfPR {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] [L.PrimCodable] (T : L.Theory) [Recursive T] : Partrec 1

isProofOf(n) returns m + 1 if n encodes a proof of the formula encoded by m; returns 0 if n does not encode any proof.

Equations

• FirstOrder.Language.isProofOfPR T = (FirstOrder.Language.isProofOfPR.inner T).covrec

def FirstOrder.Language.isProofOfPR.inner {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] [L.PrimCodable] (T : L.Theory) [Recursive T] : Partrec (0 + 2)

Equations

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

theorem FirstOrder.Language.isProofOfPR.inner_dom {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] [L.PrimCodable] {T : L.Theory} [Recursive T] (n ih : ℕ) : ((inner T).eval [n, ih]ᵥ).Dom

theorem FirstOrder.Language.isProofOfPR_dom {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] [L.PrimCodable] {T : L.Theory} [Recursive T] {n : ℕ} : ((isProofOfPR T).eval [n]ᵥ).Dom

theorem FirstOrder.Language.isProofOfPR_eval_pos_of_proof {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] [L.PrimCodable] {T : L.Theory} [Recursive T] {p : L.Formula 0} [L.HasConstEncodeZero] : T ⊢ p → ∃ (n : ℕ), Encodable.encode p + 1 ∈ (isProofOfPR T).eval [n]ᵥ

theorem FirstOrder.Language.proof_of_isProofOfPR_eval_pos {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] [L.PrimCodable] {T : L.Theory} [Recursive T] {n m : ℕ} [L.HasConstEncodeZero] : m + 1 ∈ (isProofOfPR T).eval [n]ᵥ → ∃ (p : L.Formula 0), m = Encodable.encode p ∧ T ⊢ p

theorem FirstOrder.Language.provable_iff_isProofOfPR_eval {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] [L.PrimCodable] {T : L.Theory} [Recursive T] {p : L.Formula 0} [L.HasConstEncodeZero] : T ⊢ p ↔ ∃ (n : ℕ), Encodable.encode p + 1 ∈ (isProofOfPR T).eval [n]ᵥ

def FirstOrder.Language.isProofPR {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] [L.PrimCodable] (T : L.Theory) [Recursive T] : Partrec 2

Equations

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

theorem FirstOrder.Language.isProofPR_dom {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] [L.PrimCodable] {T : L.Theory} [Recursive T] {n : ℕ} {p : L.Sentence} : ((isProofPR T).eval [n, Encodable.encode p]ᵥ).Dom

theorem FirstOrder.Language.provable_iff_isProofPR_eval_pos {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] [L.PrimCodable] {T : L.Theory} [Recursive T] {p : L.Formula 0} [L.HasConstEncodeZero] : T ⊢ p ↔ ∃ (n : ℕ), 0 < (isProofPR T).eval [n, Encodable.encode p]ᵥ

theorem FirstOrder.Language.Theory.theorems_enumerable_of_recursive {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] [L.PrimCodable] {T : L.Theory} [Recursive T] [L.HasConstEncodeZero] : IsEnumerable T.theorems

Theorems of a recursive theory is RE.

theorem FirstOrder.Language.Complete.theorems_recursive_of_recursive {L : Language} [(n : ℕ) → Encodable (L.Func n)] [(n : ℕ) → Encodable (L.Rel n)] [L.PrimCodable] {T : L.Theory} [Recursive T] [L.HasConstEncodeZero] (h : Complete T) : IsRecursive T.theorems

Theorems of a complete recursive theory is also recursive.