The taming of recurrences in computability logic through cirquent calculus. I (Q1935369)

Computability logic (CoL), introduced by the author some time ago, is a research program for developing a nonclassical logic based on constructive game semantics, where formulas are understood as games between a machine and its environment. Cirquent calculus (CC) is a novel proof theory, also introduced by the author earlier. Unlike the traditional approaches that manipulate tree-like objects such as formulas or sequents, CC deals with circuit-style constructs. This switch from trees to circuits allows one to axiomatize various logics that the Gentzen- or Hilbert-style proof-theoretic approaches have consistently failed to tame. CoL is among such logics. The present paper constructs a propositional CC system and proves its adequacy with respect to the semantics of CoL. The logical vocabulary of the fragment of CoL captured by this system consists of negation, parallel conjunction, parallel disjunction, branching recurrence, and branching corecurrence. These connectives bear resemblance with linear logic's linear negation, multiplicatives and exponentials, respectively, but induce a properly stronger logic than linear or even affine logic. The article is published in two parts, with (the present) Part I containing preliminaries and a soundness proof, and Part II containing a completeness proof. Technically, those proofs are extremely involved, and understanding them requires a lot of determination. In contrast, the first few sections of Part 1, being written in an introductory style with plenty of examples and illustrations, are quite readable and enjoyable by a wide audience.