This paper presents a soundness and completeness proof for propositional intuitionistic calculus with respect to the semantics of computability logic. The latter interprets formulas as interactive computational problems, formalized as games between a machine and its environment. Intuitionistic implication is understood as algorithmic reduction in the weakest possible — and hence most natural — sense, disjunction and conjunction as deterministic-choice combinations of problems , and “absurd” as a computational problem of universal strength.

This paper constructs a cirquent calculus system and proves its soundness and completeness with respect to the semantics of computability logic. The logical vocabulary of the system consists of negation \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${{\neg}}$$\end{document}, parallel conjunction \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${{\wedge}}$$\end{document}, parallel disjunction \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${{\vee}}$$\end{document}, branching recurrence ⫰, and branching corecurrence ⫯. The article is published in two parts, with (the previous) (...) Part I containing preliminaries and a soundness proof, and (the present) Part II containing a completeness proof. (shrink)

Edited in collaboration with FoLLI, the Association of Logic, Language and Information, this book constitutes the 4th volume of the FoLLI LNAI subline; containing the refereed proceedings of the 15th International Workshop on Logic, Language, Information and Computation, WoLLIC 2008, held in Edinburgh, UK, in July 2008. The 21 revised full papers presented together with the abstracts of 7 tutorials and invited lectures were carefully reviewed and selected from numerous submissions. The papers cover all pertinent subjects in computer science with (...) particular interest in cross-disciplinary topics. Typical areas of interest are: foundations of computing and programming; novel computation models and paradigms; broad notions of proof and belief; formal methods in software and hardware development; logical approach to natural language and reasoning; logics of programs, actions and resources; foundational aspects of information organization, search, flow, sharing, and protection. (shrink)

This paper constructs a cirquent calculus system and proves its soundness and completeness with respect to the semantics of computability logic. The logical vocabulary of the system consists of negation ${\neg}$ , parallel conjunction ${\wedge}$ , parallel disjunction ${\vee}$ , branching recurrence ⫰, and branching corecurrence ⫯. The article is published in two parts, with (the present) Part I containing preliminaries and a soundness proof, and (the forthcoming) Part II containing a completeness proof.

This paper shows that the basic logic induced by the parallel recurrence $\hspace {-2pt}\mbox {\raisebox {-0.01pt}{\@setfontsize \small {7}{8}$\wedge$}\hspace {-3.55pt}\raisebox {4.5pt}{\tiny $\mid$}\hspace {2pt}}$ of computability logic (i.e., the one in the signature $\{\neg,$\wedge$,\vee,\hspace {-2pt}\mbox {\raisebox {-0.01pt}{\@setfontsize \small {7}{8}$\wedge$}\hspace {-3.55pt}\raisebox {4.5pt}{\tiny $\mid$}\hspace {2pt}},\hspace {-2pt}\mbox {\raisebox {0.12cm}{\@setfontsize \small {7}{8}$\vee$}\hspace {-3.6pt}\raisebox {0.02cm}{\tiny $\mid$}\hspace {2pt}}\}$ ) is a proper superset of the basic logic induced by the branching recurrence $\mbox {\raisebox {-0.05cm}{$\circ$}\hspace {-0.11cm}\raisebox {3.1pt}{\tiny $\mid$}\hspace {2pt}}$ (i.e., the one in the signature $\{\neg,$\wedge$,\vee,\mbox {\raisebox {-0.05cm}{$\circ$}\hspace {-0.11cm}\raisebox (...) {3.1pt}{\tiny $\mid$}\hspace {2pt}},\mbox {\raisebox {0.12cm}{$\circ$}\hspace {-0.115cm}\raisebox {0.02cm}{\tiny $\mid$}\hspace {2pt}}\}$ ). The latter is known to be precisely captured by the cirquent calculus system CL15 , conjectured by Japaridze to remain sound—but not complete—with $\hspace {-2pt}\mbox {\raisebox {-0.01pt}{\@setfontsize \small {7}{8}$\wedge$}\hspace {-3.55pt}\raisebox {4.5pt}{\tiny $\mid$}\hspace {2pt}}$ instead of $\mbox {\raisebox {-0.05cm}{$\circ$}\hspace {-0.11cm}\raisebox {3.1pt}{\tiny $\mid$}\hspace {2pt}}$ . The present result is obtained by positively verifying that conjecture. A secondary result of the paper is showing that $\hspace {-2pt}\mbox {\raisebox {-0.01pt}{\@setfontsize \small {7}{8}$\wedge$}\hspace {-3.55pt}\raisebox {4.5pt}{\tiny $\mid$}\hspace {2pt}}$ is strictly weaker than $\mbox {\raisebox {-0.05cm}{$\circ$}\hspace {-0.11cm}\raisebox {3.1pt}{\tiny $\mid$}\hspace {2pt}}$ in the sense that, while $\mbox {\raisebox {-0.05cm}{$\circ$}\hspace {-0.11cm}\raisebox {3.1pt}{\tiny $\mid$}\hspace {2pt}}F$ logically implies $\hspace {-2pt}\mbox {\raisebox {-0.01pt}{\@setfontsize \small {7}{8}$\wedge$}\hspace {-3.55pt}\raisebox {4.5pt}{\tiny $\mid$}\hspace {2pt}}F$ , the reverse does not hold. (shrink)

