Arithmetization.ISigmaOne.Metamath.Coding

source

theorem LO.FirstOrder.Semiterm.encode_eq_toNat {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] {ξ : Type u_1} [Encodable ξ] {n : ℕ} (t : LO.FirstOrder.Semiterm L ξ n) :

Encodable.encode t = t.toNat

source

theorem LO.FirstOrder.Semiterm.toNat_func {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] {ξ : Type u_1} [Encodable ξ] {n : ℕ} {k : ℕ} (f : L.Func k) (v : Fin k → LO.FirstOrder.Semiterm L ξ n) :

(LO.FirstOrder.Semiterm.func f v).toNat = Nat.pair 2 (Nat.pair k (Nat.pair (Encodable.encode f) (Matrix.vecToNat fun (i : Fin k) => (v i).toNat))) + 1

source

@[simp]

theorem LO.FirstOrder.Semiterm.encode_emb {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] {ξ : Type u_1} [Encodable ξ] {n : ℕ} (t : LO.FirstOrder.Semiterm L Empty n) :

Encodable.encode (LO.FirstOrder.Rew.emb t) = Encodable.encode t

source

theorem LO.FirstOrder.Semiformula.encode_eq_toNat {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {ξ : Type u_1} [Encodable ξ] {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) :

Encodable.encode p = p.toNat

source

@[simp]

theorem LO.FirstOrder.Semiformula.encode_emb {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {ξ : Type u_1} [Encodable ξ] {n : ℕ} (p : LO.FirstOrder.Semisentence L n) :

Encodable.encode (LO.FirstOrder.Rew.emb.hom p) = Encodable.encode p

source

theorem LO.FirstOrder.Semiformula.Operator.lt_eq {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} [L.LT] (t : LO.FirstOrder.Semiterm L ξ n) (u : LO.FirstOrder.Semiterm L ξ n) :

(“!!t < !!u”) = LO.FirstOrder.Semiformula.rel op(<) ![t, u]

source

theorem LO.Arith.nat_cast_empty {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :

↑∅ = ∅

source

def LO.Arith.finArrowToVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} :

(Fin k → V) → V

Equations

LO.Arith.finArrowToVec x_2 = 0
LO.Arith.finArrowToVec v = cons (v 0) (LO.Arith.finArrowToVec fun (x : Fin k) => v x.succ)

source

instance LO.Arith.instGoedelQuoteForallFin_arithmetization {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} :

LO.GoedelQuote (Fin k → V) V

quasi-quotation rather than Godel quotation

Equations

LO.Arith.instGoedelQuoteForallFin_arithmetization = { quote := LO.Arith.finArrowToVec }

source

theorem LO.Arith.quote_matrix_def {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} (v : Fin k → V) :

⌜v⌝ = LO.Arith.finArrowToVec v

source

@[simp]

theorem LO.Arith.quote_nil {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :

⌜![]⌝ = 0

source

@[simp]

theorem LO.Arith.quote_singleton {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) :

⌜![a]⌝ = ?[a]

source

@[simp]

theorem LO.Arith.quote_doubleton {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) (b : V) :

⌜![a, b]⌝ = ?[a, b]

source

@[simp]

theorem LO.Arith.quote_matrix_empty {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 0 → V) :

⌜v⌝ = 0

source

theorem LO.Arith.quote_matrix_succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} (v : Fin (k + 1) → V) :

⌜v⌝ = cons (v 0) ⌜fun (i : Fin k) => v i.succ⌝

source

@[simp]

theorem LO.Arith.quote_cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} (v : Fin k → V) (a : V) :

⌜a :> v⌝ = cons a ⌜v⌝

source

@[simp]

theorem LO.Arith.quote_matrix_inj {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} (v : Fin k → V) (w : Fin k → V) :

⌜v⌝ = ⌜w⌝ ↔ v = w

source

@[simp]

theorem LO.Arith.quote_lh {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} (v : Fin k → V) :

LO.Arith.len ⌜v⌝ = ↑k

source

@[simp]

theorem LO.Arith.quote_nth_fin {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} (v : Fin k → V) (i : Fin k) :

LO.Arith.nth ⌜v⌝ ↑↑i = v i

source

@[simp]

theorem LO.Arith.quote_matrix_absolute {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} (v : Fin k → ℕ) :

↑⌜v⌝ = ⌜fun (i : Fin k) => ↑(v i)⌝

source

theorem LO.Arith.quote_eq_vecToNat {k : ℕ} (v : Fin k → ℕ) :

⌜v⌝ = Matrix.vecToNat v

source

instance LO.Arith.instGoedelQuote_arithmetization {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {α : Type u_2} [Encodable α] :

LO.GoedelQuote α V

Equations

LO.Arith.instGoedelQuote_arithmetization = { quote := fun (x : α) => ↑(Encodable.encode x) }

source

theorem LO.Arith.quote_eq_coe_encode {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {α : Type u_2} [Encodable α] (x : α) :

⌜x⌝ = ↑(Encodable.encode x)

source

@[simp]

theorem LO.Arith.quote_nat {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (n : ℕ) :

⌜n⌝ = ↑n

source

theorem LO.Arith.coe_quote {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {α : Type u_2} [Encodable α] (x : α) :

↑⌜x⌝ = ⌜x⌝

source

@[simp]

theorem LO.Arith.quote_quote {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {α : Type u_2} [Encodable α] (x : α) :

⌜⌜x⌝⌝ = ⌜x⌝

source

theorem LO.Arith.quote_eq_encode {α : Type u_2} [Encodable α] (x : α) :

⌜x⌝ = Encodable.encode x

source

@[simp]

theorem LO.Arith.val_quote {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {α : Type u_2} [Encodable α] {ξ : Type u_3} {n : ℕ} {e : Fin n → V} {ε : ξ → V} (x : α) :

LO.FirstOrder.Semiterm.valm V e ε ⌜x⌝ = ⌜x⌝

source

theorem LO.Arith.numeral_quote {α : Type u_2} [Encodable α] {ξ : Type u_3} {n : ℕ} (x : α) :

LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ℒₒᵣ ⌜x⌝) = ⌜x⌝

source

@[simp]

theorem LO.Arith.quote_inj_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {α : Type u_2} [Encodable α] {x : α} {y : α} :

⌜x⌝ = ⌜y⌝ ↔ x = y

source

theorem LO.FirstOrder.Semiterm.quote_eq_toNat (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] {n : ℕ} (t : LO.FirstOrder.SyntacticSemiterm L n) :

⌜t⌝ = ↑(LO.FirstOrder.Semiterm.toNat t)

source

@[simp]

theorem LO.FirstOrder.Semiterm.quote_bvar (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] {n : ℕ} (z : Fin n) :

⌜LO.FirstOrder.Semiterm.bvar z⌝ = LO.Arith.qqBvar ↑↑z

source

@[simp]

theorem LO.FirstOrder.Semiterm.quote_fvar (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] {n : ℕ} (x : ℕ) :

⌜LO.FirstOrder.Semiterm.fvar x⌝ = LO.Arith.qqFvar ↑x

source

theorem LO.FirstOrder.Semiterm.quote_func (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] {n : ℕ} {k : ℕ} (f : L.Func k) (v : Fin k → LO.FirstOrder.SyntacticSemiterm L n) :

⌜LO.FirstOrder.Semiterm.func f v⌝ = LO.Arith.qqFunc ↑k ⌜f⌝ ⌜fun (i : Fin k) => ⌜v i⌝⌝

source

@[simp]

theorem LO.FirstOrder.Semiterm.codeIn_inj (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] {n : ℕ} {t : LO.FirstOrder.SyntacticSemiterm L n} {u : LO.FirstOrder.SyntacticSemiterm L n} :

⌜t⌝ = ⌜u⌝ ↔ t = u

source

@[simp]

theorem LO.FirstOrder.Semiterm.quote_zero (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (n : ℕ) :

⌜LO.FirstOrder.Semiterm.func LO.FirstOrder.Language.Zero.zero ![]⌝ = ↑𝟎

source

@[simp]

theorem LO.FirstOrder.Semiterm.quote_zero' (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (n : ℕ) :

⌜‘0’⌝ = ↑𝟎

source

@[simp]

theorem LO.FirstOrder.Semiterm.quote_one (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (n : ℕ) :

⌜LO.FirstOrder.Semiterm.func LO.FirstOrder.Language.One.one ![]⌝ = ↑𝟏

source

@[simp]

theorem LO.FirstOrder.Semiterm.quote_one' (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (n : ℕ) :

⌜‘1’⌝ = ↑𝟏

source

@[simp]

theorem LO.FirstOrder.Semiterm.quote_add (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : ℕ} (t : LO.FirstOrder.SyntacticSemiterm ℒₒᵣ n) (u : LO.FirstOrder.SyntacticSemiterm ℒₒᵣ n) :

⌜LO.FirstOrder.Semiterm.func LO.FirstOrder.Language.Add.add ![t, u]⌝ = ⌜t⌝ ^+ ⌜u⌝

source

@[simp]

theorem LO.FirstOrder.Semiterm.quote_add' (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : ℕ} (t : LO.FirstOrder.SyntacticSemiterm ℒₒᵣ n) (u : LO.FirstOrder.SyntacticSemiterm ℒₒᵣ n) :

⌜‘(!!t + !!u)’⌝ = ⌜t⌝ ^+ ⌜u⌝

source

@[simp]

theorem LO.FirstOrder.Semiterm.quote_mul (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : ℕ} (t : LO.FirstOrder.SyntacticSemiterm ℒₒᵣ n) (u : LO.FirstOrder.SyntacticSemiterm ℒₒᵣ n) :

⌜LO.FirstOrder.Semiterm.func LO.FirstOrder.Language.Mul.mul ![t, u]⌝ = ⌜t⌝ ^* ⌜u⌝

source

@[simp]

theorem LO.FirstOrder.Semiterm.quote_mul' (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : ℕ} (t : LO.FirstOrder.SyntacticSemiterm ℒₒᵣ n) (u : LO.FirstOrder.SyntacticSemiterm ℒₒᵣ n) :

⌜‘(!!t * !!u)’⌝ = ⌜t⌝ ^* ⌜u⌝

source

@[simp]

theorem LO.FirstOrder.Semiterm.quote_absolute (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] {n : ℕ} (t : LO.FirstOrder.SyntacticSemiterm L n) :

↑⌜t⌝ = ⌜t⌝

source

theorem LO.FirstOrder.Semiterm.quote_eq_encode {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] {n : ℕ} (t : LO.FirstOrder.SyntacticSemiterm L n) :

⌜t⌝ = Encodable.encode t

source

theorem LO.Arith.eq_fin_of_lt_nat {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : ℕ} {x : V} (hx : x < ↑n) :

∃ (i : Fin n), x = ↑↑i

TODO: move

source

@[simp]

theorem LO.Arith.semiterm_codeIn {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : ℕ} (t : LO.FirstOrder.SyntacticSemiterm L n) :

(L.codeIn V).IsSemiterm ↑n ⌜t⌝

source

@[simp]

theorem LO.Arith.semitermVec_codeIn {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {k : ℕ} {n : ℕ} (v : Fin k → LO.FirstOrder.SyntacticSemiterm L n) :

(L.codeIn V).IsSemitermVec ↑k ↑n ⌜fun (i : Fin k) => ⌜v i⌝⌝

source

@[simp]

theorem LO.Arith.isUTermVec_codeIn {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {k : ℕ} {n : ℕ} (v : Fin k → LO.FirstOrder.SyntacticSemiterm L n) :

(L.codeIn V).IsUTermVec ↑k ⌜fun (i : Fin k) => ⌜v i⌝⌝

source

@[simp]

theorem LO.Arith.quote_termSubst {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : ℕ} {m : ℕ} (t : LO.FirstOrder.SyntacticSemiterm L n) (w : Fin n → LO.FirstOrder.SyntacticSemiterm L m) :

⌜(LO.FirstOrder.Rew.substs w) t⌝ = (L.codeIn V).termSubst ⌜fun (i : Fin n) => ⌜w i⌝⌝ ⌜t⌝

source

theorem LO.Arith.quote_termSubstVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {k : ℕ} {n : ℕ} {m : ℕ} (w : Fin n → LO.FirstOrder.SyntacticSemiterm L m) (v : Fin k → LO.FirstOrder.SyntacticSemiterm L n) :

⌜fun (i : Fin k) => ⌜(LO.FirstOrder.Rew.substs w) (v i)⌝⌝ = (L.codeIn V).termSubstVec ↑k ⌜fun (i : Fin n) => ⌜w i⌝⌝ ⌜fun (i : Fin k) => ⌜v i⌝⌝

source

@[simp]

theorem LO.Arith.quote_termShift {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : ℕ} (t : LO.FirstOrder.SyntacticSemiterm L n) :

⌜LO.FirstOrder.Rew.shift t⌝ = (L.codeIn V).termShift ⌜t⌝

source

theorem LO.Arith.quote_termShiftVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {k : ℕ} {n : ℕ} (v : Fin k → LO.FirstOrder.SyntacticSemiterm L n) :

⌜fun (i : Fin k) => ⌜LO.FirstOrder.Rew.shift (v i)⌝⌝ = (L.codeIn V).termShiftVec ↑k ⌜fun (i : Fin k) => ⌜v i⌝⌝

source

@[simp]

theorem LO.Arith.quote_termBShift {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : ℕ} (t : LO.FirstOrder.SyntacticSemiterm L n) :

⌜LO.FirstOrder.Rew.bShift t⌝ = (L.codeIn V).termBShift ⌜t⌝

source

@[simp]

theorem LO.Arith.Formalized.quote_numeral_eq_numeral {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : ℕ} (k : ℕ) :

⌜LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ℒₒᵣ k)⌝ = LO.Arith.Formalized.numeral ↑k

source

theorem LO.Arith.quote_eterm_eq_quote_emb {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] {n : ℕ} (t : LO.FirstOrder.Semiterm L Empty n) :

⌜t⌝ = ⌜LO.FirstOrder.Rew.embs t⌝

source

@[simp]

theorem LO.Arith.Formalized.quote_numeral_eq_numeral' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : ℕ} (k : ℕ) :

⌜LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ℒₒᵣ k)⌝ = LO.Arith.Formalized.numeral ↑k

source

@[simp]

theorem LO.Arith.quote_quote_eq_numeral {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : ℕ} {α : Type u_2} [Encodable α] {x : α} :

⌜⌜x⌝⌝ = LO.Arith.Formalized.numeral ⌜x⌝

source

theorem LO.FirstOrder.Semiformula.quote_eq_toNat {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {n : ℕ} (p : LO.FirstOrder.SyntacticSemiformula L n) :

⌜p⌝ = ↑(LO.FirstOrder.Semiformula.toNat p)

source

theorem LO.FirstOrder.Semiformula.quote_rel {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {n : ℕ} {k : ℕ} (R : L.Rel k) (v : Fin k → LO.FirstOrder.SyntacticSemiterm L n) :

⌜LO.FirstOrder.Semiformula.rel R v⌝ = LO.Arith.qqRel ↑k ⌜R⌝ ⌜fun (i : Fin k) => ⌜v i⌝⌝

source

theorem LO.FirstOrder.Semiformula.quote_nrel {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {n : ℕ} {k : ℕ} (R : L.Rel k) (v : Fin k → LO.FirstOrder.SyntacticSemiterm L n) :

⌜LO.FirstOrder.Semiformula.nrel R v⌝ = LO.Arith.qqNRel ↑k ⌜R⌝ ⌜fun (i : Fin k) => ⌜v i⌝⌝

source

@[simp]

theorem LO.FirstOrder.Semiformula.quote_verum {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] (n : ℕ) :

⌜⊤⌝ = LO.Arith.qqVerum

source

@[simp]

theorem LO.FirstOrder.Semiformula.quote_falsum {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] (n : ℕ) :

⌜⊥⌝ = LO.Arith.qqFalsum

source

@[simp]

theorem LO.FirstOrder.Semiformula.quote_and {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {n : ℕ} (p : LO.FirstOrder.SyntacticSemiformula L n) (q : LO.FirstOrder.SyntacticSemiformula L n) :

⌜p ⋏ q⌝ = LO.Arith.qqAnd ⌜p⌝ ⌜q⌝

source

@[simp]

theorem LO.FirstOrder.Semiformula.quote_or {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {n : ℕ} (p : LO.FirstOrder.SyntacticSemiformula L n) (q : LO.FirstOrder.SyntacticSemiformula L n) :

⌜p ⋎ q⌝ = LO.Arith.qqOr ⌜p⌝ ⌜q⌝

source

@[simp]

theorem LO.FirstOrder.Semiformula.quote_all {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {n : ℕ} (p : LO.FirstOrder.SyntacticSemiformula L (n + 1)) :

⌜∀' p⌝ = LO.Arith.qqAll ⌜p⌝

source

@[simp]

theorem LO.FirstOrder.Semiformula.quote_ex {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {n : ℕ} (p : LO.FirstOrder.SyntacticSemiformula L (n + 1)) :

⌜∃' p⌝ = LO.Arith.qqEx ⌜p⌝

source

@[simp]

theorem LO.FirstOrder.Semiformula.quote_eq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : ℕ} (t : LO.FirstOrder.SyntacticSemiterm ℒₒᵣ n) (u : LO.FirstOrder.SyntacticSemiterm ℒₒᵣ n) :

⌜LO.FirstOrder.Semiformula.rel op(=) ![t, u]⌝ = ⌜t⌝ ^= ⌜u⌝

source

@[simp]

theorem LO.FirstOrder.Semiformula.quote_neq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : ℕ} (t : LO.FirstOrder.SyntacticSemiterm ℒₒᵣ n) (u : LO.FirstOrder.SyntacticSemiterm ℒₒᵣ n) :

⌜LO.FirstOrder.Semiformula.nrel op(=) ![t, u]⌝ = ⌜t⌝ ^≠ ⌜u⌝

source

@[simp]

theorem LO.FirstOrder.Semiformula.quote_lt {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : ℕ} (t : LO.FirstOrder.SyntacticSemiterm ℒₒᵣ n) (u : LO.FirstOrder.SyntacticSemiterm ℒₒᵣ n) :

⌜LO.FirstOrder.Semiformula.rel op(<) ![t, u]⌝ = ⌜t⌝ ^< ⌜u⌝

source

@[simp]

theorem LO.FirstOrder.Semiformula.quote_nlt {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : ℕ} (t : LO.FirstOrder.SyntacticSemiterm ℒₒᵣ n) (u : LO.FirstOrder.SyntacticSemiterm ℒₒᵣ n) :

⌜LO.FirstOrder.Semiformula.nrel op(<) ![t, u]⌝ = ⌜t⌝ ^≮ ⌜u⌝

source

@[simp]

theorem LO.FirstOrder.Semiformula.quote_neq' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : ℕ} (t : LO.FirstOrder.SyntacticSemiterm ℒₒᵣ n) (u : LO.FirstOrder.SyntacticSemiterm ℒₒᵣ n) :

⌜“¬!!t = !!u”⌝ = ⌜t⌝ ^≠ ⌜u⌝

source

@[simp]

theorem LO.FirstOrder.Semiformula.quote_eq' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : ℕ} (t : LO.FirstOrder.SyntacticSemiterm ℒₒᵣ n) (u : LO.FirstOrder.SyntacticSemiterm ℒₒᵣ n) :

⌜“!!t = !!u”⌝ = ⌜t⌝ ^= ⌜u⌝

source

@[simp]

theorem LO.FirstOrder.Semiformula.quote_lt' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : ℕ} (t : LO.FirstOrder.SyntacticSemiterm ℒₒᵣ n) (u : LO.FirstOrder.SyntacticSemiterm ℒₒᵣ n) :

⌜“!!t < !!u”⌝ = ⌜t⌝ ^< ⌜u⌝

source

@[simp]

theorem LO.FirstOrder.Semiformula.quote_nlt' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : ℕ} (t : LO.FirstOrder.SyntacticSemiterm ℒₒᵣ n) (u : LO.FirstOrder.SyntacticSemiterm ℒₒᵣ n) :

⌜“¬!!t < !!u”⌝ = ⌜t⌝ ^≮ ⌜u⌝

source

@[simp]

theorem LO.FirstOrder.Semiformula.quote_semisentence_def {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {n : ℕ} (p : LO.FirstOrder.Semisentence L n) :

⌜LO.FirstOrder.Rew.emb.hom p⌝ = ⌜p⌝

source

theorem LO.FirstOrder.Semiformula.sentence_goedelNumber_def {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {ξ : Type u_2} {n : ℕ} (σ : LO.FirstOrder.Sentence L) :

⌜σ⌝ = LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ℒₒᵣ ⌜σ⌝)

source

theorem LO.FirstOrder.Semiformula.syntacticformula_goedelNumber_def {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {ξ : Type u_2} {n : ℕ} (p : LO.FirstOrder.SyntacticFormula L) :

⌜p⌝ = LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ℒₒᵣ ⌜p⌝)

source

@[simp]

theorem LO.FirstOrder.Semiformula.quote_weight {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {k : ℕ} (n : ℕ) :

⌜LO.FirstOrder.Semiformula.weight k⌝ = LO.Arith.qqVerums ↑k

source

@[simp]

theorem LO.Arith.semiformula_quote {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : ℕ} (p : LO.FirstOrder.SyntacticSemiformula L n) :

(L.codeIn V).IsSemiformula ↑n ⌜p⌝

source

@[simp]

theorem LO.Arith.semiformula_quote0 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] (p : LO.FirstOrder.SyntacticFormula L) :

(L.codeIn V).IsFormula ⌜p⌝

source

@[simp]

theorem LO.Arith.semiformula_quote1 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] (p : LO.FirstOrder.SyntacticSemiformula L 1) :

(L.codeIn V).IsSemiformula 1 ⌜p⌝

source

@[simp]

theorem LO.Arith.semiformula_quote2 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] (p : LO.FirstOrder.SyntacticSemiformula L 2) :

(L.codeIn V).IsSemiformula 2 ⌜p⌝

source

@[simp]

theorem LO.Arith.isUFormula_quote {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : ℕ} (p : LO.FirstOrder.SyntacticSemiformula L n) :

(L.codeIn V).IsUFormula ⌜p⌝

source

@[simp]

theorem LO.Arith.semiformula_quote_succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : ℕ} (p : LO.FirstOrder.SyntacticSemiformula L (n + 1)) :

(L.codeIn V).IsSemiformula (↑n + 1) ⌜p⌝

source

@[simp]

theorem LO.Arith.quote_neg {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : ℕ} (p : LO.FirstOrder.SyntacticSemiformula L n) :

⌜∼p⌝ = (L.codeIn V).neg ⌜p⌝

source

@[simp]

theorem LO.Arith.quote_imply {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : ℕ} (p : LO.FirstOrder.SyntacticSemiformula L n) (q : LO.FirstOrder.SyntacticSemiformula L n) :

⌜p ➝ q⌝ = ⌜p⌝ ^→[L.codeIn V] ⌜q⌝

source

@[simp]

theorem LO.Arith.quote_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : ℕ} (p : LO.FirstOrder.SyntacticSemiformula L n) (q : LO.FirstOrder.SyntacticSemiformula L n) :

⌜p ⭤ q⌝ = (L.codeIn V).iff ⌜p⌝ ⌜q⌝

source

@[simp]

theorem LO.Arith.quote_shift {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : ℕ} (p : LO.FirstOrder.SyntacticSemiformula L n) :

⌜(LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.shift) p⌝ = (L.codeIn V).shift ⌜p⌝

source

theorem LO.Arith.qVec_quote {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : ℕ} {m : ℕ} (w : Fin n → LO.FirstOrder.SyntacticSemiterm L m) :

(L.codeIn V).qVec ⌜fun (i : Fin n) => ⌜w i⌝⌝ = ⌜LO.Arith.qqBvar 0 :> fun (i : Fin n) => ⌜LO.FirstOrder.Rew.bShift (w i)⌝⌝

source

@[simp]

theorem LO.Arith.quote_substs {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : ℕ} {m : ℕ} (w : Fin n → LO.FirstOrder.SyntacticSemiterm L m) (p : LO.FirstOrder.SyntacticSemiformula L n) :

⌜(LO.FirstOrder.Rew.substs w).hom p⌝ = (L.codeIn V).substs ⌜fun (i : Fin n) => ⌜w i⌝⌝ ⌜p⌝

source

theorem LO.Arith.quote_sentence_eq_quote_emb {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {n : ℕ} (σ : LO.FirstOrder.Semisentence L n) :

⌜σ⌝ = ⌜LO.FirstOrder.Rew.embs.hom σ⌝

source

theorem LO.Arith.quote_substs' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : ℕ} {m : ℕ} (w : Fin n → LO.FirstOrder.Semiterm L Empty m) (σ : LO.FirstOrder.Semisentence L n) :

⌜(LO.FirstOrder.Rew.substs w).hom σ⌝ = (L.codeIn V).substs ⌜fun (i : Fin n) => ⌜w i⌝⌝ ⌜σ⌝

source

@[simp]

theorem LO.Arith.free_quote {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] (p : LO.FirstOrder.SyntacticSemiformula L 1) :

⌜(LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.free) p⌝ = (L.codeIn V).free ⌜p⌝

Typed #

source

def LO.FirstOrder.Semiterm.codeIn' (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : ℕ} (t : LO.FirstOrder.SyntacticSemiterm L n) :

(L.codeIn V).Semiterm ↑n

Equations

LO.FirstOrder.Semiterm.codeIn' V t = { val := ⌜t⌝, prop := ⋯ }

source

instance LO.FirstOrder.Semiterm.instGoedelQuoteSyntacticSemitermSemitermCodeInCast (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : ℕ} :

LO.GoedelQuote (LO.FirstOrder.SyntacticSemiterm L n) ((L.codeIn V).Semiterm ↑n)

Equations

LO.FirstOrder.Semiterm.instGoedelQuoteSyntacticSemitermSemitermCodeInCast V = { quote := LO.FirstOrder.Semiterm.codeIn' V }

source

@[simp]

theorem LO.FirstOrder.Semiterm.codeIn'_val (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : ℕ} (t : LO.FirstOrder.SyntacticSemiterm L n) :

⌜t⌝.val = ⌜t⌝

source

def LO.FirstOrder.Semiterm.vCodeIn' (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {k : ℕ} {n : ℕ} (v : Fin k → LO.FirstOrder.SyntacticSemiterm L n) :

(L.codeIn V).SemitermVec ↑k ↑n

Equations

LO.FirstOrder.Semiterm.vCodeIn' V v = { val := ⌜fun (i : Fin k) => ⌜v i⌝⌝, prop := ⋯ }

source

instance LO.FirstOrder.Semiterm.instGoedelQuoteForallFinSyntacticSemitermSemitermVecCodeInCast (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {k : ℕ} {n : ℕ} :

LO.GoedelQuote (Fin k → LO.FirstOrder.SyntacticSemiterm L n) ((L.codeIn V).SemitermVec ↑k ↑n)

Equations

LO.FirstOrder.Semiterm.instGoedelQuoteForallFinSyntacticSemitermSemitermVecCodeInCast V = { quote := LO.FirstOrder.Semiterm.vCodeIn' V }

source

@[simp]

theorem LO.FirstOrder.Semiterm.vCodeIn'_val (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : ℕ} {k : ℕ} (v : Fin k → LO.FirstOrder.SyntacticSemiterm L n) :

⌜v⌝.val = ⌜fun (i : Fin k) => ⌜v i⌝⌝

source

@[simp]

theorem LO.FirstOrder.Semiterm.codeIn'_bvar (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : ℕ} (z : Fin n) :

⌜LO.FirstOrder.Semiterm.bvar z⌝ = (L.codeIn V).bvar ↑↑z ⋯

source

@[simp]

theorem LO.FirstOrder.Semiterm.codeIn'_fvar (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : ℕ} (x : ℕ) :

⌜LO.FirstOrder.Semiterm.fvar x⌝ = (L.codeIn V).fvar ↑x

source

theorem LO.FirstOrder.Semiterm.codeIn'_func (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : ℕ} {k : ℕ} (f : L.Func k) (v : Fin k → LO.FirstOrder.SyntacticSemiterm L n) :

⌜LO.FirstOrder.Semiterm.func f v⌝ = (L.codeIn V).func ⋯ ⌜v⌝

source

@[simp]

theorem LO.FirstOrder.Semiterm.codeIn'_zero (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (n : ℕ) :

⌜LO.FirstOrder.Semiterm.func LO.FirstOrder.Language.Zero.zero ![]⌝ = LO.Arith.Formalized.typedNumeral (↑n) 0

source

@[simp]

theorem LO.FirstOrder.Semiterm.codeIn'_one (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (n : ℕ) :

⌜LO.FirstOrder.Semiterm.func LO.FirstOrder.Language.One.one ![]⌝ = LO.Arith.Formalized.typedNumeral (↑n) 1

source

@[simp]

theorem LO.FirstOrder.Semiterm.codeIn'_add (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : ℕ} (v : Fin 2 → LO.FirstOrder.SyntacticSemiterm ℒₒᵣ n) :

⌜LO.FirstOrder.Semiterm.func LO.FirstOrder.Language.Add.add v⌝ = ⌜v 0⌝ + ⌜v 1⌝

source

@[simp]

theorem LO.FirstOrder.Semiterm.codeIn'_mul (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : ℕ} (v : Fin 2 → LO.FirstOrder.SyntacticSemiterm ℒₒᵣ n) :

⌜LO.FirstOrder.Semiterm.func LO.FirstOrder.Language.Mul.mul v⌝ = ⌜v 0⌝ * ⌜v 1⌝

source

def LO.FirstOrder.Semiformula.codeIn' (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : ℕ} (p : LO.FirstOrder.SyntacticSemiformula L n) :

(L.codeIn V).Semiformula ↑n

Equations

LO.FirstOrder.Semiformula.codeIn' V p = { val := ⌜p⌝, prop := ⋯ }

source

instance LO.FirstOrder.Semiformula.goedelQuoteSyntacticSemiformulaToCodedSemiformula (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : ℕ} :

LO.GoedelQuote (LO.FirstOrder.SyntacticSemiformula L n) ((L.codeIn V).Semiformula ↑n)

Equations

LO.FirstOrder.Semiformula.goedelQuoteSyntacticSemiformulaToCodedSemiformula V = { quote := LO.FirstOrder.Semiformula.codeIn' V }

source

instance LO.FirstOrder.Semiformula.goedelQuoteSyntacticFormulaToCodedFormula (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] :

LO.GoedelQuote (LO.FirstOrder.SyntacticFormula L) (L.codeIn V).Formula

Equations

LO.FirstOrder.Semiformula.goedelQuoteSyntacticFormulaToCodedFormula V = { quote := LO.FirstOrder.Semiformula.codeIn' V }

source

@[simp]

theorem LO.FirstOrder.Semiformula.codeIn'_val (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : ℕ} (p : LO.FirstOrder.SyntacticSemiformula L n) :

⌜p⌝.val = ⌜p⌝

source

@[simp]

theorem LO.FirstOrder.Semiformula.codeIn'_verum (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] (n : ℕ) :

⌜⊤⌝ = ⊤

source

@[simp]

theorem LO.FirstOrder.Semiformula.codeIn'_falsum (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] (n : ℕ) :

⌜⊥⌝ = ⊥

source

@[simp]

theorem LO.FirstOrder.Semiformula.codeIn'_and (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : ℕ} (p : LO.FirstOrder.SyntacticSemiformula L n) (q : LO.FirstOrder.SyntacticSemiformula L n) :

⌜p ⋏ q⌝ = ⌜p⌝ ⋏ ⌜q⌝

source

@[simp]

theorem LO.FirstOrder.Semiformula.codeIn'_or (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : ℕ} (p : LO.FirstOrder.SyntacticSemiformula L n) (q : LO.FirstOrder.SyntacticSemiformula L n) :

⌜p ⋎ q⌝ = ⌜p⌝ ⋎ ⌜q⌝

source

@[simp]

theorem LO.FirstOrder.Semiformula.codeIn'_all (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : ℕ} (p : LO.FirstOrder.SyntacticSemiformula L (n + 1)) :

⌜∀' p⌝ = (⌜p⌝.cast ⋯).all

source

@[simp]

theorem LO.FirstOrder.Semiformula.codeIn'_ex (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : ℕ} (p : LO.FirstOrder.SyntacticSemiformula L (n + 1)) :

⌜∃' p⌝ = (⌜p⌝.cast ⋯).ex

source

@[simp]

theorem LO.FirstOrder.Semiformula.codeIn'_neg (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : ℕ} (p : LO.FirstOrder.SyntacticSemiformula L n) :

⌜∼p⌝ = ∼⌜p⌝

source

@[simp]

theorem LO.FirstOrder.Semiformula.codeIn'_imp (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : ℕ} (p : LO.FirstOrder.SyntacticSemiformula L n) (q : LO.FirstOrder.SyntacticSemiformula L n) :

⌜p ➝ q⌝ = ⌜p⌝ ➝ ⌜q⌝

source

@[simp]

theorem LO.FirstOrder.Semiformula.codeIn'_weight (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] (k : ℕ) (n : ℕ) :

⌜LO.FirstOrder.Semiformula.weight k⌝ = LO.Arith.verums ↑k

source

@[simp]

theorem LO.FirstOrder.Semiformula.codeIn'_eq (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : ℕ} (v : Fin 2 → LO.FirstOrder.SyntacticSemiterm ℒₒᵣ n) :

⌜LO.FirstOrder.Semiformula.rel op(=) v⌝ = ⌜v 0⌝.equals ⌜v 1⌝

source

@[simp]

theorem LO.FirstOrder.Semiformula.codeIn'_neq (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : ℕ} (v : Fin 2 → LO.FirstOrder.SyntacticSemiterm ℒₒᵣ n) :

⌜LO.FirstOrder.Semiformula.nrel op(=) v⌝ = ⌜v 0⌝.notEquals ⌜v 1⌝

source

@[simp]

theorem LO.FirstOrder.Semiformula.codeIn'_lt (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : ℕ} (v : Fin 2 → LO.FirstOrder.SyntacticSemiterm ℒₒᵣ n) :

⌜LO.FirstOrder.Semiformula.rel op(<) v⌝ = ⌜v 0⌝.lessThan ⌜v 1⌝

source

@[simp]

theorem LO.FirstOrder.Semiformula.codeIn'_nlt (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : ℕ} (v : Fin 2 → LO.FirstOrder.SyntacticSemiterm ℒₒᵣ n) :

⌜LO.FirstOrder.Semiformula.nrel op(<) v⌝ = ⌜v 0⌝.notLessThan ⌜v 1⌝

source

@[simp]

theorem LO.FirstOrder.Semiformula.codeIn'_ball (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : ℕ} (t : LO.FirstOrder.SyntacticSemiterm ℒₒᵣ n) (p : LO.FirstOrder.SyntacticSemiformula ℒₒᵣ (n + 1)) :

⌜“(∀[!!(LO.FirstOrder.Semiterm.bvar 0) < !!(LO.FirstOrder.Rew.bShift t)] !p)”⌝ = LO.Arith.Language.Semiformula.ball ⌜t⌝ (⌜p⌝.cast ⋯)

source

@[simp]

theorem LO.FirstOrder.Semiformula.codeIn'_bex (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : ℕ} (t : LO.FirstOrder.SyntacticSemiterm ℒₒᵣ n) (p : LO.FirstOrder.SyntacticSemiformula ℒₒᵣ (n + 1)) :

⌜“(∃[!!(LO.FirstOrder.Semiterm.bvar 0) < !!(LO.FirstOrder.Rew.bShift t)] !p)”⌝ = LO.Arith.Language.Semiformula.bex ⌜t⌝ (⌜p⌝.cast ⋯)

source

instance LO.FirstOrder.Semiformula.instGoedelQuoteSentenceFormulaCodeIn (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] :

LO.GoedelQuote (LO.FirstOrder.Sentence L) (L.codeIn V).Formula

Equations

LO.FirstOrder.Semiformula.instGoedelQuoteSentenceFormulaCodeIn V = { quote := fun (σ : LO.FirstOrder.Sentence L) => ⌜LO.FirstOrder.Rew.embs.hom σ⌝ }

source

theorem LO.FirstOrder.Semiformula.quote_sentence_def' (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] (σ : LO.FirstOrder.Sentence L) :

⌜σ⌝ = ⌜LO.FirstOrder.Rew.embs.hom σ⌝

source

@[simp]

theorem LO.FirstOrder.Semiformula.quote_sentence_val (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] (σ : LO.FirstOrder.Sentence L) :

⌜σ⌝.val = ⌜σ⌝

source

@[simp]

theorem LO.FirstOrder.Semiformula.codeIn''_imp (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] (σ : LO.FirstOrder.Sentence L) (π : LO.FirstOrder.Sentence L) :

⌜σ ➝ π⌝ = ⌜σ⌝ ➝ ⌜π⌝

source

theorem LO.Arith.mem_iff_mem_bitIndices {x : ℕ} {s : ℕ} :

x ∈ s ↔ x ∈ s.bitIndices

source

theorem LO.Arith.Language.IsSemiterm.sound {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : ℕ} {t : ℕ} (ht : (L.codeIn ℕ).IsSemiterm n t) :

∃ (T : LO.FirstOrder.SyntacticSemiterm L n), ⌜T⌝ = t

source

theorem LO.Arith.Language.IsSemiformula.sound {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {n : ℕ} {p : ℕ} (h : (L.codeIn ℕ).IsSemiformula n p) :

∃ (F : LO.FirstOrder.SyntacticSemiformula L n), ⌜F⌝ = p