Documentation

Foundation.FirstOrder.Arithmetic.Bootstrapping.Syntax.Term.Coding

source
noncomputable def FFL.FirstOrder.Semiterm.typedQuote (V : Type u_1) [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} :
SyntacticSemiterm L n → Arithmetic.Bootstrapping.Semiterm V L n
Equations
Instances For
    source
    @[instance_reducible]
    noncomputable instance FFL.FirstOrder.Semiterm.instGödelQuoteSyntacticSemitermSemiterm (V : Type u_1) [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} :
    GödelQuote (SyntacticSemiterm L n) (Arithmetic.Bootstrapping.Semiterm V L n)
    Equations
    source
    @[simp]
    theorem FFL.FirstOrder.Semiterm.typed_quote_bvar {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (x : Fin n) :
    ⌜bvar x⌝ = Arithmetic.Bootstrapping.Semiterm.bvar x
    source
    @[simp]
    theorem FFL.FirstOrder.Semiterm.typed_quote_fvar {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (x : ℕ) :
    ⌜fvar x⌝ = Arithmetic.Bootstrapping.Semiterm.fvar ↑x
    source
    @[simp]
    theorem FFL.FirstOrder.Semiterm.typed_quote_func {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n k : ℕ} (f : L.Func k) (v : Fin k → SyntacticSemiterm L n) :
    ⌜func f v⌝ = Arithmetic.Bootstrapping.Semiterm.func f fun (i : Fin k) => ⌜v i⌝
    source
    @[simp]
    theorem FFL.FirstOrder.Semiterm.typed_quote_shift {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (t : SyntacticSemiterm L n) :
    ⌜Rew.shift t⌝ = ⌜t⌝.shift
    source
    @[simp]
    theorem FFL.FirstOrder.Semiterm.typed_quote_bShift {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (t : SyntacticSemiterm L n) :
    ⌜Rew.bShift t⌝ = ⌜t⌝.bShift
    source
    @[simp]
    theorem FFL.FirstOrder.Semiterm.typed_quote_substs {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n m : ℕ} (t : SyntacticSemiterm L n) (w : Fin n → SyntacticSemiterm L m) :
    ⌜(Rew.subst w) t⌝ = Arithmetic.Bootstrapping.Semiterm.subst (fun (i : Fin n) => ⌜w i⌝) ⌜t⌝
    source
    @[simp]
    theorem FFL.FirstOrder.Semiterm.typed_quote_add {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {n : ℕ} (t u : SyntacticSemiterm ℒₒᵣ n) :
    ⌜‘(!!t + !!u)’⌝ = ⌜t⌝ + ⌜u⌝
    source
    @[simp]
    theorem FFL.FirstOrder.Semiterm.typed_quote_mul {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {n : ℕ} (t u : SyntacticSemiterm ℒₒᵣ n) :
    ⌜‘(!!t * !!u)’⌝ = ⌜t⌝ * ⌜u⌝
    source
    theorem FFL.FirstOrder.Semiterm.typed_quote_numeral_eq_numeral_one {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {n : ℕ} :
    ⌜↑1⌝ = Arithmetic.Bootstrapping.Arithmetic.typedNumeral 1
    source
    @[simp]
    theorem FFL.FirstOrder.Semiterm.typed_quote_numeral_eq_numeral {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {n : ℕ} (k : ℕ) :
    ⌜↑k⌝ = Arithmetic.Bootstrapping.Arithmetic.typedNumeral ↑k
    source
    theorem FFL.FirstOrder.Semiterm.typed_quote_inj {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} {t u : SyntacticSemiterm L n} :
    ⌜t⌝ = ⌜u⌝ → t = u
    source
    @[simp]
    theorem FFL.FirstOrder.Semiterm.typed_quote_inj_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} {t u : SyntacticSemiterm L n} :
    ⌜t⌝ = ⌜u⌝ ↔ t = u
    source
    @[instance_reducible]
    noncomputable instance FFL.FirstOrder.Semiterm.instGödelQuoteSyntacticSemiterm {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} :
    GödelQuote (SyntacticSemiterm L n) V
    Equations
    source
    theorem FFL.FirstOrder.Semiterm.quote_def {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (t : SyntacticSemiterm L n) :
    ⌜t⌝ = ⌜t⌝.val
    source
    theorem FFL.FirstOrder.Semiterm.quote_eq_encode {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (t : SyntacticSemiterm L n) :
    ⌜t⌝ = ↑(Encodable.encode t)
    source
    theorem FFL.FirstOrder.Semiterm.quote_eq_encode' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n k : ℕ} (v : Fin k → Semiterm L ℕ n) :
    (Arithmetic.Bootstrapping.SemitermVec.val fun (i : Fin k) => ⌜v i⌝) = ↑(Matrix.vecToNat fun (i : Fin k) => Encodable.encode (v i))
    source
    theorem FFL.FirstOrder.Semiterm.quote_eq_encode_standard {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (t : SyntacticSemiterm L n) :
    ⌜t⌝ = Encodable.encode t
    source
    theorem FFL.FirstOrder.Semiterm.coe_quote_eq_quote {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (t : SyntacticSemiterm L n) :
    ↑⌜t⌝ = ⌜t⌝
    source
    theorem FFL.FirstOrder.Semiterm.coe_quote_eq_quote' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (t : SyntacticSemiterm L n) :
    ↑⌜t⌝.val = ⌜t⌝.val
    source
    @[simp]
    theorem FFL.FirstOrder.Semiterm.quote_bvar {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (x : Fin n) :
    ⌜bvar x⌝ = Arithmetic.Bootstrapping.qqBvar ↑↑x
    source
    @[simp]
    theorem FFL.FirstOrder.Semiterm.quote_fvar {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (x : ℕ) :
    ⌜fvar x⌝ = Arithmetic.Bootstrapping.qqFvar ↑x
    source
    @[simp]
    theorem FFL.FirstOrder.Semiterm.quote_func {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n k : ℕ} (f : L.Func k) (v : Fin k → SyntacticSemiterm L n) :
    ⌜func f v⌝ = Arithmetic.Bootstrapping.qqFunc ↑k ⌜f⌝ (Arithmetic.Bootstrapping.SemitermVec.val fun (i : Fin k) => ⌜v i⌝)
    source
    @[instance_reducible]
    noncomputable instance FFL.FirstOrder.Semiterm.instGödelQuoteClosedSemitermSemiterm (V : Type u_1) [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} :
    GödelQuote (ClosedSemiterm L n) (Arithmetic.Bootstrapping.Semiterm V L n)
    Equations
    source
    theorem FFL.FirstOrder.Semiterm.empty_typed_quote_def {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (t : ClosedSemiterm L n) :
    ⌜t⌝ = ⌜Rew.emb t⌝
    source
    @[simp]
    theorem FFL.FirstOrder.Semiterm.empty_typed_quote_bvar {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (x : Fin n) :
    ⌜bvar x⌝ = Arithmetic.Bootstrapping.Semiterm.bvar x
    source
    @[simp]
    theorem FFL.FirstOrder.Semiterm.empty_typed_quote_func {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n k : ℕ} (f : L.Func k) (v : Fin k → ClosedSemiterm L n) :
    ⌜func f v⌝ = Arithmetic.Bootstrapping.Semiterm.func f fun (i : Fin k) => ⌜v i⌝
    source
    @[simp]
    theorem FFL.FirstOrder.Semiterm.empty_typed_quote_add {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {n : ℕ} (t u : ClosedSemiterm ℒₒᵣ n) :
    ⌜‘(!!t + !!u)’⌝ = ⌜t⌝ + ⌜u⌝
    source
    @[simp]
    theorem FFL.FirstOrder.Semiterm.empty_typed_quote_mul {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {n : ℕ} (t u : ClosedSemiterm ℒₒᵣ n) :
    ⌜‘(!!t * !!u)’⌝ = ⌜t⌝ * ⌜u⌝
    source
    @[simp]
    theorem FFL.FirstOrder.Semiterm.empty_typed_quote_numeral_eq_numeral {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {n : ℕ} (k : ℕ) :
    ⌜↑k⌝ = Arithmetic.Bootstrapping.Arithmetic.typedNumeral ↑k
    source
    @[instance_reducible]
    noncomputable instance FFL.FirstOrder.Semiterm.instGödelQuoteClosedSemiterm {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} :
    GödelQuote (ClosedSemiterm L n) V
    Equations
    source
    theorem FFL.FirstOrder.Semiterm.empty_quote_def {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (t : ClosedSemiterm L n) :
    ⌜t⌝ = ⌜Rew.emb t⌝
    source
    theorem FFL.FirstOrder.Semiterm.empty_quote_eq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (t : ClosedSemiterm L n) :
    ⌜t⌝ = ⌜t⌝.val
    source
    theorem FFL.FirstOrder.Semiterm.empty_quote_eq_encode {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (t : ClosedSemiterm L n) :
    ⌜t⌝ = ↑(Encodable.encode t)
    source
    @[simp]
    theorem FFL.FirstOrder.Semiterm.coe_quote {L : Language} [L.Encodable] [L.LORDefinable] {m : ℕ} {ξ : Type u_2} {n : ℕ} (t : SyntacticSemiterm L n) :
    ↑⌜t⌝ = ⌜t⌝
    source
    @[simp]
    theorem FFL.FirstOrder.Semiterm.coe_empty_quote {L : Language} [L.Encodable] [L.LORDefinable] {m : ℕ} {ξ : Type u_2} {n : ℕ} (t : ClosedSemiterm L n) :
    ↑⌜t⌝ = ⌜t⌝
    source
    theorem FFL.FirstOrder.Arithmetic.Bootstrapping.mem_iff_mem_bitIndices {x s : ℕ} :
    x ∈ s ↔ x ∈ s.bitIndices
    source
    theorem FFL.FirstOrder.Arithmetic.Bootstrapping.nat_mem_iff {x s : ℕ} :
    x ∈ s ↔ s / 2 ^ x % 2 = 1
    source
    theorem FFL.FirstOrder.Arithmetic.Bootstrapping.nat_insert_eq (x s : ℕ) :
    insert x s = if s / 2 ^ x % 2 = 1 then s else s + 2 ^ x
    source
    theorem FFL.FirstOrder.Arithmetic.Bootstrapping.IsSemiterm.sound {L : Language} [L.Encodable] [L.LORDefinable] {n t : ℕ} (ht : IsSemiterm L n t) :
    ∃ (T : SyntacticSemiterm L n), ⌜T⌝ = t