Game semantics extends the Curry–Howard isomorphism to a three-way correspondence: proofs, programs, strategies. But the universe of strategies goes beyond intuitionistic logics and lambda calculus, to capture stateful programs. In this paper we describe a logical counterpart to this extension, in which proofs denote such strategies. The system is expressive: it contains all of the connectives of Intuitionistic Linear Logic, and first-order quantification. Use of Lairdʼs sequoid operator allows proofs with imperative behaviour to be expressed. Thus, we can embed first-order (...) Intuitionistic Linear Logic into this system, Polarized Linear Logic, and an imperative total programming language.The proof system has a tight connection with a simple game model, where games are forests of plays. Formulas are modelled as games, and proofs as history-sensitive winning strategies. We provide a strong full completeness result with respect to this model: each finitary strategy is the denotation of a unique analytic proof. Infinite strategies correspond to analytic proofs that are infinitely deep. Thus, we can normalise proofs, via the semantics. (shrink)

Computability logic (CL) is a recently launched program for redeveloping logic as a formal theory of computability, as opposed to the formal theory of truth that logic has more traditionally been. Formulas in it represent computational problems, "truth" means existence of an algorithmic solution, and proofs encode such solutions. Within the line of research devoted to finding axiomatizations for ever more expressive fragments of CL, the present paper introduces a new deductive system CL12 and proves its soundness and completeness with (...) respect to the semantics of CL. Conservatively extending classical predicate calculus and offering considerable additional expressive and deductive power, CL12 presents a reasonable, computationally meaningful, constructive alternative to classical logic as a basis for applied theories. To obtain a model example of such theories, this paper rebuilds the traditional, classical-logic-based Peano arithmetic into a computability-logic-based counterpart. Among the purposes of the present contribution is to provide a starting point for what, as the author wishes to hope, might become a new line of research with a potential of interesting findings—an exploration of the presumably quite unusual metatheory of CL-based arithmetic and other CL-based applied systems. (shrink)

Within the program of finding axiomatizations for various parts of computability logic, it was proven earlier that the logic of interactive Turing reduction is exactly the implicative fragment of Heyting’s intuitionistic calculus. That sort of reduction permits unlimited reusage of the computational resource represented by the antecedent. An at least equally basic and natural sort of algorithmic reduction, however, is the one that does not allow such reusage. The present article shows that turning the logic of the first sort of (...) reduction into the logic of the second sort of reduction takes nothing more than just deleting the contraction rule from its Gentzen-style axiomatization. The first sort of interactive reduction is also shown to come in three natural versions. While those three versions are very different from each other, their logical behaviors turn out to be indistinguishable, with that common behavior being precisely captured by implicative intuitionistic logic. Among the other contributions of the present article is an informal introduction of a series of new — finite and bounded — versions of recurrence operations and the associated reduction operations. (shrink)

