Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: deprecated: logic

Topic: proofs of cut-elimination theorem

সায়ন্তন রায় (Oct 10 2022 at 14:03):

Recently I have started studying sequent calculus. The original proof of the cut-elimination theorem by Gentzen looks very complex. I was wondering if there is some very easy proof of cut-elimination (may be non-constructive) which is also applicable to a wide variety of other sequent systems. Here by the cut-rule I mean the following: if $\vdash_{\mathbf{S}}\Gamma\Rightarrow \Delta,\alpha$ and $\vdash_{\mathbf{S}}\alpha,\Gamma\Rightarrow\Delta$ then $\vdash_{\mathbf{S}}\Gamma\Rightarrow\Delta$ where $\vdash_{\mathbf{S}}\Gamma\Rightarrow\Delta$ means that there is a proof of the sequent $\Gamma\Rightarrow\Delta$ in the sequent system $\mathbf{S}$.

Zhen Lin Low (Oct 10 2022 at 14:16):

My impression is that the cut-elimination theorem is a deep result (because it is supposed to be an argument for the consistency of logic) and also delicate (i.e. sensitive to hypotheses), and my experience is that such theorems do not have "easy" proofs.

John Baez (Oct 10 2022 at 14:30):

That's my impression too, but I've never gone through this proof, so I'd like to hear people's opinions on what's the easiest proof to follow. (Of course what's easy to follow depends on the person. If you know me, you can guess what I find easy to follow.)

সায়ন্তন রায় (Oct 10 2022 at 14:39):

Actually, I am more interested to see "easy" proofs of cut-elimination theorem for the sequent systems of propositional logics.

Jean-Baptiste Vienney (Oct 10 2022 at 22:04):

The proof of cut-elimination for classic logic is complex because classical logic is a system about truth values which is quite abstract. I know more the one for linear logic.

The cut-elimination for linear logic is much more down to earth. It is really algorithmic: you have a transformation to use for each instance of the cut rule and this transformation depends of the two inference rules used before the cut rule. It gives you an algorithm with a very good property: you can apply these transformations in any order, at the end you will have a proof without any cut. The proof thus consists in:
1) List the transformation to apply to a cut depending on the two preceding used inference rules.
2) Define a measure which attributes a nonnegative integer to every proof (typically something like the sum of the depths of all cuts in the proof).
3) Prove that the measure decreases strictly when you apply a transformation.
Because the measure can't be negative, you know that you can eliminate the cuts, moreover with the good property.

Classical logic is not about algorithms but more about the truth. Proving the cut elimination is thus more about proving that the theorem is true but without any concrete algorithm. However some people know probably more about this than me and you should also have some more or less algorithmic interpretation of the cut elimination for classical logic but it's more complicated.

Ulrik Buchholtz (Oct 11 2022 at 07:25):

You can get cheap & easy proofs of cut-elimination by completeness of the cut-free calculus. But the interest in cut-elimination results often lie in the precise bounds associated with more refined versions (e.g., ordinal indexed versions).

Mike Shulman (Oct 11 2022 at 08:28):

How do you prove completeness of the cut-free calculus without basically proving cut-elimination?

Jean-Baptiste Vienney (Oct 11 2022 at 08:32):

I'm interested as well by the answer :smile:

Damiano Mazza (Oct 11 2022 at 11:49):

Actually, cut-elimination in classical logic is provable by exactly the same methods mentioned by @Jean-Baptiste Vienney. See for instance Chapter 13 of Girard, Lafont and Taylor's Proofs and Types. In fact, cut-elimination in linear logic is just a re-iteration of the usual proof for classical sequent calculus, which is very modular and applies essentially unchanged to lots of different systems (it only relies on the existence of rewriting rules for so-called principal cuts and the fact that a non-principal cut may be turned into a principal one via some commutations).

