I'll state my questions upfront and attempt to motivate/explain them afterwards.

Q1:Is there a direct way of expressing the relation "$y$ is a function of $x$" inside set theory? More precisely: Can you provide a formula of first order logic + $\in$, containing only two free variables $y$ and $x$, which directly captures the idea that "$y$ is a function of $x$"?

In case the answer to Q1 is negative, here's

Q2:Do any other foundations of mathematics (like univalent) allow one to directly formalize the relation "$y$ is a function of $x$"? Or have there been any attempts to formalize (parts of) mathematics with a language where the relation is taken as primitive/undefined?

From discussing Q1 with colleagues I've learned that it's hard to convey what my problem is, causing frustration on both sides. I suspect this is to a certain extent because we all only learned the modern definition of function (which is not the answer to Q1) and because neither the people I talk to nor myself are experts in logic/type theory/category theory. So please bear with me in (or forgive me for) this lengthy attempt at an

**Explanation/Motivation:**

The relation "*$y$ is a function of $x$*" between two things $y$ and $x$, was the original (and apparently only) way of using the word *function* in mathematics until roughly 1925. The things $y$ and $x$ were traditionally called variable quantities, and the same relation was sometimes worded differently as *"$y$ depends on $x$"*, "*$y$ is determined by $x$*" or "*$y$ changes with $x$*". This was used as a genuine mathematical proposition: something that could be proved, refuted or assumed. People would say "let $y$ be a function of $x$" just like today we might say "let $U$ be subgroup of $G$".

I could cite more than 40 well known mathematicians from Bernoulli to Courant who gave definitions of this relation, but I'll limit myself to quote eight at the end of my question. As far as I can tell, these definitions cannot be directly translated into first order logic + $\in$.

Although the word *function* assumed a different meaning with the rise of set theory an formal logic, the original relation is still used a lot among physicist, engineers or even mathematicians. Think of statements like "The pressure is a function of the volume", "The area of the circle is a function of its radius", "The number of computations is a function of the size of the matrix", "The fiber depends on the base point" etc. This even crops up in scientific communities where I wouldn't expect it. One finds it for instance in Pierce's *Types and Programming Languages* or Harper's *Practical foundations of programming languages*.

So it seems that *something being a function of something else* (or something depending on something else) is a very natural notion for many people. In fact, I have the impression that for physicists, engineers and most scientist who apply mathematics, this relation is closer to the ideas they want to express, than the modern notion of function.

Yet, I don’t see a direct way of formalizing the idea inside set theory. (The modern notion of a map $f\colon X \to Y$ is not what I'm looking for, since by itself it's not a predicate on two variables.)

I know how to capture the idea at the meta-level, by saying that a formula of first order logic is *a function of $x$*, iff its set of free variables contains at most $x$. But this is not a definition *inside* FOL. When a physicist says “The kinetic energy is a function of the velocity” he’s certainly making a physical claim and not a claim about the linguistic objects he uses to talk about physics. So this syntactic interpretation of “$y$ is a function of $x$” is not what I’m looking for.

I also know a way to encode the idea inside set theory. But I’m not completely happy with it.

First, here’s a naive and obviously wrong approach: Let $x\in X$ and $y\in Y$, call *$y$ a function of $x$*, iff there exists a map $f:X\to Y$, such that $y=f(x)$. Since every such $y\in Y$ is a function of every $x$ (use a constant map $f=(u\mapsto y))$, this is not the right definition.

Here’s a better approach: Let $x$ and $y$ be maps with equal domain, say $x:A\to X$ and $y: A \to Y$. Before giving the definition let me switch terminology: Instead of calling $x$ a "map from $A$ to $X$" I'll call it a "*variable quantity of type $X$ in context $A$*". (This change of terminology is borrowed from categorical logic/type theory. In categorical logic people say “$x$ is a generalized element of $X$ with stage of definition $A$”. But don’t assume from this, that I have a thorough understanding of categorical logic or type theory.)

**Definition:** Let $x$ and $y$ be variable quantities of type $X$ and $Y$ in the same context $A$. We call *$y$ a function of $x$*, iff there exists a map $f: X\to Y$ such that $y=f\circ x$.