Cirquent calculus is a proof system with inherent ability to account for sharing subcomponents in logical expressions. Within its framework, this article constructs an axiomatization $$\text{ CL18 }$$ CL18 of the basic propositional fragment of computability logic—the game-semantically conceived logic of computational resources and tasks. The nonlogical atoms of this fragment represent arbitrary so called static games, and the connectives of its logical vocabulary are negation and the parallel and choice versions of conjunction and disjunction. The main technical result of (...) the article is a proof of the soundness and completeness of $$\text{ CL18 }$$ CL18 with respect to the semantics of computability logic. (shrink)

Every computable function has to be continuous. To develop computability theory of discontinuous functions, we study low levels of the arithmetical hierarchy of nonuniformly computable functions on Baire space. First, we classify nonuniformly computable functions on Baire space from the viewpoint of learning theory and piecewise computability. For instance, we show that mind-change-bounded learnability is equivalent to finite View the MathML source2-piecewise computability 2 denotes the difference of two View the MathML sourceΠ10 sets), error-bounded learnability is equivalent to finite View (...) the MathML sourceΔ20-piecewise computability, and learnability is equivalent to countable View the MathML sourceΠ10-piecewise computability . Second, we introduce disjunction-like operations such as the coproduct based on BHK-like interpretations, and then, we see that these operations induce Galois connections between the Medvedev degree structure and associated Medvedev/ Muchnik-like degree structures. Finally, we interpret these results in the context of the Weihrauch degrees and Wadge-like games. (shrink)

In this paper we provide an interpretation of Aristotle's rule for the universal quantifier in Topics Θ 157a34–37 and 160b1–6 in terms of Paul Lorenzen's dialogical logic. This is meant as a contribution to the rehabilitation of the role of dialectic within the Organon. After a review of earlier views of Aristotle on quantification, we argue that this rule is related to the dictum de omni in Prior Analytics A 24b28–29. This would be an indication of the dictum’s origin in (...) the context of dialectical games. One consequence of our approach is a novel explanation of the doctrine of the existential import of the quantifiers in dialectical terms. After a brief survey of Lorenzen's dialogical logic, we offer a set of rules for dialectical games based on previous work by Castelnérac and Marion, to which we add here the rule for the universal quantifier, as interpreted in terms of its counterpart in dialogical logic. We then give textual evidence of the use of that rule in Plato's dialogues, thus showing that Aris... (shrink)

An overview of different versions and applications of Lorenzen’s dialogue game approach to the foundations of logic, here largely restricted to the realm of manyvalued logics, is presented. Among the reviewed concepts and results are Giles’s characterization of Łukasiewicz logic and some of its generalizations to other fuzzy logics, including interval based logics, a parallel version of Lorenzen’s game for intuitionistic logic that is adequate for finite- and infinite-valued Gödel logics, and a truth comparison game for infinite-valued Gödel logic.

Cirquent calculus is a novel proof theory permitting component-sharing between logical expressions. Using it, the predecessor article ‘Elementary-base cirquent calculus I: Parallel and choice connectives’ built the sound and complete axiomatization $\textbf{CL16}$ of a propositional fragment of computability logic. The atoms of the language of $\textbf{CL16}$ represent elementary, i.e. moveless, games and the logical vocabulary consists of negation, parallel connectives and choice connectives. The present paper constructs the first-order version $\textbf{CL17}$ of $\textbf{CL16}$, also enjoying soundness and completeness. The language of (...) $\textbf{CL17}$ augments that of $\textbf{CL16}$ by including choice quantifiers. Unlike classical predicate calculus, $\textbf{CL17}$ turns out to be decidable. (shrink)