Foundation.FirstOrder.Arithmetic.Bootstrapping.Syntax.Formula.Coding

class FFL.LCWQIsoGödelQuote (α : ℕ → Type u_1) (β : ℕ → Type u_2) [FirstOrder.LCWQ α] [FirstOrder.LCWQ β] :

Type (max u_1 u_2)

gq (n : ℕ) : GödelQuote (α n) (β n)
top {n : ℕ} : ⌜⊤⌝ = ⊤
bot {n : ℕ} : ⌜⊥⌝ = ⊥
and {n : ℕ} (φ ψ : α n) : ⌜φ ⋏ ψ⌝ = ⌜φ⌝ ⋏ ⌜ψ⌝
or {n : ℕ} (φ ψ : α n) : ⌜φ ⋎ ψ⌝ = ⌜φ⌝ ⋎ ⌜ψ⌝
imply {n : ℕ} (φ ψ : α n) : ⌜φ 🡒 ψ⌝ = ⌜φ⌝ 🡒 ⌜ψ⌝
neg {n : ℕ} (φ : α n) : ⌜∼φ⌝ = ∼⌜φ⌝
all {n : ℕ} (φ : α (n + 1)) : ⌜∀¹ φ⌝ = ∀¹ ⌜φ⌝
exs {n : ℕ} (φ : α (n + 1)) : ⌜∃¹ φ⌝ = ∃¹ ⌜φ⌝

Instances

@[instance_reducible]

instance FFL.LCWQIsoGödelQuote.instGödelQuote {α : ℕ → Type u_1} {β : ℕ → Type u_2} [FirstOrder.LCWQ α] [FirstOrder.LCWQ β] [LCWQIsoGödelQuote α β] (n : ℕ) :

GödelQuote (α n) (β n)

Equations

FFL.LCWQIsoGödelQuote.instGödelQuote n = FFL.LCWQIsoGödelQuote.gq n

source

@[simp]

theorem FFL.LCWQIsoGödelQuote.iff {α : ℕ → Type u_1} {β : ℕ → Type u_2} [FirstOrder.LCWQ α] [FirstOrder.LCWQ β] [LCWQIsoGödelQuote α β] {n : ℕ} (φ ψ : α n) :

⌜φ 🡘 ψ⌝ = ⌜φ⌝ 🡘 ⌜ψ⌝

source

@[simp]

theorem FFL.LCWQIsoGödelQuote.ball {α : ℕ → Type u_1} {β : ℕ → Type u_2} [FirstOrder.LCWQ α] [FirstOrder.LCWQ β] [LCWQIsoGödelQuote α β] {n : ℕ} (φ ψ : α (n + 1)) :

⌜∀¹[φ] ψ⌝ = ∀¹[⌜φ⌝] ⌜ψ⌝

source

@[simp]

theorem FFL.LCWQIsoGödelQuote.bexs {α : ℕ → Type u_1} {β : ℕ → Type u_2} [FirstOrder.LCWQ α] [FirstOrder.LCWQ β] [LCWQIsoGödelQuote α β] {n : ℕ} (φ ψ : α (n + 1)) :

⌜∃¹[φ] ψ⌝ = ∃¹[⌜φ⌝] ⌜ψ⌝

source

noncomputable def FFL.FirstOrder.Semiformula.typedQuote (V : Type u_1) [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} :

Semiproposition L n → Arithmetic.Bootstrapping.Semiformula V L n

Equations

