role of definitions in proofs

Definitions are needed to define objects and such, however I am confused as to where definitions come from. I feel that they cannot be something that we arbitrarily define because simply saying something exists does not ensure its existence and further defining something from nothing may eventually lead to a contradiction. So it seems a strange situation that we need definitions to have something to work with and prove stuff about, and yet these definitions surely need to go thru a process of proof themselves. Can someone explain what definitions are in the most primitive sense and where they come from?

Edit: let me elaborate on my confusion, I have been reading up on different logic books and somewhere came upon a definition of proof as

"Let T be a set of first order formulas. A proof from (proper axioms) T is a finite sequence of formulas ("steps") such that every step is either a logical axiom, a member of T, or the result of applying a rule of inference to previous steps in the proof."
-a proper axiom set is for example set theory axioms.

Now from this way of defining proof, it seems like the only definitions that can be used are those of the proper axioms.

As per Henning Makholm's request, lets talk about the definition of a function. Where does the $(\forall x(x\in A\implies\exists! y((x,y)\in f))$ come from? in regards to the definition just given of proof, it is not a logical axiom nor a proper axiom. Is this something that is always assumed and therefore added to a premise in any proof?

Edit2: I think Alfred yerger answered this best in his comment.I'm not saying anyone is wrong I just got the connection after reading his comment. This makes most sense when I think about it in the context of the definition of proof I provided. Definitions are shorthand for concepts we wish to define and prove about and this comes in 2 possible ways, in the hypothesis (e.g. 'let f be a function such that...') or is the property which we try and prove some particular object has (e.g. 'show f=... is a function') in this way, the definition does not claim something exists. That happens during the hypothesis of a proof as was noted by yerger. Sorry if I was being too vague when first posing this question. I will award the answer to someone who could maybe flesh this answer out a little more and maybe provide some good special cases or instances of ways definitions come about being defined. Thank you all for the contributions and I really wish I could award more than 1 point.

Solution 1:

Definitions are just shorthand.

For example "$f$ is a function from $A$ to $B$" is shorthand, in set theory, for $$f\subseteq A\times B \land \left(\forall x(x\in A\implies\exists_1 y((x,y)\in f))\right)$$

And here, even $\exists_1$ is a shorthand.

Definitions are a way to avoid writing the same thing over and over again.

Another example: Saying "$p,q$ are prime" would be really cumbersome if we couldn't define "prime." But we can say it without the definition.

Definitions do two things: They shorten language, and they clarify what concepts are important. As a rule, we name things if we want to talk about them for more than a brief moment, because it makes our discussions so much clearer.

Solution 2:

Maybe there is a confusion here between definitions and axioms. In the former, we do not assume somethings exists when defining it, we just ascribe it a name. In the latter, we postulate that some sentence holds. Take the following example in ZFC:

$\text{Axiom of Existence}: \text{there exists a set with no elements}$

Here we postulate existence of a set with no elements, but we do not define anything. Indeed, we cannot define anything because we don't know from this axiom that there is one and only one set with no elements. Now after we postulate the following:

$\text{Axiom of Extensionality}: \text{if every element of X is an element of Y and vice-versa then X=Y}$

Now we can prove the set with no elements is unique (prove it), and because of its uniqueness we can give it a name by the following definition:

$\text{Definition: the unique set with no elements is denoted by $\emptyset$ and called the empty set}$

But now if you ask why we (arbitrarily?) postulate such axioms, the straightforward answer is: because they are useful. We could postulate others.

In another sense, however, definitions are not just abbreviations.

For instance, take Frege's (1884) famous contextual definition of 'the number of Fs':

the number of Fs = the number of Gs iff there is F and G are in one-to-one correspondence

It is easy to see that 'the number of Fs' there is not just a mere shortening of the RHS. The reason is because in those kind of definitions the definiendum and definiens are of a different logical category (For a discussion see Wright 1999).

In most cases, however, definitions are just shorthand - as others have answered before. From there comes Whitehead and Russell's view that definitions are "strictly speaking, typographical conveniences" in Principia Mathematica. One could argue then that the purpose of a definition in mathematics is its fruitfulness, and the possibility of with it make demonstrations.