# Definition in Math or Axiom in First-Order Logic [duplicate]

I have been thinking about what definition is in math. For instance, we may define the power set as follows: for a set $$x$$, the power set of $$x$$, denoted by $$\mathcal{P}\left(x\right)$$, satisfies the following relation:

$$\mathcal{P}\left(x\right) = \left\{y \textrm{ is a set}\vert y \subseteq x \right\}.$$

This statement seems to be an axiom about the function symbol $$\mathcal{P}$$ in first-order logic. So can we say that all definitions in math are essentially axioms about new function or predicate symbols in first-order logic?

• Or relation symbols. Dec 24, 2021 at 3:50
• @NoahSchweber Predicates, right? Dec 24, 2021 at 3:51
• You need to be careful that your "definition" doesn't make new things provable. (Otherwise it's a definition/axiom hybrid). Specifically, any formula not containing the new symbol but which can be proved from math with the new definition needs to be provable without the definition. Dec 24, 2021 at 4:26
• – Karl
Dec 24, 2021 at 4:51
• There are two kinds of definitions. The kind that covers the power-set function-symbol is known as definitorial expansion/extension, described at "How could we formalize the introduction of new notation?" and also supported in the expected way in this Fitch-style foundational system. May 18, 2022 at 14:30