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 nary connectives on {0,1}. We say that wellformed formulas of the language are generated as follows: 1. $PROP$ is in the language. 2. If f is an nary 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?

3$\begingroup$ What do you mean finitely generated ? $\endgroup$ – Maxime Ramzi Jun 12 '19 at 23:03

$\begingroup$ This is plausible, and probably can be established on a casebycase basis using the known structure of Post’s lattice. I don’t know if there is a more uniform argument. $\endgroup$ – Emil Jeřábek Jun 13 '19 at 7:27

$\begingroup$ @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. $\endgroup$ – Emil Jeřábek Jun 13 '19 at 7:34

$\begingroup$ @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 $\endgroup$ – Maxime Ramzi Jun 13 '19 at 7:36

$\begingroup$ @Max I’m not suggesting syntax. Consequence relation is a standard term with a welldefined meaning. See e.g. the first two sections of plato.stanford.edu/entries/logicalgebraicpropositional . $\endgroup$ – 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 multipleconclusion 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 multipleconclusion 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 singleconclusion 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 singleconclusion 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.