A logical basis for constructive systems

TL;DR

This paper develops a complexity theory framework within Computability Logic (CoL), proving soundness and completeness for the CL12 system, which supports constructive and complexity-oriented reasoning.

Contribution

It introduces complexity considerations into CoL, establishes the soundness and completeness of CL12, and advocates its use for constructive applied theories.

Findings

Proves soundness and completeness of CL12 for CoL semantics.

Extends CoL with polynomial time computability.

Supports constructive and complexity-oriented reasoning.

Abstract

The work is devoted to Computability Logic (CoL) -- the philosophical/mathematical platform and long-term project for redeveloping classical logic after replacing truth} by computability in its underlying semantics (see http://www.cis.upenn.edu/~giorgi/cl.html). This article elaborates some basic complexity theory for the CoL framework. Then it proves soundness and completeness for the deductive system CL12 with respect to the semantics of CoL, including the version of the latter based on polynomial time computability instead of computability-in-principle. CL12 is a sequent calculus system, where the meaning of a sequent intuitively can be characterized as "the succedent is algorithmically reducible to the antecedent", and where formulas are built from predicate letters, function letters, variables, constants, identity, negation, parallel and choice connectives, and blind and choice quantifiers. A case is made that CL12 is an adequate logical basis for constructive applied theories, including complexity-oriented ones.