4
$\begingroup$

We know that Frege systems are required to be implicationally complete -- namely, if a set of formulas $B_1,B_2,\cdots,B_t$ imply formula $C$, then this implication can be proven in the system. I'm curious about what happens if we discard this requirement. Is there any research on the relative efficiency of non-implicationally complete Frege systems? As an example, consider the case when we want to prove that a formula with connectives $\neg,\lor,\land$ is a tautology, using only the equivalence rules of Boolean algebra, like commutativity, associativity, distributivity, etc. But we shouldn't use non-equivalence rules, like $a\models a\lor b$. I wonder if the ban of non-equivalence rules results in a superpolynomial explosion of proof size. I think this is important because it may help us understand the nature of Boolean algebra.

Update: To clarify, the "Boolean equational calculus" system I defined here is not a Frege system. I define the system to allow applying of laws of Boolean algebra anywhere inside the formula. If I allow the system to have non-equivalence rules, the system would be p-equivalent to Frege systems, so I focus on the system without these rules. I didn't find this system in Krajíček's 2019 book, but I think it's interesting to have a look at.

$\endgroup$
10
  • $\begingroup$ I don't know of any work on this specific system, but I do know of a proof system that seems interesting and is not implicationally complete, namely, "Geometric IPS" as defined in Appendix B of doi.org/10.1145/3230742. (But I don't know any follow-up work on that yet!) $\endgroup$ Sep 5 at 19:34
  • $\begingroup$ @EmilJeřábek Thanks for your comments. Could you please explain how to formulate an implicationally incomplete Frege system that is p-equivalent to the cut-free sequent calculus? Cut-free sequent calculus turns out to be complete. $\endgroup$
    – Soha
    Sep 5 at 23:05
  • $\begingroup$ @EmilJeřábek I can understand that Frege systems p-simulate Boolean calculus, since if we apply Boolean rules on a node deep in the formula tree, we can gradually go up by using the rules $\let\eq\leftrightarrow\phi\eq\psi\vdash(\phi\circ\chi)\eq(\psi\circ\chi)$. But as for Boolean calculus p-simulating Frege, how can we make sure $\phi\vdash \phi\land\phi_0$ has a polynomial-size Boolean calculus proof? $\endgroup$
    – Soha
    Sep 6 at 19:44
  • $\begingroup$ @EmilJeřábek Yeah we know that if we have $\phi\to\phi_0$ then we have $\phi\leftrightarrow\phi\land\phi_0$. But we have to prove $\phi\to\phi_0$ first. $\endgroup$
    – Soha
    Sep 6 at 20:07
  • $\begingroup$ @EmilJeřábek Oh, I understand now. We're deriving $\phi\leftrightarrow\psi$ from nothing so $\phi_0$ must be an instance of an axiom scheme, hence it must be a tautology. All of $\phi_i$'s must be tautologies because tautologies can only imply tautologies. But, if $\phi_j$ is derived from $\phi_{i_1},\phi_{i_2},\cdots,\phi_{i_t}$ via a Frege rule, how can we add $\phi_j$ to the conjunction by Boolean calculus? The Frege rule might be a weakening rule so the rule itself might not be proved by Boolean calculus. We have to consider the rule and the fact that their inputs are tautologies together. $\endgroup$
    – Soha
    Sep 7 at 6:35

1 Answer 1

2
$\begingroup$

$\let\eq\leftrightarrow\def\ru{\mathrel/}\let\ET\bigwedge$Frege systems are required to be implicationally complete to make all such systems p-equivalent, yielding a robust definition of the Frege system that does not depend on insignificant details like the choice of the primitive rules of inference. If you drop implicational completeness, this no longer holds: all such “Frege” systems are still p-simulated by standard Frege, and some are still p-equivalent, but other system are wildly different (weaker). I’m not aware of this being systematically studied anywhere, but for a case in point, it is not hard to check that the system with the following rules is p-equivalent to the cut-free sequent calculus, which is known to be very weak (see e.g. the exponential lower bounds by Statman): $$\begin{gather*} \dfrac{A}{A\lor B}\qquad \dfrac{A\lor A}A\qquad \dfrac{A\lor B}{B\lor A}\qquad \dfrac{A\lor(B\lor C)}{(A\lor B)\lor C}\qquad \dfrac{(C\lor A)\lor(B\lor D)}{(C\lor B)\lor(A\lor D)}\\ \dfrac{}{A\lor\neg A}\qquad \dfrac{C\lor A}{C\lor\neg\neg A}\qquad \dfrac{C\lor\neg A\quad C\lor\neg B}{C\lor\neg(A\lor B)} \end{gather*}$$ (If you insist on having $\land$ in the language, include $$\dfrac{C\lor A\quad C\lor B}{C\lor(A\land B)}\qquad\dfrac{C\lor(\neg A\lor\neg B)}{C\lor\neg(A\land B)}$$ as well.)

