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)?
