Supporting results for pointwise provable equality.

Internalized languages of first-order logic #

@[instance_reducible]

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

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

Equations

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

source

@[instance_reducible]

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

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

Equations

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

source

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

Type

Data and laws for LORDefinable in FFL.FirstOrder.Language.

func : Σ₀.Semisentence 2
The func construction in FFL.FirstOrder.Language.LORDefinable.
rel : Σ₀.Semisentence 2
The rel construction in FFL.FirstOrder.Language.LORDefinable.
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 PointwiseComposition.FFL.FirstOrder.Language.isFunc (L : Language) {inst✝ : L.Encodable} [self : L.LORDefinable] :

Σ₀.Semisentence 2

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

The func construction in FFL.FirstOrder.Language.LORDefinable.

Equations

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

Instances For

source

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

Σ₀.Semisentence 2

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

The rel construction in FFL.FirstOrder.Language.LORDefinable.

Equations

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

Instances For

source

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

source

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

source

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

Prop

The Is Func construction in FFL.FirstOrder.Language.

Equations

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

Instances For

source

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

Prop

The Is Rel construction in FFL.FirstOrder.Language.

Equations

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

Instances For

source

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

source

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

source

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

source

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

source

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

Σ₀ -Relation L.IsFunc via L.isFunc

source

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

Σ₀ -Relation L.IsRel via L.isRel

source

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

Σ₀ -Relation L.IsFunc

source

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

Σ₀ -Relation L.IsRel

source

@[simp]

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

ℌ-Relation L.IsFunc

source

@[simp]

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

ℌ-Relation L.IsRel

source

@[instance_reducible]

instance PointwiseComposition.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

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

source

@[instance_reducible]

instance PointwiseComposition.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

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

source

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

source

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

source

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

source

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

source

@[simp]

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

source

@[simp]

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

source

@[simp]

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

source

@[simp]

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

source

@[simp]

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

source

@[simp]

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

source

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

source

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

source

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.instLORDefinableORing :

ℒₒᵣ.LORDefinable

Equations

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

source

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.zeroIndex :

ℕ

The zero Index construction in FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.

Equations

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

Instances For

source

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.oneIndex :

ℕ

The one Index construction in FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.

Equations

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

Instances For

source

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.addIndex :

ℕ

The add Index construction in FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.

Equations

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

Instances For

source

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.mulIndex :

ℕ

The mul Index construction in FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.

Equations

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

Instances For

source

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.eqIndex :

ℕ

The eq Index construction in FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.

Equations

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

Instances For

source

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.ltIndex :

ℕ

The lt Index construction in FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.

Equations

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

Instances For

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.LOR_func_zeroIndex {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] :

ℒₒᵣ.IsFunc 0 ↑zeroIndex

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.LOR_func_oneIndex {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] :

ℒₒᵣ.IsFunc 0 ↑oneIndex

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.LOR_func_addIndex {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] :

ℒₒᵣ.IsFunc 2 ↑addIndex

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.LOR_func_mulIndex {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] :

ℒₒᵣ.IsFunc 2 ↑mulIndex

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.LOR_rel_eqIndex {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] :

ℒₒᵣ.IsRel 2 ↑eqIndex

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.LOR_rel_ltIndex {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] :

ℒₒᵣ.IsRel 2 ↑ltIndex

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.coe_zeroIndex_eq {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] :

↑zeroIndex = 0

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.coe_oneIndex_eq {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] :

↑oneIndex = 1

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.coe_addIndex_eq {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] :

↑addIndex = 0

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.coe_mulIndex_eq {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] :

↑mulIndex = 1

source

@[reducible]

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.gödelQuoteFuncLOR {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] (k : ℕ) :

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

Equations

PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.gödelQuoteFuncLOR k = PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.gödelQuoteFunc k

source

@[reducible]

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.gödelQuoteRelLOR {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] (k : ℕ) :

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

Equations

PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.gödelQuoteRelLOR k = PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.gödelQuoteRel k

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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

LeanPool.PointwiseComposition.Foundation.FirstOrder.Arithmetic.Bootstrapping.Syntax.Language

Internalized languages of first-order logic #