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
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
@[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
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
@[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
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]
Equations
- LO.Arith.finArrowToVec x_2 = 0
- LO.Arith.finArrowToVec v = cons (v 0) (LO.Arith.finArrowToVec fun (x : Fin k) => v x.succ)
Instances For
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 }
theorem
LO.Arith.quote_matrix_def
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{k : ℕ}
(v : Fin k → V)
:
@[simp]
@[simp]
@[simp]
@[simp]
theorem
LO.Arith.quote_lh
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{k : ℕ}
(v : Fin k → V)
:
LO.Arith.len ⌜v⌝ = ↑k
@[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
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) }
theorem
LO.Arith.quote_eq_coe_encode
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{α : Type u_2}
[Encodable α]
(x : α)
:
⌜x⌝ = ↑(Encodable.encode x)
@[simp]
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)
@[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)
:
@[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 : ℕ)
:
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)
:
@[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}
:
@[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 ![]⌝ = ↑𝟎
@[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 ![]⌝ = ↑𝟏
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
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
theorem
LO.Arith.eq_fin_of_lt_nat
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{n : ℕ}
{x : V}
(hx : x < ↑n)
:
TODO: move
@[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)
:
@[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)
:
@[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)
:
@[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)
:
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)
:
@[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)
:
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)
:
@[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)
:
@[simp]
theorem
LO.Arith.Formalized.quote_numeral_eq_numeral
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{n : ℕ}
(k : ℕ)
:
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)
:
@[simp]
theorem
LO.Arith.Formalized.quote_numeral_eq_numeral'
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{n : ℕ}
(k : ℕ)
:
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)
:
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)
:
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)
:
@[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)
:
@[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)
:
@[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))
:
@[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))
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
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)
:
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)
:
@[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 : ℕ)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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))
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
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)
:
@[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)
:
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)
:
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)
:
@[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)
:
Typed #
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 := ⋯ }
Instances For
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
@[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)
:
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
Instances For
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)
@[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)
:
@[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 ⋯
@[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
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)
:
@[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
@[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
@[simp]
theorem
LO.FirstOrder.Semiterm.codeIn'_add
(V : Type u_1)
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{n : ℕ}
(v : Fin 2 → LO.FirstOrder.SyntacticSemiterm ℒₒᵣ n)
:
@[simp]
theorem
LO.FirstOrder.Semiterm.codeIn'_mul
(V : Type u_1)
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{n : ℕ}
(v : Fin 2 → LO.FirstOrder.SyntacticSemiterm ℒₒᵣ n)
:
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 := ⋯ }
Instances For
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
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
@[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)
:
@[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 : ℕ)
:
@[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 : ℕ)
:
@[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)
:
@[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)
:
@[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))
:
@[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))
:
@[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)
:
@[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)
:
@[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 : ℕ)
:
@[simp]
theorem
LO.FirstOrder.Semiformula.codeIn'_eq
(V : Type u_1)
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{n : ℕ}
(v : Fin 2 → LO.FirstOrder.SyntacticSemiterm ℒₒᵣ n)
:
@[simp]
theorem
LO.FirstOrder.Semiformula.codeIn'_neq
(V : Type u_1)
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{n : ℕ}
(v : Fin 2 → LO.FirstOrder.SyntacticSemiterm ℒₒᵣ n)
:
@[simp]
theorem
LO.FirstOrder.Semiformula.codeIn'_lt
(V : Type u_1)
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{n : ℕ}
(v : Fin 2 → LO.FirstOrder.SyntacticSemiterm ℒₒᵣ n)
:
@[simp]
theorem
LO.FirstOrder.Semiformula.codeIn'_nlt
(V : Type u_1)
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{n : ℕ}
(v : Fin 2 → LO.FirstOrder.SyntacticSemiterm ℒₒᵣ n)
:
@[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 ⋯)
@[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 ⋯)
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 σ⌝ }
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)
:
@[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)
:
@[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)
:
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
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