Applications of the analogy between formulas and exponential polynomials to equivalence and normal forms

TL;DR

This paper explores the analogy between formulas and exponential polynomials to develop methods for formula equivalence, isomorphism, and normal forms, applicable in both classical and intuitionistic logic.

Contribution

It introduces a novel approach linking formulas to exponential polynomials, enabling new techniques for proving equivalence and constructing normal forms.

Findings

A method for proving formula isomorphism and equivalence via inequality checks

A constructive analogue of the arithmetical hierarchy using exp-log normal form

Results valid in both intuitionistic and classical logic

Abstract

We show some applications of the formulas-as-polynomials correspondence: 1) a method for (dis)proving formula isomorphism and equivalence based on showing (in)equality; 2) a constructive analogue of the arithmetical hierarchy, based on the exp-log normal form. The results are valid intuitionistically, as well as classically.

Equations

$$\varphi \cong \psi$$

$$\lambda x.M(Nx){=}_{\beta \eta }\lambda x.x\text{ and }\lambda y.N(My){=}_{\beta \eta }\lambda y.y.$$

$$\varphi \cong \psi \to {\mathbb{N}}^{+}\models \varphi =\psi ,$$

$$\text{HSI}⊢\varphi \dot{=}\psi \to \varphi \cong \psi .$$

$$\varphi$$

$$\varphi +\psi$$

$$(\varphi +\psi )+\xi$$

$$\varphi \psi$$

$$(\varphi \psi )\xi$$

$$\varphi (\psi +\xi )$$

$${\mathbb{N}}^{+}\models \varphi =\psi \nrightarrow \text{HSI}⊢\varphi \dot{=}\psi .$$

$$\left({\chi }_4\Rightarrow \left({\chi }_3\Rightarrow {\chi }_1\right)\vee \left({\chi }_3\Rightarrow {\chi }_1\right)\right)\wedge \left({\chi }_3\Rightarrow \left({\chi }_4\Rightarrow {\chi }_2\right)\vee \left({\chi }_4\Rightarrow {\chi }_2\right)\right),$$

$$\left({\chi }_3\Rightarrow \left({\chi }_4\Rightarrow {\chi }_1\right)\vee \left({\chi }_4\Rightarrow {\chi }_1\right)\right)\wedge \left({\chi }_4\Rightarrow \left({\chi }_3\Rightarrow {\chi }_2\right)\vee \left({\chi }_3\Rightarrow {\chi }_2\right)\right).$$

$${\mathbb{N}}^{+}\models \varphi =\psi$$

$$\varphi \cong \psi$$

$$\text{HSI}⊢\varphi \dot{=}\psi \leftrightarrow \varphi \cong \psi \leftrightarrow {\mathbb{N}}^{+}\models \varphi =\psi ,$$

$$\mathcal{L}\ni \varphi ,\psi$$

$$\Lambda \ni \lambda ,\mu ,\nu$$

$${\sigma }^{\tau }=\exp (\tau \log \sigma )$$

$$\mathbf{\Pi }\ni \gamma$$

$$\mathbf{\Sigma }\ni \beta$$

$$\forall x(\varphi \wedge \psi )$$

$$\exists x(\varphi \vee \psi )$$

$$\exists x\varphi \Rightarrow \psi$$

$$\psi \Rightarrow \forall x\varphi$$

$$\mathbf{\Pi }\ni \gamma$$

$$\mathbf{\Sigma }\ni \beta$$

$${\mathbf{\Pi }}_0\ni \gamma$$

$${\mathbf{\Sigma }}_0\ni \beta$$

$${\mathbf{\Pi }}_{\mathbf{n}+1}\ni \gamma$$

$${\mathbf{\Sigma }}_{\mathbf{n}+1}\ni \beta$$

Full text

1. Introduction

