Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Posting-Version: version B 2.10.2 9/5/84; site psuvax1.UUCP
Path: utzoo!linus!philabs!cmcl2!seismo!rochester!cmu-cs-pt!cadre!psuvax1!simon
From: simon@psuvax1.UUCP (Janos Simon)
Newsgroups: net.math
Subject: Re: Logic (for logicians)
Message-ID: <1670@psuvax1.UUCP>
Date: Fri, 19-Jul-85 13:56:15 EDT
Article-I.D.: psuvax1.1670
Posted: Fri Jul 19 13:56:15 1985
Date-Received: Sun, 21-Jul-85 03:38:36 EDT
References: <456@ttidcc.UUCP> <457@ttidcc.UUCP> <1586@hao.UUCP>
Lines: 24

<3033@cornell19 Jul 85 17:56:15 GMT
Reply-To: simon@psuvax1.UUCP (Janos Simon)
Organization: Pennsylvania State Univ.
Lines: 18
Xref: cadre net.math:829 
Summary:Connection between logic and complexity 

[]
This is probably getting way too technical, but the statement in <3033@cornell>
that complexity theory has nothing to do with logic is false ( Didn't Juris 
teach you that at Cornell ? :-) ). 

In fact, the historic paper by Cook on NP is called
"The complexity of theorem-proving procedures". More to the point, a complete
problem for co-NP (languages with their complement in NP) is to decide whether
a boolean formula is a tautology. At the same time, short, effective proofs are 
essentially NP. So, if there is a proof method for tautologies that yields
short proofs that can be checked easily, NP=co-NP (and conversely). 

There are many results along these lines - the most recent, and most exciting
is the thesis by Buss (abstract in the latest STOC proceedings) where he proves
that in some logics (weak theories of arithmetic) certain objects are defineable
iff things like P=NP happen. So, a possible proof that P\=NP could have the
form "it is impossible to prove, using these axioms, this theorem"
js