The non-constructiveness of classical logic does not manifest itself in the absence of an algorithmic procedure for eliminating cuts, but rather in the uncontrolled non-determinism of such a procedure: a single proof with cuts may reduce to a host of cut-free proofs (of the same sequent). If one wants to see proofs as programs, this is a deal-breaker because it means that programs do not have a well-defined result. By contrast, the very same procedure in intuitionistic logic is deterministic: modulo inessential commutations, every proof reduces to a unique cut-free proof. Classical sequent calculi with a deterministic cut-elimination procedure do exist, but they all require some notion of polarity which was understood only after the introduction of linear logic (so more than half a century after Gentzen).

Damiano Mazza (Oct 11 2022 at 12:03):

About the "difficulty" of the cut-elimination proof, of course it depends on the eye of the beholder but I do not find the usual proof to be particularly hard. Like many syntactic theorems, there's just a ton of cases to inspect, but there's nothing difficult conceptually: you assign an ordinal to every proof (for "pure" first order logic it will be smaller than $\omega^\omega$, so nothing scary at all), such that cut-free proofs have ordinal $0$, and then show that in every proof $\pi$ with cuts there's always a cut which may be rewritten so that the ordinal of the resulting proof is strictly smaller than the ordinal of $\pi$. Such a cut is usually immediate to find (it is one such that there are no other cuts above it, which exists by finiteness of proofs).

The number of cases heavily depends on the specific formulation of sequent calculus. For classical first-order logic, one may use a one-sided formulation, which drastically reduces the number of cases. This is the approach I take when I teach this stuff. For example, in Chapter 6 of these notes I manage to do it with only four principal cases and two commutative cases.

NB: All the above assumes that we are talking about propositional or first-order logic. Cut-elimination for higher-order logic is another story: for example, cut-elimination of second-order intuitionistic sequent calculus implies the consistency of second-order Peano arithmetic, which is huge. You need non-trivial techniques for that, essentially boiling down to Girard's reducibility candidates. I guess it is fair to say that those proofs are hard :big_smile:

Lê Thành Dũng (Tito) Nguyễn (Oct 11 2022 at 16:23):

Damiano Mazza said:

By contrast, the very same procedure in intuitionistic logic is deterministic: modulo inessential commutations, every proof reduces to a unique cut-free proof.

Indeed, but I'd add that even in intuitionistic logic, it is useful to distinguish between the proof-irrelevant "cut-admissibility" and the proof-relevant "normalization", as discussed here: https://prooftheory.blog/2020/09/07/simple-proofs-of-cut-elimination-ii-intuitionistic-logic/

Lê Thành Dũng (Tito) Nguyễn (Oct 11 2022 at 16:24):

BTW cut-elimination for classical logic is discussed in the same blog post series here: https://prooftheory.blog/2020/05/07/simpler-proofs-of-cut-elimination-i-classical-logic/

Ulrik Buchholtz (Oct 11 2022 at 20:15):

Mike Shulman said:

How do you prove completeness of the cut-free calculus without basically proving cut-elimination?

(also to @Jean-Baptiste Vienney) One way is via Schütte's search tree method. You define a canonically defined, potentially infinite, proof tree, that systematically uses all rules (and is “fair” in some sense). If this tree is finite, it gives a proof, and the key is to show that if it's infinite, you can build a countermodel (so this is a classical argument).

This has a quite different feel to it than a direct cut-elimination proof, no?

সায়ন্তন রায় (Oct 12 2022 at 06:39):

The following argument can be used to proof the cut-elimination theorem for $\bf{LK}$. But it is non-constructive, in the sense that it gives no idea regarding how to actually eliminate cuts. Suppose that,

• $\bf{PLK}$ denotes the propositional fragment of $\bf{LK}$.
• $\bf{PLK}^*$ denotes the propositional fragment of $\bf{LK}$ without cut.
• $\vdash_{\bf{PLK}}\Gamma\Rightarrow\Delta$ denotes that $\Gamma\Rightarrow\Delta$ has a proof in $\bf{LK}$.
• $\vdash_{\bf{PLK}^*}\Gamma\Rightarrow\Delta$ denotes that $\Gamma\Rightarrow\Delta$ has a cut-free proof in $\bf{LK}$.

