Internalized languages of first-order logic

@[instance_reducible]

instance FFL.FirstOrder.Arithmetic.Bootstrapping.instGödelNumberORingFunc {L : Language} [L.Encodable] (k : ℕ) : Semiterm.Operator.GödelNumber ℒₒᵣ (L.Func k)

Equations

• FFL.FirstOrder.Arithmetic.Bootstrapping.instGödelNumberORingFunc k = { gödelNumber := fun (f : L.Func k) => FFL.FirstOrder.Semiterm.Operator.numeral ℒₒᵣ (Encodable.encode f) }

@[instance_reducible]

instance FFL.FirstOrder.Arithmetic.Bootstrapping.instGödelNumberORingRel {L : Language} [L.Encodable] (k : ℕ) : Semiterm.Operator.GödelNumber ℒₒᵣ (L.Rel k)

Equations

• FFL.FirstOrder.Arithmetic.Bootstrapping.instGödelNumberORingRel k = { gödelNumber := fun (r : L.Rel k) => FFL.FirstOrder.Semiterm.Operator.numeral ℒₒᵣ (Encodable.encode r) }

class FFL.FirstOrder.Language.LORDefinable (L : Language) [L.Encodable] : Type

• func : 𝚺₀.Semisentence 2
• rel : 𝚺₀.Semisentence 2
• func_iff {k c : ℕ} : c ∈ Set.range Encodable.encode ↔ (Semiformula.Evalb ![k, c]) ↑(func L)
• rel_iff {k c : ℕ} : c ∈ Set.range Encodable.encode ↔ (Semiformula.Evalb ![k, c]) ↑(rel L)

def FFL.FirstOrder.Language.isFunc (L : Language) {inst✝ : L.Encodable} [self : L.LORDefinable] : 𝚺₀.Semisentence 2

Alias of FFL.FirstOrder.Language.LORDefinable.func.

Equations

• FFL.FirstOrder.Language.isFunc = FFL.FirstOrder.Language.LORDefinable.func

def FFL.FirstOrder.Language.isRel (L : Language) {inst✝ : L.Encodable} [self : L.LORDefinable] : 𝚺₀.Semisentence 2

Alias of FFL.FirstOrder.Language.LORDefinable.rel.

Equations

• FFL.FirstOrder.Language.isRel = FFL.FirstOrder.Language.LORDefinable.rel

theorem FFL.FirstOrder.Language.iff_isFunc {L : Language} {inst✝ : L.Encodable} [self : L.LORDefinable] {k c : ℕ} : c ∈ Set.range Encodable.encode ↔ (Semiformula.Evalb ![k, c]) ↑(LORDefinable.func L)

Alias of FFL.FirstOrder.Language.LORDefinable.func_iff.

theorem FFL.FirstOrder.Language.iff_isRel {L : Language} {inst✝ : L.Encodable} [self : L.LORDefinable] {k c : ℕ} : c ∈ Set.range Encodable.encode ↔ (Semiformula.Evalb ![k, c]) ↑(LORDefinable.rel L)

Alias of FFL.FirstOrder.Language.LORDefinable.rel_iff.

def FFL.FirstOrder.Language.IsFunc (L : Language) [L.Encodable] {V : Type u_1} [ORingStructure V] [L.LORDefinable] (arity f : V) : Prop

Equations

• L.IsFunc arity f = (FFL.FirstOrder.Semiformula.Evalb ![arity, f]) ↑L.isFunc

def FFL.FirstOrder.Language.IsRel (L : Language) [L.Encodable] {V : Type u_1} [ORingStructure V] [L.LORDefinable] (arity f : V) : Prop

Equations

• L.IsRel arity f = (FFL.FirstOrder.Semiformula.Evalb ![arity, f]) ↑L.isRel

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.isFunc_def {L : Language} [L.Encodable] {V : Type u_1} [ORingStructure V] [L.LORDefinable] (k f : V) : L.IsFunc k f ↔ (Semiformula.Evalb ![k, f]) ↑L.isFunc

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.isRel_def {L : Language} [L.Encodable] {V : Type u_1} [ORingStructure V] [L.LORDefinable] (k R : V) : L.IsRel k R ↔ (Semiformula.Evalb ![k, R]) ↑L.isRel

@[simp]

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.eval_func {L : Language} [L.Encodable] {V : Type u_1} [ORingStructure V] [L.LORDefinable] (v : Fin 2 → V) : (Semiformula.Evalb v) ↑L.isFunc ↔ L.IsFunc (v 0) (v 1)

@[simp]

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.eval_rel_iff {L : Language} [L.Encodable] {V : Type u_1} [ORingStructure V] [L.LORDefinable] (v : Fin 2 → V) : (Semiformula.Evalb v) ↑L.isRel ↔ L.IsRel (v 0) (v 1)

