Now I am a little bit confused about the mathematical definitions: Is that all the mathematical definition must be written in form like $(A \stackrel{def}{\equiv} B)$? Can they be written in form like $(A \Rightarrow (B \stackrel{def}{\equiv} C))$?

I tried to use formal language to write the definitions, but I met some problems: Here is an example:Which forme of the definition of the restriction of a function is correct? Or are they all correct?

  • Forme 1: $g \text{ is the restriction of } f \text{ to } B \stackrel{def}{\equiv} (f \text{ is a function } \wedge g \text{ is a function } \wedge dom(g)=B \wedge \forall x (x\in B \Rightarrow g(x)=f(x)) ) $

  • Forme 2: $ ( (f \text{ is a function } \wedge g \text{ is a function }) \Rightarrow (g \text{ is the restriction of } f \text{ to } B \stackrel{def}{\equiv} (dom(g)=B \wedge \forall x (x\in B \Rightarrow g(x)=f(x)) ) ) ) $

And another question: Why can we create mathematical definition? Is there any axiom which allows us to do this?


I'm not competent in mathematical logic so take my answer with a grain of salt. If anything you should also come visit "logic room" at math.stackexchange. The following is basically my way of dealing with definitions.

In short, you come into the world of mathematics with 4 things already built-in:, language(for example First order logic with $=$,$\,\in$), rules of logic (for example Fitch-style), axioms (for example ZFC) and definitorial expansion.

The purpose of logic rules and axioms is obvious, we need some formal language like FOL to be able to formalize what we write (our proofs) in a computer. Definitorial expansion is exactly the thing that we included to be able to make new definitions and add new symbols on the fly to our language. Theoretically it is possible to be able to prove theorems using just the first two built-in symbols ($=$ and $\in$) but the theorems and definitions would be so long that you wouldn't have enough time to physically write them down.

So, to answer your last question, the thing that allows us to create definitions is called definitorial expansion, but unlike the part with axioms we didn't took it on faith, definitorial expansion is backed-up by some theorems in mathematical logic that guarantee that its use (i.e. the use of new symbols and definitions that we created by definitorial expansion) won't lead to contradiction and also wont allow us to prove something new, something, that we could not have proved without using def exapansion. So definitorial expansion is perfectly fine to use, those theorems in mathematical logic just confirm that it acts like it's supposed to act, just as a shortcut to make long sentences fit a couple of symbols.

Now, this expansion actually consists of 3 parts:

Firstly, you can add new constants to your language, constants are the objects from your universe, for example some specific sets such as $\varnothing$, here $\varnothing$ is a constant symbol.

The rule is simple, suppose you have proved $$\exists ! x\, P(x)$$ that is, you have proved $\exists x P(x)$ and you have proved $\forall x_1,x_2$ if $P(x_1)$ and $P(x_2)$ then $x_1 = x_2$, where $P$ is a formula of First-Order logic with $x$ being its only free variable.

Then you can introduce a new symbol, let's call it $c$, and two axioms: $P(c)$ and forall $y$ if $P(y)$ then $y = c.$ (where $y$ is any variable that does not appear in the formula $P$) (In my system there is one more axiom $c$ : obj, but more on it later)

