LeanPool.FormalizationOfBoundedArithmetic.LanguagePeano

source

inductive FirstOrder.Language.PeanoFunc :

ℕ → Type u_1

Function symbols for the Peano arithmetic language.

zero : PeanoFunc 0
one : PeanoFunc 0
add : PeanoFunc 2
mul : PeanoFunc 2

Instances For

source

def FirstOrder.Language.instDecidableEqPeanoFunc.decEq {a✝ : ℕ} (x✝ x✝¹ : PeanoFunc a✝) :

Decidable (x✝ = x✝¹)

Equations

Instances For

source

@[implicit_reducible]

instance FirstOrder.Language.instDecidableEqPeanoFunc {a✝ : ℕ} :

DecidableEq (PeanoFunc a✝)

Equations

FirstOrder.Language.instDecidableEqPeanoFunc = FirstOrder.Language.instDecidableEqPeanoFunc.decEq

source

inductive FirstOrder.Language.PeanoRel :

ℕ → Type u_1

Relation symbols for the Peano arithmetic language.

leq : PeanoRel 2

Instances For

source

def FirstOrder.Language.instDecidableEqPeanoRel.decEq {a✝ : ℕ} (x✝ x✝¹ : PeanoRel a✝) :

Decidable (x✝ = x✝¹)

Equations

FirstOrder.Language.instDecidableEqPeanoRel.decEq FirstOrder.Language.PeanoRel.leq FirstOrder.Language.PeanoRel.leq = isTrue FirstOrder.Language.instDecidableEqPeanoRel.decEq._proof_1

Instances For

source

@[implicit_reducible]

instance FirstOrder.Language.instDecidableEqPeanoRel {a✝ : ℕ} :

DecidableEq (PeanoRel a✝)

Equations

FirstOrder.Language.instDecidableEqPeanoRel = FirstOrder.Language.instDecidableEqPeanoRel.decEq

source

def FirstOrder.Language.peano :

Language

The first-order language of Peano arithmetic used by the formalization.

Equations

FirstOrder.Language.peano = { Functions := FirstOrder.Language.PeanoFunc, Relations := FirstOrder.Language.PeanoRel }

Instances For

source

@[implicit_reducible]

instance FirstOrder.Language.peano.instIsOrdered :

peano.IsOrdered

Equations

FirstOrder.Language.peano.instIsOrdered = { leSymb := FirstOrder.Language.PeanoRel.leq }

source

@[implicit_reducible]

instance FirstOrder.Language.peano.instZeroTerm {a : Type u} :

Zero (peano.Term a)

Equations

FirstOrder.Language.peano.instZeroTerm = { zero := FirstOrder.Language.Constants.term FirstOrder.Language.PeanoFunc.zero }

source

@[implicit_reducible]

instance FirstOrder.Language.peano.instOneTerm {a : Type u} :

One (peano.Term a)

Equations

FirstOrder.Language.peano.instOneTerm = { one := FirstOrder.Language.Constants.term FirstOrder.Language.PeanoFunc.one }

source

@[implicit_reducible]

instance FirstOrder.Language.peano.instAddTerm {a : Type u} :

Add (peano.Term a)

Equations

FirstOrder.Language.peano.instAddTerm = { add := FirstOrder.Language.Functions.apply₂ FirstOrder.Language.PeanoFunc.add }

source

@[implicit_reducible]

instance FirstOrder.Language.peano.instMulTerm {a : Type u} :

Mul (peano.Term a)

Equations

FirstOrder.Language.peano.instMulTerm = { mul := FirstOrder.Language.Functions.apply₂ FirstOrder.Language.PeanoFunc.mul }

source

def FirstOrder.Language.«term_<='_» :

Lean.TrailingParserDescr

Joins two terms t₁, t₂ in a formula representing t₁ ≤ t₂.

Equations

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

Instances For

source

def FirstOrder.Language.«term_<'_» :

Lean.TrailingParserDescr

Joins two terms t₁, t₂ in a formula representing t₁ < t₂.

Equations

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

Instances For

source

def FirstOrder.Term.neq {a : Type u} {n : ℕ} {L : Language} (t1 t2 : L.Term (a ⊕ Fin n)) :

L.BoundedFormula a n

The not-equal relation of two terms as a bounded formula

Equations

FirstOrder.Term.neq t1 t2 = (t1.bdEqual t2).not

Instances For

source

def FirstOrder.Language.«term_≠'_» :

Lean.TrailingParserDescr

The not-equal relation of two terms as a bounded formula

Equations

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

Instances For

source

@[implicit_reducible]

instance FirstOrder.Language.peano.instZeroOfStructure {M : Type u_1} [h : peano.Structure M] :

Zero M

Equations

FirstOrder.Language.peano.instZeroOfStructure = { zero := FirstOrder.Language.Structure.funMap FirstOrder.Language.PeanoFunc.zero ![] }

source

@[implicit_reducible]

instance FirstOrder.Language.peano.instOneOfStructure {M : Type u_1} [h : peano.Structure M] :

One M

Equations

FirstOrder.Language.peano.instOneOfStructure = { one := FirstOrder.Language.Structure.funMap FirstOrder.Language.PeanoFunc.one ![] }

source

@[implicit_reducible]

instance FirstOrder.Language.peano.instAddOfStructure {M : Type u_1} [h : peano.Structure M] :

Add M

Equations

FirstOrder.Language.peano.instAddOfStructure = { add := fun (x y : M) => FirstOrder.Language.Structure.funMap FirstOrder.Language.PeanoFunc.add ![x, y] }

source

@[implicit_reducible]

instance FirstOrder.Language.peano.instMulOfStructure {M : Type u_1} [h : peano.Structure M] :

Mul M

Equations

FirstOrder.Language.peano.instMulOfStructure = { mul := fun (x y : M) => FirstOrder.Language.Structure.funMap FirstOrder.Language.PeanoFunc.mul ![x, y] }

source

@[implicit_reducible]

instance FirstOrder.Language.peano.instLEOfStructure {M : Type u_1} [h : peano.Structure M] :

LE M

Equations

FirstOrder.Language.peano.instLEOfStructure = { le := fun (x y : M) => FirstOrder.Language.Structure.RelMap FirstOrder.Language.PeanoRel.leq ![x, y] }

source

@[implicit_reducible]

instance FirstOrder.Language.peano.instLTOfStructure {M : Type u_1} [h : peano.Structure M] :

LT M

Equations

FirstOrder.Language.peano.instLTOfStructure = { lt := fun (x y : M) => x ≤ y ∧ ¬y ≤ x }

source

def FirstOrder.Language.peano.natToM {M : Type u_1} [h : peano.Structure M] :

ℕ → M

Interpret natural-number literals in a structure for the Peano language.

Equations

Instances For

source

@[implicit_reducible]

instance FirstOrder.Language.peano.instOfNatOfStructure {M : Type u_1} [h : peano.Structure M] (n : ℕ) :

OfNat M n

Equations

FirstOrder.Language.peano.instOfNatOfStructure n = { ofNat := FirstOrder.Language.peano.natToM n }

Documentation

LeanPool.FormalizationOfBoundedArithmetic.LanguagePeano

LeanPool.FormalizationOfBoundedArithmetic.LanguagePeano #