26
$\begingroup$

If definitions themselves are informally just maps from words to collections of other words. Then in order for one to define anything, they must inherently already have a notion of a function. I mean of course one could ask what the exact "things" our functions are mapping to and from, and then revert back to set theory or something else to represent those "things" but why not just define everything to be a function so we are mapping functions to functions? (perhaps with some axiom guaranteeing the existence of at least one function which we can use to recursively build up a bunch of other functions allowing us to express most of contemporary mathematics in the same way I've seen this done iteratively with the emptyset in ZFC)

I mean how can one read any language, much less a mathematics textbook unless they are capable of mapping words to other words i.e. using functions (albeit even if one doesn't mentally recognize it, their brain is still implementing something akin to a function).

Even in formulations of ZFC it seems functions are implicitly being used, for example the Axiom of intersection says given any two sets $A$ and $B$ there exists a set containing all the elements they have in common that one denotes by $A\cap B$.

However we essentially have just defined a function $\cap$ of two variables, taking any two sets to another set - their intersection. Similarly in propositional logic when one defines the logical conjunction $\land$ we are again defining a two variable function from truth values to other truth values.

Pre-facing a statement about mathematical objects that are being mapped to something with the words "we represent this by" or "we denote it by" merely conceals the fact one has just defined a function by hiding it as a statement in the English language. So re-iterating I don't see how anyone can learn anything without having some mental grasp of what a map/function/arrow etc. is.

For example a dictionary can be crudely expressed as a functional relation $f$ where we might have:

$$f(\texttt{apple})≡\texttt{a round fruit that grows on trees}$$

So how is it one can accept any mathematical axioms without first taking functions as a primitive, when reading and interpreting words/symbols in of itself requires their usage. If to formally define a function you must use functions then isn't that circular reasoning?

How can a person understand a simple map or visual diagram when interpreting objects, color-intensity etc. requires mentally creating a bijective map between the object being labeled and what it represents. I mean the use of any variables for that matter requires creating what amounts to a bijection, at least mentally between the letters/symbols on paper and the objects/ideas they represent. If understanding everything from written language to cave drawings requires some mental notion of a functional relation, then shouldn't it be used as a starting point?

Also from an aesthetic point of view, it seems a lot simpler to just accept some mathematical variant of a map/arrow/morphism/function etc. then to define a large number of other objects or "syntactic abbreviations" (I'm not familiar with the proper term but this is what Peter Heinig calls it) which appear to me as objects that hold almost all the same characteristics of functions. Lastly if one gets slightly looser with this idea, couldn't you argue understanding any cause and effect relationship essentially requires some mental abstraction that when modeled symbolically is functional? This could be argued as much simpler as then even non-humans would be capable of grasping similar notions, e.g. gorillas capable of rudimentary sign language can understand that by "inputting" a configuration of their hands they can "output" a banana from their owner. In any case though before I get off topic and venture into philosophy, I want to add I'm not too well versed in mathematical logic, so I'm guessing this exact thing has been covered elsewhere. In which case I would appreciate any references.

$\endgroup$

closed as off-topic by Joseph Van Name, Mark Sapir, Stefan Kohl, Gabriel C. Drummond-Cole, Chris Godsil Oct 10 '17 at 2:28

This question appears to be off-topic. The users who voted to close gave this specific reason:

  • "This question does not appear to be about research level mathematics within the scope defined in the help center." – Joseph Van Name, Mark Sapir, Stefan Kohl
If this question can be reworded to fit the rules in the help center, please edit the question.

  • 6
    $\begingroup$ i think you might be interested in Lavere's elementary category of sets: tac.mta.ca/tac/reprints/articles/11/tr11abs.html. (Or in general category theory) $\endgroup$ – Thomas Rot Aug 30 '17 at 8:11
  • 1
    $\begingroup$ Re "Even in formulations of ZFC it seems functions are implicitly being used, for example the Axiom of intersection says given any two sets $A$ and $B$ there exists a set containing all the elements they have in common that one denotes by $A\cap B$": this sentence seems almost wrong (to me): at least in how I was taught ZFC, there does not exist any "axiom of intersection". There is the Axiom of Union. The existence of the intersection of an arbitrary family of sets has to be, and is, proved later on when one develops the theory. $\endgroup$ – Peter Heinig Aug 30 '17 at 10:43
  • 4
    $\begingroup$ Re "However we essentially have just defined a function $\cap$ of two variables, taking any two sets to another set - their intersection." Because of the "essentially", this is somewhat unassailable, yet please note that $\cap$ is not usually considered a 'function' in axiomatic set theory. In axiomatic set theory, $A\cap B$ is a mere syntactic abbreviation for the symbols $\{x\colon x\in A\ \wedge\ x\in B\}$. Yes, sometimes (notably in Jech's opening chapter), $\cap$ is called an 'operation on classes', but please note that Jech himself calls it"an informal notion". $\cap$ isn't a function. $\endgroup$ – Peter Heinig Aug 30 '17 at 10:48
  • 1
    $\begingroup$ It seems to me that you are confusing the primitive notion of whatever it is that we do when we act/think with the formal notion of function. Clearly, if a function is only what I define via set theory (a rule that returns a set, roughly) then calling whatever we do 'function' is not only reductive but plain wrong. $\endgroup$ – Three Diag Aug 31 '17 at 13:56
  • 1
    $\begingroup$ You could argue that the most fundamental intuition is the notion of a set. The ability to distinguish objects is required to perform any action, more than the successive logical step of tying cause to effect. Children can distinguish shapes and persons before they can associate actions to consequences (arguably). Anyhow, whether this is a primitive notion more than that of function is philosophical speculation. And the mere resemblance of the mathematical concept to the process you model with it is no justification of anything since, and this is my point, model and modeled are distinct. $\endgroup$ – Three Diag Sep 1 '17 at 0:55
37
$\begingroup$

Let me explain one sense in which using functions or sets provides exactly equivalent foundations of mathematics, in a way that is connected with some deep ideas in set theory. There is a translation back and forth between these foundational choices.

For example, it is a standard exercise in set theory to consider how we might construct the set-theoretic universe using characteristic functions, rather than sets, since as you noted, the characteristic function seems to provide all the necessary information about a set. We want to replace every set $A$ with a function $\chi_A$, which will have value $1$ for the "elements" of $A$ and value $0$ for objects outside $A$.

But notice that we don't really mean the ordinary elements of $A$, since we want to found the entire universe using only these functions, and so we should mean the functions that represent those elements of $A$. So this should be a recursive transfinite hereditary process.

Specifically, we can build a functional version of the set-theoretic universe as follows, in a way that perhaps fulfills the idea in your comment at the end of the first paragraph in your question. Namely, just as the set-theoretic universe is built up in a cumulative hiearchy $V_\alpha$ by iterating the power set, we can undertake a similar construction for the functional universe. We start with nothing $V_0^{\{0,1\}}=\emptyset$. If $V_\alpha^{\{0,1\}}$ is defined, then we define $V^{\{0,1\}}_{\alpha+1}$ as the set of all functions with domain contained in $V_\alpha^{\{0,1\}}$ and range contained in $\{0,1\}$. At limit stages, we take unions $V_\lambda^{\{0,1\}}=\bigcup_{\alpha<\lambda} V_\alpha^{\{0,1\}}$. The final universe $V^{\{0,1\}}$ is any function that arises in this hierarchy.

One thing to notice here is that because we allowed value $0$, we will have the same "set" being represented or named by more than one function, since $0$-values indicate non-membership. So we can define by transfinite recursion a value for equality on the names $[\![f=g]\!]$ in the natural hereditary manner: the value will be $1$, if the "members" of $f$ and $g$ are also equivalent with value $1$. And we can define the truth value of the membership relation $[\![f\in g]\!]$, which will be $1$ if $f$ is equivalent to some $f'$ for which $g(f')=1$. Meanwhile, every object $a$ in the original set-theoretic universe has a canonical name $\check a$, which is the constant $1$ function on the collection $\{\check b\mid b\in a\}$.

You can extend the truth value assignments to all assertions in the language of set theory $[\![\varphi]\!]$, and the fundamental fact to prove for this particular way of undertaking the functional universe construction is that a set-theoretic statement is true in the original set-theoretic universe if and only if the value of the statement on the corresponding names is $1$. $$V\models\varphi[a]\quad\iff\quad [\![\varphi(\check a)]\!]=1.$$ The truth values on the right are all about the functional universe $V^{\{0,1\}}$, and this equivalence expresses the sense in which truth in the set-theoretic universe is exactly copied over to the functional universe.

Conversely, given any functional universe, one can extract a corresponding set-theoretic universe. So the two approaches are essentially equivalent, the set-theoretic universe or the characteristic-functional universe.

A further thing to notice next is that the functional approach to foundations opens up an intriguing possibility. Namely, although we had used truth values $\{0,1\}$, which amounts to using classical logic, suppose that we had used another logic?

For example, if we had used functions into $\newcommand\B{\mathbb{B}}\B$, a complete Boolean algebra, then we would have constructed the universe $V^{\B}$ of $\B$-valued sets, which are hereditary functions into $\B$.

Set-theorists will recognize this as the core of the forcing method, for the elements of $V^{\B}$ are precisely the $\B$-names commonly considered in forcing. The main point is that

Forcing is the method of using a functional foundations, but where one uses a complete Boolean algebra $\B$ in place of the classical logic $\{0,1\}$.

The amazing thing about forcing is that it turns out that for any complete Boolean algebra $\B$, the ZFC axioms still come out fully true, so that $[\![\varphi]\!]=1$ for any axiom $\varphi$ of ZFC. But meanwhile, other set-theoretic statements such as the continuum hypothesis or what have you, can get value $0$ or intermediate values. This is how one establishes independence results in set theory.

I find it remarkable, a profound truth about mathematical foundations, that the nature of set-theoretic truth, concerning the continuum hypothesis or other set-theoretic statements, simply flows out of the choice of which logic of truth values to have when you are building the set-theoretic universe.

Finally, let me mention that one can undertake exactly the same process using other algebras of truth values, which are not necessarily Boolean algebras. For example, using a Heyting algebra gives rise to topos theory. And using paraconsistent logics, such as the three-element logic, gives rise to paraconsistent set theory.

$\endgroup$
  • 2
    $\begingroup$ This is all explained in John Bell's Set Theory - Boolean valued models and Independence proofs, but you do a fine a job at summarizing it, +1 $\endgroup$ – Max Aug 30 '17 at 14:28
  • 2
    $\begingroup$ I feel like you jump to a conclusion when you say "But notice that we don't really mean the ordinary elements of ... So this should be a recursive transfinite hereditary process." The untyped lambda calculus is a pure theory of functions which is not hereditary or well-founded. It's just functions all the way down (and up). $\endgroup$ – Andrej Bauer Aug 30 '17 at 19:50
  • 4
    $\begingroup$ Also, when you built the "functional" universe, you refer to the notions of "domain" and "codomain" which require further explanation in terms of functions. One approach to this can use idempotents. Say that $f$ has domain $A$ and codomain $B$ (where all three are functions) when $A \circ A = A$, $B \circ B = B$, and $f = B \circ f \circ A$. This is a standard trick in category theory and lambda calculus. $\endgroup$ – Andrej Bauer Aug 30 '17 at 19:54
  • 1
    $\begingroup$ Well, the universe $V^{\{0,1\}}$ I built is functions all the way down, as you say. My remark was meant to convey the more simple-minded observation that we don't want just to replace a set with its characteristic function, since this would not have that property. $\endgroup$ – Joel David Hamkins Aug 30 '17 at 19:57
  • 1
    $\begingroup$ nice explanation of what topos and forcing essentially are about $\endgroup$ – Manfred Weis Sep 14 '17 at 10:19
15
$\begingroup$

Von Neumann (1925, 1928) proposed a foundation for mathematics with function as the primitive concept. And in his version, sets were defined as certain functions.

Later, logicians found that there was an equivalent way of doing what von Neumann did, but with sets and classes as primitives. Today we call it NBG, attributing it to von Neumann, Bernays, and Goedel.

$\endgroup$
  • 2
    $\begingroup$ “Later, logicians...”: actually von Neumann had said that right away. This is nicely discussed in Blass-Gurevich (2008, pdf). $\endgroup$ – Francois Ziegler Aug 30 '17 at 20:54
9
$\begingroup$

I would argue that functions are indeed used as a model for some parts of mathematics, and that their roles may perhaps increase in the next century so as to account for a large part of the foundation of mathematicians work.

It is true that at the start of XX century, there was a big hope that set theory may provide a unifying framework to the whole of mathematics. This predominant position is perhaps less clear nowadays. It has been challenged by category theory on one hand. You may say that arrows are an abstraction for the concept of functions. These arrows have to map objects to objects, so there is still a need for an abstraction to sets.

But that's not what I want to argue here. I think that the real challenge is coming from a part of mathematics that has since taken its own independence, namely theoretical computer science. The concept of computation can be defined in term of a Turing machine or using the $\lambda$-calculus of A. Church. That last approach uses only functions and has given rise to functional programming, a paradigm gaining increasing attention both from computer scientists, programmers and mathematicians.

If mathematics take a slightly more algorithmical viewpoint in the future, e.g. because of a continuous stream of interesting problems from the computer sciences, then a better understanding of the foundations of computation may be needed, which in turns will change the way we do mathematics. I am thinking particularly of the work of Voevodsky concerning the univalent foundations of mathematics, which revisits a part of mathematics deeply connected with set theory and category theory, namely algebraic topology. These univalent foundations are deeply connected to computer science. Combined with the Martin-Löf type theory, they provide a practical system for formalization of modern mathematics. A large amount of mathematics has been formalized using this system and modern proof assistants such as Coq and Agda. Coq has been written in Ocaml, a functional langage, so that functions and the $\lambda$-calculus are playing a very concrete role in this reformulation of mathematics. So concrete that you can run it on your computer. As far as I understand, types play the role of sets or objects in ZFC or category theory. This is recent mathematical work and I am certainly not the most qualified to talk about this. An entry point is the 2014 Bourbaki seminar of T. Coquand in french or the slides of Voevodsky.

$\endgroup$
  • $\begingroup$ Please do not take this the wrong way, I just would like to make a pedantic linguistic point, which seems useful since your answer was addressed at an OP which (presumably) is just learning this (this comment is rather addressed at the OP, not to 'school' you; you were presumably writing in a rush): the sentence "These arrows have to map objects to objects, so there is still a need for an abstraction to sets." is not wrong, yet seems misleading in more than one way. First of all, the verb 'map' simply tends to be avoided in usual contemporary category-theoretic discourse; [...] $\endgroup$ – Peter Heinig Aug 30 '17 at 10:09
  • 4
    $\begingroup$ one just does not say that "arrows have to map objects". The 'arrows' are logical primitives, aka sorts. Yes, in a usual formalization of category theory, the sort of both the domain and the codomain of each arrow is 'object', but that's all there is to it, and it's somehow mediated by the $\mathrm{dom}$ and $\mathrm{cod}$ functions. Second, "abstraction to sets" seems a contradiction in terms, or malapropism, or whatever similar word you allow, in a rather strong sense: if sets enter the picture, then in CT one speaks of concretization, which usually is the antonym of "abstraction". $\endgroup$ – Peter Heinig Aug 30 '17 at 10:13
8
$\begingroup$

Edit October 11, 2017

While rereading an article of McLarty's cite below, I just stumbled over a passage highly relevant to the OP, and I think it will be useful to the opening poster. Lest I forget it, I'll quickly add it to the thread, without lengthily giving background for MacLarty's quite advanced article.

How the new addition relates to this thread.

This addition nicely corresponds both with Thomas Rot's comment, which first mentioned ETCS, and also with

"It is true that at the start of XX century, there was a big hope that set theory may provide a unifying framework to the whole of mathematics. This predominant position is perhaps less clear nowadays. It has been challenged by category theory on one hand. You may say that arrows are an abstraction for the concept of functions. These arrows have to map objects to objects, so there is still a need for an abstraction to sets."

[source is second paragraph of this]

Incidentally, to repeat myself, one should not fail to mention that the formulation 'arrows have to map objects to objects' in loc. cit. is, while of course not technically false, an unusual thing to say. The 'arrow's of category theory are something like a 'logical primitive', or a 'sort', or whatever similar word you allow; the arrows are syntax, and proudly so, in particular they need not be interpreted as maps, at least not if by the word 'map' you mean the set-theoretic kind of 'map'(='functional graph'='right-unique binary relation'). Also, more seriously, 'map objects to objects' can look to inexperienced eyes like 'the domain of an arrow contains things called 'objects' and these are being mapped by the arrow', which is not the usual interpretation: the objects are equal to the domain and codomain, respectively.

Enough of the usage guide. Coudy is of course right in emphasizing that there is both a philosophical and historical motivation behind the notion of 'arrow's, and of course, historically, most arrows in early category theory were and are interpreted as functions.

This is what McLarty's passage sheds more light on.

The addition proper.

The source is

Colin McLarty: Exploring Categorical Structuralism. Philosophia Mathematica 3(12), 2004, pp. 37-53.

A scan of the passage is (a text-format transcription follows below; color added)

   

and, having recently been reminded that one should, if possible, make passages available also in text-format to help visually-impaired readers, a verbatim transcription of the above passage now follows:

3. Presupposition Hellman follows Feferman [1977] saying categorical foundations presuppose a theory of sets and functions. More precisely: 'There is frank acknowledgement that the notion of function is presupposed, at least informally, in formulating category theory' (p. 133). What does it mean to presuppose something informally? For one thing it means the axioms do not formally presuppose any such thing. If thy did, Feferman or Hellman could show where they do it. It turns out to mean the axioms are motivated by an informal idea of function. [emphasis emphasized; but please note that at this point McLarty is still in the process of repeating what Hellman imputed the axioms to be motivated by, an imputation with which he seems to politely disagree] Certainly ETCS is motivated by an informal ideal of sets and functions. [note the emphasis on ETCS conveyed by the 'Certainly'; McLarty seems to agree that ETCS is so motivated, in particular since ETCS's axiom are more 'assertory' than the general 1-category-axioms] Hellman (pp. 134-135) gives reasons why this is illegitimate, at least in the case of categorical axioms, which I cannot entirely understand. It may hang on his belief that 'category theory-at least as presented in axioms-if "forma" or "schematic": unlike the axioms of set theory, its axioms are not assertory (p. 135). But this confuses the general category axioms with specific categorical foundations such as ETCS. I discuss this further in the next section.

Again, no background for McLarty's article is given here; to understand it, you'll have to study the literature. I end with adding the beginning of Lavere's PNAS 52 article; this seems a harmonious conclusion to this addition to this answer, since in a sense, in Lawvere's article, purely categorical foundations, and set-theoretic sets-and-mappings-foundations, are being reconciled.


Former version of this answer: footnotes to (a comment to) Gerald Edgar's answer.

This is mostly a historical footnote to answers that others have already given. Except for the yellow, which is to highlight what I think makes this contribution 'on-topic' for this thread, the colors in the translation used are not intended to mean anything (which is also rather obvious), the green-blue-alternation is rather to facilitate reading. (And the gray is for what I think needs no translation. And the 'redded' footnote is a footnote von Neumann makes in a part of the text that I leave out, so I do not translate this either; it would lead too far afield: the point of all of this is to give historical background to what Gerald Edgar in effect already remarked: that von Neumann about a century ago wrote he preferred functions over sets to axiomatize set theory. And this is not meant as an 'ipse dixit', i.e. not meant to say 'functions are the better foundation for set theory because von Neumann said so', rather as a historical background and an experiment in communication (in particular the colors in the side-by-side translation).

Strictly speaking this is not an answer to the OP's question, who asked about axiomatizing mathematics, not 'only' set theory, and 'axiomatizing mathematics' has never been done by anyone.

Also, I consider my answer to be a mere piece of historical background to the accepted answer, which is more modern and in touch with contemporary set theory. It is rather a long footnote to what Gerald Edgar and Francois Ziegler already mentioned about von Neumann, and an exercise in using the wonders of electronic writing media.

First, for readers' convenience, a relevant passage from the Blass--Grurevich article referenced by Francois Ziegler:

   

My knowledge of the history of mathematics is insufficient to put von Neumann's 1925 proposal in historical context. Von Neumann's 1925 paper can be considered as the first step towards what in modern times goes by the name of NBG set theory. It should to be pointed out that functions are nowadays not emphasized as logical primitives in NBG.

Excerpt from von Neumann's relevant article: Journal für die reine und angewandte Mathematik. Volume 154. Pages 219-240. The yellow passages are what makes this an on-topic contribution to the OP's question. The blue and green passages are to facilitate comparison with the translation

enter image description here

End of translation.

To give a brief summary, partly of things others have already mentioned:

  • Mathematically, in set theory one can switch between sets and functions rather freely.

  • Historically, there was once a proposal, in 1925 by von Neumann, to use 'function' as the primitive concept (or, more precisely, to use two primitive sorts13, one called 'argument', the other called 'function', and, interestingly, some but not all 'function's being allowed to be 'argument's, too.

  • Yet, somewhat ironically, while this proposal indeed was adopted and used, notably by Kurt Gödel in technical mathematical work, it evolved into what nowadays is known as von Neumann–Bernays–Gödel set theory, or 'NBG' for short, and even though von Neumann is part of the eponym, and even though von Neumann argued for using 'function' as a primitive, this was changed by later developers and nowadays in NBG 'function' is not a primitive notion.

  • There is no clear mathematical reason (known to me) for not making 'function' a primitive notion in NBG.

  • The 'why' in the OP's title, and some of the OP text, is touching on non-mathematical matters which mathematics intentionally keeps silent about.

Footnotes to the translation.

1 Explanation: in the preceding two pages, which I leave out, von Neumann in charming German had given a history of the first three decades of set theory from Cesare Burali-Forti, arranging the protagonists into two 'groups' according to their, as he puts it, method of 'rehabilitation' of the injured-by-antinomies 19th century set theory; method of rehabilitation of the first group: radical criticisim of the logic used to work with (naive-) sets (recall that set-theory is considered mathematics, not logic, to the point that to this day axioms like those of ZFC tend to be distinguished by terms like 'mathematical axiom' from 'logical axioms', so trying to rescue set-theory by doing something about the logic used to work with sets is indeed usually considered quite a distinct method of 'rehabilitation' than proposing one axiom-system or the other; von Neumann seems to consider this method too extreme [my interpretation], opting himself to use the method of the second group: method of the second group: keep classical logic, yet prohibit the use of naive-sets, rather propose an axiom system in which 'set' appears as a by-itself-meaningless logical primitive, and prove that the system is good. Von Neumann places his work in the second group.

2 I keep von Neumann's choice of words; nowadays this is more-or-less considered a synonym for 'axioms', though not by all, and especially not in the past. I seem to recall that a letter from Hilbert to Frege has survived in which Hilbert feels it necessary to justify why he uses the word 'axiom'. What the fuss is about is that 'axiom' tended to be seen a less neutral term than 'postulate', with 'axiom' having (had) a connotation of 'evidently true by itself', not only a formal 'postulate'. Whether von Neumann chose 'postulate' consciously I do not know, yet it is the more neutral choice of words, more in keeping with his attempt to give a neutral/formal system to do set-theory with (though his choice of title jarrs with this, of course, though this may be purely cultural/linguistic, since 'Eine Postulatisierung der Mengenlehre' would have used a lexically inexistant word and probably wouldn't have found favor with the editors of the journal he is publishing it in.

3 I consciously opt for the unidiomatic literal translation 'free-of-contradictions-proof' instead of the customary yet more opaque term 'consistency proof'.

4 Von Neumann here sounds like he does not really know what to make of Brouwer's 'utterance'.

EDIT October 11, 2017: thanks to F. Ziegler for pointing out that von Neumann here is referencing his own footnote, but the number of this interal footnote was misprinted as 2 instead of 1, for whatever reason.

FORMER VERSION: Please also note that the article of Brouwer's that von Neumann references does not have a page numbered 220., it runs from p. 203 to p. 208 of the relevant journal volume (Jber. Deutsch. Math.-Vereinig. Bd. 28 (1919) S. 203–208); presumably von Neumann references his own page 220 here, in whose footnote I could not find what he means. I cursorily read Brouwer's "Intuitionistische Mengenlehre"; confusingly, there exist at least two articles of Brouwer's with that title, see

   

and

enter image description here

Upon this cursory reading, I did not see Brouwer writing about the interesting topic of 'intuitionistic consistency proofs for axiom systems' that von Neumann is hinting at here. I simply do not know what he means with his reference to the "Äußerung" of Brouwer's. Maybe this is an interesting question in and of itself, yet I expect this to be very well documented by Brouwer scholars.

5 I consciously use the repetitive-sounding 'construct set-constructions'. This is not meaningless. Constructing the usual set-constructions is an important problem, then and now.

6 Literally, these mean 'axiom-of-filtering-out' and 'axiom-of-replacement'. Roughly, these correspond to what nowadays are called 'Axiom of Separation' and 'Axiom of Replacement'.

7 I consciously avoid translating von Neumann's "Argument-Funktionen" as 'argument-functions', since to contemporary minds this would look misleadingly similar to the $\mathrm{dom}$-function of 1-category-theory, which is something quite different.

8 A perhaps overly charitable reading of von Neumann's original would interpret his use of 'in' in 'in diesen Bereichen' (instead of 'auf diesen Bereichen') as him here eschewing a claim that $[\cdot,\cdot]$ were a total function on a 'collection of all arguments'.

9 Beginning with this formula, von Neumann often omits the comma in the 'operation $[x,y]$. It is not clear whether this is intentional. This is also not addressed in the (short) list of errata which he published soon after. An over-interpretation would be that here von Neumann is coming close to ETCS-style notation $x\circ f$, or $xf$, with $1\xrightarrow[]{x}\mathcal{E}$ a 'global element', and both $x$ and $f$ having the same sort, called 'morphism', this, I think, would be reading to much into this line: this already begins with von Neumann still keeping the 'non-diagrammtical' order of arguments; moreover, while he in this line he indeed temporarily introduces another sort, called 'Variable', and considers both $f$ and $x$ to have this one informal sort, von Neumann here is rather writing on the meta-level: he has written explicitly that formally the first 'variable' is to be considered of sort 'Funktion' and the second 'variable' is to be considered to have the sort 'Argument'.

10 With this 'nur 2 Werte'='only 2 values' von Neumann really means $\leq 2$, since for example to construct the empty set we seem to need a function which takes only one value.

11 Relevant historical background reading on 'Bestimmtheitsaxiom's, roughly from the time of von Neumann's article provides Abraham Robinson: On the Independence of the Axioms of Definiteness. The Journal of Symbolic Logic, Vol. 4, No. 2 (Jun., 1939), pp. 69-72.

12 In a strict sense, I think that (0) the accepted answer does not answer the OP's question, (1) this is not the accepted answer's fault since (1.0) the accepted answer does not even claim to answer the OP's question, rather correctly begins with "Let me explain one sense in which using functions or sets provides exactly equivalent foundations of mathematics, in a way that is connected with some deep ideas in set theory. There is a translation back and forth between these foundational choices.", saying what the answer is and (1.1) the OP's question, I think, rests on a premise which I am inclined to deny, since mathematics for the most part, barring perhaps synthetic geometry and some proofs without words, evidently is founded on functions, or function-like ideas, (1.2) the 'why' in the OP's title is a tall order: taken seriously it would entail a frightening tangle of philosophical, psychological, physical, and what not, speculation. There certainly is not the clear-cut mathematical 'answer' for whatever this 'why' is asking a reason for. While it is conceivable that a question of form of the title of the OP might have a rather definite mathematical answer (think of someone asking 'Why aren't Zermelo's natural numbers $\{\}$, $\{\{\}\}$, $\dotsc,$ used predominantly as a model for the (much older, much more international) idea of 'number', instead of von Neumann's ordinals $\{\}$, $\{\{\}\}$, $\{ \{\} , \{\{\}\}\}$, for which there are mathematical reasons. ') , I think that this OP does not have a reasonably precise answer.

13 Perhaps one shouldn't even say 'sort' here. I briefly tried to see BNG in the framework of categorical logic, which is the field which currently uses 'sort' in a precise technical way, and it seems not to fit here. I keep it for pragmatic reasons. Saying 'type' here is not an option, for obvious reasons.

$\endgroup$
  • $\begingroup$ About your footnote 4 about von Neumann’s footnote 3 referencing his footnote 2: “(s. o. S. 220, Fußnote 2)” means “siehe oben”, so certainly an internal reference as you guessed. Moreover he really means Fußnote 1 — a misprint likely due to different pagination in his manuscript. $\endgroup$ – Francois Ziegler Sep 4 '17 at 6:19
  • $\begingroup$ [To whom it may concern: I only noticed that this thread (which had been active for so long) has been put on hold after having hit the submit-button for the recent relevant addition. By and large one should of course not work against the 'on hold' mechanism.] $\endgroup$ – Peter Heinig Oct 11 '17 at 8:43
  • 6
    $\begingroup$ If I see one more use of that tiny typeface, I'm going to edit it into oblivion. $\endgroup$ – Gerry Myerson Oct 11 '17 at 11:22
4
$\begingroup$

Actually, Jan Kuper has taken your notion seriously. In the abstract to his his paper, "An Axiomatic Theory for Partial Functions" (Information and Computation 107, 104-150 (1993)) he writes:

We describe an axiomatic theory for the concept of one-place, partial function, where function is taken in its extensional sense. The theory is rather general; i.e. concepts such as natural number and set are definable, and topics such as nonstrictness and self application can be handled. It contains a model of the (extensional) lambda calculus, and commonly applied mechanisms (such as currying and inductive definability) are possible. Furthermore, the theory is equi-consistent with and equally as powerful as $ZF$ Set Theory. The theory (called Axiomatic Function Theory, $AFT$) is described in the language of classical first order predicate logic with equality and one nonlogical predicat symbol for function application. By means of some notational conventions, we describe a method within this logic to handle undefinedness in a natural way.

Note also what Kuper says as regards the concept of function, found in the third paragraph of the Introduction, pg. 104:

The concept of function seems to be equally as fundamental as the concept of set; e.g.. notions such as natural number, set, and ordered $n$-tuple can be easily defined, using only the concepts of partial function and function application. Furthermore, a naive way of defining functions and operating on them leads to the Russell Paradox. To avoid the Russell Paradox, we develop a Zermelo-Fraenkel-like system of axioms, which gives us an intuitively very reasonable axiomatization of the concept of partial function. We want the theory to be rather general, so we allow self application and related topics (though not for all functions), we indicate a natural way to handle non-strict functions, and we add a functional form of the Axiom of Choice [see Axiom 8, pg. 139--my comment].

(This paper is a free download from Science Direct. Just google "An Axiomatic Theory for Partial Functions", and click on the appropriate website.)

I hope this helps.

$\endgroup$
  • $\begingroup$ Nice answer. But wasn't there an article about this in the Monthly just recently? That's more recent than Kuper. $\endgroup$ – Mikhail Katz Sep 14 '17 at 7:43
  • $\begingroup$ See Tom Leinster, Rethinking set theory. $\endgroup$ – Mikhail Katz Sep 14 '17 at 7:53
  • $\begingroup$ @MikhailKatz: I'm familiar with the Leinster paper, but could you provide the cite for the article in the Monthly? Thanks. Chose the Kuper paper because he (Kuper) seemed a kindred spirit to the $OP$. $\endgroup$ – Thomas Benjamin Sep 14 '17 at 11:33
  • $\begingroup$ American Mathematical Monthly 121 (2014), no. 5, 403-415 $\endgroup$ – Mikhail Katz Sep 14 '17 at 11:44
  • $\begingroup$ @MikhailKatz: Thanks. I am used to Leinster's arXiv preprint. Any signficant changes from the preprint in the _Monthly_version? $\endgroup$ – Thomas Benjamin Sep 14 '17 at 12:13

Not the answer you're looking for? Browse other questions tagged or ask your own question.