For example, you can prove using the axiom of the empty set and the axiom of extensionality that $\exists ! x\, ($forall $y\, y \notin x)$ (you can see that this sentence is indeed of the form $\exists ! x P(x)$ where $P(x) := (\forall y\, y \notin x)$.

Thus you can introduce a new constant symbol $\varnothing$ and two axioms: $\forall y\, y \notin \varnothing$ and $\forall z \, (\forall y\, y \not \in z) \implies z = \varnothing$. (see, here I had to use new variable $z$ instead of $y$ this is why I added "(where $y$ is any variable that does not appear in the formula $P$)" sentence to deal with the annoying variable substitutions, I won't mention stuff like that in the following rules.

Second part is about predicates (that is, properties like $n$ is even or $f$ is continuous or $x < y$)

Here, if you have proved that "forall $x_1,x_2,\ldots x_n$ if $C(x_1,x_2,\ldots x_n)$ then $\phi(x_1,x_2,\ldots x_n)$ : bool"

or "forall $x_1,x_2,\ldots x_n \in S_1,S_2,\ldots S_n$ if $C(x_1,x_2,\ldots x_n)$ then $\phi(x_1,x_2,\ldots x_n)$ : bool"

or "forall $x_1,x_2,\ldots x_n\, \phi(x_1,x_2,\ldots x_n)$ : bool"

or "forall $x_1,x_2,\ldots x_n \in S_1,S_2,\ldots S_n\, \phi(x_1,x_2,\ldots x_n)$ : bool"

then you can introduce a new predicate-symbol $P$ and a new logic rule $x_1,x_2,...,x_n (\in S_1,S_2,..S_n) (C(x_1,...x_n)) ⊢ P(x_1,..x_n) \iff \phi(x_1,..x_n)$.

This rule should be understood as follows: you first check that $x_1,..x_n$ (which are some terms of your language FOL) are in those sets (S_1,..S_n) (if you have proved the version with the sets) and if $x_1,..x_n$ satisfy condition $C$ (if you have proved the version with condition) if they do then you can use this axiom $P(x_1,..x_n) \iff \phi(x_1,..x_n)$.

Also you have a rule that if $x_1,x_2,\ldots,x_n$ in your sets $S_1, S_2,\ldots, S_n$ and $C(x_1,x_2,...x_n)$ : bool then you can deduce that $$P(x_1,x_2,\ldots,x_n) : bool$$ once again, you don't have to check the conditions that $x_i$ are in the sets $S_i$ or that they make the condition $C$ : bool if you didn't prove the corresponding versions.

How to check whether a given formula in FOL has type :bool :

Suppose that $t_0,t_1, S_1,S_2$ are terms of your current language FOL; $A,B$ are some formulas of FOL then

$t_0, t_1$ : obj $ ⊢ t_0 = t_1$ : bool

$t_0, t_1$ : obj $ ⊢ t_0 \in t_1$ : bool

$t_0 \in S_1, t_1 \in S_2$ $⊢ t_0 = t_1$ : bool

$t_0 \in S_1, t_1 \in S_2$ $⊢ t_0 \in t_1$ : bool

$A, B$ : bool $⊢ A $ and $B$ : bool, $A$ or $B$ : bool, $A \implies B$ : bool, not $A$ : bool

$A$ : bool, if you suppose that $A$ is true and are able to deduce that $B$ : bool $ ⊢ A$ and $B$ : bool, $A \implies B$ : bool.

$(x$ : obj $⊢ \phi(x)$ : bool) $⊢ \forall x \phi(x)$ : bool, $\exists x \phi(x)$ : bool

Also there are some logic rules that work as follows:

$A$ : bool $ ⊢$ you may say "Suppose that $A$"

For example $3 = 4$ : bool, you may say "Suppose that $(3 = 4)$" and reason further saying "but $(3 \neq 4)$ thus not $(3 = 4)$". You are not allowed to say, "suppose $1/0 = 4$" because you won't be able to deduce that $1/0$ : obj.

$A$ : bool $⊢ A$ or not $A$, you may say $3 = 4$ or $3 != 4$ but you can't say $(1/0 = 4)$ or $(1/0 != 4)$.

Let us make some examples: you can deduce that $\forall x (x \in \mathbb{Z}$ and $\exists k \in \mathbb{Z}\, x = 2k)$ : bool.

This is how: I won't write it too formally but by given rules you assume that you have some term $x \in \mathbb{Z}$ and you have some term $k \in \mathbb{Z}$ and then try to deduce that $x = 2k$ : bool, Suppose you have defined $2$ to be constant (constant-symbol) such that $2 \in \mathbb{Z}$ and you have defined multiplication $\cdot$ to be a function (functional symbol) such that $\forall x,y \in \mathbb{Z}\, xy \in \mathbb{Z}$ then you may confirm that $2k \in \mathbb{Z}$ and since $\mathbb{Z}$ was another constant-symbol it is certainly a term of your language and therefore by the rule $t_0 \in S_1, t_1 \in S_2 ⊢ t_0 = t_1$ : bool you may confirm that $x = 2k$ : bool.

Thus you can define $\forall x (x$ is even $\iff x \in \mathbb{Z}$ and $\exists k \in \mathbb{Z} x = 2k)$

This will give even(1/2) = false,

Now adressing your second question, you might have wanted to have even(1/2) = undefined that is you do not even want to speak about parity of rational numbers because it makes sense only to speak about parity of integer numbers. This makes sense and generally the only distinction between predicates of the form $B$ iff $C$ and if $A$ then $B$ iff $C$ is if you want to make them be false when they don't make sense or if you don't even want to speak about them when they don't make sense (i.e. when the condition $A$ is not satisfied) I prefer the second variant so we would like to have the following definition:

$x \in \mathbb{Z}$$x$ is even $\iff \exists k \in Z\, x = 2k$

and as a special case:

$\forall x \in \mathbb{Z} (x$ is even $\iff (\exists k \in Z x = 2k)$.

The proof of its validity is the same as the previous case. Here, you won't be able to deduce that even(1/2) = false, you won't even be able to talk about even(1/2) because to talk about it you would have to be able to conclude that $\frac{1}{2} \in \mathbb{Z}$

Also you can check that you can have both your definitons from the post (forme1 and forme 2) now and to use the second one you'd first have to deduce that $f$ and $g$ are functions.

Now for the third part, functional symbols:

Suppose you have proved that $\forall x_1,x_2,\ldots,x_n$ if $P(\forall x_1,x_2,\ldots,x_n)$ then $\exists ! y \phi(\forall x_1,x_2,\ldots,x_n,y)$

From this you may add a new functional symbol $f$ and new rules

$P(x_1,x_2,\ldots,x_n)$$\phi(x_1,x_2,\ldots,x_n,f(x_1,x_2,\ldots,x_n)$ and

$P(x_1,x_2,\ldots,x_n)$$\forall y\, \phi(x_1,x_2,\ldots,x_n,y) \implies y = f(x_1,x_2,\ldots,x_n)$,

$P(x_1,x_2,\ldots,x_n)$$f(x_1,\ldots,x_n)$ : obj

the condition part $P(x_1,..x_n)$ is optional, that is you can prove that $\forall x_1,x_2,\ldots,x_n\, \exists ! y\, \phi(\forall x_1,x_2,\ldots,x_n,y)$ and use the same rules without first checking any condition $P$.

The second part allows you to also create functions via definitorial expansion (that is, set-theoretic functions that are subsets of $S \times T$ from functional symbols! This is very comfortable for practice. Suppose you have proved

$$\forall x_1,x_2,..x_n \in S_1,S_2,..S_n\, \exists ! y \in T\, \phi(x_1,..x_n,y)$$

then you can add a new functional symbolf $f$ and have axioms

$\forall x_1,x_2,\ldots,x_n \in S_1,\ldots,S_n\, f(x_1,x_2,\ldots,x_n) \in T$,

$\forall x_1,x_2,\ldots,x_n \in S_1,\ldots,S_n\, phi(x_1,x_2,\ldots,x_n,f(x_1,x_2,\ldots,x_n)$,

$\forall x_1,x_2,\ldots,x_n \in S_1,\ldots,S_n\, \forall y \in T \,\phi(x_1,x_2,\ldots,x_n,y) \implies y = f(x_1,x_2,\ldots,x_n)$

but not only that! You may also conclude that you have a term $f_0$ such that $f_0\colon S_1 \times ... \times S_n \to T$ and $\forall x_1...x_n \in S_1,..S_n\, Val(f_0,(x_1,...x_n)) = f(x_1,..x_n)$, where $Val$ is a functional symbol such that if $f$ is a function and $x$ in dom($f$) ⊢ $(x,Val(f,x)) \in f$, $Val(f,x)$ means the very same element $y$ that satifies $(x,y) \in f$. So you can denote $Val(f,x)$ as $f(x)$.

So for example you can prove that $\forall n \in \mathbb{N_{>0}}\, \exists ! y \in \mathbb{N}\, y = \frac{1}{n}$ with this you can create a functional symbol (let's call it an $f$) such that $\forall n \in \mathbb{N_{>0}}\, f(n) = 1/n$ and that there is also a term $f_0$ such that $f_0\colon \mathbb{N_{>0}} \to \mathbb{N}$ and $\forall n \in {N_{>0}}\, f_0(n) = 1/n$ basically what this means is that there is also a function that acts like this functional symbol $f$ we created.

The last thing concerning $A \stackrel{def}{\equiv} B$ or $A \stackrel{def}{=} B$ notation, which is the same as saying $(A :\equiv B)$ or $A := B$ this is just a fancy way of writing definitorial expansion

For example when we say let $\forall A\, \forall B\, A \subset B \stackrel{def}{\equiv} \forall x \in A\, x \in B$ what we really did here was that we first (implicitly) deduced that $A,B ⊢ \forall x \in A\, x \in B$ : bool and after that we used def expansion to get $A,B$ : obj $⊢ A \subset B \iff \forall x \in A\, x \in B$ or, equivalently $\forall A,B A \subset B \iff \forall x \in A\, x \in B$.

Another example when in a proof we say "let $M := \varepsilon/2$" what we are really doing here we implicitly deduce $\exists ! x\, x = \varepsilon/2$ and then we use def expansion to get constant-symbol $M$ such that it has property $P(x) := (x = \varepsilon/2)$ that is, $M = \varepsilon/2$.

Also See this How could we formalize the introduction of new notation? and this Why do we not have to prove definitions?

  • $\begingroup$ Thank you for your answers. It helps me a lot. But i also hope to see other peoples views. $\endgroup$ – Tzi yan Tschen Mar 9 at 12:01
  • $\begingroup$ @TziyanTschen Sure, just remember you can always come to the logic room, there are users far more competent in logic than me and also if you didn't understand some parts in my answer you can always ask questions here or in the logic room. I guess some practical examples of actual proofs there a lot of new definitions are made would be very helpful. I didn't include them in my post because I was exhausted at the time I was writing it but I can add some examples now or explain some things in the logic room. $\endgroup$ – famesyasd Mar 9 at 14:09

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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