Skip to main content

Timeline for answer to Statements that imply $\mathbf{P}\neq \mathbf{NP}$ by Jan Johannsen

Current License: CC BY-SA 4.0

Post Revisions

13 events
when toggle format what by license comment
S Apr 25, 2022 at 7:45 history suggested Martin CC BY-SA 4.0
added a doi-link instead of the dead Project Euclid link
Apr 23, 2022 at 7:57 review Suggested edits
S Apr 25, 2022 at 7:45
Nov 11, 2015 at 16:24 vote accept Dominic van der Zypen
Oct 14, 2014 at 20:01 comment added Jan Johannsen Yes, that's also what Iddo was saying in his comment above. Nevertheless I think it's a natural property to ask of a proof system that proofs should be efficiently checkable.
Oct 14, 2014 at 18:46 comment added Joshua Grochow But then the very definition of proof that is being used here is tightly bound up with time complexity, and in particular with the class $\mathsf{P}$...
Oct 14, 2014 at 14:18 comment added Jan Johannsen 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.
Oct 14, 2014 at 14:13 comment added cody I'm confused: i can build a "proof system" by saying, $\varepsilon$ is a proof for $P$ iff $P$ is a tautology. Every proof has length 1 and is therefore polynomially bounded. Don't you need a couple more assumptions on what constitutes a proof?
Oct 12, 2014 at 15:57 comment added Iddo Tzameret @Damiano, the OP asks for problems seemingly unrelated to complexity or Turing machines that imply $NP\neq P$. Jan's suggestion is a very good one; I was only arguing that it is directly related to complexity and Turimg machines (by definitions).
Oct 11, 2014 at 17:59 comment added Damiano Mazza @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?
Oct 11, 2014 at 17:48 comment added Iddo Tzameret @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.
Oct 11, 2014 at 17:37 comment added Damiano Mazza @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...
Oct 11, 2014 at 14:18 comment added Iddo Tzameret 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}$.
Oct 10, 2014 at 11:24 history answered Jan Johannsen CC BY-SA 3.0