instance FFL.FirstOrder.Language.IsFunc.defined {L : Language} [L.Encodable] {V : Type u_1} [ORingStructure V] [L.LORDefinable] : 𝚺₀-Relation L.IsFunc via L.isFunc

instance FFL.FirstOrder.Language.IsRel.defined {L : Language} [L.Encodable] {V : Type u_1} [ORingStructure V] [L.LORDefinable] : 𝚺₀-Relation L.IsRel via L.isRel

instance FFL.FirstOrder.Language.IsFunc.definable {L : Language} [L.Encodable] {V : Type u_1} [ORingStructure V] [L.LORDefinable] : 𝚺₀-Relation L.IsFunc

instance FFL.FirstOrder.Language.IsRel.definable {L : Language} [L.Encodable] {V : Type u_1} [ORingStructure V] [L.LORDefinable] : 𝚺₀-Relation L.IsRel

@[simp]

instance FFL.FirstOrder.Language.IsFunc.definable' {L : Language} [L.Encodable] {V : Type u_1} [ORingStructure V] [L.LORDefinable] (ℌ : Arithmetic.HierarchySymbol) : ℌ-Relation L.IsFunc

@[simp]

instance FFL.FirstOrder.Language.IsRel.definable' {L : Language} [L.Encodable] {V : Type u_1} [ORingStructure V] [L.LORDefinable] (ℌ : Arithmetic.HierarchySymbol) : ℌ-Relation L.IsRel

@[instance_reducible]

instance FFL.FirstOrder.Arithmetic.Bootstrapping.gödelQuoteFunc {L : Language} [L.Encodable] {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] (k : ℕ) : GödelQuote (L.Func k) V

Equations

• FFL.FirstOrder.Arithmetic.Bootstrapping.gödelQuoteFunc k = { quote := fun (f : L.Func k) => ↑(Encodable.encode f) }

@[instance_reducible]

instance FFL.FirstOrder.Arithmetic.Bootstrapping.gödelQuoteRel {L : Language} [L.Encodable] {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] (k : ℕ) : GödelQuote (L.Rel k) V

Equations

