Re: alternate characterization of the class NP?

On Jun 9, 4:57 pm, tc...@xxxxxxxxxxxxx wrote:
In article <2bd3a75b-a49d-4f2e-a5f4-e6d9dd84c...@xxxxxxxxxxxxxxxxxxxxxxxxxxx>,

 <cplxp...@xxxxxxxxx> wrote:
In other words, NP2 consists of all languages for which members of the
language can be proven to be as such by a formal proof in polynomial
space with respect to the length of each respective member.  I've
replaced a simple certificate with a formal proof.

Without fussing over the details of your definition, I can say that you're
on the wrong track.  Any definition in terms of formal proofs will have to
specify which axioms for mathematics you're using.  But the definition of
NP is independent of any such choice.

If you Google "Goedel completely convinced Turing's paper" then you will
find quotations from Goedel where he emphasizes that computability is an
"absolute" notion in the sense that it does not depend on a choice of
axioms for mathematics.  He wasn't convinced of this at first but became
convinced by reading Turing's paper.

If you're still barking up this tree then you probably haven't yet
internalized the notion that *formal* mathematical proofs are always
relative to some arbitrary choice of axioms.
--
Tim Chow       tchow-at-alum-dot-mit-dot-edu
The range of our projectiles---even ... the artillery---however great, will
never exceed four of those miles of which as many thousand separate us from
the center of the earth.  ---Galileo, Dialogues Concerning Two New Sciences

Thanks for addressing this...my goal was to attempt to show that P =
NP is formally independent of ZFC. I was assuming that the axioms are
the axioms of ZFC, and I was hoping to find a language L such that I
could prove that L is provably in P but such that the question of
whether or not L is formally independent. I was hoping to arrive at a
characterization of NP in ZFC that does not depend on Turing machines.

Does this change anything? I wasn't sure what you meant by barking up
the wrong tree. Does that mean that the characterization I gave is
not the same as NP, or just that what I was considering is unlikely to
be a fruitful approach?

I do understand, now that you've pointed this out, that computation is
independent of logical theories. However, valid formal proofs can be
verified in polynomial time...which is why I am interested in this. I
suppose the problem is that it's theoretically possible that for some
languages, the size of the proof generated from the certificate might
be exponentially larger than the size of the certificate.

If I'm just not getting it I apologize....

-Phil
.

Relevant Pages

  • Re: [Lit.] Buffer overruns
    ... >> In my experience the most difficult language feature is not buffer ... some errors will have to be catered for at run time and not at design time. ... in retrospect to be an error in the formal proof (actually in the ... languages because they exist as a part of the language design. ...
    (sci.crypt)
  • Re: What is a proof, exactly?
    ... >> In Norm Megill's formalization of set theory in Metamath, a formal proof ... The complete proof of a theorem all the way back to axioms can be ... to try to find the longest path back to an ... interesting and important set theory results along the way. ...
    (sci.logic)
  • Re: Well Ordering the Reals
    ... or a clarification of what my idea is when it's ... formal proof that can be unambiguously checked for correctness. ... the proof from those axioms is checkable. ...
    (sci.math)
  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... We say we have a formal proof: you say can I see it. ... proof (according to the standard meaning in mathematics). ... that you want not only a formalized proof, but also the natural language ... we are not using the axioms of Euclid. ...
    (sci.logic)
  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... We say we have a formal proof: you say can I see it. ... proof (according to the standard meaning in mathematics). ... in just a few simple lines using only principles from elementary ... we are not using the axioms of Euclid. ...
    (sci.logic)