<p>The answer occurred to me right after I finished typing up the post. Rather than delete it, I figured I would post it anyway in case anyone else has the same question.</p>
<hr />
<h2>Answer</h2>
<p>The mistake in the proposed proof is that in order to use Lemma II.2.24, I implicitly assume that if <span class="math-container">$\forall \Phi \vDash S$</span>, then <span class="math-container">$\Phi \vDash S$</span>. However, this is not necessarily true! Let <span class="math-container">$P$</span> be a 1-ary predicate of <span class="math-container">$\mathcal{L}$</span>, and consider the example of <span class="math-container">$\Phi := \{P(b)\}$</span>, and <span class="math-container">$S := \rightarrow \forall x Px$</span>. Clearly <span class="math-container">$\forall \Phi \vDash S$</span>, but it is not the case that <span class="math-container">$Pb \vDash \forall xPx$</span>.</p>

CC BY-SA 4.0
2023-04-09T23:56:54.860Z
2023-04-09T23:56:54.860Z
Johnny
<p>The version of Buss's proof I'm referring to is the proof of Lemma II.2.24 in <em>Logical Foundations of Proof Complexity</em> by Cook and Nguyen. In the interest of keeping this question self-contained I've provided all the particularities of the book in the &quot;Notations, Conventions and Definitions&quot; section at the end of this question.</p>
<hr />
<h2>Background</h2>
<p><strong>Theorem II.2.23:</strong> Let <span class="math-container">$\mathcal{L}$</span> be a first-order language which does not contain the equality symbol. Let <span class="math-container">$\Phi$</span> be a set of formulas of <span class="math-container">$\mathcal{L}$</span>, and <span class="math-container">$\Gamma \rightarrow \Delta$</span> be a sequent of <span class="math-container">$\mathcal{L}$</span>. There is an LK-<span class="math-container">$\Phi$</span> proof of <span class="math-container">$\Gamma \rightarrow \Delta$</span> iff <span class="math-container">$\forall \Phi \vDash \Gamma \rightarrow \Delta$</span>.</p>
<p>The proof of this theorem relies on the following Lemma.</p>
<p><strong>Lemma II.2.24:</strong> If <span class="math-container">$\Phi \vDash \Gamma \rightarrow \Delta$</span>, then there is a cut-free LK proof of <span class="math-container">$C_1, C_2, ..., C_k, \Gamma \rightarrow \Delta$</span>, where <span class="math-container">$\{C_i : i \in [k]\}$</span> is a finite subset of <span class="math-container">$\Phi$</span>.</p>
<p>My question pertains specifically to the proof of completeness.</p>
<p><strong>Proof of completeness direction of Theorem II.2.23:</strong> Let <span class="math-container">$\Phi$</span> be a set of formulas such that <span class="math-container">$\forall \Phi \vDash \Gamma \rightarrow \Delta$</span>. By Lemma II.2.24, we know there is finite subset <span class="math-container">${C_1,...,C_k}$</span> of <span class="math-container">$\Phi$</span> such that there is an LK proof <span class="math-container">$\pi$</span> of <span class="math-container">$S := \forall C_1, ..., \forall C_k, \Gamma \rightarrow \Delta$</span>. Notice that if we can derive, for any <span class="math-container">$i \in [k]$</span>, the sequent <span class="math-container">$\rightarrow \forall C_i$</span>, then we are done: by weakening each such sequent appropriately, we can apply the cut rule to remove <span class="math-container">$\forall C_i$</span> from <span class="math-container">$S$</span>. Applying all such cuts yields an LK-<span class="math-container">$\Phi$</span> proof <span class="math-container">$\pi'$</span> of the sequent <span class="math-container">$\Gamma \rightarrow \Delta$</span>.</p>
<p>It remains to show that we can derive <span class="math-container">$\forall C_i$</span>. Starting from nonlogical axiom <span class="math-container">$\rightarrow C_i$</span>, we can apply the right <span class="math-container">$\forall$</span>-introduction rule for each free variable in <span class="math-container">$C_i$</span>. <span class="math-container">$\blacksquare$</span></p>
<p>Note that in <span class="math-container">$\pi'$</span> above, we cut on formulas of the form <span class="math-container">$\forall C_i$</span>. Since <span class="math-container">$\pi'$</span> is an LK-<span class="math-container">$\Phi$</span> proof and not an LK-<span class="math-container">$\forall \Phi$</span> proof, this means that <span class="math-container">$\pi'$</span> is not necessarily anchored. However according to the book (assuming certain conditions on <span class="math-container">$\Phi$</span>), it is possible to show that an anchored LK-<span class="math-container">$\Phi$</span> proof of <span class="math-container">$\Gamma \rightarrow \Delta$</span> exists. In the book, this is Theorem II.2.28. Proving this theorem is Exercise II.2.29.</p>
<hr />
<h2>My Question</h2>
<p>How isn't the following simple modification to the proof above a proof of anchored derivational completeness of LK?</p>
<p><strong>(Proposed) Proof:</strong> Let <span class="math-container">$\Phi$</span> be a set of <span class="math-container">$\mathcal{L}$</span>-formulas such that <span class="math-container">$\forall \Phi \vDash S$</span>, where <span class="math-container">$S := \Gamma \rightarrow \Delta$</span>. By Lemma II.2.24, we know there is finite subset <span class="math-container">${C_1,...,C_k}$</span> of <span class="math-container">$\Phi$</span> such that there is a <strong>cut-free</strong> LK proof <span class="math-container">$\pi$</span> of <span class="math-container">$S := C_1, ..., C_k, \Gamma \rightarrow \Delta$</span>. For any <span class="math-container">$i \in [k]$</span>, by weakening each nonlogical axiom <span class="math-container">$\rightarrow C_i$</span> appropriately, we can apply the cut rule to remove <span class="math-container">$C_i$</span> from <span class="math-container">$S$</span>. Applying all such cuts yields an LK-<span class="math-container">$\Phi$</span> proof <span class="math-container">$\pi''$</span> of the sequent <span class="math-container">$\Gamma \rightarrow \Delta$</span>.</p>
<p>Since the only cuts in <span class="math-container">$\pi''$</span> are on <span class="math-container">$C_i \in \Phi$</span>, we conclude <span class="math-container">$\pi''$</span> is an anchored LK-<span class="math-container">$\Phi$</span> proof of <span class="math-container">$\Gamma \rightarrow \Delta$</span>. <span class="math-container">$\blacksquare$</span></p>
<hr />
<h2>Notations, Conventions and Definitions</h2>
<p>Let <span class="math-container">$\mathcal{L}$</span> be a first order language. We define two disjoint, infinite set of variables of <span class="math-container">$\mathcal{L}$</span>: <em>free</em> variables, and <em>bound</em> variables. As a convention, in any formula <span class="math-container">$A$</span> of <span class="math-container">$\mathcal{L}$</span> we require that there are no bound occurrences of free variables and that there are no free occurrences of bound variables in <span class="math-container">$A$</span>.</p>
<p>We say formula <span class="math-container">$B$</span> is a logical consequence of <span class="math-container">$A$</span>, denoted <span class="math-container">$A \vDash B$</span>, if for every <span class="math-container">$\mathcal{L}$</span>-structure <span class="math-container">$\mathcal{M}$</span> and every object assignment <span class="math-container">$\sigma$</span> from the variables of <span class="math-container">$L$</span> to the universe <span class="math-container">$M$</span> of <span class="math-container">$\mathcal{M}$</span>, if <span class="math-container">$\mathcal{M}$</span> satisfies <span class="math-container">$A$</span> under <span class="math-container">$\sigma$</span>, denoted <span class="math-container">$\mathcal{M} \vDash A[\sigma]$</span>, then <span class="math-container">$\mathcal{M} \vDash B[\sigma]$</span>.</p>
<p>If <span class="math-container">$\Phi$</span> is a set of formulas <span class="math-container">$\{A_i\}$</span>, then we say <span class="math-container">$\mathcal{M}$</span> satisfies <span class="math-container">$\Phi$</span> under <span class="math-container">$\sigma$</span>, denoted <span class="math-container">$\mathcal{M} \vDash \Phi[\sigma]$</span>, if <span class="math-container">$\mathcal{M} \vDash A_i[\sigma]$</span> for all <span class="math-container">$i$</span>. We say <span class="math-container">$B$</span> is a logical consequence of <span class="math-container">$\Phi$</span>, denoted <span class="math-container">$\Phi \vDash B$</span>, if <span class="math-container">$\mathcal{M} \vDash \Phi[\sigma]$</span> implies <span class="math-container">$\mathcal{M} \vDash B[\sigma]$</span>.</p>
<p>Let <span class="math-container">$S := \Gamma \rightarrow \Delta$</span> be a sequent where <span class="math-container">$\Gamma := \{A_1, ..., A_m\}$</span> and <span class="math-container">$\Delta := \{B_1, ..., B_n\}$</span> are sets of <span class="math-container">$\mathcal{L}$</span>-formulas. We define <span class="math-container">$A_S$</span> as the first order formula</p>
<p><span class="math-container">$$\lnot A_1 \lor \lnot A_2 \lor ... \lor \lnot A_m \lor B_1 \lor B_2 \lor ... \lor B_n$$</span></p>
<p>and we say that <span class="math-container">$\mathcal{M}$</span> satsifies <span class="math-container">$S$</span> under <span class="math-container">$\sigma$</span>, denoted <span class="math-container">$\mathcal{M} \vDash S[\sigma]$</span>, if <span class="math-container">$\mathcal{M} \vDash A_S[\sigma]$</span>. We say <span class="math-container">$S$</span> is a logical consequence of <span class="math-container">$\Phi$</span>, denoted <span class="math-container">$\Phi \vDash S$</span>, if <span class="math-container">$\mathcal{M} \vDash \Phi[\sigma]$</span> implies <span class="math-container">$\mathcal{M} \vDash S[\sigma]$</span>.</p>
<p>An LK proof of <span class="math-container">$S$</span> is a tree <span class="math-container">$\pi$</span> with root is <span class="math-container">$S$</span> whose leaves are sequents <span class="math-container">$A \rightarrow A$</span> for any formula <span class="math-container">$A$</span>, <span class="math-container">$\bot \rightarrow$</span>, or <span class="math-container">$\rightarrow \top$</span> (we call these sequents <em>logical axioms</em>) and whose internal nodes are sequents such that if node <span class="math-container">$S'$</span> has set of children <span class="math-container">$H$</span>, then <span class="math-container">$H$</span> is the set of hypothesis (top) sequents and <span class="math-container">$S'$</span> is the conclusion (bottom) sequent of one of the following rules.</p>
<p><a href="https://i.sstatic.net/U6Sbh.png" rel="nofollow noreferrer"><img src="https://i.sstatic.net/U6Sbh.png" alt="PK rules" /></a></p>
<p><a href="https://i.sstatic.net/a9rBZ.png" rel="nofollow noreferrer"><img src="https://i.sstatic.net/a9rBZ.png" alt="LK bonus rules" /></a></p>
<p>where <span class="math-container">$A(t)$</span> is the formula obtained by replacing all free occurrences of <span class="math-container">$x$</span> in <span class="math-container">$A(x)$</span> (i.e. the occurrences of <span class="math-container">$x$</span> in <span class="math-container">$\forall x A(x)$</span> which become free when we remove the <span class="math-container">$\forall x$</span> quantifier), with a term <span class="math-container">$t$</span> consisting entirely of free variables. Similarly, <span class="math-container">$A(b)$</span> is the formula obtained by replacing all free occurrences of <span class="math-container">$x$</span> in <span class="math-container">$A(x)$</span> by free variable <span class="math-container">$b$</span>. In the left <span class="math-container">$\exists$</span>-introduction and right <span class="math-container">$\forall$</span>-introduction rules, <span class="math-container">$b$</span> must not occur anywhere in the conclusion sequent.</p>
<p>An LK-<span class="math-container">$\Phi$</span> proof of <span class="math-container">$S$</span> is an LK proof of <span class="math-container">$S$</span> in which we allow the leaves to be sequents of the form <span class="math-container">$\rightarrow A_i$</span> for <span class="math-container">$A_i \in \Phi$</span>, which we call <em>nonlogical axioms</em>, in addition to the logical axioms.</p>
<p>We say that an LK-<span class="math-container">$\Phi$</span> proof is <em>cut-free</em> if it does not use the cut rule, and we say that it is <em>anchored</em> if the only formulas it cuts appear in <span class="math-container">$\Phi$</span>.</p>
<p>Note that two rules of <span class="math-container">$LK$</span> aren't &quot;sound&quot; in the sense that the conclusion sequent is not a logical consequence of the hypothesis sequent: right <span class="math-container">$\forall$</span>-introduction and left <span class="math-container">$\exists$</span>-introduction. As such, it is necessary to tweak the usual definition of soundness a bit in order to speak of the soundness of LK. We do this with the <em>universal closure</em>.</p>
<p>The universal closure of <span class="math-container">$A$</span>, denoted <span class="math-container">$\forall A$</span>, is the formula <span class="math-container">$\forall x_1 ... \forall x_k A$</span>, where <span class="math-container">$x_1, ..., x_k$</span> are all the free variables of <span class="math-container">$A$</span>. We define the universal closure of <span class="math-container">$\Phi$</span>, denoted <span class="math-container">$\forall \Phi$</span>, as <span class="math-container">$\{\forall A_i\}$</span>.</p>

