A logical basis for constructive systems
arXiv:1003.0425 · doi:10.1093/logcom/exr009
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.
References in corpus (14)
- Sequential operators in computability logic
- Introduction to Cirquent Calculus and Abstract Resource Semantics
- Propositional computability logic I
- Cirquent calculus deepened
- Computability Logic: a formal theory of interaction
- From truth to computability I
- The intuitionistic fragment of computability logic at the propositional level
- Propositional Computability Logic II
- Intuitionistic computability logic
- From truth to computability II
- Many concepts and two logics of algorithmic reduction
- Toggling operators in computability logic
- The logic of interactive Turing reduction
- Towards applied theories based on computability logic
Cited by in corpus (8)
- The taming of recurrences in computability logic through cirquent calculus, Part I
- From formulas to cirquents in computability logic
- Introduction to clarithmetic II
- On the system CL12 of computability logic
- Introduction to clarithmetic I
- The taming of recurrences in computability logic through cirquent calculus, Part II
- Build your own clarithmetic I: Setup and completeness
- Elementary-base cirquent calculus I: Parallel and choice connectives