3
$\begingroup$

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?

$\endgroup$
7
  • 2
    $\begingroup$ Or relation symbols. $\endgroup$
    – Noah Schweber
    Dec 24, 2021 at 3:50
  • $\begingroup$ @NoahSchweber Predicates, right? $\endgroup$
    – Ziqi Fan
    Dec 24, 2021 at 3:51
  • 1
    $\begingroup$ 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. $\endgroup$
    – TomKern
    Dec 24, 2021 at 4:26
  • 2
    $\begingroup$ See extension by definitions. $\endgroup$
    – Karl
    Dec 24, 2021 at 4:51
  • 4
    $\begingroup$ 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. $\endgroup$
    – user21820
    May 18, 2022 at 14:30

0

Reset to default

Browse other questions tagged .