FFL.FirstOrder.Semiformula.typedQuote V (FFL.FirstOrder.Semiformula.rel R v) = FFL.FirstOrder.Arithmetic.Bootstrapping.Semiformula.rel R fun (i : Fin arity) => ⌜v i⌝
FFL.FirstOrder.Semiformula.typedQuote V (FFL.FirstOrder.Semiformula.nrel R v) = FFL.FirstOrder.Arithmetic.Bootstrapping.Semiformula.nrel R fun (i : Fin arity) => ⌜v i⌝
FFL.FirstOrder.Semiformula.typedQuote V FFL.FirstOrder.Semiformula.verum = ⊤
FFL.FirstOrder.Semiformula.typedQuote V FFL.FirstOrder.Semiformula.falsum = ⊥
FFL.FirstOrder.Semiformula.typedQuote V (FFL.FirstOrder.Semiformula.and φ ψ) = FFL.FirstOrder.Semiformula.typedQuote V φ ⋏ FFL.FirstOrder.Semiformula.typedQuote V ψ
FFL.FirstOrder.Semiformula.typedQuote V (FFL.FirstOrder.Semiformula.or φ ψ) = FFL.FirstOrder.Semiformula.typedQuote V φ ⋎ FFL.FirstOrder.Semiformula.typedQuote V ψ
FFL.FirstOrder.Semiformula.typedQuote V (FFL.FirstOrder.Semiformula.all φ) = ∀¹ FFL.FirstOrder.Semiformula.typedQuote V φ
FFL.FirstOrder.Semiformula.typedQuote V (FFL.FirstOrder.Semiformula.exs φ) = ∃¹ FFL.FirstOrder.Semiformula.typedQuote V φ

Instances For

source