• FFL.FirstOrder.Arithmetic.Bootstrapping.gödelQuoteRel k = { quote := fun (R : L.Rel k) => ↑(Encodable.encode R) }

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.quote_func_def {L : Language} [L.Encodable] {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {k : ℕ} (f : L.Func k) : ⌜f⌝ = ↑(Encodable.encode f)

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.quote_rel_def {L : Language} [L.Encodable] {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {k : ℕ} (R : L.Rel k) : ⌜R⌝ = ↑(Encodable.encode R)

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.isFunc_quote_quote {L : Language} [L.Encodable] {V : Type u_1} [ORingStructure V] [L.LORDefinable] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {k x : ℕ} : L.IsFunc ↑k ↑x ↔ ∃ (f : L.Func k), Encodable.encode f = x

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.isRel_quote_quote {L : Language} [L.Encodable] {V : Type u_1} [ORingStructure V] [L.LORDefinable] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {k x : ℕ} : L.IsRel ↑k ↑x ↔ ∃ (R : L.Rel k), Encodable.encode R = x

@[simp]

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.codeIn_func_quote {L : Language} [L.Encodable] {V : Type u_1} [ORingStructure V] [L.LORDefinable] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {k : ℕ} (f : L.Func k) : L.IsFunc ↑k ⌜f⌝

@[simp]

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.codeIn_rel_quote {L : Language} [L.Encodable] {V : Type u_1} [ORingStructure V] [L.LORDefinable] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {k : ℕ} (r : L.Rel k) : L.IsRel ↑k ⌜r⌝

@[simp]

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.quote_func_inj {L : Language} [L.Encodable] {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {k : ℕ} (f₁ f₂ : L.Func k) : ⌜f₁⌝ = ⌜f₂⌝ ↔ f₁ = f₂

@[simp]

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.quote_rel_inj {L : Language} [L.Encodable] {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {k : ℕ} (R₁ R₂ : L.Rel k) : ⌜R₁⌝ = ⌜R₂⌝ ↔ R₁ = R₂

@[simp]

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.coe_quote_func_nat {L : Language} [L.Encodable] {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {k : ℕ} (f : L.Func k) : ↑⌜f⌝ = ⌜f⌝

@[simp]

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.coe_quote_rel_nat {L : Language} [L.Encodable] {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {k : ℕ} (R : L.Rel k) : ↑⌜R⌝ = ⌜R⌝

theorem FFL.FirstOrder.Language.ORing.of_mem_range_encode_func {k f : ℕ} : f ∈ Set.range Encodable.encode ↔ k = 0 ∧ f = 0 ∨ k = 0 ∧ f = 1 ∨ k = 2 ∧ f = 0 ∨ k = 2 ∧ f = 1

theorem FFL.FirstOrder.Language.ORing.of_mem_range_encode_rel {k r : ℕ} : r ∈ Set.range Encodable.encode ↔ k = 2 ∧ r = 0 ∨ k = 2 ∧ r = 1

TODO: move to Basic/Syntax/Bootstrapping.Language.lean

@[instance_reducible]

instance FFL.FirstOrder.Arithmetic.Bootstrapping.instLORDefinableORing : ℒₒᵣ.LORDefinable

Equations

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

def FFL.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.zeroIndex : ℕ

Equations

• FFL.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.zeroIndex = Encodable.encode FFL.FirstOrder.Language.Zero.zero

def FFL.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.oneIndex : ℕ

Equations

• FFL.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.oneIndex = Encodable.encode FFL.FirstOrder.Language.One.one

def FFL.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.addIndex : ℕ

Equations

• FFL.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.addIndex = Encodable.encode FFL.FirstOrder.Language.Add.add

def FFL.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.mulIndex : ℕ

Equations

• FFL.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.mulIndex = Encodable.encode FFL.FirstOrder.Language.Mul.mul

def FFL.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.eqIndex : ℕ

Equations

• FFL.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.eqIndex = Encodable.encode op(=)

def FFL.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.ltIndex : ℕ

Equations

• FFL.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.ltIndex = Encodable.encode op(<)

@[simp]

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.LOR_func_zeroIndex {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : ℒₒᵣ.IsFunc 0 ↑zeroIndex

@[simp]

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.LOR_func_oneIndex {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : ℒₒᵣ.IsFunc 0 ↑oneIndex

@[simp]

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.LOR_func_addIndex {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : ℒₒᵣ.IsFunc 2 ↑addIndex

@[simp]

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.LOR_func_mulIndex {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : ℒₒᵣ.IsFunc 2 ↑mulIndex

@[simp]

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.LOR_rel_eqIndex {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : ℒₒᵣ.IsRel 2 ↑eqIndex

@[simp]

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.LOR_rel_ltIndex {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : ℒₒᵣ.IsRel 2 ↑ltIndex

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.func_def_LOR : ℒₒᵣ.isFunc = HierarchySymbol.Semiformula.mkSigma ((“!!(Semiterm.bvar 0) = 0”) ⋏ (“!!(Semiterm.bvar 1) = 0”) ⋎ (“!!(Semiterm.bvar 0) = 0”) ⋏ (“!!(Semiterm.bvar 1) = 1”) ⋎ (“!!(Semiterm.bvar 0) = 2”) ⋏ (“!!(Semiterm.bvar 1) = 0”) ⋎ (“!!(Semiterm.bvar 0) = 2”) ⋏ (“!!(Semiterm.bvar 1) = 1”)) instLORDefinableORing._proof_1

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.rel_def_LOR : ℒₒᵣ.isRel = HierarchySymbol.Semiformula.mkSigma ((“!!(Semiterm.bvar 0) = 2”) ⋏ (“!!(Semiterm.bvar 1) = 0”) ⋎ (“!!(Semiterm.bvar 0) = 2”) ⋏ (“!!(Semiterm.bvar 1) = 1”)) instLORDefinableORing._proof_2

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.coe_zeroIndex_eq {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : ↑zeroIndex = 0

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.coe_oneIndex_eq {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : ↑oneIndex = 1

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.coe_addIndex_eq {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : ↑addIndex = 0

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.coe_mulIndex_eq {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : ↑mulIndex = 1

@[reducible]

instance FFL.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.gödelQuoteFuncLOR {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (k : ℕ) : GödelQuote (ℒₒᵣ.Func k) V

Equations

• FFL.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.gödelQuoteFuncLOR k = FFL.FirstOrder.Arithmetic.Bootstrapping.gödelQuoteFunc k

@[reducible]

instance FFL.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.gödelQuoteRelLOR {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (k : ℕ) : GödelQuote (ℒₒᵣ.Rel k) V

Equations

• FFL.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.gödelQuoteRelLOR k = FFL.FirstOrder.Arithmetic.Bootstrapping.gödelQuoteRel k

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.isFunc_iff_LOR {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {k f : V} : ℒₒᵣ.IsFunc k f ↔ k = 0 ∧ f = ⌜Language.Zero.zero⌝ ∨ k = 0 ∧ f = ⌜Language.One.one⌝ ∨ k = 2 ∧ f = ⌜Language.Add.add⌝ ∨ k = 2 ∧ f = ⌜Language.Mul.mul⌝

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.isRel_iff_LOR {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {k R : V} : ℒₒᵣ.IsRel k R ↔ k = 2 ∧ R = ⌜op(=)⌝ ∨ k = 2 ∧ R = ⌜op(<)⌝