9
$\begingroup$

In first order logic it is common (and just about necessary) to introduce new symbols which have been defined in terms of the "fundamental" symbols of a given theory. For instance, the signature of set theory is often defined as containing only a binary relation symbol $\in$, but then one quickly adds the constant symbol $\emptyset$, binary relation $\subseteq$, unary function $\mathcal{P}$, and so on. As another example, one can develop the theory of linear orders using the partial order $\leq$ as the fundamental symbol, satisfying the axioms of reflexivity, antisymmetry, transitivity, and totality, and then define $x < y$ to mean $x \leq y \wedge x \neq y$; or one can start with $<$ as the fundamental symbol, satisfying the axioms of irreflexivity, transitivity, and trichotomy, and then define $x \leq y$ to mean $x < y \vee x=y$; the claim is that the resulting theories are equivalent.

These all seem clear enough, but I'm trying to put together a set of rules for how to do this in general, and haven't found such a set in the books I have on my shelf (Srivastava's Course in Mathematical Logic, Enderton's Mathematical Introduction to Logic, and Manin's Course in Mathematical Logic for Mathematicians). Here's what I think works:

  • To define a new constant symbol $\alpha$, characterized by the formula $\phi(\alpha)$ having $\alpha$ as the only free variable, one first proves $\exists! x: \phi(x)$. A formula $\psi(\alpha)$ is then interpreted to mean $\forall v: (\phi(v) \rightarrow \psi(v))$, where $v$ is not free in $\psi$. As an example, to define the symbol 0 in the theory of rings, one uses the formula $\phi(0)$ given by $\forall x: (x+0=x \wedge 0+x=x)$; the theorem $\forall x: 0 \cdot x = 0$ is then interpreted as $$ \forall x: \forall y: [\forall x: (x+y=x \wedge y+x=x) \rightarrow y \cdot x = y]. $$
  • To define a new relation $R(x_1,\dots,x_n)$ whose free variables are a subset of $\{x_1, \dots, x_n\}$, characterized by the formula $\phi(x_1, \dots,x_n)$, one interprets any formula $\psi$ using $R$ by replacing each occurrence of $R$ with $\phi$. This is probably the most straightforward of the three rules. For example, if one defines $x < y$ to mean $x \leq y \wedge x \neq y$, then the axiom $\forall x: \forall y: (x < y \vee y < x \vee x \neq y)$ is interpreted as $$ \forall x: \forall y: [(x \leq y \wedge x \neq y) \vee (y \leq x \wedge y \neq x) \vee x=y]. $$
  • To define a new function $f(x_1,\dots,x_n)$ by the formula $\phi(x_1,\dots,x_n,y)$, one proves $\forall x_1: \dots \forall x_n: \exists! y: \phi(x_1,\dots,x_n,y)$. To interpret formulas involving $f$, it suffices by recursion to interpret atomic formulas $R(t_1,\dots,t_k)$ where $R$ is a relation and $t_1,\dots,t_k$ are terms. Suppose that among the terms $t_1,\dots,t_k$ there are $m$ occurrences of the symbol $f$, of the form $f(a_j^{(1)},\dots,a_j^{(n)})$ for $j=1,\dots,m$. Let $v_1, \dots, v_m$ be variables not used in $t_1,\dots,t_k$. Let $t_1',\dots,t_k'$ be the terms obtained by replacing the occurrences of $f$ by $v_1,\dots,v_m$. Then the formula $R(t_1,\dots,t_k)$ is interpreted as $\phi(a_1^{(1)}, \dots, a_1^{(n)},v_1)\wedge \dots \wedge \phi(a_m^{(1)},\dots,a_m^{(n)},v_m) \wedge R(t_1',\dots,t_n')$. As an example, in group theory one uses the theorem $\forall x: \exists! y: x \cdot y = e$ to define a unary function $^{-1}$, and the theorem $\forall x: \forall y: (x \cdot y)^{-1} = y^{-1} \cdot x^{-1}$ is interpreted as $$\forall x: \forall y: \exists u: \exists v: \exists w: [(x \cdot y) \cdot u = e \wedge y \cdot v = e \wedge x \cdot w = e \wedge u = v \cdot w ].$$

Questions:

  • Is this correct?
  • Is there a more efficient way to do this (especially the bit about functions)?
$\endgroup$
  • $\begingroup$ The "basic rule" for a $n$-ary functional symbol (constants are $0$-ary functional symbols) is : we can add a new nonlogical axiom $y = f(y_1 . . . y_n) \leftrightarrow Q (y, y_1, . . . , y_n)$, provided we have a proof of the formula $(\exists! y) Q(y, y_1, . . . , y_n)$. So, e.g. in set theory, we have : $y = \emptyset \leftrightarrow (\forall x)x \notin y$. $\endgroup$ – Mauro ALLEGRANZA Feb 11 '14 at 13:08
4
$\begingroup$

What you've written looks along the right lines.

New relational expressions can be thought of as mere shorthand. But we have to be careful introducing new constants, to ensure they have a denotation (or at least, we have to do that in standard FOL, where empty terms are not allowed). Likewise, we have to be careful introducing new function expression to define them in terms of relations which are (provably) functional. Which is why those two cases involve some fussing.

There's a pretty clear and careful treatment of these matters in another standard text, namely Mendelson's Introduction to Mathematical Logic, 4ed §2.9. (Indeed, having now checked, this seems to be a just a resetting of §2.9 of the first edition.)

$\endgroup$

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.