Return to Question

What is authoritative canonical formal definition of function?

For example,

According to Wolfram MathWorld, $$isafun_1(f)\;\leftrightarrow\; \forall a\in f\;(\exists x\exists y \;\langle x,y\rangle = a) \; \wedge \; \forall x\forall y_1\forall y_2\;((\langle x,y_1\rangle\in f\wedge\langle x,y_2\rangle \in f)\rightarrow y_1=y_2))$$

According to Bourbaki "Elements de Mathematiques, Theorie des Ensembles", $$ isafun_2(f)\;\leftrightarrow\; \exists d\exists g\exists c\;(\langle d,g,c\rangle=f \;\wedge\;isafun_1(g)\;\wedge$$ $$\;\wedge\; \forall x(x \in d\rightarrow \exists y(\langle x,y\rangle \in g)) \;\wedge\; \forall x\forall y(\langle x,y\rangle \in g\rightarrow (x \in d\wedge y\in c))) $$

How to make agree definition of function as triple with extensional equality $$ \forall f\forall g\;[\;(isafun(f)\wedge isafun(g)) \; \rightarrow \; [\;(\forall x(\;f(x)=g(x)\;))\leftrightarrow f=g\;]\;] $$ ?

Why such divergences in definitions exist?

Upd: Two additional questions:

1. Why function is not a pair in $isafun_2$? First component of triple is perfectly derivable from the second.

2. What word function exactly means if no underlying theory is specified in context? Define it informally, please.

What is authoritative canonical formal definition of function?

For example,

According to Wolfram MathWorld, $$isafun_1(f)\;\leftrightarrow\; \forall a\in f\;(\exists x\exists y \;\langle x,y\rangle = a) \; \wedge \; \forall x\forall y_1\forall y_2\;((\langle x,y_1\rangle\in f\wedge\langle x,y_2\rangle \in f)\rightarrow y_1=y_2))$$

According to Bourbaki "Elements de Mathematiques, Theorie des Ensembles", $$ isafun_2(f)\;\leftrightarrow\; \exists d\exists g\exists c\;(\langle d,g,c\rangle=f \;\wedge\;isafun_1(g)\;\wedge$$ $$\;\wedge\; \forall x(x \in d\rightarrow \exists y(\langle x,y\rangle \in g)) \;\wedge\; \forall x\forall y(\langle x,y\rangle \in g\rightarrow (x \in d\wedge y\in c))) $$

How to make agree definition of function as triple with extensional equality $$ \forall f\forall g\;[\;(isafun(f)\wedge isafun(g)) \; \rightarrow \; [\;(\forall x(\;f(x)=g(x)\;))\leftrightarrow f=g\;]\;] $$ ?

Why such divergences in definitions exist?

Upd: Two additional questions:

1. Why function is not a pair in $isafun_2$? First component of triple is perfectly derivable from the second.

2. What word function exactly means if no underlying theory is specified in context? If I build fully formal knowledge base about mathematics for automated reasoning and want to add notion of contextless function -- how I must describe it?

What is authoritative canonical formal definition of function?

For example,

According to Wolfram MathWorld, $$isafun_1(f)\;\leftrightarrow\; \forall a\in f\;(\exists x\exists y \;\langle x,y\rangle = a) \; \wedge \; \forall x\forall y_1\forall y_2\;((\langle x,y_1\rangle\in f\wedge\langle x,y_2\rangle \in f)\rightarrow y_1=y_2))$$

According to Bourbaki "Elements de Mathematiques, Theorie des Ensembles", $$ isafun_2(f)\;\leftrightarrow\; \exists d\exists g\exists c\;(\langle d,g,c\rangle=f \;\wedge\;isafun_1(g)\;\wedge$$ $$\;\wedge\; \forall x(x \in d\rightarrow \exists y(\langle x,y\rangle \in g)) \;\wedge\; \forall x\forall y(\langle x,y\rangle \in g\rightarrow (x \in d\wedge y\in c))) $$

How to make agree definition of function as triple with extensional equality $$ \forall f\forall g\;[\;(isafun(f)\wedge isafun(g)) \; \rightarrow \; [\;(\forall x(\;f(x)=g(x)\;))\leftrightarrow f=g\;]\;] $$ ?

Why such divergences in definitions exist?

Upd: Two additional questions:

1. Why function is not a pair in $isafun_2$? First component of triple is perfectly derivable from the second.

2. What word function exactly means if no underlying theory is specified in context?

Upd: Is this definition correct?

Contextless function defined as:

1. Something denoted by symbol or term.
2. That term may be followed by list of terms in parentheses.
3. Which is called arguments.
4. Such a construction is called application.
5. If f -- function, and x and y -- arguments, then f(x)=f(y) derivable from x=y regardless of presense of Leibniz law. This is very suspicious point.

What is authoritative canonical formal definition of function?

For example,

