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?

  • 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 case-by-case 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 well-defined meaning. See e.g. the first two sections of plato.stanford.edu/entries/logic-algebraic-propositional . $\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 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.

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.