theorem FFL.FirstOrder.Semiformula.typedQuote_neg {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (φ : Semiproposition L n) :

typedQuote V (∼φ) = ∼typedQuote V φ

source

@[instance_reducible]

noncomputable instance FFL.FirstOrder.Semiformula.instLCWQIsoGödelQuoteSemipropositionSemiformula {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] :

LCWQIsoGödelQuote (Semiproposition L) (Arithmetic.Bootstrapping.Semiformula V L)

Equations

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

source

@[simp]

theorem FFL.FirstOrder.Semiformula.typed_quote_rel {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n k : ℕ} (R : L.Rel k) (v : Fin k → SyntacticSemiterm L n) :

⌜rel R v⌝ = Arithmetic.Bootstrapping.Semiformula.rel R fun (i : Fin k) => ⌜v i⌝

source

@[simp]

theorem FFL.FirstOrder.Semiformula.typed_quote_nrel {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n k : ℕ} (R : L.Rel k) (v : Fin k → SyntacticSemiterm L n) :

⌜nrel R v⌝ = Arithmetic.Bootstrapping.Semiformula.nrel R fun (i : Fin k) => ⌜v i⌝

source

@[simp]

theorem FFL.FirstOrder.Semiformula.typed_quote_shift {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (φ : Semiproposition L n) :

⌜Rewriting.shift φ⌝ = ⌜φ⌝.shift

source

@[simp]

theorem FFL.FirstOrder.Semiformula.typed_quote_substs {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n m : ℕ} (w : Fin n → SyntacticSemiterm L m) (φ : Semiproposition L n) :

⌜φ ⇜ w⌝ = Arithmetic.Bootstrapping.Semiformula.subst (fun (i : Fin n) => ⌜w i⌝) ⌜φ⌝

source

@[simp]

theorem FFL.FirstOrder.Semiformula.free_quote {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (φ : Semiproposition L 1) :

⌜Rewriting.free φ⌝ = ⌜φ⌝.free

source

@[simp]

theorem FFL.FirstOrder.Semiformula.typed_quote_eq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {n : ℕ} (t u : SyntacticSemiterm ℒₒᵣ n) :

⌜“!!t = !!u”⌝ = ⌜t⌝.equals ⌜u⌝

source

@[simp]

theorem FFL.FirstOrder.Semiformula.typed_quote_ne {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {n : ℕ} (t u : SyntacticSemiterm ℒₒᵣ n) :

⌜∼(“!!t = !!u”)⌝ = ⌜t⌝.notEquals ⌜u⌝

source

@[simp]

theorem FFL.FirstOrder.Semiformula.typed_quote_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {n : ℕ} (t u : SyntacticSemiterm ℒₒᵣ n) :

⌜“!!t < !!u”⌝ = ⌜t⌝.lessThan ⌜u⌝

source

@[simp]

theorem FFL.FirstOrder.Semiformula.typed_quote_nlt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {n : ℕ} (t u : SyntacticSemiterm ℒₒᵣ n) :

⌜∼(“!!t < !!u”)⌝ = ⌜t⌝.notLessThan ⌜u⌝

source

theorem FFL.FirstOrder.Semiformula.ne_iff_val_ne {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (φ ψ : Arithmetic.Bootstrapping.Semiformula V L n) :

φ ≠ ψ ↔ φ.val ≠ ψ.val

source

theorem FFL.FirstOrder.Semiformula.typed_quote_inj {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} {φ₁ φ₂ : Semiproposition L n} :

⌜φ₁⌝ = ⌜φ₂⌝ → φ₁ = φ₂

source

@[simp]

theorem FFL.FirstOrder.Semiformula.typed_quote_inj_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} {φ₁ φ₂ : Semiproposition L n} :

⌜φ₁⌝ = ⌜φ₂⌝ ↔ φ₁ = φ₂

source

@[instance_reducible]

noncomputable instance FFL.FirstOrder.Semiformula.instGödelQuoteSemiproposition {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} :

GödelQuote (Semiproposition L n) V

Equations

FFL.FirstOrder.Semiformula.instGödelQuoteSemiproposition = { quote := fun (φ : FFL.FirstOrder.Semiproposition L n) => ⌜φ⌝.val }

source

theorem FFL.FirstOrder.Semiformula.quote_def {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (φ : Semiproposition L n) :

⌜φ⌝ = ⌜φ⌝.val

source

@[simp]

theorem FFL.FirstOrder.Semiformula.quote_isSemiformula {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (φ : Semiproposition L n) :

Arithmetic.Bootstrapping.IsSemiformula L ↑n ⌜φ⌝

source

@[simp]

theorem FFL.FirstOrder.Semiformula.quote_isSemiformula₀ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (φ : Proposition L) :

Arithmetic.Bootstrapping.IsSemiformula L 0 ⌜φ⌝

source

@[simp]

theorem FFL.FirstOrder.Semiformula.quote_isSemiformul₁ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (φ : Semiproposition L 1) :

Arithmetic.Bootstrapping.IsSemiformula L 1 ⌜φ⌝

source

@[simp]

theorem FFL.FirstOrder.Semiformula.quote_rel {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n k : ℕ} (R : L.Rel k) (v : Fin k → SyntacticSemiterm L n) :

⌜rel R v⌝ = Arithmetic.Bootstrapping.qqRel ↑k ⌜R⌝ (Arithmetic.Bootstrapping.SemitermVec.val fun (i : Fin k) => ⌜v i⌝)

source

@[simp]

theorem FFL.FirstOrder.Semiformula.quote_nrel {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n k : ℕ} (R : L.Rel k) (v : Fin k → SyntacticSemiterm L n) :

⌜nrel R v⌝ = Arithmetic.Bootstrapping.qqNRel ↑k ⌜R⌝ (Arithmetic.Bootstrapping.SemitermVec.val fun (i : Fin k) => ⌜v i⌝)

source

@[simp]

theorem FFL.FirstOrder.Semiformula.quote_verum {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} :

⌜⊤⌝ = Arithmetic.Bootstrapping.qqVerum

source

@[simp]

theorem FFL.FirstOrder.Semiformula.quote_falsum {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} :

⌜⊥⌝ = Arithmetic.Bootstrapping.qqFalsum

source

@[simp]

theorem FFL.FirstOrder.Semiformula.quote_and {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (φ ψ : Semiproposition L n) :

⌜φ ⋏ ψ⌝ = Arithmetic.Bootstrapping.qqAnd ⌜φ⌝ ⌜ψ⌝

source

@[simp]

theorem FFL.FirstOrder.Semiformula.quote_or {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (φ ψ : Semiproposition L n) :

⌜φ ⋎ ψ⌝ = Arithmetic.Bootstrapping.qqOr ⌜φ⌝ ⌜ψ⌝

source

@[simp]

theorem FFL.FirstOrder.Semiformula.quote_all {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (φ : Semiproposition L (n + 1)) :

⌜∀¹ φ⌝ = Arithmetic.Bootstrapping.qqAll ⌜φ⌝

source

@[simp]

theorem FFL.FirstOrder.Semiformula.quote_ex {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (φ : Semiproposition L (n + 1)) :

⌜∃¹ φ⌝ = Arithmetic.Bootstrapping.qqExs ⌜φ⌝

source

theorem FFL.FirstOrder.Semiformula.quote_shift {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (φ : Semiproposition L n) :

⌜Rewriting.shift φ⌝ = Arithmetic.Bootstrapping.shift L ⌜φ⌝

source

theorem FFL.FirstOrder.Semiformula.quote_eq_encode {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (φ : Semiproposition L n) :

⌜φ⌝ = ↑(Encodable.encode φ)

source

theorem FFL.FirstOrder.Semiformula.coe_quote_eq_quote {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (φ : Semiproposition L n) :

↑⌜φ⌝ = ⌜φ⌝

source

theorem FFL.FirstOrder.Semiformula.coe_quote_eq_quote' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (φ : Semiproposition L n) :

↑⌜φ⌝.val = ⌜φ⌝.val

source

theorem FFL.FirstOrder.Semiformula.quote_eq_encode_nat {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (φ : Semiproposition L n) :

⌜φ⌝ = Encodable.encode φ

source

theorem FFL.FirstOrder.Semiformula.primrec_quote_natCast {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} [L.Primcodable] :

Primrec fun (φ : Semiproposition L n) => ⌜φ⌝

source

@[simp]

theorem FFL.FirstOrder.Semiformula.quote_inj_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} {φ₁ φ₂ : Semiproposition L n} :

⌜φ₁⌝ = ⌜φ₂⌝ ↔ φ₁ = φ₂

source

@[instance_reducible]

noncomputable instance FFL.FirstOrder.Semiformula.instLCWQIsoGödelQuoteSemisentenceSemiformula {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] :

LCWQIsoGödelQuote (Semisentence L) (Arithmetic.Bootstrapping.Semiformula V L)

Equations

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

source

@[simp]

theorem FFL.FirstOrder.Semiformula.coe_quote {L : Language} [L.Encodable] [L.LORDefinable] {m : ℕ} {ξ : Type u_2} {n : ℕ} (φ : Semiproposition L n) :

↑⌜φ⌝ = ⌜φ⌝

source

@[simp]

theorem FFL.FirstOrder.Semiformula.quote_quote_eq_numeral {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n m : ℕ} (φ : Semiproposition L n) :

⌜⌜φ⌝⌝ = Arithmetic.Bootstrapping.Arithmetic.typedNumeral ⌜φ⌝

source

theorem FFL.FirstOrder.Sentence.typed_quote_def {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (σ : Semisentence L n) :

⌜σ⌝ = ⌜Rewriting.emb σ⌝

source

@[simp]

theorem FFL.FirstOrder.Sentence.typed_quote_eq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {n : ℕ} (t u : ClosedSemiterm ℒₒᵣ n) :

⌜“!!t = !!u”⌝ = ⌜t⌝.equals ⌜u⌝

source

@[simp]

theorem FFL.FirstOrder.Sentence.typed_quote_ne {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {n : ℕ} (t u : ClosedSemiterm ℒₒᵣ n) :

⌜∼(“!!t = !!u”)⌝ = ⌜t⌝.notEquals ⌜u⌝

source

@[simp]

theorem FFL.FirstOrder.Sentence.typed_quote_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {n : ℕ} (t u : ClosedSemiterm ℒₒᵣ n) :

⌜“!!t < !!u”⌝ = ⌜t⌝.lessThan ⌜u⌝

source

@[simp]

theorem FFL.FirstOrder.Sentence.typed_quote_nlt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {n : ℕ} (t u : ClosedSemiterm ℒₒᵣ n) :

⌜∼(“!!t < !!u”)⌝ = ⌜t⌝.notLessThan ⌜u⌝

source

@[instance_reducible]

noncomputable instance FFL.FirstOrder.Sentence.instGödelQuoteSemisentence {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} :

GödelQuote (Semisentence L n) V

Equations

FFL.FirstOrder.Sentence.instGödelQuoteSemisentence = { quote := fun (σ : FFL.FirstOrder.Semisentence L n) => ⌜FFL.FirstOrder.Rewriting.emb σ⌝ }

source

theorem FFL.FirstOrder.Sentence.quote_def {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (σ : Semisentence L n) :

⌜σ⌝ = ⌜Rewriting.emb σ⌝

source

theorem FFL.FirstOrder.Sentence.quote_eq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (σ : Semisentence L n) :

⌜σ⌝ = ⌜σ⌝.val

source

@[simp]

theorem FFL.FirstOrder.Sentence.quote_isSemiformula {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (φ : Semisentence L n) :

Arithmetic.Bootstrapping.IsSemiformula L ↑n ⌜φ⌝

source

@[simp]

theorem FFL.FirstOrder.Sentence.quote_isSemiformula₀ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (φ : Sentence L) :

Arithmetic.Bootstrapping.IsSemiformula L 0 ⌜φ⌝

source

@[simp]

theorem FFL.FirstOrder.Sentence.quote_isSemiformul₁ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (φ : Semisentence L 1) :

Arithmetic.Bootstrapping.IsSemiformula L 1 ⌜φ⌝

source

theorem FFL.FirstOrder.Sentence.quote_eq_encode {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (σ : Semisentence L n) :

⌜σ⌝ = ↑(Encodable.encode σ)

source

theorem FFL.FirstOrder.Sentence.coe_quote_eq_quote {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (σ : Semisentence L n) :

↑⌜σ⌝ = ⌜σ⌝

source

theorem FFL.FirstOrder.Sentence.quote_eq_encode_nat {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (σ : Semisentence L n) :

⌜σ⌝ = Encodable.encode σ

source

theorem FFL.FirstOrder.Sentence.primrec_quote_natCast {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} [L.Primcodable] :

Primrec fun (σ : Semisentence L n) => ⌜σ⌝

source

@[simp]

theorem FFL.FirstOrder.Sentence.val_quote {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {m : ℕ} {ξ : Type u_2} {n : ℕ} {bv : Fin m → V} {fv : ξ → V} (σ : Semisentence L n) :

Semiterm.val bv fv ⌜σ⌝ = ⌜σ⌝

source

@[simp]

theorem FFL.FirstOrder.Sentence.coe_quote {L : Language} [L.Encodable] [L.LORDefinable] {m : ℕ} {ξ : Type u_2} {n : ℕ} (σ : Semisentence L n) :

↑⌜σ⌝ = ⌜σ⌝

source

@[simp]

theorem FFL.FirstOrder.Sentence.quote_quote_eq_numeral {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n m : ℕ} (σ : Semisentence L n) :

⌜⌜σ⌝⌝ = Arithmetic.Bootstrapping.Arithmetic.typedNumeral ⌜σ⌝

source

@[simp]

theorem FFL.FirstOrder.Sentence.quote_inj_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} {σ₁ σ₂ : Semisentence L n} :

⌜σ₁⌝ = ⌜σ₂⌝ ↔ σ₁ = σ₂

source

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.IsSemiformula.sound {L : Language} [L.Encodable] [L.LORDefinable] {n φ : ℕ} (h : IsSemiformula L n φ) :

∃ (F : Semiproposition L n), ⌜F⌝ = φ