(It would be suggestive to switch notation from $f{\circ} x$ to $f(x)$, so we could write $y=f(x)$ when $y$ is a function of $x$. I'll refrain from doing this, since $f(x)$ has an established meaning in set theory.)

Since my post is getting long, I won’t explain why this definition captures the original idea quite well. Let me only say why I don't consider it a *direct way* of capturing it: It seems backwards from a historical perspective. Mathematicians first had the notion of something being a function of something else, and only from there did they arrive at maps and sets. With this approach we first need to make sense of maps and sets, in order to arrive at the original idea. This might not be a strong counter argument, but if I wanted to use the original idea when teaching calculus, I would need a lot of preparation and overhead with this approach. What I’d like to have instead, is a formalization of mathematics where the relation can be used "out of the box".

The other thing I don’t like about this (maybe due to my lack of knowledge of categorical logic) has to do with the context $A$ and what Anders Kock calls an “important abuse of notation”. To illustrate: suppose I have two variables quantities $x,y$ of type $\mathbb{R}$ in some context $A$. If I now assume something additional about these variables, like the equation $y=x^2$, this assumption should change the context from $A$ to a new context $B$. This $B$ is the domain of the equalizer $e:B\to A$ of the two maps $x^2,y\colon A\to \mathbb{R}$. The abuse of notation consist in denoting the "new" variable quantities $x\circ e, y\circ e$ in context $B$, with the same letters $x,y$. I suspect this abuse is considered important, since in everyday mathematics it's natural to keep the names of mathematical objects, even when additional assumptions are added to the context. In fact, if I’m not mistaken, in a type theory with identity types there is no abuse of notation involved when changing the context from $A\vdash (x,y) \colon \mathbb{R}^2$ to $A, e\colon y=x^2 \vdash (x,y) \colon \mathbb{R}^2$. So maybe type theorist also already know a language where one can talk of "functions **of** something" in a way that's closer to how way mathematicians did until the 1920's?

**Some historical definitions of "$y$ is a function of $x$":**

*Johann Bernoulli* 1718,
in *Remarques sur ce qu’on a donné jusqu’ici de solutions des Problêmes sur les isoprimetres*,
p. 241:

Definition. We call a function of a variable quantity, a quantity composed in any way whatsoever of the variable quantity and constants.

(I'd call this the first definition. Leibniz, who initiated the use of the word function in mathematics around 1673, gave a definition even earlier. But his is not directly compatible with Bernoulli's, even though he later approved of Bernoulli's definition.)

*Euler*, 1755 in *Institutiones calculi differentialis*, Preface p.VI:

Thus when some quantities so depend on other quantities, that if the latter are changed the former undergo change, then the former quantities are called

functions of the latter; this definition applies rather widely, and all ways, in which one quantity could be determined by others, are contained in it. If therefore $x$ denotes a variable quantity, then all quantities, which depend upon $x$ in any way, or are determined by it, are called functions of it.

*Cauchy*, 1821 in *Cours d'analyse*, p. 19:

When variable quantities are related to each other such that the values of some of them being given one can find all of the others, we consider these various quantities to be expressed by means of several among them, which therefore take the name

independent variables. The other quantities expressed by means of the independent variables are calledfunctionsof those same variables.

*Bolzano*, ca. 1830 in *Erste Begriffe der allgemeinen Grössenlehre*,

The variable quantity $W$ is a

functionof one or more variable quantities $X,Y,Z$, if there exist certain propositions of the form: "the quantity $W$ has the properties $w,w_{1},w_{2}$,", which can be deduced from certain propositions of the form "the quantity $X$ has the properties $\xi,\xi',\xi''$, -- the quantity $Y$ has the properties $\eta,\eta',\eta''$; the quantity $Z$ has the properties $\zeta,\zeta',\zeta''$, etc.

*Dirichlet*, 1837 in *Über die Darstellung ganz willkürlicher Functionen durch Sinus- und Cosinusreihen*:

Imagine $a$ and $b$ two fixed values and $x$ a variable quantity, which continuously assumes all values between $a$ and $b$. If now a unique finite $y$ corresponds to each $x$, in such a way that when $x$ ranges continuously over the interval from $a$ to $b$, ${y=f(x)}$ also varies continuously, then $y$ is called a continuous function of $x$ for this interval.

(Many historians call this the first modern definition of function. I disagree, since Dirichlet calls $y$ the function, not $f$.)

*Riemann*, 1851 in *Grundlagen für eine allgemeine Theorie der Functionen einer veränderlichen complexen Grösse*

If one thinks of $z$ as a variable quantity, which may gradually assume all possible real values, then, if to any of its values corresponds a unique value of the indeterminate quantity $w$, we call $w$ a function of $z$.

*Peano*, 1884 in *Calcolo differenziale e principii di calcolo integrale* p.3:

Among the variables there are those to which we can assign arbitrarily and successively different values, called

independent variables, and others whose values depend on the values given to the first ones. These are calleddependent variablesor.functions of the first ones

*Courant*, 1934 in *Differential and Integral Calculus Vol. 1*, p.14:

In order to give a general definition of the mathematical concept of function, we fix upon a definite interval of our number scale, say the interval between the numbers $a$ and $b$, and consider the totality of numbers $x$ which belong to this interval, that is, which, satisfy the relation $$ a\leq x \leq b. $$ If we consider the symbol $x$ as denoting at will any of the numbers in this interval, we call it a

(continuous) variablein theinterval.If now to each value of $x$ in this interval there corresponds a single definite value $y$, where $x$ and $y$ are connected by any law whatsoever, we say that $y$

is a function of$x$

(It's funny how at after Cauchy many mathematicians talk of *values* of variables, which is not something we're allowed to do in set theory. (What's the value of a set or of the element of a set?). Yet, if one looks at modern type theory literature, it's full of talk of "values" again.)

from the set of possible "states"- is auseful new idea: sometimes the way we approached things historically is fundamentally non-optimal. (cont'd) $\endgroup$can and shouldlearn; I think it would be a bit tricky at first, but ultimately would actually help them understand the basic properties of functions (in particular, by not being confused by the very question you ask here). Re: your second satisfaction, I disagree that we have an obligation to change the codomain when we gain new information ("... this assumption should change the context ..."). Can you explain why you think this is something we need to do? $\endgroup$28more comments