It is a normal practice to use a minimal set of operators in logical systems and construe the other operators as abbreviations.
Let's look at the propositional logic:
If $\mathcal{V}$ denotes the set of variables $v_0, v_1, \dots$ we can define the set of propositional formulas as the smallest set $L_0 \supseteq \mathcal{V}$ of strings closed under building the negation and the conjunction. So we have: $$L_0 = \mathcal{V} \cup \{\neg \varphi \,;\, \varphi \in L_0\} \cup \{(\varphi \wedge \psi) \,;\, \varphi,\psi \in L_0\}$$ Then we introduce $(\varphi \vee \psi)$, $(\varphi \rightarrow \psi)$ and $(\varphi \leftrightarrow \psi)$ iteratively as abbreviations for $\neg(\neg \varphi \wedge \neg \psi)$, $(\neg \varphi \vee \psi)$ and $((\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi))$, respectively. We can be more exact and define an extended set of formulas $L$ such that $$L = \mathcal{V} \cup \{\neg \varphi \,;\, \varphi \in L\} \cup \{(\varphi \ast \psi) \,;\, \ast \in \{ \wedge,\vee,\rightarrow, \leftrightarrow \}, \varphi,\psi \in L\}$$ and define the "one-step-reduction" $R : L \to L$ recursively by $$\alpha \mapsto \begin{cases} \alpha , & \alpha \in \mathcal{V} \\ \neg R(\varphi), & \alpha = \neg\varphi \\ (R(\varphi)\wedge R(\psi) ), & \alpha = (\varphi \wedge \psi) \\ \neg(\neg \varphi \wedge \neg \psi), & \alpha = (\varphi \vee \psi) \\ (\neg \varphi \vee \psi), & \alpha = (\varphi \rightarrow \psi) \\ ((\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi)), & \alpha = (\varphi \leftrightarrow \psi) \\ \end{cases}$$
Proposition 0: For all $\alpha \in L$ exists an $n \in \mathbb{N}$ such that $$R^n(\alpha) \in L_0$$ Therefore we can define a "reduction" $Red : L \to L_0$ by $$\alpha \mapsto R^d(\alpha), \quad\text{where } d := \min \{n \in \mathbb{N} \,;\, R^n(\alpha) \in L_0\}$$
In my diploma thesis I needed a more general result:
Let $\langle a_1, \dots, a_n \rangle$ denote the $n$-tuple of $a_1, \dots, a_n$. We define $\mathcal{V} := \{v_k \,;\, k \in \mathbb{N}\}$, where $v_k := \langle 0, k \rangle$ (solely to be sure that variables are distinct from the other formulas I'll define).
Choose a set $I \subseteq \mathbb{N}\setminus \{0\}$ of "operators". We assign an arity $n_i \in \mathbb{N}$ to each operator $i \in I$. Now we can define a set of formulas $L$ such that: $$L = \mathcal{V} \cup \{\langle i, \vec{\varphi} \rangle \,;\, i \in I, \vec{\varphi} \in L^{n_i}\}$$ So the "application" of an operator $i \in I$ to formulas $\varphi_1, \dots, \varphi_{n_i}$ is given by $\langle i, \langle \varphi_1, \dots, \varphi_{n_i} \rangle \rangle$. The "operators used in a formula" are determined by $$ \operatorname{op} : L \to \mathcal{P}(I), \alpha \mapsto \begin{cases} \emptyset, & \alpha \in \mathcal{V} \\ \{i\} \cup \bigcup_{1 \le k \le n_i} \operatorname{op}(\varphi_k), & \alpha = \langle i, \langle \varphi_1, \dots, \varphi_{n_i} \rangle \rangle \end{cases}$$
Some of the operators $I_0 \subseteq I$ we call primary operators. The set of "primary" formulas $L_0$ is determined by: $$L_0 = \mathcal{V} \cup \{\langle i, \vec{\varphi} \rangle \,;\, i \in I_0, \vec{\varphi} \in L_0^{n_i}\}$$
For each non-primary operator $i \in I \setminus I_0$ choose a "defining formula" $\delta_i$ (that contains exactly the variables $v_1, \dots , v_{n_i}$) such that the relation ${\prec} \subseteq I \times I$ given by $$ i \prec j \quad\text{:iff}\quad j \in I \setminus I_0 \text{ and } i \in \operatorname{op}(\delta_j) $$ is well-founded. (This prevents circular "operator definitions".)
If we define for $\vec{\psi} = \langle \psi_1, \dots, \psi_{n} \rangle \in L^n$ a substitution $\operatorname{Sub} : L \to L, \alpha \mapsto \alpha[\vec{\psi}]$ by $$ \alpha[\vec{\psi}] = \begin{cases} \psi_k, & \alpha = v_k, \ k \in \{1,\dots,n\} \\ \alpha, & \alpha = v_k, \ k \notin \{1,\dots,n\} \\ \langle i, \langle \varphi_1[\vec{\psi}], \dots, \varphi_{n_i}[\vec{\psi}] \rangle \rangle, & \alpha = \langle i, \langle \varphi_1, \dots, \varphi_{n_i} \rangle \rangle \\ \end{cases} $$ we can "unpack" an $\langle i, \vec{\varphi} \rangle$ with $i \in I \setminus I_0$ to $\delta_i[\vec{\varphi}]$. More precisely: We define the "one-step-reduction" $R : L \to L$ by $$\alpha \mapsto \begin{cases} \alpha , & \alpha \in \mathcal{V} \\ \langle i, \langle R(\varphi_1), \dots, R(\varphi_{n_i}) \rangle \rangle , & \alpha = \langle i, \langle \varphi_1, \dots, \varphi_{n_i} \rangle \rangle, i \in I_0 \\ \delta_i[\vec{\varphi}] , & \alpha = \langle i, \vec{\varphi} \rangle, i \notin I_0 \\ \end{cases}$$
Then we get the analogue of Proposition 0.
Proposition 1: For all $\alpha \in L$ exists an $n \in \mathbb{N}$ such that $$R^n(\alpha) \in L_0$$ Therefore we can define a "reduction" $Red : L \to L_0$ by $$\alpha \mapsto R^d(\alpha), \quad\text{where } d := \min \{n \in \mathbb{N} \,;\, R^n(\alpha) \in L_0\}$$
Intuitively it is almost obvious that Proposition 1 (and 0) is true. But the proof of it in my thesis is quite complicated (I defined 6 other well-founded relations including a relation on the Kleene closure of the Kleene closure of $I$). My question is therefore:
Does someone have an idea for a simpler proof or is there a common theorem which I can use here?
Remark:
To see that Proposition 1 is a generalisation of Proposition 0:
- Let $I = \{i_\neg, i_\wedge, i_\vee, i_\rightarrow, i_\leftrightarrow\}$ be an arbitrary subset of $\mathbb{N}\setminus \{0\}$ with 5 elements
- $I_0 := \{i_\neg, i_\wedge\}$
- $n_{i_\neg} := 1$ and $n_i := 2$ for $i \in I \setminus \{i_\neg\}$
- write $\neg \varphi$ for $\langle i_\neg, \langle \varphi \rangle \rangle$ and $(\varphi \ast \psi)$ for $\langle i_\ast, \langle \varphi, \psi \rangle \rangle$ if $\ast \in \{\wedge, \vee, \rightarrow, \leftrightarrow\}$
- define $\delta_{i_\vee} := \neg (\neg v_1 \wedge \neg v_2)$, $\delta_{i_\rightarrow} := (\neg v_1 \vee v_2)$ and $\delta_{i_\leftrightarrow} := ( (v_1 \rightarrow v_2) \wedge (v_2 \rightarrow v_1) )$
