# Is the consequence relation of a finite set of boolean connectives finitely generated?

I asked this question on math stack exchange, but it didn't receive any answers. Consider a countably infinite set of variables called $$PROP$$. We augment $$PROP$$ with a finite set of boolean connectives, that is, a finite set of n-ary connectives on {0,1}. We say that well-formed formulas of the language are generated as follows: 1. $$PROP$$ is in the language. 2. If f is an n-ary connectives, and there are already n formulas, then the concatenation of those n formulas with f is in the language. We define a consequence relation, by saying that a set of formulas S implies a formula F, iff there is no Boolean valuation that simultaneously makes all members of S true but F false. My question is, for any finite set of Boolean connectives, is the consequence relation finitely generated?

• What do you mean finitely generated ? – Maxime Ramzi Jun 12 '19 at 23:03
• This is plausible, and probably can be established on a case-by-case basis using the known structure of Post’s lattice. I don’t know if there is a more uniform argument. – Emil Jeřábek Jun 13 '19 at 7:27
• @Max A froquacks $X$ is finitely generated if there exists a finite $X_0\subseteq X$ such that $X$ is the least froquacks that contains $X_0$. For (presumably structural) consequence relations, this means that the consequence relation is axiomatizable by substitution instances of a finite set of rules. – Emil Jeřábek Jun 13 '19 at 7:34
• @EmilJeřábek Yes, my problem was that it's not clear what a "consequence relation" is here - it's not clear if the OP means syntax (which you suggest) or something else here – Maxime Ramzi Jun 13 '19 at 7:36
• @Max I’m not suggesting syntax. Consequence relation is a standard term with a well-defined meaning. See e.g. the first two sections of plato.stanford.edu/entries/logic-algebraic-propositional . – Emil Jeřábek Jun 13 '19 at 7:42

The answer is yes, but the proof involves tedious checking of various cases, and I will only sketch the main points below. Let $$L$$ be the given finite set of connectives, and $$C$$ the clone that it generates (i.e., the set of Boolean functions definable by $$L$$-formulas). I will name clones using the notation from Wikipedia.

First, the multiple-conclusion consequence relation (in the sense of Shoesmith & Smiley) on $$L$$-formulas, defined by $$\Gamma\models^{m}\Delta\iff\text{there is no valuation that makes all \phi\in\Gamma true and all \phi\in\Delta false,}$$ is always finitely generated (as a structural multiple-conclusion consequence relation): it is easy to see that it can be explicitly axiomatized as follows. For each $$n$$-ary connective $$f\in L$$, and each $$\vec a\in\{0,1\}^n$$, postulate $$\{\phi_i:a_i=1\}\vdash f(\vec\phi),\{\phi_i:a_i=0\}\tag{A1}$$ if $$f(\vec a)=1$$, and $$\{\phi_i:a_i=1\},f(\vec\phi)\vdash\{\phi_i:a_i=0\}\tag{A0}$$ if $$f(\vec a)=0$$.

Let me denote by $$\vdash^{m}$$ the corresponding sequent calculus that has instances of (A0), (A1), and $$\phi\vdash\phi$$ as initial sequents, and includes the usual structural rules and the cut rule.

For the ordinary single-conclusion consequence relation, I will need to distinguish several cases.

Case 1: $$C$$ contains $$x\lor y$$, i.e., $$C\supseteq{\bigvee}\mathrm P$$.

First, the logic of $$\lor$$ alone can be easily axiomatized, e.g. as follows: \begin{align*} \phi&\vdash\phi\lor\psi\\ \phi\lor\phi&\vdash\phi\\ \phi\lor\psi&\vdash\psi\lor\phi\\ \phi\lor(\psi\lor\chi)&\vdash(\phi\lor\psi)\lor\chi\\ (\phi\lor\psi)\lor(\chi\lor\omega)&\vdash(\phi\lor\chi)\lor(\psi\lor\omega) \end{align*} Now, it suffices to extend this to a finitely axiomatized single-conclusion calculus $$\vdash^s$$ such that $$\Gamma\vdash^m\Delta\iff\Gamma\vdash^s\bigvee\Delta.$$ Actually, in order to handle the cut rule, we will need a stronger hypothesis: we will define $$\vdash^s$$ so that $$\Gamma\vdash^m\Delta\implies\{z\lor\phi:\phi\in\Gamma\}\vdash^sz\lor\bigvee\Delta,\tag{2}$$ where $$z$$ is a variable that does not occur in the proof of $$\Gamma\vdash^m\Delta$$. I will write $$z\lor\Gamma=\{z\lor\phi:\phi\in\Gamma\}$$.

