Internalized languages of first-order logic #

source

@[implicit_reducible]

instance LO.FirstOrder.Arithmetic.Bootstrapping.instGödelNumberORingFunc {L : Language} [L.Encodable] (k : ℕ) :

Semiterm.Operator.GödelNumber ℒₒᵣ (L.Func k)

Equations

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

source

@[implicit_reducible]

instance LO.FirstOrder.Arithmetic.Bootstrapping.instGödelNumberORingRel {L : Language} [L.Encodable] (k : ℕ) :

Semiterm.Operator.GödelNumber ℒₒᵣ (L.Rel k)

Equations

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

source

class LO.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)

Instances

source

def LO.FirstOrder.Language.isFunc (L : Language) {inst✝ : L.Encodable} [self : L.LORDefinable] :

𝚺₀.Semisentence 2

Alias of LO.FirstOrder.Language.LORDefinable.func.

Equations

LO.FirstOrder.Language.isFunc = LO.FirstOrder.Language.LORDefinable.func

Instances For

source

def LO.FirstOrder.Language.isRel (L : Language) {inst✝ : L.Encodable} [self : L.LORDefinable] :

𝚺₀.Semisentence 2

Alias of LO.FirstOrder.Language.LORDefinable.rel.

Equations

LO.FirstOrder.Language.isRel = LO.FirstOrder.Language.LORDefinable.rel

Instances For

source

theorem LO.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 LO.FirstOrder.Language.LORDefinable.func_iff.

source

theorem LO.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 LO.FirstOrder.Language.LORDefinable.rel_iff.

source

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

Prop

Equations

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

Instances For

source

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

Prop

Equations

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

Instances For

source

theorem LO.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

source

theorem LO.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

source

@[simp]

theorem LO.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)

source

@[simp]

theorem LO.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)

source

instance LO.FirstOrder.Language.IsFunc.defined {L : Language} [L.Encodable] {V : Type u_1} [ORingStructure V] [L.LORDefinable] :

𝚺₀ -Relation L.IsFunc via L.isFunc

source

instance LO.FirstOrder.Language.IsRel.defined {L : Language} [L.Encodable] {V : Type u_1} [ORingStructure V] [L.LORDefinable] :

𝚺₀ -Relation L.IsRel via L.isRel

source

instance LO.FirstOrder.Language.IsFunc.definable {L : Language} [L.Encodable] {V : Type u_1} [ORingStructure V] [L.LORDefinable] :

𝚺₀ -Relation L.IsFunc

source

instance LO.FirstOrder.Language.IsRel.definable {L : Language} [L.Encodable] {V : Type u_1} [ORingStructure V] [L.LORDefinable] :

𝚺₀ -Relation L.IsRel

source

@[simp]

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

ℌ-Relation L.IsFunc

source

@[simp]

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

ℌ-Relation L.IsRel

source

@[implicit_reducible]

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

GödelQuote (L.Func k) V

Equations

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

source

@[implicit_reducible]

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

GödelQuote (L.Rel k) V

Equations

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

source

theorem LO.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)

source

theorem LO.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)

source

theorem LO.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

source

theorem LO.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

source

@[simp]

theorem LO.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⌝

source

@[simp]

theorem LO.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⌝

source

@[simp]

theorem LO.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₂

source

@[simp]

theorem LO.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₂

source

@[simp]

theorem LO.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⌝

source

@[simp]

theorem LO.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⌝

source

theorem LO.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

source

theorem LO.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

source

@[implicit_reducible]

instance LO.FirstOrder.Arithmetic.Bootstrapping.instLORDefinableORing :

ℒₒᵣ.LORDefinable

Equations

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

source

def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.zeroIndex :

ℕ

Equations

LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.zeroIndex = Encodable.encode LO.FirstOrder.Language.Zero.zero

Instances For

source

def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.oneIndex :

ℕ

Equations

LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.oneIndex = Encodable.encode LO.FirstOrder.Language.One.one

Instances For

source

def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.addIndex :

ℕ

Equations

LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.addIndex = Encodable.encode LO.FirstOrder.Language.Add.add

Instances For

source

def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.mulIndex :

ℕ

Equations

LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.mulIndex = Encodable.encode LO.FirstOrder.Language.Mul.mul

Instances For

source

def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.eqIndex :

ℕ

Equations

LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.eqIndex = Encodable.encode op(=)

Instances For

source

def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.ltIndex :

ℕ

Equations

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

Instances For

source

@[simp]

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

ℒₒᵣ.IsFunc 0 ↑zeroIndex

source

@[simp]

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

ℒₒᵣ.IsFunc 0 ↑oneIndex

source

@[simp]

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

ℒₒᵣ.IsFunc 2 ↑addIndex

source

@[simp]

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

ℒₒᵣ.IsFunc 2 ↑mulIndex

source

@[simp]

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

ℒₒᵣ.IsRel 2 ↑eqIndex

source

@[simp]

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

ℒₒᵣ.IsRel 2 ↑ltIndex

source

theorem LO.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

source

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

↑zeroIndex = 0

source

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

↑oneIndex = 1

source

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

↑addIndex = 0

source

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

↑mulIndex = 1

source

@[reducible]

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

GödelQuote (ℒₒᵣ.Func k) V

Equations

LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.gödelQuoteFuncLOR k = LO.FirstOrder.Arithmetic.Bootstrapping.gödelQuoteFunc k

source

@[reducible]

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

GödelQuote (ℒₒᵣ.Rel k) V

Equations

LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.gödelQuoteRelLOR k = LO.FirstOrder.Arithmetic.Bootstrapping.gödelQuoteRel k

source

theorem LO.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 ⌝

source

theorem LO.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(<)⌝

Documentation

Foundation.FirstOrder.Bootstrapping.Syntax.Language

Internalized languages of first-order logic #