Representation theorem #

This file formalizes Representation Theorem.

In the first part, we prove one direction, that any partial recursive function is weakly representable in Q (rep_iff_of_mem). Moreover, in PA we prove the uniqueness (rep_unique) and the totality of primitive recursive functions (repPrim_total).
In the second part, we prove the converse direction, that any weakly representable relation is enumerable in ω-consistent extension of Q (enumerable_iff_weakly_representable), and any strongly representable relation is recursive in consistent extension of Q (recursive_iff_strongly_representable). Note that the ω-consistency condition in the former can be weakened to consistency, but to prove that we need Gödel's fixed point construction and Rosser's trick -- we will prove that in future.

source

@[irreducible]

def FirstOrder.Language.peano.rep {n : ℕ} :

Partrec n → peano.Formula (n + 1)

The representation formula of a partial recursive function.

Instances For

source

theorem FirstOrder.Language.peano.rep_const {n m : ℕ} :

rep (Partrec.const m) = #0 ≐ ofNat m

source

theorem FirstOrder.Language.peano.rep_succ :

rep Partrec.succ = #0 ≐ succ #1

source

theorem FirstOrder.Language.peano.rep_proj {n✝ : ℕ} {i : Fin n✝} :

rep (Partrec.proj i) = #0 ≐ #i.succ

source

theorem FirstOrder.Language.peano.rep_comp {k n : ℕ} {f : Partrec k} {g : Fin k → Partrec n} :

