When the conjecture $\mathbf{P} = \mathbf{NP}$ or $\mathbf{P} \neq \mathbf{NP}$ is set (e.g. by the Clay Mathematical Institute by S. Cook, see here) what mathematical axiomatic system is assumed?

In order to prove or disprove such statements, you need to assume some axioms. Which ones? Only the Peano (2nd order formal language) arithmetic? The Zermelo–Fraenkel set theory with the axiom of choice? Smaller axiomatic set theories (e.g. Gödel's constructible sets, where the continuum hypothesis holds too, see here)?

Obviously, it should be an axiomatic theory that accepts the countable infinite. But which in particular? Is there any published result that would prove them consistent in a particular axiomatic set theory? (In other words, defining a model in which it is true, but not claiming to be true in all models).

  • 1
    $\begingroup$ its generally based on the TM model which has not been shown to have any particular dependence on the choice of set theory axioms... so far! $\endgroup$
    – vzn
    Jul 1 '14 at 15:23
  • 1
    $\begingroup$ You might find this interesting scottaaronson.com/papers/pnp.pdf. Among other very interesting things, the survey talks about why if P vs NP were independent of PA, then we'd almost prove P=NP. For example, independence implies NP is in $\mathsf{DTIME}(n^{\alpha(n)})$ where $\alpha(n)$ is the inverse Ackermann functions. $\endgroup$ Jul 1 '14 at 23:27
  • 1
    $\begingroup$ see also results in TCS independent of ZFC which indicates roughly "not much so far"... $\endgroup$
    – vzn
    Jul 2 '14 at 1:44
  • 4
    $\begingroup$ @SashoNikolov: if I am not mistaken, what you say is true if independence is proved using currently known general techniques (e.g. forcing, classical realizability, etc.). In fact, the argument you are alluding to rests on the fact that: 1) there are $\Pi^0_1$ sentences implying $P\neq NP$ (such as "$SAT$ does not have quasi-polynomial circuits"); 2) those techniques generate only models satisfying every $\Pi^0_1$ sentence true in the standard model. This shows that current techniques are probably useless for the independence of P vs NP, not that independence is unlikely in general. $\endgroup$ Jul 2 '14 at 14:06
  • 1
    $\begingroup$ @DamianoMazza Thanks Damiano, you are right, apologies for making an incredibly strong claim. $\endgroup$ Jul 2 '14 at 20:16

It's not specified. When there is a serious enough candidate paper purporting to resolve P ≟ NP, a Special Advisory Committee will be formed to decide whether (and to whom) to award the prize. I presume that the Special Advisory Committee will decide whether your system of axioms is acceptable. If you assume Z-F with choice, I guarantee you they will take it. If you assume P ≠ NP as an axiom, I guarantee you they won't.

  • 1
    $\begingroup$ It would be quite interesting/bizarre if choice is required for the proof (i.e. ZFC works, ZF doesn't). $\endgroup$
    – usul
    Jul 1 '14 at 13:55
  • $\begingroup$ I thank the people for their answers so far. It makes sense that it is not specified and it is variable which axiomatic (set theory) system is assumed. It seems to me that in a quite restrictive axiomatic set theory (or restrictive model of axiomatic set theory) it is more probable that one can prove that NP=EXPTIME and in a more pluralistic (axiomatic system or model of set theory) more probable that NP is not EXPTIME (finer grades of complexity differences). $\endgroup$ Jul 1 '14 at 15:14
  • $\begingroup$ And even it might happen that one can come with a proof, that inside Peano Arithmetic (with sets definable from logical formulas only without axioms of set theory) the famous conjectures are independent and not provable (Unless there is already a result about these conjectures inside Peano Arithmetic or a simpler impossibility argument which I do not know). $\endgroup$ Jul 1 '14 at 15:15
  • 3
    $\begingroup$ No one seriously thinks that P != NP is independent of ZFC. We don't know of any non-contrived mathematical statements that are independent of ZFC (other than the obvious Godelian ones). This outcome just isn't going to happen. $\endgroup$ Jul 3 '14 at 19:43
  • 2
    $\begingroup$ @usul: It's not just bizarre, it is in fact impossible. ZFC is conservative over ZF for arithmetical statements. $\endgroup$ Jul 10 '14 at 8:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.