# Growth of a set of propositional formulas under partial evaluation

Definitions: Let $$n \in \mathbb{N}, n \geq 1$$. We write $$|\alpha|$$ to denote the length in characters of an expression $$\alpha$$ in propositional logic. We define partial evaluation in the normal way where evaluation is applied to an expression containing constants until no more evaluation is possible. So for example if we start with the expression $$a \land b$$ and apply the substitution $$\{ b \rightarrow true \}$$, we get $$a \land true$$ which after partial evaluation leaves us with $$a$$. The biconditional is defined as usual: $$\alpha \leftrightarrow \beta$$ iff $$\alpha \rightarrow \beta \land \alpha \leftarrow \beta$$. If $$\alpha$$ and $$\beta$$ are formulas, then we'll say $$\alpha$$ and $$\beta$$ are equivalent if $$\alpha \leftrightarrow \beta$$ is true for all satisfying assignments. We consider $$\alpha$$ distinct from $$\beta$$ if they are not equivalent.

Instances of $$\alpha$$ are constrained to have $$4n$$ input variables. From those $$4n$$ variables, we choose any subset $$S$$ where $$|S| \leq n$$. We require that for all subsets $$S$$, $$\alpha$$ must yield a distinct propositional expression after partial evaluation for each possible truth assignment to $$S$$.

Here is an example of a possible $$\alpha$$ where $$n=1$$, so there are $$4n = 4$$ variables $$a,b,c,d$$. There could well be many other possible versions of $$\alpha$$.

$$\alpha_1 = (a \land b) \lor (a \land c) \lor (a \land d) \lor (b \land c) \lor (b \land d) \lor (c \land d)$$

If $$a$$ is true, we get the following after partial evaluation and simplification:

$$b \lor c \lor d$$

If $$a$$ is false, we get the following different function after partial evaluation:

$$(b \land c) \lor (b \land d) \lor (c \land d)$$

We notice that all the 8 possible expressions generated in this way over the four variables $$a,b,c,d$$ and the two truth values are indeed distinct from one another. The empty substitution where $$S = \emptyset$$ for $$n=0$$ simply yields $$\alpha_1$$, which is distinct from the other 8.

Question: Let $$\beta$$ be an expression built from the usual operations $$\land$$, $$\lor$$, and $$\lnot$$. Is there an equivalent set of expressions $$\beta_n$$ for some $$\alpha_n$$ (where $$\alpha_n \leftrightarrow \beta_n$$) such that the growth of $$|\beta_n|$$ is polynomially bounded, that is, there is some constant $$c$$ such that $$|\beta_n| = O(n^c)$$? Or is this impossible for any set of $$\alpha_n$$ that satisfies the constraints above? Does it make any difference if the $$\beta_n$$ are Boolean circuits?

Motivation: I am looking for a counterexample to the claim that no algorithm running in polynomial time has a polynomial size circuit that satisfies the $$\alpha$$ requirements.

• @D.W.: Thanks for writing. Yes, I mean that $\alpha \leftrightarrow \beta$ holds for all assignments to the variables. If you're thinking about forms of $\beta$ that have additional intermediate variables, let me know and I can try to specify that. Sep 10, 2023 at 20:40
• Thank you. In the future, please edit the question with clarifications, rather than putting clarifications in the comments. We want the question to read well for someone who encounters it for the first time. I've made an edit to incorporate this information. Thank you!
– D.W.
Sep 11, 2023 at 3:03
• What's the motivation? I expect the answer is almost certainly "no, there exist $\alpha$ for which there is no polynomial-size $\beta$ that is equivalent". There are a huge number of functions that can be computed, vastly larger than the number of polynomial-size formulas.
– D.W.
Sep 11, 2023 at 3:04
• @D.W.: Thanks for the correction to my original posting, and my apologies for making this editorial blunder again :). I'm hoping for the result that every $\alpha$ must have an exponential $\beta$ and no polynomial ones. Sep 11, 2023 at 5:16
• That seems very unlikely to be true; consider any $\alpha$ that is already polynomial size (and meets your requirements). I'm wondering what is the motivation for studying this.
– D.W.
Sep 11, 2023 at 5:40