Patrick Nicodemus (Mar 20 2023 at 22:31): Patrick Nicodemus (Mar 20 2023 at 22:31):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?
Guillaume Melquiond (Mar 21 2023 at 07:13):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.)
Meven Lennon-Bertrand (Mar 21 2023 at 09:57):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?)
Guillaume Melquiond (Mar 21 2023 at 13:18):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.
Ali Caglayan (Mar 21 2023 at 14:23):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.
Ali Caglayan (Mar 21 2023 at 14:26):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.
Ali Caglayan (Mar 21 2023 at 14:27):I'm not sure Guillaume's example works since you have 2^k, which I don't think is definable in Q.
Ali Caglayan (Mar 21 2023 at 14:28):Or actually nevermind, I see that was meant to be a fixed constant in the metatheory now.
Gaëtan Gilbert (Mar 21 2023 at 14:41):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: Jun 05 2023 at 10:01 UTC