# Must mathematical definitions be formal? If so, why?

Recently on Math SE, I offered the following definition of a "pre-function":

A pre-function f from X to Y will be defined as a "function" which in general is not well-defined.

This was rejected by other users, apparently because it was not a "formal" definition.

My question is this: Must mathematical definitions be formal? If so, why?

• Your pre-function is a relation and - except for the fact that makes little sense to "change name" to something that is already widely used - it seems to me "formally" correct. Commented Feb 27, 2016 at 14:02
• You say correctly that "xfy iff (x,y)∈f". But "xfy=ufv" is not, because xfy, i.e. (x,y)∈f is a formula, i.e. a statement and not a term (i.e. a name) and in the language of set theory equality (=) is defined between objects (i.e. sets) and not between formulae. We have that (x,y)=(u,v) iff x=u and y=v, because equality between sets holds when the sets have the same elements, and the def of ordered pair ensures that two couples are equal exactly when ... Commented Feb 27, 2016 at 16:15
• I'm voting to close this question as off-topic because this seems to hinge completely on the use of terms as defined with the specific discipline math. (i.e., it's not asking anything deep about the nature of defining and as such is not really a good fit philosophy.SE -- instead it ought to fit better with math.SE (but I can't answer for why if they think it does not fit)) Commented Mar 2, 2016 at 10:43
• @ChrisSunami thanks for doing the work to make this a better question. I've removed my close. Commented Mar 2, 2016 at 22:38
• Here is a definition of what a mathematical definition is. This is the info you're missing. A mathematical definition must have some specific properties; and if it lacks those properties, it's not a definition. abstractmath.org/MM/MMDefs.htm Commented Mar 3, 2016 at 0:40

It depends at the level you're working on; mathematics has a body of work that is precise: like the theory of groups or vector spaces.

But before a notion becomes formalisable it is informal, vague and imprecise.

For example the notion of space, can be traced back to Liebniz's analysis situ - a notion that has many different formal avatars: differential manifolds, sheaves, topological spaces and sites.

Another example drawn from contemporary mathematics is the field of one element; a field being a certain mathematical structure where one can add, multiply or divide without limit; so the integers aren't a field, since one divided by two is a fraction and not an integer; the NLab go on to say:

various phenomena in the context algebraic/arithmetic geometry over finite fields [with a size n] can be seen as reflecting interesting facts when one extrapolates to the case n=1, even though, of course, there is no such field; since all fields have 1 & 0 distinct [so must have at least two elements].

In fact, there is such a field! It's just 0; with the obvious operations

0+0=0

0 x 0 = 0

0/0 =0

However including such a field in the usual idea of a field spoils other properties that are important; so it's best excluded by stipulating 1 & 0 are distinct; and this is why that stipulation is there; hence this isn't the object that one looks for when is looking for this field of a single element.

So here we have an object, which is precisely named as the field of one element; and whose theory is named as absolute geometry; whose possible properties are well-defined, but no object *at first * is there...it must be found, invented, or discovered.

Arguably, formal definitions --ones that are strict and unambiguous --are foundational to mathematics. To phrase that in another way, mathematics IS formal definitions, and the relationships between them.

We can see why if we take a look at your proposed definition:

A pre-function f from X to Y will be defined as a "function" which in general is not well-defined.

On the face of this, it looks plausible. We picture the set of all functions, and divide it into two exclusive subsets. One subset is well-defined functions, the other set then becomes "pre-functions." But for something to be considered a mathematical function, it must be well-defined, therefore the other subset is empty.

So now we're creating a new category, "functions," (with the scare quotes) which includes actual functions as well as "pre-functions." But what is a function if not what mathematics defines it as? It looks like you're looking at mappings from X to Y. You mean all non- well-defined mappings from X to Y. But what exactly does that mean?

The questions go on and on. Eventually you either end up well-defining your concept formally, or you finish with something that isn't appropriate for mathematical usage, because it is ambiguous, and subject to interpretation.

• I have two questions, (1) Why formal definitions are unambiguous? So for as I know definitions are just strings of some symbols which are basically 'meaningless'. Their meaning depend on our interpretation of them in model. How can then the question of unambiguity of these definitions be satisfactorily answered?
– user13627
Commented Mar 3, 2016 at 13:03
• (2) Suppose that we are trying to 'construct' the mathematical object called 'pre-function'. We know what a function is. Say that it satisfies properties a, b and c where we take property c as "well-definedness". Now can't we say that if a mathematical object satisfies a and b we will call it a pre-function? If not then why not?
– user13627
Commented Mar 3, 2016 at 13:03
• @user170039 well-defined just means that the particular object you're considering has all the necessary properties to be a function. Well-definedness is trivial if you consider the whole class of functions. Using your example, it's impossible for any object to satisfy a and b but not c, because property c is equivalent to "a and b".
– Era
Commented Mar 3, 2016 at 15:07
• @Era: I don't understand your example. Can you clarify a bit?
– user13627
Commented Mar 3, 2016 at 17:32
• @user170039 The idea is that ALL mathematical functions are "well-defined." A non-well-defined function is like a married bachelor. The reason formal definitions are (mostly) unambiguous is because they are painstakingly built step by step from very simple foundations. It's possible that the simple foundations might change (for instance, Euclid's axioms) but at least no additional ambiguity is added along the way. Compare your definition, which adds a great deal of new ambiguity to the idea of "function." Commented Mar 3, 2016 at 17:38

When we say formal we mean "of or relating to logical form as opposed to function or meaning" (ty Google dictionary). A formal definition is one which relates the subject matter to some statement of logic. For instance `if x > 2 then y is 4` is a logical statement. If we define `f(x) = 4 | x in {x > 2}` then we have a formal definition of `f`. It's even formal to say that `f(x) = {} | x in {}` - this is known as the empty function. Even simple operations like addition are functions! Expressions, which utilize operators, cannot exist, except as free-floating numbers or symbols. This helps to explain why so many posters have focused on relating this back to functions: without the concept of a function (which is formal and well-defined by definition) it is impossible to do what you and I would call "math" - all that remains is free-floating numbers, whose definitions are no more "mathematical" than are the definitions of bachelors or garbage trucks.

I'd be curious to hear an example of a definition which is mathematical but not formal, but as of now I don't think it's possible, given what we mean by mathematical and what we mean by formal.