1
$\begingroup$

I just want to ask a very elementary question.

When we introduce a "definition" in a first order logical system. For example when we say

Define: $Empty(x) \iff \not \exists y (y \in x) $

Isn't that definition itself an "axiom", call it a definitional axiom.

I'm asking this because the one place predicate symbol Empty() is actually new, it is not among the listed primitives of say Zermelo, which has only identity and membership as primitive symbols.

So when we are stating definitions are we in effect stating axioms? but instead of being about characterizing a primitive, they are definitional axioms giving a complete reference to a specified set of symbols in the system.

Is that correct?

Now if that is the case, then why we don't call it axiom when we state it, I mean why we don't say for example:

Definitional axiom 1) $Empty(x) \iff \not \exists y (y \in x)$

Zuhair

Improve this question
$\endgroup$
  • $\begingroup$ They are axioms in the sense that they tie a term to a condition. They are not really assumptions baked into a model of reality; these are true axioms (e.g. the parallel postulate). $\endgroup$ – ncmathsadist Feb 7 '19 at 12:48
  • $\begingroup$ I mean syntactically speaking, or lets say formally speaking what are we to classify those definitional statements, aren't they axioms??? $\endgroup$ – Zuhair Feb 7 '19 at 12:50
  • $\begingroup$ I would refer to them as "definitions," as distinct from "axiom" in the sense I have stated it. $\endgroup$ – ncmathsadist Feb 7 '19 at 12:52
  • $\begingroup$ I see, so you have another category of sentences inside a formal system (by formal system I mean the syntactical part of an axiom system), so we have theorems, axioms, and definitions, but how you can account for those, the syntactical side understands no semantics at all. $\endgroup$ – Zuhair Feb 7 '19 at 12:54
  • $\begingroup$ Unlike the addition of an axiom, the addition of a definition doesn't change the formal system, it just attaches a name to a certain property which already existed in the formal system. ZFC with the definition of ${\rm Empty}$ added is still ZFC. No theorems become true or false by the addition of the definition, and any new theorems stated with the symbol can be equivalently stated in the original system by replacing the symbol with its definition. $\endgroup$ – user856 Feb 7 '19 at 12:59
1
$\begingroup$

A definition can indeed not be proven nor disproven and can be considered an axiom.

Improve this answer
$\endgroup$
  • $\begingroup$ I know that we can add them as axioms. But I think that syntactically (formally) speaking, actually they are axioms. $\endgroup$ – Zuhair Feb 7 '19 at 12:52
  • 1
    $\begingroup$ @Zuhair: did I contradict this ? By the way, you probably mean semantically. Syntactically, nothing distinguishes the proposition $p$ from the axiom $p$. $\endgroup$ – Yves Daoust Feb 7 '19 at 12:53
  • $\begingroup$ there is, axiom p is not provable in the system from other sentences. while theorems are. (I mean formally). $\endgroup$ – Zuhair Feb 7 '19 at 12:55
  • $\begingroup$ @Zuhair: why do you keep repeating what has already been said ? $\endgroup$ – Yves Daoust Feb 7 '19 at 13:00
  • 1
    $\begingroup$ Possibly the way how I wrote it render's it an axiom, there are other ways to introduce a definition like meta-theoretically as a string substitution rule, like in saying that the string "empty(x)" can substitute the string "$\not \exists y (y \in x)$", so this way "empty(x)" would be a meta-theoretic abbreviation of "$\not \exists y (y \in x)$", I think this kind of introduction rule on meta-theoretic level is not axiomatic. $\endgroup$ – Zuhair Feb 8 '19 at 11:05
0
$\begingroup$

I've already asked myself this question, and comparing my knowledge with other people opinions, I found that the answer is no.

Definitions are not axioms; definitions are simply shorthands of a bigger and longer string of symbols.

For example, in set theory we always see that the espression "$x \subseteq y$" is defined as: $$x \subseteq y \Longleftrightarrow \forall z(z \in x \Rightarrow z \in y ). $$

Note that between "$x \subseteq y$" and "$\forall z(z \in x \Rightarrow z \in y)$" there is the "$\Longleftrightarrow$" (I used the longer version to emphasise that the statement is a definition).

But this statement is written in our imaginary "computer" or "piece of paper" where it's written all the mathematics (at least, I like to think about it like that), where everything is either an axiom or something proved using the axioms or the theorems proved before, this statement should be a theorem or an axiom too.

So, formally thinking about it, it should be a theorem or an axiom. It isn't a theorem, because it hasn't been proved, so it should be an axiom. So giving this statement, it looks like we are adding a new axiom to our theory, and this would mean that all the definitions that have been given in mathematics history are axioms! This wouldn't make sense.

What is really going on here, is that the statement is actually an abbreviation for a longer string of symbols, namely "$\forall z(z \in x \Rightarrow z \in y)$". Abbreviations are required to talk in an easier way of mathematical relations. Formally speaking, shorthands of symbols are a "new" informal version of the formal language symbols.

Usually, mathematics is done in an informal level, or at least not as formally as when we give the axioms of mathematics. The axioms are stated in a formal language, but then nothing stop us to use abbreviations of them and still do mathematics correctly. Somethimes, in proofs or definitions, we even use our informal natural language.

So definitions -at least in high level mathematics- are not given in a formal level. We could consider them some "meta"-statements that makes the formal language of the theory more comfortable to us. Even if you don't like to see it like that, at least we know for sure that definitions tend to make the the mathematical language more and more informal. But remember that hidden behing those shorthands, there are a lot of mathematical formal strings! Take for example the definition of limit,

$$\lim_{x \to c} f(x) = L \Longleftrightarrow_{def} \forall \epsilon \in \mathbb{R^+} \exists \delta \in \mathbb{R^+} \forall x \in D: \big(0 < \mid x-c \mid < \delta \Rightarrow \mid f(x) - L \mid < \epsilon \big)$$ it is an abbreviation of a very complicated string of symbols -that are shorthand themselves-! So, when you are proving that $$\lim_{x \to 2}x^2 = 4$$ you are really proving all that complicated stuff with the $\epsilon$-$\delta$ definition of limit with $f(x)=x^2, c= 2$ and $L=4$.

We could consider also the definition of definite integral, that is a new term that we introduce to abbreviate a much more complicated one (a limit). In that case, what is being defined is a term, so we use the equality simbol $=$, but it's the same idea that we use with $ \Longleftrightarrow.$ It's just a shorthand.

In conclusion, if you want to be clear in a formal point of view, I personally would mark that the statement is a definition using $\Longleftrightarrow_{def}$ and $=_{def}$ (as I used before for the limit definition), so that you can clearly see that the expression is not a strictly formal string of symbols anymore and it's rather an abbreviation.

I hope this helps :D

Improve this answer
$\endgroup$

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