<lo.logic><proof-complexity><first-order-logic>
Why isn't the proof obtained using Buss's proof of the derivational completeness of LK anchored?
Johnny
# Why isn't the proof obtained using Buss's proof of the derivational completeness of LK anchored?

(Asked by: username_0 on 2023-04-09)

The version of Buss's proof I'm referring to is the proof of Lemma II.2.24 in *Logical Foundations of Proof Complexity* by Cook and Nguyen. In the interest of keeping this question self-contained I've provided all the particularities of the book in the "Notations, Conventions and Definitions" section at the end of this question.

---

## Background

**Theorem II.2.23:** Let $\mathcal{L}$ be a first-order language which does not contain the equality symbol. Let $\Phi$ be a set of formulas of $\mathcal{L}$, and $\Gamma \rightarrow \Delta$ be a sequent of $\mathcal{L}$. There is an LK-$\Phi$ proof of $\Gamma \rightarrow \Delta$ iff $\forall \Phi \vDash \Gamma \rightarrow \Delta$.

The proof of this theorem relies on the following Lemma.

**Lemma II.2.24:** If $\Phi \vDash \Gamma \rightarrow \Delta$, then there is a cut-free LK proof of $C\_1, C\_2, ..., C\_k, \Gamma \rightarrow \Delta$, where $\{C\_i : i \in [k]\}$ is a finite subset of $\Phi$.

