Timeline for Lengths of proofs and quasilinear time
Current License: CC BY-SA 4.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 24, 2018 at 17:58 | comment | added | Dmytro Taranovsky | @lambda.xy.x By proof length, I mean the length of the binary string encoding the proof. Note that while there are different reasonable uncompressed binary encodings of formulas, their sizes agree up to a polylogarithmic (in proof length) factor given that a variable name uses $O(\log n)$ bits. | |
| Oct 24, 2018 at 11:11 | comment | added | lambda.xy.x | By the way, thanks for the link - I was aware that in higher order logic, ∀X.X→X subsumes the cut rule but I forgot that you can use it as an axiom scheme in first order logic as well. | |
| Oct 24, 2018 at 11:07 | comment | added | lambda.xy.x | It seems we have different notions of usual because I assume explicit contraction rules by default :-) If you use a sequent calculus with built-in contraction, there is still a linear proof of the formula with n applications of w:r,∀:r,... . The sequent size never grows beyond two formulas as well. Could you perhaps clarify what the "number of bits" measures? | |
| Oct 24, 2018 at 1:16 | comment | added | Dmytro Taranovsky | @lambda.xy.x The insight of the question is that for proofs in ZFC, all sufficiently powerful appropriate proof systems are in fact quasilinear-time equivalent, with the question being to give (with proof) a natural example of such a proof system. | |
| Oct 24, 2018 at 1:16 | comment | added | Dmytro Taranovsky | @lambda.xy.x If each application of ∀:r includes a copy of the formulas used (as is standard), the number of bits is quadratic. Also, by "typical proof systems", I only meant proof systems with the cut rule or a reasonable substitute, but see Cut-free proofs in ZFC. | |
| Oct 23, 2018 at 23:45 | comment | added | lambda.xy.x | Reading on further, I'm not even sure if you speak about proof checking or the sizes of the actual proofs :( | |
| Oct 23, 2018 at 23:40 | comment | added | lambda.xy.x | I would also be surprised if the non-elementary speedup of a sequent calculus with cut against one without cut can be remedied by picking the right axiom system. So I'm not even sure about the "typical proof systems are equivalent up to a polynomial factor." If I remember correctly, proof systems are often incomparable when it comes to proof complexity in the sense that there are formulas F and G such that proof system A has a short proof of F and a long proof of G but a proof system B has a short proof of G and a long proof of F. | |
| Oct 23, 2018 at 23:32 | comment | added | lambda.xy.x | I'm still trying to understand the actual question, but I'm wondering why a sequent calculus proof of ∀x1...∀xn 0=0 should be quadratic in the formula size. It should be n applications of ∀:r inferred from 0=0 as an instance of the reflexivity axiom of equality. | |
| Oct 13, 2018 at 21:19 | history | asked | Dmytro Taranovsky | CC BY-SA 4.0 |