Coding

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

theorem LO.FirstOrder.Semiterm.toNat_func {L : Language} {ξ : Type u_1} [Encodable ξ] [(k : ℕ) → Encodable (L.Func k)] {n k : ℕ} (f : L.Func k) (v : Fin k → Semiterm L ξ n) : (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

@[simp]

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

TODO: move to Foundation

theorem LO.FirstOrder.Semiformula.embedding_rel {L : Language} {ξ : Type u_1} {ο : Type u_2} {n : ℕ} [IsEmpty ο] {k : ℕ} (R : L.Rel k) (v : Fin k → Semiterm L ο n) : ↑(rel R v) = rel R fun (i : Fin k) => Rew.emb (v i)

theorem LO.FirstOrder.Semiformula.embedding_nrel {L : Language} {ξ : Type u_1} {ο : Type u_2} {n : ℕ} [IsEmpty ο] {k : ℕ} (R : L.Rel k) (v : Fin k → Semiterm L ο n) : ↑(nrel R v) = nrel R fun (i : Fin k) => Rew.emb (v i)

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

theorem LO.FirstOrder.Semiformula.encode_rel {L : Language} {ξ : Type u_1} [Encodable ξ] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {n arity : ℕ} (R : L.Rel arity) (v : Fin arity → Semiterm L ξ n) : Encodable.encode (rel R v) = Nat.pair 0 (Nat.pair arity (Nat.pair (Encodable.encode R) (Matrix.vecToNat fun (i : Fin arity) => Encodable.encode (v i)))) + 1

theorem LO.FirstOrder.Semiformula.encode_nrel {L : Language} {ξ : Type u_1} [Encodable ξ] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {n arity : ℕ} (R : L.Rel arity) (v : Fin arity → Semiterm L ξ n) : Encodable.encode (nrel R v) = Nat.pair 1 (Nat.pair arity (Nat.pair (Encodable.encode R) (Matrix.vecToNat fun (i : Fin arity) => Encodable.encode (v i)))) + 1

theorem LO.FirstOrder.Semiformula.encode_verum {L : Language} {ξ : Type u_1} [Encodable ξ] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {n : ℕ} : Encodable.encode ⊤ = Nat.pair 2 0 + 1

theorem LO.FirstOrder.Semiformula.encode_falsum {L : Language} {ξ : Type u_1} [Encodable ξ] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {n : ℕ} : Encodable.encode ⊥ = Nat.pair 3 0 + 1

theorem LO.FirstOrder.Semiformula.encode_and {L : Language} {ξ : Type u_1} [Encodable ξ] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {n : ℕ} (φ ψ : Semiformula L ξ n) : Encodable.encode (φ ⋏ ψ) = Nat.pair 4 (Nat.pair φ.toNat ψ.toNat) + 1

theorem LO.FirstOrder.Semiformula.encode_or {L : Language} {ξ : Type u_1} [Encodable ξ] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {n : ℕ} (φ ψ : Semiformula L ξ n) : Encodable.encode (φ ⋎ ψ) = Nat.pair 5 (Nat.pair φ.toNat ψ.toNat) + 1

theorem LO.FirstOrder.Semiformula.encode_all {L : Language} {ξ : Type u_1} [Encodable ξ] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {n : ℕ} (φ : Semiformula L ξ (n + 1)) : Encodable.encode (∀' φ) = Nat.pair 6 φ.toNat + 1

theorem LO.FirstOrder.Semiformula.encode_ex {L : Language} {ξ : Type u_1} [Encodable ξ] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {n : ℕ} (φ : Semiformula L ξ (n + 1)) : Encodable.encode (∃' φ) = Nat.pair 7 φ.toNat + 1

@[simp]

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

theorem LO.FirstOrder.Semiformula.Operator.lt_eq {L : Language} {ξ : Type u_1} {n : ℕ} [L.LT] (t u : Semiterm L ξ n) : (“!!t < !!u”) = rel op(<) ![t, u]

theorem LO.Arith.nat_cast_empty {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] : ↑∅ = ∅

def LO.Arith.finArrowToVec {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {k : ℕ} : (Fin k → V) → V

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

noncomputable instance LO.Arith.instGoedelQuoteForallFin {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {k : ℕ} : GoedelQuote (Fin k → V) V

quasi-quotation rather than Godel quotation

Equations

• LO.Arith.instGoedelQuoteForallFin = { quote := LO.Arith.finArrowToVec }

theorem LO.Arith.quote_matrix_def {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {k : ℕ} (v : Fin k → V) : ⌜v⌝ = finArrowToVec v

@[simp]

theorem LO.Arith.quote_nil {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] : ⌜![]⌝ = 0

@[simp]

theorem LO.Arith.quote_singleton {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (a : V) : ⌜![a]⌝ = ?[a]

@[simp]

theorem LO.Arith.quote_doubleton {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (a b : V) : ⌜![a, b]⌝ = ?[a, b]

@[simp]

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

theorem LO.Arith.quote_matrix_succ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {k : ℕ} (v : Fin (k + 1) → V) : ⌜v⌝ = cons (v 0) ⌜fun (i : Fin k) => v i.succ⌝

@[simp]

theorem LO.Arith.quote_cons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {k : ℕ} (v : Fin k → V) (a : V) : ⌜a :> v⌝ = cons a ⌜v⌝

@[simp]

theorem LO.Arith.quote_matrix_inj {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {k : ℕ} (v w : Fin k → V) : ⌜v⌝ = ⌜w⌝ ↔ v = w

@[simp]

theorem LO.Arith.quote_lh {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {k : ℕ} (v : Fin k → V) : len ⌜v⌝ = ↑k

@[simp]

theorem LO.Arith.quote_nth_fin {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {k : ℕ} (v : Fin k → V) (i : Fin k) : nth ⌜v⌝ ↑↑i = v i

@[simp]

theorem LO.Arith.quote_matrix_absolute {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {k : ℕ} (v : Fin k → ℕ) : ↑⌜v⌝ = ⌜fun (i : Fin k) => ↑(v i)⌝

theorem LO.Arith.quote_eq_vecToNat {k : ℕ} (v : Fin k → ℕ) : ⌜v⌝ = Matrix.vecToNat v

@[implicit_reducible]

instance LO.Arith.instGoedelQuote {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {α : Type u_2} [Encodable α] : GoedelQuote α V

Equations

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

theorem LO.Arith.quote_eq_coe_encode {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {α : Type u_2} [Encodable α] (x : α) : ⌜x⌝ = ↑(Encodable.encode x)

@[simp]

theorem LO.Arith.quote_nat {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (n : ℕ) : ⌜n⌝ = ↑n

theorem LO.Arith.coe_quote {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {α : Type u_2} [Encodable α] (x : α) : ↑⌜x⌝ = ⌜x⌝

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

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

@[simp]

theorem LO.Arith.val_quote {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {α : Type u_2} [Encodable α] {ξ : Type u_3} {n : ℕ} {e : Fin n → V} {ε : ξ → V} (x : α) : FirstOrder.Semiterm.valm V e ε ⌜x⌝ = ⌜x⌝

theorem LO.Arith.numeral_quote {α : Type u_2} [Encodable α] {ξ : Type u_3} {n : ℕ} (x : α) : ↑(FirstOrder.Semiterm.Operator.numeral ℒₒᵣ ⌜x⌝) = ⌜x⌝

@[simp]

theorem LO.Arith.quote_inj_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {α : Type u_2} [Encodable α] {x y : α} : ⌜x⌝ = ⌜y⌝ ↔ x = y

theorem LO.FirstOrder.Semiterm.quote_eq_toNat (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Language} [(k : ℕ) → Encodable (L.Func k)] {n : ℕ} (t : SyntacticSemiterm L n) : ⌜t⌝ = ↑(toNat t)

@[simp]

theorem LO.FirstOrder.Semiterm.quote_bvar (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Language} [(k : ℕ) → Encodable (L.Func k)] {n : ℕ} (z : Fin n) : ⌜bvar z⌝ = Arith.qqBvar ↑↑z

@[simp]

theorem LO.FirstOrder.Semiterm.quote_fvar (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Language} [(k : ℕ) → Encodable (L.Func k)] {n : ℕ} (x : ℕ) : ⌜fvar x⌝ = Arith.qqFvar ↑x

theorem LO.FirstOrder.Semiterm.quote_func (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Language} [(k : ℕ) → Encodable (L.Func k)] {n k : ℕ} (f : L.Func k) (v : Fin k → SyntacticSemiterm L n) : ⌜func f v⌝ = Arith.qqFunc ↑k ⌜f⌝ ⌜fun (i : Fin k) => ⌜v i⌝⌝

@[simp]

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

@[simp]

theorem LO.FirstOrder.Semiterm.quote_zero (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (n : ℕ) : ⌜func Language.Zero.zero ![]⌝ = ↑qqZero

@[simp]

theorem LO.FirstOrder.Semiterm.quote_zero' (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (n : ℕ) : ⌜↑0⌝ = ↑qqZero

@[simp]

theorem LO.FirstOrder.Semiterm.quote_one (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (n : ℕ) : ⌜func Language.One.one ![]⌝ = ↑qqOne

@[simp]

theorem LO.FirstOrder.Semiterm.quote_one' (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (n : ℕ) : ⌜↑1⌝ = ↑qqOne

@[simp]

theorem LO.FirstOrder.Semiterm.quote_add (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : ℕ} (t u : SyntacticSemiterm ℒₒᵣ n) : ⌜func Language.Add.add ![t, u]⌝ = ⌜t⌝ ^+ ⌜u⌝

@[simp]

theorem LO.FirstOrder.Semiterm.quote_add' (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : ℕ} (t u : SyntacticSemiterm ℒₒᵣ n) : ⌜‘(!!t + !!u)’⌝ = ⌜t⌝ ^+ ⌜u⌝

@[simp]

theorem LO.FirstOrder.Semiterm.quote_mul (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : ℕ} (t u : SyntacticSemiterm ℒₒᵣ n) : ⌜func Language.Mul.mul ![t, u]⌝ = ⌜t⌝ ^* ⌜u⌝

@[simp]

theorem LO.FirstOrder.Semiterm.quote_mul' (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : ℕ} (t u : SyntacticSemiterm ℒₒᵣ n) : ⌜‘(!!t * !!u)’⌝ = ⌜t⌝ ^* ⌜u⌝

@[simp]

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

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

theorem LO.Arith.eq_fin_of_lt_nat {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : ℕ} {x : V} (hx : x < ↑n) : ∃ (i : Fin n), x = ↑↑i

TODO: move

@[simp]

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

@[simp]

theorem LO.Arith.semitermVec_codeIn {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [DefinableLanguage L] {k n : ℕ} (v : Fin k → FirstOrder.SyntacticSemiterm L n) : (L.codeIn V).IsSemitermVec ↑k ↑n ⌜fun (i : Fin k) => ⌜v i⌝⌝

@[simp]

theorem LO.Arith.isUTermVec_codeIn {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [DefinableLanguage L] {k n : ℕ} (v : Fin k → FirstOrder.SyntacticSemiterm L n) : (L.codeIn V).IsUTermVec ↑k ⌜fun (i : Fin k) => ⌜v i⌝⌝

@[simp]

theorem LO.Arith.quote_termSubst {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [DefinableLanguage L] {n m : ℕ} (t : FirstOrder.SyntacticSemiterm L n) (w : Fin n → FirstOrder.SyntacticSemiterm L m) : ⌜(FirstOrder.Rew.substs w) t⌝ = (L.codeIn V).termSubst ⌜fun (i : Fin n) => ⌜w i⌝⌝ ⌜t⌝

theorem LO.Arith.quote_termSubstVec {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [DefinableLanguage L] {k n m : ℕ} (w : Fin n → FirstOrder.SyntacticSemiterm L m) (v : Fin k → FirstOrder.SyntacticSemiterm L n) : ⌜fun (i : Fin k) => ⌜(FirstOrder.Rew.substs w) (v i)⌝⌝ = (L.codeIn V).termSubstVec ↑k ⌜fun (i : Fin n) => ⌜w i⌝⌝ ⌜fun (i : Fin k) => ⌜v i⌝⌝

@[simp]

theorem LO.Arith.quote_termShift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [DefinableLanguage L] {n : ℕ} (t : FirstOrder.SyntacticSemiterm L n) : ⌜FirstOrder.Rew.shift t⌝ = (L.codeIn V).termShift ⌜t⌝

theorem LO.Arith.quote_termShiftVec {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [DefinableLanguage L] {k n : ℕ} (v : Fin k → FirstOrder.SyntacticSemiterm L n) : ⌜fun (i : Fin k) => ⌜FirstOrder.Rew.shift (v i)⌝⌝ = (L.codeIn V).termShiftVec ↑k ⌜fun (i : Fin k) => ⌜v i⌝⌝

@[simp]

theorem LO.Arith.quote_termBShift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [DefinableLanguage L] {n : ℕ} (t : FirstOrder.SyntacticSemiterm L n) : ⌜FirstOrder.Rew.bShift t⌝ = (L.codeIn V).termBShift ⌜t⌝

@[simp]

theorem LO.Arith.Formalized.quote_numeral_eq_numeral {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : ℕ} (k : ℕ) : ⌜↑k⌝ = numeral ↑k

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

@[simp]

theorem LO.Arith.Formalized.quote_numeral_eq_numeral' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : ℕ} (k : ℕ) : ⌜↑k⌝ = numeral ↑k

@[simp]

theorem LO.Arith.quote_quote_eq_numeral {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : ℕ} {α : Type u_2} [Encodable α] {x : α} : ⌜⌜x⌝⌝ = Formalized.numeral ⌜x⌝

theorem LO.FirstOrder.Semiformula.quote_eq_toNat {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {n : ℕ} (φ : SyntacticSemiformula L n) : ⌜φ⌝ = ↑(toNat φ)

theorem LO.FirstOrder.Semiformula.quote_rel {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {n k : ℕ} (R : L.Rel k) (v : Fin k → SyntacticSemiterm L n) : ⌜rel R v⌝ = Arith.qqRel ↑k ⌜R⌝ ⌜fun (i : Fin k) => ⌜v i⌝⌝

theorem LO.FirstOrder.Semiformula.quote_nrel {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {n k : ℕ} (R : L.Rel k) (v : Fin k → SyntacticSemiterm L n) : ⌜nrel R v⌝ = Arith.qqNRel ↑k ⌜R⌝ ⌜fun (i : Fin k) => ⌜v i⌝⌝

@[simp]

theorem LO.FirstOrder.Semiformula.quote_verum {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] (n : ℕ) : ⌜⊤⌝ = Arith.qqVerum

@[simp]

theorem LO.FirstOrder.Semiformula.quote_falsum {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] (n : ℕ) : ⌜⊥⌝ = Arith.qqFalsum

@[simp]

theorem LO.FirstOrder.Semiformula.quote_and {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {n : ℕ} (φ ψ : SyntacticSemiformula L n) : ⌜φ ⋏ ψ⌝ = Arith.qqAnd ⌜φ⌝ ⌜ψ⌝

@[simp]

theorem LO.FirstOrder.Semiformula.quote_or {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {n : ℕ} (φ ψ : SyntacticSemiformula L n) : ⌜φ ⋎ ψ⌝ = Arith.qqOr ⌜φ⌝ ⌜ψ⌝

@[simp]

theorem LO.FirstOrder.Semiformula.quote_all {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {n : ℕ} (φ : SyntacticSemiformula L (n + 1)) : ⌜∀' φ⌝ = Arith.qqAll ⌜φ⌝

@[simp]

theorem LO.FirstOrder.Semiformula.quote_ex {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {n : ℕ} (φ : SyntacticSemiformula L (n + 1)) : ⌜∃' φ⌝ = Arith.qqEx ⌜φ⌝

@[simp]

theorem LO.FirstOrder.Semiformula.quote_eq {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : ℕ} (t u : SyntacticSemiterm ℒₒᵣ n) : ⌜rel op(=) ![t, u]⌝ = ⌜t⌝ ^= ⌜u⌝

@[simp]

theorem LO.FirstOrder.Semiformula.quote_neq {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : ℕ} (t u : SyntacticSemiterm ℒₒᵣ n) : ⌜nrel op(=) ![t, u]⌝ = ⌜t⌝ ^≠ ⌜u⌝

@[simp]

theorem LO.FirstOrder.Semiformula.quote_lt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : ℕ} (t u : SyntacticSemiterm ℒₒᵣ n) : ⌜rel op(<) ![t, u]⌝ = ⌜t⌝ ^< ⌜u⌝

@[simp]

theorem LO.FirstOrder.Semiformula.quote_nlt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : ℕ} (t u : SyntacticSemiterm ℒₒᵣ n) : ⌜nrel op(<) ![t, u]⌝ = ⌜t⌝ ^</ ⌜u⌝

@[simp]

theorem LO.FirstOrder.Semiformula.quote_neq' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : ℕ} (t u : SyntacticSemiterm ℒₒᵣ n) : ⌜“¬!!t = !!u”⌝ = ⌜t⌝ ^≠ ⌜u⌝

@[simp]

theorem LO.FirstOrder.Semiformula.quote_eq' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : ℕ} (t u : SyntacticSemiterm ℒₒᵣ n) : ⌜“!!t = !!u”⌝ = ⌜t⌝ ^= ⌜u⌝

@[simp]

theorem LO.FirstOrder.Semiformula.quote_lt' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : ℕ} (t u : SyntacticSemiterm ℒₒᵣ n) : ⌜“!!t < !!u”⌝ = ⌜t⌝ ^< ⌜u⌝

@[simp]

theorem LO.FirstOrder.Semiformula.quote_nlt' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : ℕ} (t u : SyntacticSemiterm ℒₒᵣ n) : ⌜“¬!!t < !!u”⌝ = ⌜t⌝ ^</ ⌜u⌝

@[simp]

theorem LO.FirstOrder.Semiformula.quote_semisentence_def {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {n : ℕ} (φ : Semisentence L n) : ⌜↑φ⌝ = ⌜φ⌝

theorem LO.FirstOrder.Semiformula.sentence_goedelNumber_def {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {ξ : Type u_2} {n : ℕ} (σ : Sentence L) : ⌜σ⌝ = ↑(Semiterm.Operator.numeral ℒₒᵣ ⌜σ⌝)

theorem LO.FirstOrder.Semiformula.syntacticformula_goedelNumber_def {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {ξ : Type u_2} {n : ℕ} (φ : SyntacticFormula L) : ⌜φ⌝ = ↑(Semiterm.Operator.numeral ℒₒᵣ ⌜φ⌝)

@[simp]

theorem LO.FirstOrder.Semiformula.quote_weight {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {k : ℕ} (n : ℕ) : ⌜weight k⌝ = Arith.qqVerums ↑k

@[simp]

theorem LO.Arith.semiformula_quote {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [DefinableLanguage L] {n : ℕ} (φ : FirstOrder.SyntacticSemiformula L n) : (L.codeIn V).IsSemiformula ↑n ⌜φ⌝

@[simp]

theorem LO.Arith.semiformula_quote0 {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [DefinableLanguage L] (φ : FirstOrder.SyntacticFormula L) : (L.codeIn V).IsFormula ⌜φ⌝

@[simp]

theorem LO.Arith.semiformula_quote1 {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [DefinableLanguage L] (φ : FirstOrder.SyntacticSemiformula L 1) : (L.codeIn V).IsSemiformula 1 ⌜φ⌝

@[simp]

theorem LO.Arith.semiformula_quote2 {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [DefinableLanguage L] (φ : FirstOrder.SyntacticSemiformula L 2) : (L.codeIn V).IsSemiformula 2 ⌜φ⌝

@[simp]

theorem LO.Arith.isUFormula_quote {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [DefinableLanguage L] {n : ℕ} (φ : FirstOrder.SyntacticSemiformula L n) : (L.codeIn V).IsUFormula ⌜φ⌝

@[simp]

theorem LO.Arith.semiformula_quote_succ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [DefinableLanguage L] {n : ℕ} (φ : FirstOrder.SyntacticSemiformula L (n + 1)) : (L.codeIn V).IsSemiformula (↑n + 1) ⌜φ⌝

@[simp]

theorem LO.Arith.quote_neg {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [DefinableLanguage L] {n : ℕ} (φ : FirstOrder.SyntacticSemiformula L n) : ⌜∼φ⌝ = (L.codeIn V).neg ⌜φ⌝

@[simp]

theorem LO.Arith.quote_imply {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [DefinableLanguage L] {n : ℕ} (φ ψ : FirstOrder.SyntacticSemiformula L n) : ⌜φ ==> ψ⌝ = ⌜φ⌝ ^→[L.codeIn V] ⌜ψ⌝

@[simp]

theorem LO.Arith.quote_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [DefinableLanguage L] {n : ℕ} (φ ψ : FirstOrder.SyntacticSemiformula L n) : ⌜φ <=> ψ⌝ = (L.codeIn V).iff ⌜φ⌝ ⌜ψ⌝

@[simp]

theorem LO.Arith.quote_shift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [DefinableLanguage L] {n : ℕ} (φ : FirstOrder.SyntacticSemiformula L n) : ⌜FirstOrder.Rewriting.shift φ⌝ = (L.codeIn V).shift ⌜φ⌝

theorem LO.Arith.qVec_quote {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [DefinableLanguage L] {n m : ℕ} (w : Fin n → FirstOrder.SyntacticSemiterm L m) : (L.codeIn V).qVec ⌜fun (i : Fin n) => ⌜w i⌝⌝ = ⌜qqBvar 0 :> fun (i : Fin n) => ⌜FirstOrder.Rew.bShift (w i)⌝⌝

@[simp]

theorem LO.Arith.quote_substs {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [DefinableLanguage L] {n m : ℕ} (w : Fin n → FirstOrder.SyntacticSemiterm L m) (φ : FirstOrder.SyntacticSemiformula L n) : ⌜φ <~ w⌝ = (L.codeIn V).substs ⌜fun (i : Fin n) => ⌜w i⌝⌝ ⌜φ⌝

theorem LO.Arith.quote_sentence_eq_quote_emb {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {n : ℕ} (σ : FirstOrder.Semisentence L n) : ⌜σ⌝ = ⌜(FirstOrder.Rewriting.app FirstOrder.Rew.embs) σ⌝

theorem LO.Arith.quote_substs' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [DefinableLanguage L] {n m : ℕ} (w : Fin n → FirstOrder.Semiterm L Empty m) (σ : FirstOrder.Semisentence L n) : ⌜σ <~ w⌝ = (L.codeIn V).substs ⌜fun (i : Fin n) => ⌜w i⌝⌝ ⌜σ⌝

@[simp]

theorem LO.Arith.free_quote {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [DefinableLanguage L] (φ : FirstOrder.SyntacticSemiformula L 1) : ⌜FirstOrder.Rewriting.free φ⌝ = (L.codeIn V).free ⌜φ⌝

Typed

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

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

Equations

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

@[simp]

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

noncomputable instance LO.FirstOrder.Semiterm.instGoedelQuoteForallFinSyntacticSemitermSemitermVecCodeInCast (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [Arith.DefinableLanguage L] {k n : ℕ} : GoedelQuote (Fin k → SyntacticSemiterm L n) ((L.codeIn V).SemitermVec ↑k ↑n)

Equations

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

@[simp]

theorem LO.FirstOrder.Semiterm.vCodeIn'_val (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [Arith.DefinableLanguage L] {n k : ℕ} (v : Fin k → SyntacticSemiterm L n) : ⌜v⌝.val = ⌜fun (i : Fin k) => ⌜v i⌝⌝

@[simp]

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

@[simp]

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

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

@[simp]

theorem LO.FirstOrder.Semiterm.codeIn'_zero (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (n : ℕ) : ⌜func Language.Zero.zero ![]⌝ = Arith.Formalized.typedNumeral (↑n) 0

@[simp]

theorem LO.FirstOrder.Semiterm.codeIn'_one (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (n : ℕ) : ⌜func Language.One.one ![]⌝ = Arith.Formalized.typedNumeral (↑n) 1

@[simp]

theorem LO.FirstOrder.Semiterm.codeIn'_add (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : ℕ} (v : Fin 2 → SyntacticSemiterm ℒₒᵣ n) : ⌜func Language.Add.add v⌝ = ⌜v 0⌝ + ⌜v 1⌝

@[simp]

theorem LO.FirstOrder.Semiterm.codeIn'_mul (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : ℕ} (v : Fin 2 → SyntacticSemiterm ℒₒᵣ n) : ⌜func Language.Mul.mul v⌝ = ⌜v 0⌝ * ⌜v 1⌝

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[simp]

theorem LO.FirstOrder.Semiformula.codeIn'_val (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [Arith.DefinableLanguage L] {n : ℕ} (φ : SyntacticSemiformula L n) : ⌜φ⌝.val = ⌜φ⌝

@[simp]

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

@[simp]

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

@[simp]

theorem LO.FirstOrder.Semiformula.codeIn'_and (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [Arith.DefinableLanguage L] {n : ℕ} (φ ψ : SyntacticSemiformula L n) : ⌜φ ⋏ ψ⌝ = ⌜φ⌝ ⋏ ⌜ψ⌝

@[simp]

theorem LO.FirstOrder.Semiformula.codeIn'_or (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [Arith.DefinableLanguage L] {n : ℕ} (φ ψ : SyntacticSemiformula L n) : ⌜φ ⋎ ψ⌝ = ⌜φ⌝ ⋎ ⌜ψ⌝

@[simp]

theorem LO.FirstOrder.Semiformula.codeIn'_all (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [Arith.DefinableLanguage L] {n : ℕ} (φ : SyntacticSemiformula L (n + 1)) : ⌜∀' φ⌝ = (⌜φ⌝.cast ⋯).all

@[simp]

theorem LO.FirstOrder.Semiformula.codeIn'_ex (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [Arith.DefinableLanguage L] {n : ℕ} (φ : SyntacticSemiformula L (n + 1)) : ⌜∃' φ⌝ = (⌜φ⌝.cast ⋯).ex

@[simp]

theorem LO.FirstOrder.Semiformula.codeIn'_neg (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [Arith.DefinableLanguage L] {n : ℕ} (φ : SyntacticSemiformula L n) : ⌜∼φ⌝ = ∼⌜φ⌝

@[simp]

theorem LO.FirstOrder.Semiformula.codeIn'_imp (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [Arith.DefinableLanguage L] {n : ℕ} (φ ψ : SyntacticSemiformula L n) : ⌜φ ==> ψ⌝ = ⌜φ⌝ ==> ⌜ψ⌝

@[simp]

theorem LO.FirstOrder.Semiformula.codeIn'_weight (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [Arith.DefinableLanguage L] (k n : ℕ) : ⌜weight k⌝ = Arith.verums ↑k

@[simp]

theorem LO.FirstOrder.Semiformula.codeIn'_eq (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : ℕ} (v : Fin 2 → SyntacticSemiterm ℒₒᵣ n) : ⌜rel op(=) v⌝ = ⌜v 0⌝.equals ⌜v 1⌝

@[simp]

theorem LO.FirstOrder.Semiformula.codeIn'_neq (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : ℕ} (v : Fin 2 → SyntacticSemiterm ℒₒᵣ n) : ⌜nrel op(=) v⌝ = ⌜v 0⌝.notEquals ⌜v 1⌝

@[simp]

theorem LO.FirstOrder.Semiformula.codeIn'_lt (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : ℕ} (v : Fin 2 → SyntacticSemiterm ℒₒᵣ n) : ⌜rel op(<) v⌝ = ⌜v 0⌝.lessThan ⌜v 1⌝

@[simp]

theorem LO.FirstOrder.Semiformula.codeIn'_nlt (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : ℕ} (v : Fin 2 → SyntacticSemiterm ℒₒᵣ n) : ⌜nrel op(<) v⌝ = ⌜v 0⌝.notLessThan ⌜v 1⌝

@[simp]

theorem LO.FirstOrder.Semiformula.codeIn'_ball (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : ℕ} (t : SyntacticSemiterm ℒₒᵣ n) (φ : SyntacticSemiformula ℒₒᵣ (n + 1)) : ⌜“(∀[!!(Semiterm.bvar 0) < !!(Rew.bShift t)] !φ)”⌝ = Arith.Language.Semiformula.ball ⌜t⌝ (⌜φ⌝.cast ⋯)

@[simp]

theorem LO.FirstOrder.Semiformula.codeIn'_bex (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : ℕ} (t : SyntacticSemiterm ℒₒᵣ n) (φ : SyntacticSemiformula ℒₒᵣ (n + 1)) : ⌜“(∃[!!(Semiterm.bvar 0) < !!(Rew.bShift t)] !φ)”⌝ = Arith.Language.Semiformula.bex ⌜t⌝ (⌜φ⌝.cast ⋯)

@[implicit_reducible]

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

Equations

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

theorem LO.FirstOrder.Semiformula.quote_sentence_def' (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [Arith.DefinableLanguage L] (σ : Sentence L) : ⌜σ⌝ = ⌜(Rewriting.app Rew.embs) σ⌝

@[simp]

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

@[simp]

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

theorem LO.Arith.mem_iff_mem_bitIndices {x s : ℕ} : x ∈ s ↔ x ∈ s.bitIndices

theorem LO.Arith.Language.IsSemiterm.sound {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [DefinableLanguage L] {n t : ℕ} (ht : (L.codeIn ℕ).IsSemiterm n t) : ∃ (T : FirstOrder.SyntacticSemiterm L n), ⌜T⌝ = t

theorem LO.Arith.Language.IsSemiformula.sound {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [DefinableLanguage L] {n φ : ℕ} (h : (L.codeIn ℕ).IsSemiformula n φ) : ∃ (F : FirstOrder.SyntacticSemiformula L n), ⌜F⌝ = φ