My question pertains specifically to the proof of completeness.

**Proof of completeness direction of Theorem II.2.23:** Let $\Phi$ be a set of formulas such that $\forall \Phi \vDash \Gamma \rightarrow \Delta$. By Lemma II.2.24, we know there is finite subset ${C\_1,...,C\_k}$ of $\Phi$ such that there is an LK proof $\pi$ of $S := \forall C\_1, ..., \forall C\_k, \Gamma \rightarrow \Delta$. Notice that if we can derive, for any $i \in [k]$, the sequent $\rightarrow \forall C\_i$, then we are done: by weakening each such sequent appropriately, we can apply the cut rule to remove $\forall C\_i$ from $S$. Applying all such cuts yields an LK-$\Phi$ proof $\pi'$ of the sequent $\Gamma \rightarrow \Delta$.

It remains to show that we can derive $\forall C\_i$. Starting from nonlogical axiom $\rightarrow C\_i$, we can apply the right $\forall$-introduction rule for each free variable in $C\_i$. $\blacksquare$

Note that in $\pi'$ above, we cut on formulas of the form $\forall C\_i$. Since $\pi'$ is an LK-$\Phi$ proof and not an LK-$\forall \Phi$ proof, this means that $\pi'$ is not necessarily anchored. However according to the book (assuming certain conditions on $\Phi$), it is possible to show that an anchored LK-$\Phi$ proof of $\Gamma \rightarrow \Delta$ exists. In the book, this is Theorem II.2.28. Proving this theorem is Exercise II.2.29.

