1
$\begingroup$

This question concerns the derivational soundness and completeness of the first-order proof system LK (without equality) as presented in Logical Foundations of Proof Complexity by Cook and Nguyen. In the interest of keeping this question self-contained for the reader unfamiliar with the particularities of this book, I've included a "Notations, Conventions and Definitions" section at the end of this question.


Background

The way precise way in which the derivational soundness and completeness of LK is stated in the book is as follows.

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$. $\diamond$

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$. $\diamond$

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.

Theorem II.2.28: Let $\mathcal{L}$ be a first-order language which does not contain the equality symbol. Suppose that $\Phi$ is a set of formulas closed under substitution of terms for variables (i.e. if $A(b)$ is in $\Phi$, then $A(t)$ is also in $\Phi$ for any term $t$ consisting entirely of free variables). If $\Gamma \rightarrow \Delta$ is a sequent of $\mathcal{L}$ which is a logical consequence of $\Phi$, then there is an anchored LK-$\Phi$ proof of $\Gamma \rightarrow \Delta$. $\diamond$


Question

Rather than state the derivational soundness and completeness of LK as in Theorem II.2.23 above, why don't we state it as follows instead?

(Alternative) Theorem: 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}$.

(Soundness) If there is an LK-$\Phi$ proof of $\Gamma \rightarrow \Delta$, then $\Gamma \rightarrow \Delta$ is a logical consequence of $\forall \Phi$

(Completeness) If $\Gamma \rightarrow \Delta$ is a logical consequence of $\Phi$, then there is an LK-$\Phi$ proof of $\Gamma \rightarrow \Delta$. $\diamond$

The soundness statement is as in the Theorem II.2.23, so we need only prove completeness. However, this can be done via a simple modification to the proof for Theorem II.2.23.

Proof of (Alternative) Completeness: Let $\Phi$ be a set of $\mathcal{L}$-formulas such that $\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$. $\blacksquare$

Note that $\Phi \vDash S$ implies $\forall \Phi \vDash S$, but the converse isn't necessarily true. As such, the alternative derivational completeness is weaker than the version of derivational completeness in Theorem II.2.23 in the sense that the latter implies the former. However unlike the proof for Theorem II.2.23, the proof of the alternative derivational completeness above is anchored. We did not require any additional theorems with non-trivial proofs like Theorem II.2.28 or constraints on $\Phi$.

So then why doesn't this alternative statement of the derivational completeness of LK suffice? The reason why I ask this question here and not on math stack exchange is I'm particularly interested in if somehow the alternative version of derivational completeness is insufficient for results in proof complexity or bounded arithmetic. Do we lose anything by not requiring that derivational soundness and completeness of LK be exact converses of eachother?


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

LK bonus rules

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\}$.

$\endgroup$

0

Your Answer

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