The language of propositional formulas bears a striking similarity to the languages of exponential polynomials, when one identifies $\phi\vee\psi$ with $\phi+\psi$, $\phi\wedge\psi$ with $\phi\times\psi$, $\psi\Rightarrow\phi$ with $\phi^{\psi}$, and atomic propositions $\chi_{i}$ with variables. This algebraic notation for formulas is often used in categorical logic and type theory [9], however some of the deeper logical implications of the analogy between formulas and exponential polynomials are seldom pointed out. In this paper, we review some of the logical implications in relation to formula equivalence, formula isomorphism, and formula normal forms.

We first deal with the propositional case and later, in Section 3, we will extend the analogy between formulas and exponential polynomials to the first-order case. We work in the context of intuitionistic logic, but, since the results are about formula equivalence, they are also relevant classically.

Central will be the notion of formula isomorphism, defined as an extension of intuitionistic equivalence—purely logical equivalence with no use of extra-logical axioms such as induction, choice, Church’s thesis, etc.—with a property expressing that the equivalent formulas, when seen as sets of their proofs, have isomorphic structures. To be concrete, we will use the language of typed lambda calculus and the associated $\beta$-$\eta$-equality relation to denote extensional equivalence between natural deduction trees that represent proofs. We define the isomorphism between formulas $\phi$ and $\psi$ by

[TABLE]

This definition of isomorphism via typed lambda terms is equivalent to the categorical approach to proof representations; see for instance [3]. What is meant is that, not only does $M$ prove the implication $\phi\Rightarrow\psi$ and $N$ prove $\psi\Rightarrow\phi$, but also that any proof $x$ of $\psi$ can be mapped to a proof $Nx$ of $\phi$ and then back to the same proof $x$ of $\psi$, that is, without loss of information; and analogously for any proof $y$ of $\phi$. For a simple example of formulas that are equivalent but not isomorphic, consider the equivalence $\alpha\wedge\alpha\Leftrightarrow\alpha$, where $\alpha$ has for instance exactly 2 possible proofs.

Some rationale for why formula isomorphism is the “right” form of equivalence for intuitionistic logic is given in [1], but in this paper we are primarily interested in the notion because of its link to exponential polynomials, explained in the next section.

2. (Dis)proving propositional formula isomorphism

We start with a well known fact from categorical logic and typed lambda calculi (e.g. [4]),

[TABLE]

linking isomorphism of formulas to realizability in $\mathbb{N}^{+}$. The expression on the right is the standard model theoretic one: for any instantiation of the variables with positive natural numbers, $\phi$ and $\psi$ compute to the same number111This number is always positive, because the exponential polynomials that we need for the analogy to formulas have positive coefficients only.. This immediately gives a method for disproving formula isomorphism.

Corollary 1**.**

To show that $\phi\not\cong\psi$, it is enough to show (by whatever means, i.e., algebra, analysis, etc.) that $\phi\neq\psi$.

Although the method directly follows from basic relation between isomorphism and equality, we think that it is interesting to mention, because it can be much simpler to employ than:

• •

showing that there is no proof term for $\phi\Rightarrow\psi$ or a proof term for $\psi\Rightarrow\phi$;

• •

showing that no proof term for $\phi\Rightarrow\psi$ and proof term for $\psi\Rightarrow\phi$ can be $\beta$-$\eta$-equal;

• •

proving that $\phi\Leftrightarrow\neg\psi$ (or vice versa); or

• •

building a model that realizes $\phi$ but does not realize $\psi$ (or vice versa).

Of course, it is not a method for disproving equivalence, because even when $\phi\not\cong\psi$, $\phi\Leftrightarrow\psi$ may still hold. But, the following link between equality and isomorphism allows to prove equivalence:

[TABLE]

The expression $\text{HSI}\vdash\phi~{}\dot{=}~{}\psi$ means that the equality between the exponential polynomials $\phi$ and $\psi$ is derivable from the so called high-school identities:

[TABLE]

Corollary 2**.**

To show that $\phi\cong\psi$, it is enough to show that $\phi=\psi$ is derivable by the high-school identities.