As for the second question, the Boolean equational calculus (let me denote it E) is p-equivalent to standard Frege (F). I will sketch the argument below. Let $\top$ be a fixed tautology. Observe that similar to Frege, if $A\equiv B$ is any valid constant-size Boolean identity, then for any substitution $\sigma$, we can replace $\sigma(A)$ in $C$ with $\sigma(B)$ by an E-derivation of size linear in the size of $\sigma$ (we just take a $\sigma$-instance of a fixed E-derivation of $B$ from $A$).

Proposition 1.

  • Given an E-derivation of $B$ from $A$, we can construct in polynomial time an F-proof of $A\eq B$.
  • Given an E-derivation of $A$ from $\top$, we can construct in polynomial time an F-proof of $A$.

Proof: First, if $A\ru B$ is any basic rule of E, then $A\eq B$ is a constant-size tautology, hence its substitution instances have linear-size F-proofs. Then a single-step E-derivation $C\vdash D$, where we replace a subformula $\sigma(A)$ with $\sigma(B)$, is simulated by a polynomial-size F-proof where we first derive $\sigma(A)\eq\sigma(B)$, and then we propagate the equivalence upwards using instances of $P\eq Q\ru(P\circ R)\eq(Q\circ R)$, where $\circ$ is any connective.

Now, given an E-derivation $A=A_1,\dots,A_n=B$, we construct F-proofs of $A_1\eq A_2,\dots,A_{n-1}\eq A_n$ as indicated, and chain them together to a proof of $A_1\eq A_n$ using instances of $P\eq Q,Q\eq R\ru P\eq R$.

Proposition 2.

  • Given an F-proof of $A\eq B$, we can construct in polynomial time an E-derivation of $B$ from $A$.
  • Given an F-proof of $A$, we can construct in polynomial time an E-derivation of $A$ from $\top$.

Proof: Let $A_1,\dots,A_n=(A\eq B)$ be an F-proof. We first construct an E-derivation $$\tag1\label1A\vdash A\land A_1\vdash\dots\vdash A\land A_1\land\dots\land A_n$$ (arbitrarily bracketed). Write $C_i=A\land\ET_{j\le i}A_j$ for $i=0,\dots,n$, where we identify $C_0$ with $A$. In order to derive $C_i$ from $C_{i-1}$, assume that $A_i$ was derived in the original proof by an instance of an F-rule from $A_{j_1},\dots,A_{j_c}$, where $j_1,\dots,j_c<i$. We first apply a sequence of instances of associativity and commutativity to reorder the conjunction in $C_{i-1}$ to the form $\dots\land(A_{j_1}\land\dots\land A_{j_c})$. Since $$(A_{j_1}\land\dots\land A_{j_c})\equiv(A_{j_1}\land\dots\land A_{j_c}\land A_i)$$ is an instance of a constant-size Boolean identity, we can construct a linear-size E-derivation $\dots\land(A_{j_1}\land\dots\land A_{j_c})\vdash\dots\land(A_{j_1}\land\dots\land A_{j_c}\land A_i)$, and if needed, we apply associativity and commutativity to reorder the conjuction back to form $C_i$.

Since $A_n$ is $A\eq B$, we can use the Boolean identity $(A\land(A\eq B))\equiv(B\land(A\eq B))$ to derive $$\tag2\label2A\land A_1\land\dots\land A_n\vdash B\land A_1\land\dots\land A_n.$$ Finally, we apply the same argument as in $\eqref1$ backwards to derive $$\tag3\label3B\land A_1\land\dots\land A_n\vdash B\land A_1\land\dots\land A_{n-1}\vdash\dots\vdash B\land A_1\vdash B.$$ Together, $\eqref1$, $\eqref2$, and $\eqref3$ yield an E-derivation $A\vdash B$.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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