# Termination of “unpacking” abbreviations

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

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.

• The problem with your rank function is that $R$ is not strictly decreasing in this rank. Let's use my example: For $u,v \in \mathcal{V}$ we have $rank(u \rightarrow v) = 1$ and $rank(R(u \rightarrow v)) = rank(\neg u \vee v) = 1$. If we define an additional (senseless) operator $(\varphi \triangledown \psi)$ with $delta_{i_\triangledown} := (v_1 \rightarrow v_2) \vee (v_2 \rightarrow v_1)$ we even get $rank(u \triangledown v) = 1$ and $rank(R(u \triangledown v)) = rank((u \rightarrow v) \vee (v \rightarrow u)) = 2$. – Popov Florino Feb 13 at 1:34
• Until now I couldn't find an appropriate rank function into the natural numbers. In my complicated proof I have a rank function into $\omega^{\omega^\omega}$ (I defined it by use of a map into the Kleene closure of the Kleene closure of $I$). – Popov Florino Feb 13 at 1:59
• I see what you are saying. I incorrectly assumed each $i \in I$ was defined in terms of operators only from $I_0$. I still think it is possible to get a ranking in $\omega$. The idea would be to assign an ordinal $\beta_i$ to each $i \in I$ such that if $I$ is defined using operators $j_1 ,,,, j_k$ (repeated with appropriate multiplicity), then $\beta_i > \beta_{j_1} + \dots + \beta_{j_n}$. Then define $$rank(\langle i , \langle \phi_1, \dots \phi_n \rangle \rangle := max(rank(\phi_1),\dots,rank(\phi_n)) + \beta_i$$. R should now be strictly decreasing. – James Feb 13 at 4:18
• In your case of $\nabla$, it would need to be assigned an ordinal $\beta$ of at least $6 > 2 + 1 + 2$, the sum of the ordinals assigned to $\rightarrow$, $\vee$ and $\rightarrow$. I'm not sure if this will make you own proof any easier. You will still need to do an induction on the complexity of definitions. – James Feb 13 at 4:30