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



Termination of "unpacking" abbreviations
A simple idea which might neaten your proof is to define a notion of the "rank" of a formula, which measures the nesting non-primary operators used in the inductive definition of that formula. 


This rank can be defined by induction on formulas by: 


* $rank(\varphi) := 0$ for $\varphi \in L\_0$
* $rank(\langle i , \langle \varphi\_1 , \dots , \varphi\_n \rangle \rangle) := max\{rank(\varphi\_1),\dots ,rank(\varphi\_n)\}$ for $i$ a primary operator.
* $rank(\langle i , \langle \varphi\_1 , \dots , \varphi\_n \rangle \rangle) := 1 + max\{rank(\varphi\_1),\dots ,rank(\varphi\_n)\}$ for $i$ a non-primary operator.


Every formula is thus assigned a rank in $\mathbb{N}$. Now just prove $R$ is strictly decreasing in rank.




---


Please note the comments. 