rep (f.comp g) = ∃^[k] ((⋀ (i : Fin k), (rep (g i))[#(i.castAdd' (n + 1)) ∷ᵥ Subst.shift 1 ∘ₛ Subst.shift k]ₚ) ⩑ (rep f)[#(Fin.addNat 0 k) ∷ᵥ Subst.embed k]ₚ)

source

theorem FirstOrder.Language.peano.rep_prec {a✝ : ℕ} {f : Partrec a✝} {g : Partrec (a✝ + 2)} :

rep (f.prec g) = ∃' (∃' ((rep f)[#0 ∷ᵥ Subst.shift 4]ₚ ⩑ beta (#0) (#1) 0) ⩑ ∀[≺ #2] ∃' ∃' ((rep g)[#0 ∷ᵥ #2 ∷ᵥ #1 ∷ᵥ Subst.shift 6]ₚ ⩑ beta #1 #3 #2 ⩑ beta (#0) (#3) (succ #2)) ⩑ beta #1 #0 #2 ⩑ ∀[≺ #0] (∃' ((rep f)[#0 ∷ᵥ Subst.shift 5]ₚ ⩑ nbeta (#0) (#1) 0) ⩒ ∃[≺ #3] ∃' ∃' ((rep g)[#0 ∷ᵥ #2 ∷ᵥ #1 ∷ᵥ Subst.shift 7]ₚ ⩑ beta #1 #3 #2 ⩑ nbeta (#0) (#3) (succ #2))))

source

theorem FirstOrder.Language.peano.rep_mu {a✝ : ℕ} {f : Partrec (a✝ + 1)} :

rep f.mu = ∃' (rep f)[≔ₛ succ #0]ₚ ⩑ ∀[≺ #0] (rep f)[0 ∷ᵥ #0 ∷ᵥ Subst.shift 2]ₚ

source

@[reducible, inline]

abbrev FirstOrder.Language.peano.repPrim {n : ℕ} (f : Primrec n) :

peano.Formula (n + 1)

Equations

FirstOrder.Language.peano.repPrim f = FirstOrder.Language.peano.rep (Partrec.ofPrim f)

Instances For

source

theorem FirstOrder.Language.peano.Sigma₁.rep {a✝ : ℕ} {f : Partrec a✝} :

Sigma₁ (peano.rep f)

source

def FirstOrder.Language.peano.repRel {n : ℕ} (f : Partrec n) :

peano.Formula n

Equations

FirstOrder.Language.peano.repRel f = ∃' (FirstOrder.Language.peano.rep f)[≔ₛ FirstOrder.Language.peano.succ #0]ₚ

Instances For

source

theorem FirstOrder.Language.peano.Sigma₁.repRel {a✝ : ℕ} {f : Partrec a✝} :

Sigma₁ (peano.repRel f)

source

theorem FirstOrder.Language.Proof.existsN_andN_of_andN_exists {n m : ℕ} {L : Language} {Γ : L.FormulaSet n} {v : Vec (L.Formula (n + 1)) m} :

Γ ⊢ (⋀ (i : Fin m), ∃' v i) ⇒ ∃^[m] (⋀ (i : Fin m), (v i)[#(i.castAdd' n) ∷ᵥ Subst.shift m]ₚ)

source

theorem FirstOrder.Language.Theory.Q.rep_iff_of_mem {n : ℕ} {v : Vec ℕ n} {m k : ℕ} {t : peano.Term k} {f : Partrec n} (h : m ∈ f.eval v) :

↑ᵀ^[k] Q ⊢ (peano.rep f)[t ∷ᵥ Subst.of fun (i : Fin n) => peano.ofNat (v i)]ₚ ⇔ t ≐ peano.ofNat m

source

theorem FirstOrder.Language.Theory.Q.repPrim_iff {n k : ℕ} {t : peano.Term k} {v : Vec ℕ n} {f : Primrec n} :

↑ᵀ^[k] Q ⊢ (peano.repPrim f)[t ∷ᵥ Subst.of fun (i : Fin n) => peano.ofNat (v i)]ₚ ⇔ t ≐ peano.ofNat (f.eval v)

source

theorem FirstOrder.Language.Theory.Q.rep_of_mem {n : ℕ} {v : Vec ℕ n} {m k : ℕ} {f : Partrec n} (h : m ∈ f.eval v) :

↑ᵀ^[k] Q ⊢ (peano.rep f)[peano.ofNat m ∷ᵥ Subst.of fun (i : Fin n) => peano.ofNat (v i)]ₚ

source

theorem FirstOrder.Language.Theory.Q.neg_rep_of_not_mem {n : ℕ} {v : Vec ℕ n} {m k : ℕ} {f : Partrec n} (hf : (f.eval v).Dom) (h : m ∉ f.eval v) :

↑ᵀ^[k] Q ⊢ ~ (peano.rep f)[peano.ofNat m ∷ᵥ Subst.of fun (i : Fin n) => peano.ofNat (v i)]ₚ

source

theorem FirstOrder.Language.Theory.Q.repRel_of_pos {n : ℕ} {v : Vec ℕ n} {k : ℕ} {f : Partrec n} :

0 < f.eval v → ↑ᵀ^[k] Q ⊢ (peano.repRel f)[Subst.of fun (i : Fin n) => peano.ofNat (v i)]ₚ

source

theorem FirstOrder.Language.Theory.Q.neg_repRel_of_zero {n : ℕ} {v : Vec ℕ n} {k : ℕ} {f : Partrec n} :

0 ∈ f.eval v → ↑ᵀ^[k] Q ⊢ ~ (peano.repRel f)[Subst.of fun (i : Fin n) => peano.ofNat (v i)]ₚ

source

theorem FirstOrder.Language.Theory.PA.rep_prec_iff {k : ℕ} {f : Partrec k} {g : Partrec (k + 2)} :

↑ᵀ^[k + 2] PA ⊢ peano.rep (f.prec g) ⇔ ∃' (∃' ((peano.rep f)[#0 ∷ᵥ Subst.shift 4]ₚ ⩑ peano.beta (#0) (#1) 0) ⩑ ∀[≺ #2] ∃' ∃' ((peano.rep g)[#0 ∷ᵥ #2 ∷ᵥ #1 ∷ᵥ Subst.shift 6]ₚ ⩑ peano.beta #1 #3 #2 ⩑ peano.beta (#0) (#3) (peano.succ #2)) ⩑ peano.beta #1 #0 #2)

source

theorem FirstOrder.Language.Theory.PA.rep_prec_iff' {n k : ℕ} {t₁ t₂ : peano.Term k} {σ : Vec (peano.Term k) n} {f : Partrec n} {g : Partrec (n + 2)} :

↑ᵀ^[k] PA ⊢ (peano.rep (f.prec g))[t₁ ∷ᵥ t₂ ∷ᵥ σ]ₚ ⇔ ∃' (∃' ((peano.rep f)[#0 ∷ᵥ σ ∘ₛ Subst.shift 2]ₚ ⩑ peano.beta (#0) (#1) 0) ⩑ ∀[≺ ↑ₜt₂] ∃' ∃' ((peano.rep g)[#0 ∷ᵥ #2 ∷ᵥ #1 ∷ᵥ σ ∘ₛ Subst.shift 4]ₚ ⩑ peano.beta #1 #3 #2 ⩑ peano.beta (#0) (#3) (peano.succ #2)) ⩑ peano.beta ↑ₜt₁ #0 ↑ₜt₂)

source

theorem FirstOrder.Language.Theory.PA.rep_prec_zero_iff {n k : ℕ} {t : peano.Term k} {σ : Vec (peano.Term k) n} {f : Partrec n} {g : Partrec (n + 2)} :

↑ᵀ^[k] PA ⊢ (peano.rep (f.prec g))[t ∷ᵥ 0 ∷ᵥ σ]ₚ ⇔ (peano.rep f)[t ∷ᵥ σ]ₚ

source

theorem FirstOrder.Language.Theory.PA.rep_prec_succ_iff {n k : ℕ} {t₁ t₂ : peano.Term k} {σ : Vec (peano.Term k) n} {f : Partrec n} {g : Partrec (n + 2)} :

↑ᵀ^[k] PA ⊢ (peano.rep (f.prec g))[t₁ ∷ᵥ peano.succ t₂ ∷ᵥ σ]ₚ ⇔ ∃' ((peano.rep (f.prec g))[#0 ∷ᵥ ↑ₜt₂ ∷ᵥ σ ∘ₛ Subst.shift 1]ₚ ⩑ (peano.rep g)[↑ₜt₁ ∷ᵥ ↑ₜt₂ ∷ᵥ #0 ∷ᵥ σ ∘ₛ Subst.shift 1]ₚ)

source

theorem FirstOrder.Language.Theory.PA.rep_unique {n k : ℕ} {t₁ : peano.Term k} {σ : Vec (peano.Term k) n} {t₂ : peano.Term k} {f : Partrec n} :

↑ᵀ^[k] PA ⊢ (peano.rep f)[t₁ ∷ᵥ σ]ₚ ⇒ (peano.rep f)[t₂ ∷ᵥ σ]ₚ ⇒ t₁ ≐ t₂

source

theorem FirstOrder.Language.Theory.PA.repPrim_total {n k : ℕ} {f : Primrec n} (σ : peano.Subst n k) :

↑ᵀ^[k] PA ⊢ ∃' (peano.repPrim f)[⇑ₛσ]ₚ

source

instance FirstOrder.Language.peano.instEncodableFunc {n : ℕ} :

Encodable (peano.Func n)

Equations

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

source

instance FirstOrder.Language.peano.instEncodableRel {n : ℕ} :

Encodable (peano.Rel n)

Equations

FirstOrder.Language.peano.instEncodableRel = inferInstanceAs (Encodable Empty)

source

instance FirstOrder.Language.peano.instPrimCodable :

peano.PrimCodable

Equations

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

source

instance FirstOrder.Language.peano.instHasConstEncodeZero :

peano.HasConstEncodeZero

source

def FirstOrder.Language.peano.zeroPR :

Primrec 0

Equations

FirstOrder.Language.peano.zeroPR = FirstOrder.Language.Term.funcPR.comp₃ Primrec.zero Primrec.zero Primrec.zero

Instances For

source

theorem FirstOrder.Language.peano.zeroPR_eval (n : ℕ) :

zeroPR.eval []ᵥ = Encodable.encode 0

source

def FirstOrder.Language.peano.succPR :

Primrec 1

Equations

FirstOrder.Language.peano.succPR = FirstOrder.Language.Term.funcPR.comp₃ (Primrec.const 1) Primrec.zero (Primrec.pair.comp₂ (Primrec.proj 1) Primrec.zero)

Instances For

source

theorem FirstOrder.Language.peano.succPR_eval {n : ℕ} {t : peano.Term n} :

succPR.eval [Encodable.encode t]ᵥ = Encodable.encode (succ t)

source

def FirstOrder.Language.peano.ofNatPR :

Primrec 1

Equations

FirstOrder.Language.peano.ofNatPR = FirstOrder.Language.peano.zeroPR.prec (FirstOrder.Language.peano.succPR.comp₁ (Primrec.proj 1))

Instances For

source

theorem FirstOrder.Language.peano.ofNatPR_eval {m : ℕ} (n : ℕ) :

ofNatPR.eval [m]ᵥ = Encodable.encode (ofNat m)

source

theorem FirstOrder.Language.Theory.Q.enumerable_iff_weakly_representable {α : Type u_1} [Encodable α] {s : Set α} {T : peano.Theory} [Recursive T] [Q ⊆ᵀ T] (h : peano.OmegaConsistent T) :

IsEnumerable s ↔ ∃ (p : peano.Formula 1), ∀ (x : α), x ∈ s ↔ T ⊢ p[[peano.ofEncode x]ᵥ ]ₚ

In an ω-consistent recursive theory T extending Q, a set is weakly representable in T iff it is enumerable. The ω-consistency condition can be weakened to consistency using Rosser's trick.

source

theorem FirstOrder.Language.Theory.Q.recursive_iff_strongly_representable {α : Type u_1} [Encodable α] {s : Set α} {T : peano.Theory} [Recursive T] [Q ⊆ᵀ T] (h : Consistent T) :

IsRecursive s ↔ ∃ (p : peano.Formula 1), (∀ x ∈ s, T ⊢ p[[peano.ofEncode x]ᵥ ]ₚ) ∧ ∀ x ∉ s, T ⊢ ~ p[[peano.ofEncode x]ᵥ ]ₚ

In a consistent theory T extending Q, a set is strongly representable in T iff it is recursive.

source

instance FirstOrder.Language.Theory.instRecursiveSentencePeanoQ :

Recursive Q

Equations

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

source

instance FirstOrder.Language.Theory.instRecursiveSentencePeanoPA :

Recursive PA

Equations

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

Documentation

MathematicalLogic.FirstOrder.Theories.Peano.Representation

Representation theorem #