To prove cut elimination for $\bf{PLK}$ means to show that: for all $\Gamma,\Delta$, $\vdash_{\bf{PLK}}\Gamma\Rightarrow\Delta$ implies that $\vdash_{\bf{PLK}^*}\Gamma\Rightarrow\Delta$. We induct on the number of connectives in $\Gamma\cup\Delta$. If it is $0$ then we are done (there are only four cases to consider). So, assume that if $\vdash_{\bf{PLK}}\Gamma\Rightarrow\Delta$ implies that $\vdash_{\bf{PLK}^*}\Gamma\Rightarrow\Delta$ whenever the total number of connectives in $\Gamma$ and $\Delta$ is $n$. For the induction step, consider the case when it is $n+1$ and suppose e.g., that $\Delta=\Delta',\alpha\land\beta$. So, $\Gamma\Rightarrow\Delta$ is the same as $\Gamma\Rightarrow\Delta',\alpha\land\beta$. Then each of the premise of the right-$\land$-introduction rule has total number of connectives strictly less than $n+1$. So, by induction hypothesis, each has a cut-free proof. Consequently, it follows that $\Gamma\Rightarrow\Delta$ has a cut-free proof as well. (Of course, one needs to consider other cases as well.)

This argument looks pretty ''simple'' to me (unless I am gravely mistaken), although, may not be "informative" due to its non-constructive nature.

Ryan Wisnesky (Oct 12 2022 at 07:18):

Hm, I'm not sure I understand why that proof is non-constructive- where does it use excluded middle or double negation elimination or axioms of choice, etc? Couldn't you turn its inductive argument into a recursive algorithm? IIRC, the usual place where proofs of strong normalization for various type theories (such as system F, whose terms are proofs in 2nd order logic) fail is in the inductive step, where the number of connectives actually increases via substitution when you e.g. consider the case of a lambda abstraction applied to an argument, or a 'type lambda' applied to a type argument.

Jean-Baptiste Vienney (Oct 12 2022 at 09:59):

The method for your proof seems slightly incorrect and I think you are effectively mistaken.

If you suppose that $\vdash_{\bf{PLK}} \Gamma \Rightarrow \Delta', \alpha \wedge \beta$, how do you know that it is provable in $\bf{PLK}$ using a right-$\wedge$-introduction as last step, which produce $\alpha \wedge \beta$? This proposition is probably true but it would be difficult to prove it without assuming first a result such as the cut elimination or the completeness of $\bf{PLK}$.

To prove a result on all the proofs of a sequent calculus, it is usually better to induct on the structure of proofs than on the number of connectives in the sequents. What it means is that the initialization is the case of a proof reduced to an axiom and for the induction you have one step for every inference rules. For instance for the right-$\wedge$-introduction, you are going to prove that if your theorem is true for $\pi_{1}:\Gamma \Rightarrow \Delta, A, \Delta'$ and for $\pi_{2}:\Gamma' \Rightarrow \Delta'', B, \Delta'''$, then it is true for the proof starting from $\pi_{1}$ at the left and $\pi_{2}$ at the right, followed by right-$\wedge$-introduction which gives $\pi:\Gamma,\Gamma' \Rightarrow \Delta, \Delta'', A \wedge B, \Delta', \Delta'''$. For the case of inference rules which are preceded by only one proof, such as the contraction rule, your are going to suppose that your theorem is true for the proof $\pi_{1}$ before the contraction and show that it is true for $\pi$ which is equal to $\pi_{1}$ followed by the contraction step. You thus have as many case for the induction that the number of inference rules in your sequent calculus.

Using such a method, you can probably prove the cut elimination without assuming before a result which looks to come logically after the cut elimination.

As written upper, you have mainly two class of methods to prove cut elimination: the syntactic ones ie. proving the cut elimination with an inductive proof and the semantics one ie. proving completeness of the calculus without the cut rule with another method and then deduce the cut elimination. In any case, it is never super fast to prove cut elimination.

সায়ন্তন রায় (Oct 12 2022 at 13:28):

Many thanks for all the helpful comments.

Damiano Mazza (Oct 14 2022 at 16:56):

