Semantics and Logical structure in Definitions

Solution 1:

Some theory

See George Tourlakis, Lectures in Logic and Set Theory. Volume 1 : Mathematical Logic (2003), I.7. Defined Symbols, page 112-on :

We start with a theory $\Gamma$, spoken in some basic formal language $L$. As the development of $\Gamma$ proceeds, gradually and continuously we extend $L$ into languages $L_n$, for $n ≥ 0$ (we have set $L_0 = L$). The theory itself is being extended by stages, as a sequence $\Gamma_n$, $n ≥ 0$. [...] At that same stage we also add to $\Gamma_n$ the defining nonlogical axiom of the new symbol in question.

Specifically, if $\varphi(x_1, ..., x_n)$ is some formula, we then can introduce a new predicate symbol “$P$” that stands for $\varphi$.

This entails adding $P$ to $L_k$ as a newn-ary predicate symbol, and adding

$P(x_1, ... x_n) ↔ \varphi(x_1, ..., x_n)$

to $\Gamma_k$ as the defining axiom for $P$.

Thus, we can start with the formula $\varphi(n) := \exists y(n = 2 \times y)$ and extend the "basic" language with the new predicate $Even(n)$ and the theory with the defining axiom :

$Even(n) \leftrightarrow \exists y(n = 2 \times y)$.

This is "implicitly" universally quantified, i.e. : $\forall n [Even(n) \leftrightarrow \exists y(n = 2 \times y) ]$.

Comment

About the natural language, my "feeling" is that :

a number $n$ is even if it is divisible by $2$

is a "correct" form for a definition; "a number $n$" must be interpreted as "a number $n$ whatver" i.e. as having $n$ universally quantified.

I would prefer to "read" :

every number $n$ is even if it is divisible by $2$

as meaning : "for every number $n$, $n$ is even if it is divisible by $2$", which amount to the same statement.

Question (1) :

when trying to prove "$x$ is even" what exactly should I do ?

$Even(n)$ is defined as : $\exists y(n = 2 \times y)$; thus, proving that e.g. $6 = 2 \times 3$, by rule of logic we can derive : $\exists y(6 = 2 \times y)$, which - by definition - is :

$Even(6)$.

Question (2) :

suppose $R$ is a partial order on a set $A, B⊆A$, and $b∈B$. Then $b$ is called an $R$-smallest element of $B$ (or just a smallest element if $R$ is clear from the context) if $∀x∈B(bRx)$. How do I express this definiton in logical symbols(are $A,b,B,R$ free or bound?)?

See Tourlakis, cit, page 114 :

In this case we have to add a new $n$-ary function symbol $f$ into $L_k$ by a definition. That is, we add $f$ to $L_k$ and also add the following formula to $\Gamma_k$ as a new nonlogical axiom:

$y = f(y_1, ... y_n) ↔ \varphi(y, y_1, ... y_n)$

provided we have a proof in $\Gamma_k$ of the formula : $(∃!y) \varphi(y, y_1, ... y_n)$.

In our example, assuming for simplicity that we have already introduced with a definition the symbol $PO(x,y)$ as an abbreviation for "$x$ is a Partial Order on $y$", we can introduce the following symbol $min(x,y,z)$ as an abbreviation for "the smallest element of $z$ for the relation $x$ on $y$" by the definition :

$\forall R \forall A \forall B \forall b \quad [ b = min(R,A,B) \leftrightarrow (R \subseteq A \times A \land PO(R,A) \land B \subseteq A \land b \in B \land \forall x (x\in B \rightarrow bRx)) ]$

Now, according to this definition, the answer to the question :

what should I do if I want to prove that $z$ is a $H$-smallest element of $M$ ?

is straightforward. You have to prove that, for $z \in M$ :

$\forall x (x\in M \rightarrow zHx)$.