For each initial sequent $$\Gamma\vdash^m\Delta$$ as in (A0) or (A1), we include in $$\vdash^s$$ the corresponding sequent given by (2). Then we can show that (2) holds by induction on the length of proof in $$\vdash^m$$. The case of initial sequents holds by the definition of $$\vdash^s$$, and structural rules are easy. In order to simulate the cut rule $$\frac{\Gamma\vdash^m\phi,\Delta\qquad\Gamma,\phi\vdash^m\Delta}{\Gamma\vdash^m\Delta},$$ let $$\delta=\bigvee\Delta$$; by the induction hypothesis, we have \begin{align} z\lor\Gamma&\vdash^sz\lor\phi\lor\delta,\tag3\\ z\lor\Gamma,z\lor\phi&\vdash^sz\lor\delta.\tag4 \end{align} By substituting $$z/(z\lor\delta)$$ in (4), and some manipulation with $$\lor$$, we obtain $$z\lor\delta\lor\Gamma,z\lor\phi\lor\delta\vdash^sz\lor\delta\lor\delta\vdash^sz\lor\delta.$$ Using $$z\lor\psi\vdash^sz\lor\delta\lor\psi$$ for $$\psi\in\Gamma$$, and (3), we obtain $$z\lor\Gamma\vdash^sz\lor\delta.$$ I have swept under the rug the minor problem that we may need to handle empty disjunctions, if some sequent in the $$\vdash^m$$ proof has an empty consequent.

Now, (2) implies that the calculus $$\vdash^s$$ is complete: if $$\Gamma\models\psi$$, then $$\Gamma\vdash^m\psi$$, hence $$z\lor\Gamma\vdash^sz\lor\psi$$ by $$(2)$$. Since $$\phi\vdash^sz\lor\phi$$ for $$\phi\in\Gamma$$, this gives $$\Gamma\vdash^sz\lor\psi$$. Substituting $$z/\psi$$, we obtain $$\Gamma\vdash^s\psi\lor\psi\vdash^s\psi.$$

Case 2: $$C$$ contains $$(x\lor y)\land z$$ or $$\mathrm{maj}(x,y,z)$$, i.e., $$C\supseteq\mathrm{MPT_0^\infty}$$ or $$C\supseteq\mathrm{DM}$$.

In this case, we have a ternary formula $$x\lor^zy$$ such that $$x\lor^1y$$ is equivalent to $$x\lor y$$. We use it to simulate the calculus $$\vdash^s$$ we defined in the proof of Case 1: we choose yet another fresh variable $$t$$, and use $$\lor^t$$ in place of $$\lor$$ in the whole argument, while including $$t$$ in the antecedents of all sequents (to ensure that all sequents we need as axioms are actually valid).

In the end, for $$\Gamma\models\psi$$, we obtain a proof of $$t,\Gamma\vdash^s\psi.$$ If $$\Gamma\ne\emptyset$$, we substitute an element of $$\Gamma$$ for $$t$$ to obtain $$\Gamma\vdash^s\psi$$. If $$\Gamma=\emptyset$$, then $$\psi$$ is a tautology, i.e., $$1\in C$$, which means $${\lor}\in C$$, which means we are in Case 1 after all.

Case 3: $$C\subseteq\bigwedge$$, i.e., every $$f\in L$$ is equivalent to either a conjunction of a subset of variables, or a constant $$0$$ or $$1$$.

In this case, after eliminating redundant variables, the axioms (A1) and (A0) of $$\vdash^m$$ already have at most one formula in the consequent, hence we can use them to axiomatize $$\vdash^s$$ (putting an extra formula in the consequent if it is empty).

Case 4: $$\mathrm{AP}\subseteq C\subseteq\mathrm A$$.

Here, all formulas denote affine functions over $$\mathbf F_2$$. In this case, it is more convenient to dualize the notation so that $$0$$ is true, and $$1$$ is false. We can define $$+$$, possibly by a formula using an extra constant that we handle as in Case 3. Similarly to $$\lor$$, it is easy to give a finite axiom system that makes any formula interderivable with a (canonically bracketed) sum of variables, + possibly constant $$1$$. On top of that, simple linear algebra shows that an affine function $$\psi$$ follows from a set of affine functions $$\Gamma$$ iff $$\psi$$ or $$1$$ is a linear combination of $$\Gamma$$, i.e., a sum of a subset of $$\Gamma$$. These can be performed by the rules $$\phi,\psi\vdash\phi+\psi$$ and $$1\vdash\phi$$. I will skip the details.

Case 5: $$C=\mathrm{UD}$$ or $$C=\mathrm U$$.

That is, $$C$$ contains $$\neg$$, while every formula is equivalent to a variable, to a negated variable, or possibly to a constant. This case is left as an easy exercise.

By inspection of Post’s lattice, there are no more cases.