A PSPACE-Complete First Order Fragment of Computability Logic

TL;DR

This paper proves that a specific fragment of Computability Logic, which excludes blind quantifiers, is PSPACE-complete, highlighting its computational complexity and potential for extracting algorithms from proofs.

Contribution

It extends previous results by establishing the PSPACE-completeness of this logic fragment, deepening understanding of its computational complexity.

Findings

The fragment without blind quantifiers is PSPACE-complete.

This extends earlier polynomial space decidability results.

Provides insights into the computational complexity of logic fragments.

Abstract

In a recently launched research program for developing logic as a formal theory of (interactive) computability, several very interesting logics have been introduced and axiomatized. These fragments of the larger Computability Logic aim not only to describe "what" can be computed, but also provide a mechanism for extracting computational algorithms from proofs. Among the most expressive and fundamental of these is CL4, known to be (constructively) sound and complete with respect to the underlying computational semantics. Furthermore, the fragment of CL4 not containing blind quantifiers was shown to be decidable in polynomial space. The present work extends this result and proves that this fragment is, in fact, PSPACE-complete.