Note that not every true equality between exponential polynomials is derivable by the high-school identities (HSI),

[TABLE]

This is a consequence of the negative solution to Tarski’s high-school algebra problem [2]. A typical operation that one can perform in the model, but not in the derivation, is canceling. Here is a simple example of a $\phi$ and a $\psi$, such that $\mathbb{N}^{+}\vDash\phi=\psi$ and $\phi\cong\psi$, but $\text{HSI}\not\vdash\phi~{}\dot{=}~{}\psi$, due to Martin [11]:

[TABLE]

It is possible to “repair” HSI by extending it to an enumerable set of axioms HSI* due to Wilkie [12], that, in addition to the HSI, contains all true equalities between ordinary (i.e., non-exponential) positive polynomials, possibly with negative coefficients. Then, we do get that

[TABLE]

however it is not clear how to prove in general that $\text{HSI}^{*}\vdash\phi~{}\dot{=}~{}\psi$ implies $\phi\cong\psi$, since the ordinary polynomial equalities we have added to HSI* may contain negative coefficients. A partial solution is given in [7].

Finally, we remark that, although the analogy between isomorphism and equality can be delicate for certain kind of formulas—the formulas of the kind of Martin—very often it works seamlessly. There are also some general results in this direction based on the form of formulas in question, such as the following one.

Proposition 1** ([5, 10, 7]).**

For the class $\mathcal{L}$ of formulas of Gurevič–Levitz, we have that, for all $\phi,\psi\in\mathcal{L}$,

[TABLE]

where the class $\mathcal{L}$ is defined inductively:

[TABLE]

where $\lambda_{0}\in\Lambda$ but $\lambda_{0}$ contains no proposition (i.e., variable) $\pi_{i}$.

For these kinds of formulas, equivalence and isomorphism can be proved by showing equality of exponential polynomials (by whichever mathematical means) and not only by deriving equality via the axioms HSI.

3. Intuitionistic “prenex” normal form

For ordinary (i.e., non-exponential) polynomials, equality is decidable and so is isomorphism. This fragment of polynomials corresponds to the fragment of formulas constructed from the two logical connectives $\{\vee,\wedge\}$. If we consider the fragment $\{\Rightarrow,\wedge\}$, the situation is the same. In both cases, it is a consequence of the fact that there is a canonical normal form for the formulas (polynomials) in question.

In the general case when all of the connectives $\{\wedge,\vee,\Rightarrow\}$ are present, a canonical normal form is not known. However, we sometimes find [6] the following transformation

[TABLE]

that allows to derive a quasi222The normal form is “quasi”, because, unlike the normal form for ordinary polynomials, it is not canonical, i.e., there are equal exponential polynomials that do not have the same normal form. normal form for exponential polynomials.

Theorem 1** (Theorem 2.1 of [1]).**

Every propositional formula $\phi$ can be normalized to a formula $\left\|{\phi}\right\|$, such that $\phi\cong\left\|{\phi}\right\|$ and $\left\|{\phi}\right\|\in\mathbf{\Pi}\cup\mathbf{\Sigma}$, where the classes $\mathbf{\Pi}$ and $\mathbf{\Sigma}$ are defined inductively and mutually as follows:

[TABLE]

where $\chi_{i}$ are prime formulas.

To extend the normal form to the first-order quantifiers, we adopt an extended exponential polynomial notation: we write $\exists x\phi$ as $x\phi$ and $\forall x\phi$ as $\phi^{x}$, the distinction between conjunctions and existential quantifiers, and implications and universal quantifiers, being made by a variable convention: we “left-multiply” and “exponentiate” by the lowercase Latin letters $x,y,z$ in order to express quantifiers, while if we do it with Greek $\phi,\psi$, it means that we are making a conjunction and implication. Using this notation, the following formula isomorphisms acquire the form of equations:

[TABLE]

