There are a number of results in proof theory which state results about blow-up of proofs during cut elimination, i. e. that the only cut free proofs of a theorem can be much larger than proofs with cut.

This is intuitive to me because if cut elimination is thought of as computation it just means that a normal form of a program can be much larger than the original program, which will be true whenever you can write fast growing functions in the programming language.

My question is, are there natural examples of this phenomenon? What are some simple classes of theorems that have short proofs with cut but the only cut free proofs are long?

I would not be surprised if the cut-free proof of `P 0 -> (forall n, P n -> P (n+1)) -> P (2^k)`

is exponentially larger when the constant `k`

grows. (Disclaimer: I am assuming that there is no axiom scheme of recurrence for `P`

here.)

If `P`

the constant `nat`

and the induction defines a fast-growing function, this exactly corresponds to the intuition on normal forms above. Now swap `nat`

for a more proof-like type, and you'd get the same behaviour. (Btw, even if there is a recurrence scheme, recurrence is an eliminator, so it creates a cut, right? So it would be eliminated away?)

It depends on your logic framework. For example, in Peano's arithmetic, the formula I gave has a constant-size cut-free proof. So, my disclaimer was just here to exclude this kind of degenerate proof.

In proof theory textbooks there is usually mention of an example of a proof with cut that takes up 1 or two pages but the cut eliminated form would amount to something about matter in the universe. I traced it back to an article from George Boolos called "Don't eliminate cut". Though actually reading the article I did not really get the impression it was such a concrete example.

I suppose for Q my guess would be that since we don't have exponentiation we probably won't get huge cut-free proofs. Don't know if it is polynomial tho.

I'm not sure Guillaume's example works since you have 2^k, which I don't think is definable in Q.

Or actually nevermind, I see that was meant to be a fixed constant in the metatheory now.

with

```
Inductive even : nat -> Prop := even0 : even 0 | evenSS : forall n, even n -> even (S (S n)).
```

you can define a lemma `evenTwice : forall x:Z, even (Z.to_nat (2 * x))`

Then `evenTwice x`

with a literal `x`

has size `n = log x`

but reducing it produces a proof of size `2^n = x`

Last updated: Mar 03 2024 at 15:01 UTC