@Ulrik Buchholtz

One way is via Schütte's search tree method.

If I am not mistaken, this proof method crucially uses cut. The proof I know builds the countermodel by observing that the infinite tree generated by an unprovable formula $A$ contains an infinite branch in which, roughly, for every closed formula $B$, either $B$ itself appears in the branch or $\lnot B$ does, and the set of formulas that appear in the branch is an ideal of formulas. This is fundamental because it implies that the formulas not appearing in the branch are an ultrafilter of formulas and, therefore, a model of $\lnot A$ (because $A$ appears at the root of the tree). Now, if you never use cut, by the subformula property your infinite tree would only contain subformulas of $A$, so the reasoning above cannot work. So, as far as I understand, Schütte's method shows the completeness of first-order classical sequent calculus with cuts. Am I missing something?

Ulrik Buchholtz (Oct 15 2022 at 13:53):

Damiano Mazza said:

Ulrik Buchholtz

One way is via Schütte's search tree method.

If I am not mistaken, this proof method crucially uses cut. The proof I know builds the countermodel by observing that the infinite tree generated by an unprovable formula $A$ contains an infinite branch in which, roughly, for every closed formula $B$, either $B$ itself appears in the branch or $\lnot B$ does, and the set of formulas that appear in the branch is an ideal of formulas. This is fundamental because it implies that the formulas not appearing in the branch are an ultrafilter of formulas and, therefore, a model of $\lnot A$ (because $A$ appears at the root of the tree). Now, if you never use cut, by the subformula property your infinite tree would only contain subformulas of $A$, so the reasoning above cannot work. So, as far as I understand, Schütte's method shows the completeness of first-order classical sequent calculus with cuts. Am I missing something?

I think you're thinking of the Rasiowa–Sikorski proof. This is different from the search tree method. I mentioned Schütte, but similar things were done independently by Beth, Hintikka, and Kanger. See Herbelin–Ilik for these references. And indeed, in this method you don't use cut rules. Extensions of this method were then used by Tait, Prawitz, and Takahashi (independently) to prove Takeuti's conjecture (i.e., cut-free completeness of second order logic wrt Henkin semantics). This was done before Girard gave a strong normalization style proof.

সায়ন্তন রায় (Mar 19 2023 at 16:14):

I didn't want to open a new topic just for this question because I think that the answer to this question is probably very simple, which, for some reason I am unable to figure out. The question is: Is there any argument to prove that there is no proof of $\bot$ in $\mathbf{PLK}$ (the propositional fragment of $\mathbf{LK}$) without using soundness theorem, completeness theorem, subformula property and/or any consequence of cut-elimination theorem?

Ryan Wisnesky (Mar 19 2023 at 16:32):

I only know of three ways to prove that there is no proof of false in any system: strong normalization / cut elimination, or construct an explicit model, or show that if there is no model, some other contradiction follows. How would you try to do this for some other logic / fragment thereof?

সায়ন্তন রায় (Mar 19 2023 at 16:38):

@Ryan Wisnesky I was hoping to proceed in the following manner: Suppose that there is a proof of $\bot$ in $\bf{PLK}$. Consider any such proof of minimal height. Then in the last step before $\bot$ only cut can be used. I was hoping to somehow contradict the minimality assumption, but could not.

Ryan Wisnesky (Mar 19 2023 at 16:49):

Yeah, that definitely sounds like a cut-based approach. Since your logic is propositional, do you really need the machinery of cut elimination, etc? Maybe a straight inductive argument would work? It's usually in dealing with quantifiers where the hard part of strong normalization arguments are.

সায়ন্তন রায় (Mar 19 2023 at 16:51):

Unfortunately, that's precisely where I have been stuck.

সায়ন্তন রায় (Mar 19 2023 at 17:02):

Probably what you are saying is to apply induction on the step number and on the statement that at no step do we get a sequent in which both sides are empty.

Ryan Wisnesky (Mar 19 2023 at 18:21):

I'm not sure, but the usual advice when stuck on an inductive proof is to strength the inductive hypothesis or induct on something else, so good luck!