If we add these equations to the axioms of HSI, we will thus still preserve isomorphism. However, we do not know whether a relation to model theoretic equality will hold, such as the one in the propositional case. The reason is that we have extended the language of exponential polynomials, and one needs to find an interpretation for the new arithmetic operations $x(\cdot)$ and $(\cdot)^{x}$. Nevertheless, the representation of formulas as extended exponential polynomials is sufficient to show a normal form theorem for first-order formulas.

Theorem 2** (Theorem 4.1 of [1]).**

Every first-order formula $\phi$ can be normalized to a formula $\left\|{\phi}\right\|$, such that $\phi\cong\left\|{\phi}\right\|$ and $\left\|{\phi}\right\|\in\mathbf{\Pi}\cup\mathbf{\Sigma}$, where the classes $\mathbf{\Pi}$ and $\mathbf{\Sigma}$ are defined inductively and mutually as follows:

[TABLE]

where $\chi_{i}$ are prime formulas.

Intuitionistically, this theorem is interesting, because we do not have a notion of arithmetical hierarchy as versatile as the one of classical logic; see [1] for a discussion. Classically, one can also use this hierarchy as an alternative to the standard one.

To make the link to the classical arithmetical hierarchy, we will first need to assign levels to the hierarchy from the last theorem.

Definition 1**.**

The intuitionistic arithmetical hierarchy is defined by assigning levels, $\boldsymbol{\Sigma_{n}},\boldsymbol{\Pi_{n}}$, for $n\in\mathbb{N}$, to the formula classes $\boldsymbol{\Sigma}$ and $\boldsymbol{\Pi}$, in the following way:

[TABLE]

We also extend the relation “$\in$” from formulas satisfying the inductive definition to all formulas, in the following way: $F\in\boldsymbol{\Pi_{n}}$ iff $\left\|{F}\right\|\in\boldsymbol{\Pi_{n}}$; $F\in\boldsymbol{\Sigma_{n+1}}$ iff $\left\|{F}\right\|\in\boldsymbol{\Sigma_{n+1}}$.

The relation to the classical arithmetical hierarchy is given by the following theorem, where the levels of the classical hierarchy are denoted $\Sigma^{0}_{n}$ and $\Pi^{0}_{n}$, that is, with a zero superscript and no bold face.

Theorem 3** (Propositions 4.7 and 4.8 of [1]).**

Say that a formula $\phi$ is classically represented in $\boldsymbol{\Sigma_{n}}$ (or $\boldsymbol{\Pi_{n}}$) when there is a formula $\phi^{\prime}\in\boldsymbol{\Sigma_{n}}$ (or $\boldsymbol{\Pi_{n}}$) such that $\phi$ and $\phi^{\prime}$ are classically equivalent.

If $\phi\in\Sigma^{0}_{n}$, then $\phi$ is classically represented in $\boldsymbol{\Sigma_{n}}$. If $\phi\in\Pi^{0}_{n}$, then $\phi$ is classically represented in $\boldsymbol{\Pi_{n}}$.

Suppose that $\psi$ is in prenex normal form and with alternating quantifiers. Then: $\psi\in\boldsymbol{\Sigma_{n}}$ implies $\psi\in\Sigma^{0}_{n}$; $\psi\in\boldsymbol{\Pi_{n}}$ implies $\psi\in\Pi^{0}_{n}$.

As a corollary, we get that the intuitionistic hierarchy is proper.

Corollary 3** (Corollary 4.9 of [1]).**

For $n\geq 0$, $\boldsymbol{\Sigma_{n}}\subsetneq\boldsymbol{\Sigma_{n+1}}$, $\boldsymbol{\Sigma_{n}}\subsetneq\boldsymbol{\Pi_{n+1}}$, $\boldsymbol{\Pi_{n}}\subsetneq\boldsymbol{\Sigma_{n+1}}$, and $\boldsymbol{\Pi_{n}}\subsetneq\boldsymbol{\Pi_{n+1}}$.

One can think of the exp-log normal form of formulas as the constructive analogue of the prenex normal form from classical logic.