Take the 2-minute tour ×
Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It's 100% free, no registration required.

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).

share|improve this question
1  
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! –  vzn Jul 1 at 15:23
1  
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. –  Sasho Nikolov Jul 1 at 23:27
1  
see also results in TCS independent of ZFC which indicates roughly "not much so far"... –  vzn Jul 2 at 1:44
4  
@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. –  Damiano Mazza Jul 2 at 14:06
1  
@DamianoMazza Thanks Damiano, you are right, apologies for making an incredibly strong claim. –  Sasho Nikolov Jul 2 at 20:16

1 Answer 1

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.

share|improve this answer
1  
It would be quite interesting/bizarre if choice is required for the proof (i.e. ZFC works, ZF doesn't). –  usul Jul 1 at 13:55
    
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). –  Constantine Kyritsis Jul 1 at 15:14
    
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). –  Constantine Kyritsis Jul 1 at 15:15
3  
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. –  David Harris Jul 3 at 19:43
1  
@usul: It's not just bizarre, it is in fact impossible. ZFC is conservative over ZF for arithmetical statements. –  Emil Jeřábek Jul 10 at 8:41

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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