According to Wolfram MathWorld, $$isafun_1(f)\;\leftrightarrow\; \forall a\in f\;(\exists x\exists y \;\langle x,y\rangle = a) \; \wedge \; \forall x\forall y_1\forall y_2\;((\langle x,y_1\rangle\in f\wedge\langle x,y_2\rangle \in f)\rightarrow y_1=y_2))$$

According to Bourbaki "Elements de Mathematiques, Theorie des Ensembles", $$ isafun_2(f)\;\leftrightarrow\; \exists d\exists g\exists c\;(\langle d,g,c\rangle=f \;\wedge\;isafun_1(g)\;\wedge$$ $$\;\wedge\; \forall x(x \in d\rightarrow \exists y(\langle x,y\rangle \in g)) \;\wedge\; \forall x\forall y(\langle x,y\rangle \in g\rightarrow (x \in d\wedge y\in c))) $$

How to make agree definition of function as triple with extensional equality $$ \forall f\forall g\;[\;(isafun(f)\wedge isafun(g)) \; \rightarrow \; [\;(\forall x(\;f(x)=g(x)\;))\leftrightarrow f=g\;]\;] $$ ?

Why such divergences in definitions exist?

Upd: Two additional questions:

1. Why function is not a pair in $isafun_2$? First component of triple is perfectly derivable from the second.

2. What word function exactly means if no underlying theory is specified in context? Define it informally, please.

What is authoritative canonical formal definition of function?

For example,

According to Wolfram MathWorld, $$isafun_1(f)\;\leftrightarrow\; \forall a\in f\;(\exists x\exists y \;\langle x,y\rangle = a) \; \wedge \; \forall x\forall y_1\forall y_2\;((\langle x,y_1\rangle\in f\wedge\langle x,y_2\rangle \in f)\rightarrow y_1=y_2))$$

According to Bourbaki "Elements de Mathematiques, Theorie des Ensembles", $$ isafun_2(f)\;\leftrightarrow\; \exists d\exists g\exists c\;(\langle d,g,c\rangle=f \;\wedge\;isafun_1(g)\;\wedge$$ $$\;\wedge\; \forall x(x \in d\rightarrow \exists y(\langle x,y\rangle \in g)) \;\wedge\; \forall x\forall y(\langle x,y\rangle \in g\rightarrow (x \in d\wedge y\in c))) $$

How to make agree definition of function as triple with extensional equality $$ \forall f\forall g\;[\;(isafun(f)\wedge isafun(g)) \; \rightarrow \; [\;(\forall x(\;f(x)=g(x)\;))\leftrightarrow f=g\;]\;] $$ ?

Why such divergences in definitions exist?

Upd: Two additional questions:

1. Why function is not a pair in $isafun_2$? First component of triple is perfectly derivable from the second.

2. What word function exactly means if no underlying theory is specified in context?

Upd: Is this definition correct?

Contextless function defined as:

1. Something denoted by symbol or term.
2. That term may be followed by list of terms in parentheses.
3. Which is called arguments.
4. Such a construction is called application.
5. If f -- function, and x and y -- arguments, and if from any proposition P(x) may be derived proposition P(y) (that is, P is a proposition with its holes and P(x) is that proposition with holes full of x's), then from any proposition Q(f(x)) may be derived proposition Q(f(y)).

What is authoritative canonical formal definition of function?

For example,

According to Wolfram MathWorld, $$isafun_1(f)\;\leftrightarrow\; \forall a\in f\;(\exists x\exists y \;\langle x,y\rangle = a) \; \wedge \; \forall x\forall y_1\forall y_2\;((\langle x,y_1\rangle\in f\wedge\langle x,y_2\rangle \in f)\rightarrow y_1=y_2))$$

According to Bourbaki "Elements de Mathematiques, Theorie des Ensembles", $$ isafun_2(f)\;\leftrightarrow\; \exists d\exists g\exists c\;(\langle d,g,c\rangle=f \;\wedge\;isafun_1(g)\;\wedge$$ $$\;\wedge\; \forall x(x \in d\rightarrow \exists y(\langle x,y\rangle \in g)) \;\wedge\; \forall x\forall y(\langle x,y\rangle \in g\rightarrow (x \in d\wedge y\in c))) $$

How to make agree definition of function as triple with extensional equality $$ \forall f\forall g\;[\;(isafun(f)\wedge isafun(g)) \; \rightarrow \; [\;(\forall x(\;f(x)=g(x)\;))\leftrightarrow f=g\;]\;] $$ ?

Why such divergences in definitions exist?

Upd: Two additional questions:

1. Why function is not a pair in $isafun_2$? First component of triple is perfectly derivable from the second.

2. What word function exactly means if no underlying theory is specified in context?

Upd: Is this definition correct?

Contextless function defined as:

1. Something denoted by symbol or term.
2. That term may be followed by list of terms in parentheses.
3. Which is called arguments.
4. Such a construction is called application.
5. If f -- function, and x and y -- arguments, then f(x)=f(y) derivable from x=y regardless of presense of Leibniz law. This is very suspicious point.