[FOM] Foundational Challenge

[Lew Gordeew]

Zitat von "Timothy Y. Chow" <tchow at math.princeton.edu>:

> Martin Dowd wrote:
>
>> A problem I just ran in to in some complexity theory research seems  
>> relevant here. Program verification is a venerable branch of  
>> computer science, and has bee used in the sphere packing project I  
>> believe. But some very simple problems have seemingly "inherently  
>> long" proofs. For example, the fact that a particular Turing  
>> machine computes x+y may be formulated as an equation of polynomial  
>> time arithmetic. A proof in polynomial time arithmetic would be  
>> long. I don't think any work has been done in this area. Using  
>> known program verification methods, a short proof could probably be  
>> given for something like a loop program.
>> Ab initio, it doesn't seem that any amount of "improvement" to the  
>> formal system would be likely to reduce the length of a proof for  
>> the Turing machine.
>> - Martin Dowd
>
> I made some related remarks back in 2007, and touched on the subject  
> again in 2014.
>
> https://cs.nyu.edu/pipermail/fom/2007-June/011667.html
> https://cs.nyu.edu/pipermail/fom/2007-July/011740.html
>
> https://cs.nyu.edu/pipermail/fom/2014-August/018057.html
>
> In other words, we already have examples of theorems that have a  
> PSPACE flavor to them, indicating that they're unlikely to have  
> short certificates (I'm afraid I'm currently a skeptic of Gordeev  
> and Haeusler's claims to have proven NP = PSPACE).

I'm afraid that the said indication is based upon conventional  
(linear, or tree-like) implementation of formal provability. By  
contrast, we consider dag-like presentation of Prawitz's natural  
deductions. Clearly, the size of proof trees can exponentially exceed  
the size of corresponding (say, compressed) proof dags. We observed  
that a suitable two-fold tree-to-dag horizontal compression yields  
short certificates of tautologies in minimal propositional logic,  
which eventually leads to NP = PSPACE.

The two-fold compression in question consists of two parts that are  
elaborated in [1] and [2], respectively. First compression is  
sufficiently constructive and it yields a short (polynomial) proof-dag  
(called a deduction frame) whose validity verification, however,  
requires special exponential database. This compression is followed by  
our second compression (called cleansing) of the said deduction frame,  
which is essentially nondeterministic as its definition makes use of  
the mentioned exponential database. The resulting short(er)  
proof-subdag has a desired short certificate for its validity  
verification. This is sufficient for NP = PSPACE.

The entire construction is exponential in time, but I suppose that the  
search for corresponding polynomial dag-like proof might be feasible.

[1] L. Gordeev, E. H. Haeusler, Proof Compression and NP Versus  
PSPACE, Studia Logica (107) (1): 55{83 (2019)

[2] L. Gordeev, E. H. Haeusler, Proof Compression and NP Versus PSPACE  
II (submitted); it is a slight extension of:

[3] L. Gordeev, Proof Compression and NP Versus PSPACE. Part 2,  
arXiv:1907.03858 (2019)

Best,
LG