Re: Is this proof valid?

On Feb 16, 12:46 pm, Patricia Shanahan <p...@xxxxxxx> wrote:
cplxp...@xxxxxxxxx wrote:
On Feb 16, 11:47 am, Patricia Shanahan <p...@xxxxxxx> wrote:
cplxp...@xxxxxxxxx wrote:
Working in ZFC, consider another arbitrary formal theory X.  We say
that the decision problem PROVABLE_X is the decision problem
associated with determining if an inputted binary string represents a
provable theorem in X.
Now we prove the following lemma in ZFC:  'If X is inconsistent,
PROVABLE_X is an element of P.'  Proof:  Assume X is inconsistent..
Then every wff in X is a provably true theorem.  Thus, all we must do
is verify that an inputted binary string is a wff.  This can be done
in polynomial time; thus, PROVABLE_X is an element of P.
Still working in ZFC, assume P != NP.  Because theorem proving in ZFC
is NP-hard, it follows that PROVABLE_ZFC is not an element of P.  By
our lemma, we have, 'PROVABLE_ZFC is not an element of P --> ZFC is
consistent.'  Thus, P != NP --> ZFC is consistent.  By Godel's second
incompleteness theorem, we can conclude:  if ZFC is consistent, P !=
NP can never be proven true.
How do you relate the idea of some problem not being in P to the issue
of P != NP? P == NP and P != NP are both consistent with the existence
of problems that are in neither P nor NP.

Patricia

The idea is that, given a proposition, verifying that it is a theorem
is NP-hard.  (In fact, I think it may be EXPTIME-hard also....)  Thus,
if P = NP could be proven false, that would imply that no NP-hard
problem could be solved in polynomial time. Proving any theorem in ZFC
while knowing the length of the proof is NP-complete; so I assume that
proving a theorem WITHOUT knowing the length would also be NP-hard,
since the proof length will be at least as great as the length of the
theorem.

Remember that proof of NP-Hardness, unlike proof of NP-Completeness,
does *not* imply membership in NP. Do you have a proof that your problem
is in NP? If not, what is the relevance of its NP-Hardness and
non-membership in P to the provability of P != NP?

In other words, what have you done to disprove the following combination:

P != NP is provable, but many problems, including all of EXPTIME and all
the undecidable problems, are in neither P nor NP.

Patricia

No, theorem proving, as I have described it, is not in NP.

I'm trying to think of how to explain this a little better.
Abbreviate my NP-hard problem as "H". The idea is this:

If H can be solved in polynomial time, P = NP.
(by contraposition...)
If P != NP, H cannot be solved in polynomial time.

Then, using ideas from formal logic, I (attempt to) show that if H
cannot be solved in polynomial time, then ZFC is provably consistent.

So we have:

1) If H can be solved in polynomial time, P = NP
2) (by 1) If P != NP, H cannot be solved in polynomial time.
3) If H cannot be solved in polynomial time, ZFC is consistent.
4) (by 2 and 3) If P != NP, ZFC is consistent.

Godel's second incompleteness theorem states that any formal theory
that can prove its own consistency is inconsistent. Thus, from 4), we
can conclude that if we have a proof that P != NP, it follows as a
direct consequence that ZFC is consistent, and therefore we have a
proof that ZFC is inconsistent.

From this, we conclude that unless ZFC is inconsistent, P != NP can
never be proven. It's primarily a formal logic proof.

-Phil
.

Relevant Pages

  • Re: Why is ZF not finitely axiomatizable?
    ... first-order logic is provable in ZFC. ... conclude from the provability of the cut-elimination theorem that it ... quantifier complexity less than equal to P. Alas, induction is not ...
    (sci.logic)
  • Re: Why is ZF not finitely axiomatizable?
    ... first-order logic is provable in ZFC. ... conclude from the provability of the cut-elimination theorem that it ... we come to what might well be regarded as the "real reason" ZFC ...
    (sci.logic)
  • Re: THIS STATEMENT HAS NO PROOF IN ANY SYSTEM = true or false?
    ... The first point is that ZFC is a set of axioms whereas V is the class of all ... To formalize "S is provable in ZFC" we need to ... The provability predicate is a monstrously complicated thing if written ... What is probably generating confusion is the familiar sociological fact ...
    (sci.math)
  • Re: THIS STATEMENT HAS NO PROOF IN ANY SYSTEM = true or false?
    ... The first point is that ZFC is a set of axioms whereas V is the class of all ... To formalize "S is provable in ZFC" we need to ... The provability predicate is a monstrously complicated thing if written ... What is probably generating confusion is the familiar sociological fact ...
    (sci.logic)
  • Re: THIS STATEMENT HAS NO PROOF IN ANY SYSTEM = true or false?
    ... The first point is that ZFC is a set of axioms whereas V is the class of all ... To formalize "S is provable in ZFC" we need to ... The provability predicate is a monstrously complicated thing if written ... What is probably generating confusion is the familiar sociological fact ...
    (comp.theory)