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

## 1 Answer

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.

• 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
• Be sure to show this post to your advisor and discuss how it can be incorporated into your thesis. Be aware of the possibility that (the entity that contributes to MathOverflow under the user handle) James may wish to remain anonymous, but still deserves attribution for presenting the helping idea on MathOverflow. Gerhard "Working To Preserve Some Anonymity" Paseman, 2019.02.18. – Gerhard Paseman Feb 18 at 15:41