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

Question

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?

Answer 1

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.