---

## My Question

How isn't the following simple modification to the proof above a proof of anchored derivational completeness of LK?

**(Proposed) Proof:** Let $\Phi$ be a set of $\mathcal{L}$-formulas such that $\forall \Phi \vDash S$, where $S := \Gamma \rightarrow \Delta$. By Lemma II.2.24, we know there is finite subset ${C\_1,...,C\_k}$ of $\Phi$ such that there is a **cut-free** LK proof $\pi$ of $S := C\_1, ..., C\_k, \Gamma \rightarrow \Delta$. For any $i \in [k]$, by weakening each nonlogical axiom $\rightarrow C\_i$ appropriately, we can apply the cut rule to remove $C\_i$ from $S$. Applying all such cuts yields an LK-$\Phi$ proof $\pi''$ of the sequent $\Gamma \rightarrow \Delta$.

Since the only cuts in $\pi''$ are on $C\_i \in \Phi$, we conclude $\pi''$ is an anchored LK-$\Phi$ proof of $\Gamma \rightarrow \Delta$. $\blacksquare$

---

## Notations, Conventions and Definitions

Let $\mathcal{L}$ be a first order language. We define two disjoint, infinite set of variables of $\mathcal{L}$: *free* variables, and *bound* variables. As a convention, in any formula $A$ of $\mathcal{L}$ we require that there are no bound occurrences of free variables and that there are no free occurrences of bound variables in $A$.

We say formula $B$ is a logical consequence of $A$, denoted $A \vDash B$, if for every $\mathcal{L}$-structure $\mathcal{M}$ and every object assignment $\sigma$ from the variables of $L$ to the universe $M$ of $\mathcal{M}$, if $\mathcal{M}$ satisfies $A$ under $\sigma$, denoted $\mathcal{M} \vDash A[\sigma]$, then $\mathcal{M} \vDash B[\sigma]$.

