Skip to main content
Theoretical Computer Science

You are not logged in. Your edit will be placed in a queue until it is peer reviewed.

We welcome edits that make the post easier to understand and more valuable for readers. Because community members review edits, please try to make the post substantially better than how you found it, for example, by fixing grammar or adding additional resources and hyperlinks.

Required fields*

9
  • 3
    $\begingroup$ I would think that (by the definition of a propositional proof system for the $\mathsf{coNP}$-complete language of tautologies), the assumption ("There is no proof system for propositional logic in which every tautology $\varphi$ has a proof of polynomial (in the length of $\varphi$) length") is almost identical to assuming $\mathsf{NP}\neq\mathsf{coNP}$; and hence almost identical to assuming $\mathsf{NP}\neq\mathsf{P}$. $\endgroup$ Commented Oct 11, 2014 at 14:18
  • $\begingroup$ @IddoTzameret: but we do need to know that TAUTOLOGY is $\mathsf{coNP}$-complete, right? And that is not trivial. I guess this example is just reaffirming the interest of having "natural" complete problems: we may talk about complexity classes without explicitly talking about the machines used to define them (which seems to be what the OP is asking). Or maybe I misunderstood your comment... $\endgroup$ Commented Oct 11, 2014 at 17:37
  • 1
    $\begingroup$ @Damiano, I think the fact that TAUT is coNP-complete is trivial, in the sense that it is implied by its definition and the NP completeness of SAT. $\endgroup$ Commented Oct 11, 2014 at 17:48
  • $\begingroup$ @IddoTzameret, Ok, but you do agree that the $\mathsf{NP}$-completeness of SAT is not trivial, right? That's essentially what I was saying. I mean, between the statement "$\mathsf{NP}\neq\mathsf{coNP}$" formulated in terms of Turing-machines and their runtime and the stament "there is no polynomially bounded propositional proof system" I see a non-trivial gap, they definitely don't look "almost identical". That gap is in the completeness of TAUT or SAT, whichever you like, but it's there. Don't you agree? $\endgroup$ Commented Oct 11, 2014 at 17:59
  • 1
    $\begingroup$ Yes, the property "$p$ is a proof of $\varphi$" must be checkable in polynomial (in $|p|$ and $|\varphi|$) time . And it must be sound and complete, i.e., a formula should have a proof iff it is a tautology. $\endgroup$ Commented Oct 14, 2014 at 14:18