If $\Phi$ is a set of formulas $\{A\_i\}$, then we say $\mathcal{M}$ satisfies $\Phi$ under $\sigma$, denoted $\mathcal{M} \vDash \Phi[\sigma]$, if $\mathcal{M} \vDash A\_i[\sigma]$ for all $i$. We say $B$ is a logical consequence of $\Phi$, denoted $\Phi \vDash B$, if $\mathcal{M} \vDash \Phi[\sigma]$ implies $\mathcal{M} \vDash B[\sigma]$.

Let $S := \Gamma \rightarrow \Delta$ be a sequent where $\Gamma := \{A\_1, ..., A\_m\}$ and $\Delta := \{B\_1, ..., B\_n\}$ are sets of $\mathcal{L}$-formulas. We define $A\_S$ as the first order formula

$$\lnot A\_1 \lor \lnot A\_2 \lor ... \lor \lnot A\_m \lor B\_1 \lor B\_2 \lor ... \lor B\_n$$

and we say that $\mathcal{M}$ satsifies $S$ under $\sigma$, denoted $\mathcal{M} \vDash S[\sigma]$, if $\mathcal{M} \vDash A\_S[\sigma]$. We say $S$ is a logical consequence of $\Phi$, denoted $\Phi \vDash S$, if $\mathcal{M} \vDash \Phi[\sigma]$ implies $\mathcal{M} \vDash S[\sigma]$.

An LK proof of $S$ is a tree $\pi$ with root is $S$ whose leaves are sequents $A \rightarrow A$ for any formula $A$, $\bot \rightarrow$, or $\rightarrow \top$ (we call these sequents *logical axioms*) and whose internal nodes are sequents such that if node $S'$ has set of children $H$, then $H$ is the set of hypothesis (top) sequents and $S'$ is the conclusion (bottom) sequent of one of the following rules.

[![PK rules](https://i.sstatic.net/U6Sbh.png)](https://i.sstatic.net/U6Sbh.png)

[![LK bonus rules](https://i.sstatic.net/a9rBZ.png)](https://i.sstatic.net/a9rBZ.png)

where $A(t)$ is the formula obtained by replacing all free occurrences of $x$ in $A(x)$ (i.e. the occurrences of $x$ in $\forall x A(x)$ which become free when we remove the $\forall x$ quantifier), with a term $t$ consisting entirely of free variables. Similarly, $A(b)$ is the formula obtained by replacing all free occurrences of $x$ in $A(x)$ by free variable $b$. In the left $\exists$-introduction and right $\forall$-introduction rules, $b$ must not occur anywhere in the conclusion sequent.

An LK-$\Phi$ proof of $S$ is an LK proof of $S$ in which we allow the leaves to be sequents of the form $\rightarrow A\_i$ for $A\_i \in \Phi$, which we call *nonlogical axioms*, in addition to the logical axioms.

We say that an LK-$\Phi$ proof is *cut-free* if it does not use the cut rule, and we say that it is *anchored* if the only formulas it cuts appear in $\Phi$.

Note that two rules of $LK$ aren't "sound" in the sense that the conclusion sequent is not a logical consequence of the hypothesis sequent: right $\forall$-introduction and left $\exists$-introduction. As such, it is necessary to tweak the usual definition of soundness a bit in order to speak of the soundness of LK. We do this with the *universal closure*.

The universal closure of $A$, denoted $\forall A$, is the formula $\forall x\_1 ... \forall x\_k A$, where $x\_1, ..., x\_k$ are all the free variables of $A$. We define the universal closure of $\Phi$, denoted $\forall \Phi$, as $\{\forall A\_i\}$.

**Tags:** lo.logic, proof-complexity, first-order-logic


---

## 1 answers

### Answer by username_0 on 2023-04-09. Score: 3 | Accepted answer

The answer occurred to me right after I finished typing up the post. Rather than delete it, I figured I would post it anyway in case anyone else has the same question.

---

## Answer

The mistake in the proposed proof is that in order to use Lemma II.2.24, I implicitly assume that if $\forall \Phi \vDash S$, then $\Phi \vDash S$. However, this is not necessarily true! Let $P$ be a 1-ary predicate of $\mathcal{L}$, and consider the example of $\Phi := \{P(b)\}$, and $S := \rightarrow \forall x Px$. Clearly $\forall \Phi \vDash S$, but it is not the case that $Pb \vDash \forall xPx$.


---

