-
A propositional cirquent calculus for computability logic
Authors:
Giorgi Japaridze
Abstract:
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 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 sta…
▽ More
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 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
CL18 with respect to the semantics of computability logic.
△ Less
Submitted 9 June, 2024;
originally announced June 2024.
-
Observation of high-energy neutrinos from the Galactic plane
Authors:
R. Abbasi,
M. Ackermann,
J. Adams,
J. A. Aguilar,
M. Ahlers,
M. Ahrens,
J. M. Alameddine,
A. A. Alves Jr.,
N. M. Amin,
K. Andeen,
T. Anderson,
G. Anton,
C. Argüelles,
Y. Ashida,
S. Athanasiadou,
S. Axani,
X. Bai,
A. Balagopal V.,
S. W. Barwick,
V. Basu,
S. Baur,
R. Bay,
J. J. Beatty,
K. -H. Becker,
J. Becker Tjus
, et al. (364 additional authors not shown)
Abstract:
The origin of high-energy cosmic rays, atomic nuclei that continuously impact Earth's atmosphere, has been a mystery for over a century. Due to deflection in interstellar magnetic fields, cosmic rays from the Milky Way arrive at Earth from random directions. However, near their sources and during propagation, cosmic rays interact with matter and produce high-energy neutrinos. We search for neutrin…
▽ More
The origin of high-energy cosmic rays, atomic nuclei that continuously impact Earth's atmosphere, has been a mystery for over a century. Due to deflection in interstellar magnetic fields, cosmic rays from the Milky Way arrive at Earth from random directions. However, near their sources and during propagation, cosmic rays interact with matter and produce high-energy neutrinos. We search for neutrino emission using machine learning techniques applied to ten years of data from the IceCube Neutrino Observatory. We identify neutrino emission from the Galactic plane at the 4.5$σ$ level of significance, by comparing diffuse emission models to a background-only hypothesis. The signal is consistent with modeled diffuse emission from the Galactic plane, but could also arise from a population of unresolved point sources.
△ Less
Submitted 10 July, 2023;
originally announced July 2023.
-
Graph Neural Networks for Low-Energy Event Classification & Reconstruction in IceCube
Authors:
R. Abbasi,
M. Ackermann,
J. Adams,
N. Aggarwal,
J. A. Aguilar,
M. Ahlers,
M. Ahrens,
J. M. Alameddine,
A. A. Alves Jr.,
N. M. Amin,
K. Andeen,
T. Anderson,
G. Anton,
C. Argüelles,
Y. Ashida,
S. Athanasiadou,
S. Axani,
X. Bai,
A. Balagopal V.,
M. Baricevic,
S. W. Barwick,
V. Basu,
R. Bay,
J. J. Beatty,
K. -H. Becker
, et al. (359 additional authors not shown)
Abstract:
IceCube, a cubic-kilometer array of optical sensors built to detect atmospheric and astrophysical neutrinos between 1 GeV and 1 PeV, is deployed 1.45 km to 2.45 km below the surface of the ice sheet at the South Pole. The classification and reconstruction of events from the in-ice detectors play a central role in the analysis of data from IceCube. Reconstructing and classifying events is a challen…
▽ More
IceCube, a cubic-kilometer array of optical sensors built to detect atmospheric and astrophysical neutrinos between 1 GeV and 1 PeV, is deployed 1.45 km to 2.45 km below the surface of the ice sheet at the South Pole. The classification and reconstruction of events from the in-ice detectors play a central role in the analysis of data from IceCube. Reconstructing and classifying events is a challenge due to the irregular detector geometry, inhomogeneous scattering and absorption of light in the ice and, below 100 GeV, the relatively low number of signal photons produced per event. To address this challenge, it is possible to represent IceCube events as point cloud graphs and use a Graph Neural Network (GNN) as the classification and reconstruction method. The GNN is capable of distinguishing neutrino events from cosmic-ray backgrounds, classifying different neutrino event types, and reconstructing the deposited energy, direction and interaction vertex. Based on simulation, we provide a comparison in the 1-100 GeV energy range to the current state-of-the-art maximum likelihood techniques used in current IceCube analyses, including the effects of known systematic uncertainties. For neutrino event classification, the GNN increases the signal efficiency by 18% at a fixed false positive rate (FPR), compared to current IceCube methods. Alternatively, the GNN offers a reduction of the FPR by over a factor 8 (to below half a percent) at a fixed signal efficiency. For the reconstruction of energy, direction, and interaction vertex, the resolution improves by an average of 13%-20% compared to current maximum likelihood techniques in the energy range of 1-30 GeV. The GNN, when run on a GPU, is capable of processing IceCube events at a rate nearly double of the median IceCube trigger rate of 2.7 kHz, which opens the possibility of using low energy neutrinos in online searches for transient events.
△ Less
Submitted 11 October, 2022; v1 submitted 7 September, 2022;
originally announced September 2022.
-
Cirquent calculus in a nutshell
Authors:
Giorgi Japaridze,
Bikal Lamichhane
Abstract:
This paper is a brief and informal presentation of cirquent calculus, a novel proof system for resource-conscious logics. As such, it is a refinement of sequent calculus with mechanisms that allow to explicitly account for the possibility of sharing of subexpressions/subresources between different expressions/resources. This is achieved by dealing with circuit-style constructs, termed cirquents, i…
▽ More
This paper is a brief and informal presentation of cirquent calculus, a novel proof system for resource-conscious logics. As such, it is a refinement of sequent calculus with mechanisms that allow to explicitly account for the possibility of sharing of subexpressions/subresources between different expressions/resources. This is achieved by dealing with circuit-style constructs, termed cirquents, instead of formulas, sequents or other tree-like structures. The approach exhibits greater expressiveness, flexibility and efficiency compared to the more traditional proof-theoretic approaches.
△ Less
Submitted 27 August, 2021;
originally announced August 2021.
-
A Convolutional Neural Network based Cascade Reconstruction for the IceCube Neutrino Observatory
Authors:
R. Abbasi,
M. Ackermann,
J. Adams,
J. A. Aguilar,
M. Ahlers,
M. Ahrens,
C. Alispach,
A. A. Alves Jr.,
N. M. Amin,
R. An,
K. Andeen,
T. Anderson,
I. Ansseau,
G. Anton,
C. Argüelles,
S. Axani,
X. Bai,
A. Balagopal V.,
A. Barbano,
S. W. Barwick,
B. Bastian,
V. Basu,
V. Baum,
S. Baur,
R. Bay
, et al. (343 additional authors not shown)
Abstract:
Continued improvements on existing reconstruction methods are vital to the success of high-energy physics experiments, such as the IceCube Neutrino Observatory. In IceCube, further challenges arise as the detector is situated at the geographic South Pole where computational resources are limited. However, to perform real-time analyses and to issue alerts to telescopes around the world, powerful an…
▽ More
Continued improvements on existing reconstruction methods are vital to the success of high-energy physics experiments, such as the IceCube Neutrino Observatory. In IceCube, further challenges arise as the detector is situated at the geographic South Pole where computational resources are limited. However, to perform real-time analyses and to issue alerts to telescopes around the world, powerful and fast reconstruction methods are desired. Deep neural networks can be extremely powerful, and their usage is computationally inexpensive once the networks are trained. These characteristics make a deep learning-based approach an excellent candidate for the application in IceCube. A reconstruction method based on convolutional architectures and hexagonally shaped kernels is presented. The presented method is robust towards systematic uncertainties in the simulation and has been tested on experimental data. In comparison to standard reconstruction methods in IceCube, it can improve upon the reconstruction accuracy, while reducing the time necessary to run the reconstruction by two to three orders of magnitude.
△ Less
Submitted 26 July, 2021; v1 submitted 27 January, 2021;
originally announced January 2021.
-
Fundamentals of computability logic 2020
Authors:
Giorgi Japaridze
Abstract:
This article is a semitutorial-style survey of computability logic. An extended online version of it is maintained at http://www.csc.villanova.edu/~japaridz/CL/ .
This article is a semitutorial-style survey of computability logic. An extended online version of it is maintained at http://www.csc.villanova.edu/~japaridz/CL/ .
△ Less
Submitted 1 November, 2020; v1 submitted 1 April, 2019;
originally announced April 2019.
-
Elementary-base cirquent calculus II: Choice quantifiers
Authors:
Giorgi Japaridze
Abstract:
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 CL16 of a propositional fragment of computability logic (see http://www.csc.villanova.edu/~japaridz/CL/ ). The atoms of the language of CL16 represent…
▽ More
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 CL16 of a propositional fragment of computability logic (see http://www.csc.villanova.edu/~japaridz/CL/ ). The atoms of the language of 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 CL17 of CL16, also enjoying soundness and completeness. The language of CL17 augments that of CL18 by including choice quantifiers. Unlike classical predicate calculus, CL17 turns out to be decidable.
△ Less
Submitted 19 February, 2019;
originally announced February 2019.
-
Computability logic: Giving Caesar what belongs to Caesar
Authors:
Giorgi Japaridze
Abstract:
The present article is a brief informal survey of computability logic --- the game-semantically conceived formal theory of computational resources and tasks. This relatively young nonclassical logic is a conservative extension of classical first order logic but is much more expressive than the latter, yielding a wide range of new potential application areas. In a reasonable (even if not strict) se…
▽ More
The present article is a brief informal survey of computability logic --- the game-semantically conceived formal theory of computational resources and tasks. This relatively young nonclassical logic is a conservative extension of classical first order logic but is much more expressive than the latter, yielding a wide range of new potential application areas. In a reasonable (even if not strict) sense the same holds for intuitionistic and linear logics, which allows us to say that CoL reconciles and unifies the three traditions of logical thought (and beyond) on the basis of its natural and "universal" game semantics. A comprehensive online survey of the subject can be found at http://www.csc.villanova.edu/~japaridz/CL/ .
△ Less
Submitted 13 February, 2019;
originally announced February 2019.
-
Elementary-base cirquent calculus I: Parallel and choice connectives
Authors:
Giorgi Japaridze
Abstract:
Cirquent calculus is a proof system manipulating circuit-style constructs rather than formulas. Using it, this article constructs a sound and complete axiomatization CL16 of the propositional fragment of computability logic (the game-semantically conceived logic of computational problems - see http://www.csc.villanova.edu/~japaridz/CL/ ) whose logical vocabulary consists of negation and parallel a…
▽ More
Cirquent calculus is a proof system manipulating circuit-style constructs rather than formulas. Using it, this article constructs a sound and complete axiomatization CL16 of the propositional fragment of computability logic (the game-semantically conceived logic of computational problems - see http://www.csc.villanova.edu/~japaridz/CL/ ) whose logical vocabulary consists of negation and parallel and choice connectives, and whose atoms represent elementary, i.e. moveless, games.
△ Less
Submitted 16 July, 2017;
originally announced July 2017.
-
A survey of computability logic
Authors:
Giorgi Japaridze
Abstract:
This article presents a survey of computability logic: its philosophy and motivations, main concepts and most significant results obtained so far. A continuously updated online version of this article is maintained at http://www.csc.villanova.edu/~japaridz/CL/ .
This article presents a survey of computability logic: its philosophy and motivations, main concepts and most significant results obtained so far. A continuously updated online version of this article is maintained at http://www.csc.villanova.edu/~japaridz/CL/ .
△ Less
Submitted 14 December, 2016;
originally announced December 2016.
-
Build your own clarithmetic II: Soundness
Authors:
Giorgi Japaridze
Abstract:
Clarithmetics are number theories based on computability logic (see http://www.csc.villanova.edu/~japaridz/CL/ ). Formulas of these theories represent interactive computational problems, and their "truth" is understood as existence of an algorithmic solution. Various complexity constraints on such solutions induce various versions of clarithmetic. The present paper introduces a parameterized/schem…
▽ More
Clarithmetics are number theories based on computability logic (see http://www.csc.villanova.edu/~japaridz/CL/ ). Formulas of these theories represent interactive computational problems, and their "truth" is understood as existence of an algorithmic solution. Various complexity constraints on such solutions induce various versions of clarithmetic. The present paper introduces a parameterized/schematic version CLA11(P1,P2,P3,P4). By tuning the three parameters P1,P2,P3 in an essentially mechanical manner, one automatically obtains sound and complete theories with respect to a wide range of target tricomplexity classes, i.e. combinations of time (set by P3), space (set by P2) and so called amplitude (set by P1) complexities. Sound in the sense that every theorem T of the system represents an interactive number-theoretic computational problem with a solution from the given tricomplexity class and, furthermore, such a solution can be automatically extracted from a proof of T. And complete in the sense that every interactive number-theoretic problem with a solution from the given tricomplexity class is represented by some theorem of the system. Furthermore, through tuning the 4th parameter P4, at the cost of sacrificing recursive axiomatizability but not simplicity or elegance, the above extensional completeness can be strengthened to intensional completeness, according to which every formula representing a problem with a solution from the given tricomplexity class is a theorem of the system. This article is published in two parts. The previous Part I has introduced the system and proved its completeness, while the present Part II is devoted to proving soundness.
△ Less
Submitted 21 September, 2016; v1 submitted 29 October, 2015;
originally announced October 2015.
-
Build your own clarithmetic I: Setup and completeness
Authors:
Giorgi Japaridze
Abstract:
Clarithmetics are number theories based on computability logic (see http://www.csc.villanova.edu/~japaridz/CL/ ). Formulas of these theories represent interactive computational problems, and their "truth" is understood as existence of an algorithmic solution. Various complexity constraints on such solutions induce various versions of clarithmetic. The present paper introduces a parameterized/schem…
▽ More
Clarithmetics are number theories based on computability logic (see http://www.csc.villanova.edu/~japaridz/CL/ ). Formulas of these theories represent interactive computational problems, and their "truth" is understood as existence of an algorithmic solution. Various complexity constraints on such solutions induce various versions of clarithmetic. The present paper introduces a parameterized/schematic version CLA11(P1,P2,P3,P4). By tuning the three parameters P1,P2,P3 in an essentially mechanical manner, one automatically obtains sound and complete theories with respect to a wide range of target tricomplexity classes, i.e. combinations of time (set by P3), space (set by P2) and so called amplitude (set by P1) complexities. Sound in the sense that every theorem T of the system represents an interactive number-theoretic computational problem with a solution from the given tricomplexity class and, furthermore, such a solution can be automatically extracted from a proof of T. And complete in the sense that every interactive number-theoretic problem with a solution from the given tricomplexity class is represented by some theorem of the system. Furthermore, through tuning the 4th parameter P4, at the cost of sacrificing recursive axiomatizability but not simplicity or elegance, the above extensional completeness can be strengthened to intensional completeness, according to which every formula representing a problem with a solution from the given tricomplexity class is a theorem of the system. This article is published in two parts. The present Part I introduces the system and proves its completeness, while Part II is devoted to proving soundness.
△ Less
Submitted 13 September, 2016; v1 submitted 29 October, 2015;
originally announced October 2015.
-
On resources and tasks
Authors:
Giorgi Japaridze
Abstract:
Essentially being an extended abstract of the author's 1998 PhD thesis, this paper introduces an extension of the language of linear logic with a semantics which treats sentences as tasks rather than true/false statements. A resource is understood as an agent capable of accomplishing the task expressed by such a sentence. It is argued that the corresponding logic can be used as a planning logic, w…
▽ More
Essentially being an extended abstract of the author's 1998 PhD thesis, this paper introduces an extension of the language of linear logic with a semantics which treats sentences as tasks rather than true/false statements. A resource is understood as an agent capable of accomplishing the task expressed by such a sentence. It is argued that the corresponding logic can be used as a planning logic, whose advantage over the traditional comprehensive planning logics is that it avoids the representationalframe problem and significantly alleviates the inferential frame problem.
△ Less
Submitted 11 December, 2013;
originally announced December 2013.
-
The IceProd Framework: Distributed Data Processing for the IceCube Neutrino Observatory
Authors:
M. G. Aartsen,
R. Abbasi,
M. Ackermann,
J. Adams,
J. A. Aguilar,
M. Ahlers,
D. Altmann,
C. Arguelles,
J. Auffenberg,
X. Bai,
M. Baker,
S. W. Barwick,
V. Baum,
R. Bay,
J. J. Beatty,
J. Becker Tjus,
K. -H. Becker,
S. BenZvi,
P. Berghaus,
D. Berley,
E. Bernardini,
A. Bernhard,
D. Z. Besson,
G. Binder,
D. Bindig
, et al. (262 additional authors not shown)
Abstract:
IceCube is a one-gigaton instrument located at the geographic South Pole, designed to detect cosmic neutrinos, iden- tify the particle nature of dark matter, and study high-energy neutrinos themselves. Simulation of the IceCube detector and processing of data require a significant amount of computational resources. IceProd is a distributed management system based on Python, XML-RPC and GridFTP. It…
▽ More
IceCube is a one-gigaton instrument located at the geographic South Pole, designed to detect cosmic neutrinos, iden- tify the particle nature of dark matter, and study high-energy neutrinos themselves. Simulation of the IceCube detector and processing of data require a significant amount of computational resources. IceProd is a distributed management system based on Python, XML-RPC and GridFTP. It is driven by a central database in order to coordinate and admin- ister production of simulations and processing of data produced by the IceCube detector. IceProd runs as a separate layer on top of other middleware and can take advantage of a variety of computing resources, including grids and batch systems such as CREAM, Condor, and PBS. This is accomplished by a set of dedicated daemons that process job submission in a coordinated fashion through the use of middleware plugins that serve to abstract the details of job submission and job management from the framework.
△ Less
Submitted 22 August, 2014; v1 submitted 22 November, 2013;
originally announced November 2013.
-
On the system CL12 of computability logic
Authors:
Giorgi Japaridze
Abstract:
Computability logic (see http://www.csc.villanova.edu/~japaridz/CL/) is a long-term project for redevelo** logic on the basis of a constructive game semantics, with games seen as abstract models of interactive computational problems. Among the fragments of this logic successfully axiomatized so far is CL12 --- a conservative extension of classical first-order logic, whose language augments that…
▽ More
Computability logic (see http://www.csc.villanova.edu/~japaridz/CL/) is a long-term project for redevelo** logic on the basis of a constructive game semantics, with games seen as abstract models of interactive computational problems. Among the fragments of this logic successfully axiomatized so far is CL12 --- a conservative extension of classical first-order logic, whose language augments that of classical logic with the so called choice sorts of quantifiers and connectives. This system has already found fruitful applications as a logical basis for constructive and complexity-oriented versions of Peano arithmetic, such as arithmetics for polynomial time computability, polynomial space computability, and beyond. The present paper introduces a third, indispensable complexity measure for interactive computations termed amplitude complexity, and establishes the adequacy of CL12 with respect to A-amplitude, S-space and T-time computability under certain minimal conditions on the triples (A,S,T) of function classes. This result very substantially broadens the potential application areas of CL12. The paper is self-contained, and targets readers with no prior familiarity with the subject.
△ Less
Submitted 25 July, 2015; v1 submitted 1 March, 2012;
originally announced March 2012.
-
The taming of recurrences in computability logic through cirquent calculus, Part II
Authors:
Giorgi Japaridze
Abstract:
This paper constructs a cirquent calculus system and proves its soundness and completeness with respect to the semantics of computability logic (see http://www.cis.upenn.edu/~giorgi/cl.html). The logical vocabulary of the system consists of negation, parallel conjunction, parallel disjunction, branching recurrence, and branching corecurrence. The article is published in two parts, with (the previo…
▽ More
This paper constructs a cirquent calculus system and proves its soundness and completeness with respect to the semantics of computability logic (see http://www.cis.upenn.edu/~giorgi/cl.html). The logical vocabulary of the system consists of negation, parallel conjunction, parallel disjunction, 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.
△ Less
Submitted 19 June, 2011;
originally announced June 2011.
-
The taming of recurrences in computability logic through cirquent calculus, Part I
Authors:
Giorgi Japaridze
Abstract:
This paper constructs a cirquent calculus system and proves its soundness and completeness with respect to the semantics of computability logic (see http://www.cis.upenn.edu/~giorgi/cl.html). The logical vocabulary of the system consists of negation, parallel conjunction, parallel disjunction, branching recurrence, and branching corecurrence. The article is published in two parts, with (the presen…
▽ More
This paper constructs a cirquent calculus system and proves its soundness and completeness with respect to the semantics of computability logic (see http://www.cis.upenn.edu/~giorgi/cl.html). The logical vocabulary of the system consists of negation, parallel conjunction, parallel disjunction, 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.
△ Less
Submitted 19 September, 2012; v1 submitted 19 May, 2011;
originally announced May 2011.
-
A new face of the branching recurrence of computability logic
Authors:
Giorgi Japaridze
Abstract:
This letter introduces a new, substantially simplified version of the branching recurrence operation of computability logic (see http://www.cis.upenn.edu/~giorgi/cl.html), and proves its equivalence to the old, "canonical" version.
This letter introduces a new, substantially simplified version of the branching recurrence operation of computability logic (see http://www.cis.upenn.edu/~giorgi/cl.html), and proves its equivalence to the old, "canonical" version.
△ Less
Submitted 21 November, 2011; v1 submitted 5 February, 2011;
originally announced February 2011.
-
Introduction to clarithmetic III
Authors:
Giorgi Japaridze
Abstract:
The present paper constructs three new systems of clarithmetic (arithmetic based on computability logic --- see http://www.cis.upenn.edu/~giorgi/cl.html): CLA8, CLA9 and CLA10. System CLA8 is shown to be sound and extensionally complete with respect to PA-provably recursive time computability. This is in the sense that an arithmetical problem A has a t-time solution for some PA-provably recursive…
▽ More
The present paper constructs three new systems of clarithmetic (arithmetic based on computability logic --- see http://www.cis.upenn.edu/~giorgi/cl.html): CLA8, CLA9 and CLA10. System CLA8 is shown to be sound and extensionally complete with respect to PA-provably recursive time computability. This is in the sense that an arithmetical problem A has a t-time solution for some PA-provably recursive function t iff A is represented by some theorem of CLA8. System CLA9 is shown to be sound and intensionally complete with respect to constructively PA-provable computability. This is in the sense that a sentence X is a theorem of CLA9 iff, for some particular machine M, PA proves that M computes (the problem represented by) X. And system CLA10 is shown to be sound and intensionally complete with respect to not-necessarily-constructively PA-provable computability. This means that a sentence X is a theorem of CLA10 iff PA proves that X is computable, even if PA does not "know" of any particular machine M that computes X.
△ Less
Submitted 20 November, 2012; v1 submitted 4 August, 2010;
originally announced August 2010.
-
Separating the basic logics of the basic recurrences
Authors:
Giorgi Japaridze
Abstract:
This paper shows that, even at the most basic level, the parallel, countable branching and uncountable branching recurrences of Computability Logic (see http://www.cis.upenn.edu/~giorgi/cl.html) validate different principles.
This paper shows that, even at the most basic level, the parallel, countable branching and uncountable branching recurrences of Computability Logic (see http://www.cis.upenn.edu/~giorgi/cl.html) validate different principles.
△ Less
Submitted 15 November, 2011; v1 submitted 8 July, 2010;
originally announced July 2010.
-
Introduction to clarithmetic II
Authors:
Giorgi Japaridze
Abstract:
The earlier paper "Introduction to clarithmetic I" constructed an axiomatic system of arithmetic based on computability logic (see http://www.cis.upenn.edu/~giorgi/cl.html), and proved its soundness and extensional completeness with respect to polynomial time computability. The present paper elaborates three additional sound and complete systems in the same style and sense: one for polynomial spac…
▽ More
The earlier paper "Introduction to clarithmetic I" constructed an axiomatic system of arithmetic based on computability logic (see http://www.cis.upenn.edu/~giorgi/cl.html), and proved its soundness and extensional completeness with respect to polynomial time computability. The present paper elaborates three additional sound and complete systems in the same style and sense: one for polynomial space computability, one for elementary recursive time (and/or space) computability, and one for primitive recursive time (and/or space) computability.
△ Less
Submitted 23 April, 2013; v1 submitted 19 April, 2010;
originally announced April 2010.
-
Introduction to clarithmetic I
Authors:
Giorgi Japaridze
Abstract:
"Clarithmetic" is a generic name for formal number theories similar to Peano arithmetic, but based on computability logic (see http://www.cis.upenn.edu/~giorgi/cl.html) instead of the more traditional classical or intuitionistic logics. Formulas of clarithmetical theories represent interactive computational problems, and their "truth" is understood as existence of an algorithmic solution. Imposing…
▽ More
"Clarithmetic" is a generic name for formal number theories similar to Peano arithmetic, but based on computability logic (see http://www.cis.upenn.edu/~giorgi/cl.html) instead of the more traditional classical or intuitionistic logics. Formulas of clarithmetical theories represent interactive computational problems, and their "truth" is understood as existence of an algorithmic solution. Imposing various complexity constraints on such solutions yields various versions of clarithmetic. The present paper introduces a system of clarithmetic for polynomial time computability, which is shown to be sound and complete. Sound in the sense that every theorem T of the system represents an interactive number-theoretic computational problem with a polynomial time solution and, furthermore, such a solution can be efficiently extracted from a proof of T. And complete in the sense that every interactive number-theoretic problem with a polynomial time solution is represented by some theorem T of the system. The paper is written in a semitutorial style and targets readers with no prior familiarity with computability logic.
△ Less
Submitted 23 August, 2011; v1 submitted 24 March, 2010;
originally announced March 2010.
-
A logical basis for constructive systems
Authors:
Giorgi Japaridze
Abstract:
The work is devoted to Computability Logic (CoL) -- the philosophical/mathematical platform and long-term project for redevelo** 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 s…
▽ More
The work is devoted to Computability Logic (CoL) -- the philosophical/mathematical platform and long-term project for redevelo** 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.
△ Less
Submitted 14 March, 2011; v1 submitted 1 March, 2010;
originally announced March 2010.
-
From formulas to cirquents in computability logic
Authors:
Giorgi Japaridze
Abstract:
Computability logic (CoL) (see http://www.cis.upenn.edu/~giorgi/cl.html) is a recently introduced semantical platform and ambitious program for redevelo** logic as a formal theory of computability, as opposed to the formal theory of truth that logic has more traditionally been. Its expressions represent interactive computational tasks seen as games played by a machine against the environment, a…
▽ More
Computability logic (CoL) (see http://www.cis.upenn.edu/~giorgi/cl.html) is a recently introduced semantical platform and ambitious program for redevelo** logic as a formal theory of computability, as opposed to the formal theory of truth that logic has more traditionally been. Its expressions represent interactive computational tasks seen as games played by a machine against the environment, and "truth" is understood as existence of an algorithmic winning strategy. With logical operators standing for operations on games, the formalism of CoL is open-ended, and has already undergone series of extensions. This article extends the expressive power of CoL in a qualitatively new way, generalizing formulas (to which the earlier languages of CoL were limited) to circuit-style structures termed cirquents. The latter, unlike formulas, are able to account for subgame/subtask sharing between different parts of the overall game/task. Among the many advantages offered by this ability is that it allows us to capture, refine and generalize the well known independence-friendly logic which, after the present leap forward, naturally becomes a conservative fragment of CoL, just as classical logic had been known to be a conservative fragment of the formula-based version of CoL. Technically, this paper is self-contained, and can be read without any prior familiarity with CoL.
△ Less
Submitted 27 April, 2011; v1 submitted 11 June, 2009;
originally announced June 2009.
-
Toggling operators in computability logic
Authors:
Giorgi Japaridze
Abstract:
Computability logic (CL) (see http://www.cis.upenn.edu/~giorgi/cl.html ) is a research program for redevelo** logic as a formal theory of computability, as opposed to the formal theory of truth which it has more traditionally been. Formulas in CL stand for interactive computational problems, seen as games between a machine and its environment; logical operators represent operations on such ent…
▽ More
Computability logic (CL) (see http://www.cis.upenn.edu/~giorgi/cl.html ) is a research program for redevelo** logic as a formal theory of computability, as opposed to the formal theory of truth which it has more traditionally been. Formulas in CL stand for interactive computational problems, seen as games between a machine and its environment; logical operators represent operations on such entities; and "truth" is understood as existence of an effective solution. The formalism of CL is open-ended, and may undergo series of extensions as the studies of the subject advance. So far three -- parallel, sequential and choice -- sorts of conjunction and disjunction have been studied. The present paper adds one more natural kind to this collection, termed toggling. The toggling operations can be characterized as lenient versions of choice operations where choices are retractable, being allowed to be reconsidered any finite number of times. This way, they model trial-and-error style decision steps in interactive computation. The main technical result of this paper is constructing a sound and complete axiomatization for the propositional fragment of computability logic whose vocabulary, together with negation, includes all four -- parallel, toggling, sequential and choice -- kinds of conjunction and disjunction. Along with toggling conjunction and disjunction, the paper also introduces the toggling versions of quantifiers and recurrence operations.
△ Less
Submitted 1 May, 2010; v1 submitted 22 April, 2009;
originally announced April 2009.
-
Ptarithmetic
Authors:
Giorgi Japaridze
Abstract:
The present article introduces ptarithmetic (short for "polynomial time arithmetic") -- a formal number theory similar to the well known Peano arithmetic, but based on the recently born computability logic (see http://www.cis.upenn.edu/~giorgi/cl.html) instead of classical logic. The formulas of ptarithmetic represent interactive computational problems rather than just true/false statements, and…
▽ More
The present article introduces ptarithmetic (short for "polynomial time arithmetic") -- a formal number theory similar to the well known Peano arithmetic, but based on the recently born computability logic (see http://www.cis.upenn.edu/~giorgi/cl.html) instead of classical logic. The formulas of ptarithmetic represent interactive computational problems rather than just true/false statements, and their "truth" is understood as existence of a polynomial time solution. The system of ptarithmetic elaborated in this article is shown to be sound and complete. Sound in the sense that every theorem T of the system represents an interactive number-theoretic computational problem with a polynomial time solution and, furthermore, such a solution can be effectively extracted from a proof of T. And complete in the sense that every interactive number-theoretic problem with a polynomial time solution is represented by some theorem T of the system.
The paper is self-contained, and can be read without any previous familiarity with computability logic.
△ Less
Submitted 26 February, 2010; v1 submitted 17 February, 2009;
originally announced February 2009.
-
Towards applied theories based on computability logic
Authors:
Giorgi Japaridze
Abstract:
Computability logic (CL) (see http://www.cis.upenn.edu/~giorgi/cl.html) is a recently launched program for redevelo** 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…
▽ More
Computability logic (CL) (see http://www.cis.upenn.edu/~giorgi/cl.html) is a recently launched program for redevelo** 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.
△ Less
Submitted 16 November, 2009; v1 submitted 22 May, 2008;
originally announced May 2008.
-
Sequential operators in computability logic
Authors:
Giorgi Japaridze
Abstract:
Computability logic (CL) (see http://www.cis.upenn.edu/~giorgi/cl.html) is a semantical platform and research program for redevelo** logic as a formal theory of computability, as opposed to the formal theory of truth which it has more traditionally been. Formulas in CL stand for (interactive) computational problems, understood as games between a machine and its environment; logical operators r…
▽ More
Computability logic (CL) (see http://www.cis.upenn.edu/~giorgi/cl.html) is a semantical platform and research program for redevelo** logic as a formal theory of computability, as opposed to the formal theory of truth which it has more traditionally been. Formulas in CL stand for (interactive) computational problems, understood as games between a machine and its environment; logical operators represent operations on such entities; and "truth" is understood as existence of an effective solution, i.e., of an algorithmic winning strategy.
The formalism of CL is open-ended, and may undergo series of extensions as the study of the subject advances. The main groups of operators on which CL has been focused so far are the parallel, choice, branching, and blind operators. The present paper introduces a new important group of operators, called sequential. The latter come in the form of sequential conjunction and disjunction, sequential quantifiers, and sequential recurrences. As the name may suggest, the algorithmic intuitions associated with this group are those of sequential computations, as opposed to the intuitions of parallel computations associated with the parallel group of operations: playing a sequential combination of games means playing its components in a sequential fashion, one after one.
The main technical result of the present paper is a sound and complete axiomatization of the propositional fragment of computability logic whose vocabulary, together with negation, includes all three -- parallel, choice and sequential -- sorts of conjunction and disjunction. An extension of this result to the first-order level is also outlined.
△ Less
Submitted 15 October, 2008; v1 submitted 9 December, 2007;
originally announced December 2007.
-
Cirquent calculus deepened
Authors:
Giorgi Japaridze
Abstract:
Cirquent calculus is a new proof-theoretic and semantic framework, whose main distinguishing feature is being based on circuits, as opposed to the more traditional approaches that deal with tree-like objects such as formulas or sequents. Among its advantages are greater efficiency, flexibility and expressiveness. This paper presents a detailed elaboration of a deep-inference cirquent logic, whic…
▽ More
Cirquent calculus is a new proof-theoretic and semantic framework, whose main distinguishing feature is being based on circuits, as opposed to the more traditional approaches that deal with tree-like objects such as formulas or sequents. Among its advantages are greater efficiency, flexibility and expressiveness. This paper presents a detailed elaboration of a deep-inference cirquent logic, which is naturally and inherently resource conscious. It shows that classical logic, both syntactically and semantically, is just a special, conservative fragment of this more general and, in a sense, more basic logic -- the logic of resources in the form of cirquent calculus. The reader will find various arguments in favor of switching to the new framework, such as arguments showing the insufficiency of the expressive power of linear logic or other formula-based approaches to develo** resource logics, exponential improvements over the traditional approaches in both representational and proof complexities offered by cirquent calculus, and more. Among the main purposes of this paper is to provide an introductory-style starting point for what, as the author wishes to hope, might have a chance to become a new line of research in proof theory -- a proof theory based on circuits instead of formulas.
△ Less
Submitted 1 April, 2008; v1 submitted 10 September, 2007;
originally announced September 2007.
-
Many concepts and two logics of algorithmic reduction
Authors:
Giorgi Japaridze
Abstract:
Within the program of finding axiomatizations for various parts of computability logic, it was proved 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…
▽ More
Within the program of finding axiomatizations for various parts of computability logic, it was proved 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 (Turing) 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 (in isolation) 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. An online source on computability logic can be found at http://www.cis.upenn.edu/~giorgi/cl.html
△ Less
Submitted 12 October, 2008; v1 submitted 1 June, 2007;
originally announced June 2007.
-
The intuitionistic fragment of computability logic at the propositional level
Authors:
Giorgi Japaridze
Abstract:
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 --…
▽ More
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 (disjunction = machine's choice, conjunction = environment's choice), and "absurd" as a computational problem of universal strength. See http://www.cis.upenn.edu/~giorgi/cl.html for a comprehensive online source on computability logic.
△ Less
Submitted 11 February, 2006; v1 submitted 5 February, 2006;
originally announced February 2006.
-
The logic of interactive Turing reduction
Authors:
Giorgi Japaridze
Abstract:
The paper gives a soundness and completeness proof for the implicative fragment of intuitionistic calculus with respect to the semantics of computability logic, which understands intuitionistic implication as interactive algorithmic reduction. This concept -- more precisely, the associated concept of reducibility -- is a generalization of Turing reducibility from the traditional, input/output so…
▽ More
The paper gives a soundness and completeness proof for the implicative fragment of intuitionistic calculus with respect to the semantics of computability logic, which understands intuitionistic implication as interactive algorithmic reduction. This concept -- more precisely, the associated concept of reducibility -- is a generalization of Turing reducibility from the traditional, input/output sorts of problems to computational tasks of arbitrary degrees of interactivity. See http://www.cis.upenn.edu/~giorgi/cl.html for a comprehensive online source on computability logic.
△ Less
Submitted 11 February, 2006; v1 submitted 28 December, 2005;
originally announced December 2005.
-
In the beginning was game semantics
Authors:
Giorgi Japaridze
Abstract:
This article presents an overview of computability logic -- the game-semantically constructed logic of interactive computational tasks and resources. There is only one non-overview, technical section in it, devoted to a proof of the soundness of affine logic with respect to the semantics of computability logic. A comprehensive online source on the subject can be found at http://www.cis.upenn.edu…
▽ More
This article presents an overview of computability logic -- the game-semantically constructed logic of interactive computational tasks and resources. There is only one non-overview, technical section in it, devoted to a proof of the soundness of affine logic with respect to the semantics of computability logic. A comprehensive online source on the subject can be found at http://www.cis.upenn.edu/~giorgi/cl.html
△ Less
Submitted 24 October, 2008; v1 submitted 18 July, 2005;
originally announced July 2005.
-
Introduction to Cirquent Calculus and Abstract Resource Semantics
Authors:
Giorgi Japaridze
Abstract:
This paper introduces a refinement of the sequent calculus approach called cirquent calculus. While in Gentzen-style proof trees sibling (or cousin, etc.) sequents are disjoint sequences of formulas, in cirquent calculus they are permitted to share elements. Explicitly allowing or disallowing shared resources and thus taking to a more subtle level the resource-awareness intuitions underlying sub…
▽ More
This paper introduces a refinement of the sequent calculus approach called cirquent calculus. While in Gentzen-style proof trees sibling (or cousin, etc.) sequents are disjoint sequences of formulas, in cirquent calculus they are permitted to share elements. Explicitly allowing or disallowing shared resources and thus taking to a more subtle level the resource-awareness intuitions underlying substructural logics, cirquent calculus offers much greater flexibility and power than sequent calculus does. A need for substantially new deductive tools came with the birth of computability logic (see http://www.cis.upenn.edu/~giorgi/cl.html) - the semantically constructed formal theory of computational resources, which has stubbornly resisted any axiomatization attempts within the framework of traditional syntactic approaches. Cirquent calculus breaks the ice. Removing contraction from the full collection of its rules yields a sound and complete system for the basic fragment CL5 of computability logic. Doing the same in sequent calculus, on the other hand, throws out the baby with the bath water, resulting in the strictly weaker affine logic. An implied claim of computability logic is that it is CL5 rather than affine logic that adequately materializes the resource philosophy traditionally associated with the latter. To strengthen this claim, the paper further introduces an abstract resource semantics and shows the soundness and completeness of CL5 with respect to it.
△ Less
Submitted 23 December, 2005; v1 submitted 27 June, 2005;
originally announced June 2005.
-
From truth to computability II
Authors:
Giorgi Japaridze
Abstract:
Computability logic is a formal theory of computational tasks and resources. Formulas in it represent interactive computational problems, and "truth" is understood as algorithmic solvability. Interactive computational problems, in turn, are defined as a certain sort games between a machine and its environment, with logical operators standing for operations on such games. Within the ambitious pro…
▽ More
Computability logic is a formal theory of computational tasks and resources. Formulas in it represent interactive computational problems, and "truth" is understood as algorithmic solvability. Interactive computational problems, in turn, are defined as a certain sort games between a machine and its environment, with logical operators standing for operations on such games. Within the ambitious program of finding axiomatizations for incrementally rich fragments of this semantically introduced logic, the earlier article "From truth to computability I" proved soundness and completeness for system CL3, whose language has the so called parallel connectives (including negation), choice connectives, choice quantifiers, and blind quantifiers. The present paper extends that result to the significantly more expressive system CL4 with the same collection of logical operators. What makes CL4 expressive is the presence of two sorts of atoms in its language: elementary atoms, representing elementary computational problems (i.e. predicates, i.e. problems of zero degree of interactivity), and general atoms, representing arbitrary computational problems. CL4 conservatively extends CL3, with the latter being nothing but the general-atom-free fragment of the former. Removing the blind (classical) group of quantifiers from the language of CL4 is shown to yield a decidable logic despite the fact that the latter is still first-order. A comprehensive online source on computability logic can be found at http://www.cis.upenn.edu/~giorgi/cl.html
△ Less
Submitted 19 July, 2005; v1 submitted 16 January, 2005;
originally announced January 2005.
-
Intuitionistic computability logic
Authors:
Giorgi Japaridze
Abstract:
Computability logic (CL) is a systematic formal theory of computational tasks and resources, which, in a sense, can be seen as a semantics-based alternative to (the syntactically introduced) linear logic. With its expressive and flexible language, where formulas represent computational problems and "truth" is understood as algorithmic solvability, CL potentially offers a comprehensive logical ba…
▽ More
Computability logic (CL) is a systematic formal theory of computational tasks and resources, which, in a sense, can be seen as a semantics-based alternative to (the syntactically introduced) linear logic. With its expressive and flexible language, where formulas represent computational problems and "truth" is understood as algorithmic solvability, CL potentially offers a comprehensive logical basis for constructive applied theories and computing systems inherently requiring constructive and computationally meaningful underlying logics.
Among the best known constructivistic logics is Heyting's intuitionistic calculus INT, whose language can be seen as a special fragment of that of CL. The constructivistic philosophy of INT, however, has never really found an intuitively convincing and mathematically strict semantical justification. CL has good claims to provide such a justification and hence a materialization of Kolmogorov's known thesis "INT = logic of problems". The present paper contains a soundness proof for INT with respect to the CL semantics. A comprehensive online source on CL is available at http://www.cis.upenn.edu/~giorgi/cl.html
△ Less
Submitted 14 June, 2006; v1 submitted 4 November, 2004;
originally announced November 2004.
-
From truth to computability I
Authors:
Giorgi Japaridze
Abstract:
The recently initiated approach called computability logic is a formal theory of interactive computation. See a comprehensive online source on the subject at http://www.cis.upenn.edu/~giorgi/cl.html . The present paper contains a soundness and completeness proof for the deductive system CL3 which axiomatizes the most basic first-order fragment of computability logic called the finite-depth, elem…
▽ More
The recently initiated approach called computability logic is a formal theory of interactive computation. See a comprehensive online source on the subject at http://www.cis.upenn.edu/~giorgi/cl.html . The present paper contains a soundness and completeness proof for the deductive system CL3 which axiomatizes the most basic first-order fragment of computability logic called the finite-depth, elementary-base fragment. Among the potential application areas for this result are the theory of interactive computation, constructive applied theories, knowledgebase systems, systems for resource-bound planning and action. This paper is self-contained as it reintroduces all relevant definitions as well as main motivations.
△ Less
Submitted 19 July, 2005; v1 submitted 20 July, 2004;
originally announced July 2004.
-
Propositional Computability Logic II
Authors:
Giorgi Japaridze
Abstract:
Computability logic is a formal theory of computational tasks and resources. Its formulas represent interactive computational problems, logical operators stand for operations on computational problems, and validity of a formula is understood as being a scheme of problems that always have algorithmic solutions. A comprehensive online source on the subject is available at http://www.cis.upenn.edu/…
▽ More
Computability logic is a formal theory of computational tasks and resources. Its formulas represent interactive computational problems, logical operators stand for operations on computational problems, and validity of a formula is understood as being a scheme of problems that always have algorithmic solutions. A comprehensive online source on the subject is available at http://www.cis.upenn.edu/~giorgi/cl.html . The earlier article "Propositional computability logic I" proved soundness and completeness for the (in a sense) minimal nontrivial fragment CL1 of computability logic. The present paper extends that result to the significantly more expressive propositional system CL2. What makes CL2 more expressive than CL1 is the presence of two sorts of atoms in its language: elementary atoms, representing elementary computational problems (i.e. predicates), and general atoms, representing arbitrary computational problems. CL2 conservatively extends CL1, with the latter being nothing but the general-atom-free fragment of the former.
△ Less
Submitted 20 June, 2004; v1 submitted 18 June, 2004;
originally announced June 2004.
-
Computability Logic: a formal theory of interaction
Authors:
Giorgi Japaridze
Abstract:
Computability logic is a formal theory of (interactive) computability in the same sense as classical logic is a formal theory of truth. This approach was initiated very recently in "Introduction to computability logic" (Annals of Pure and Applied Logic 123 (2003), pp.1-99). The present paper reintroduces computability logic in a more compact and less technical way. It is written in a semitutoria…
▽ More
Computability logic is a formal theory of (interactive) computability in the same sense as classical logic is a formal theory of truth. This approach was initiated very recently in "Introduction to computability logic" (Annals of Pure and Applied Logic 123 (2003), pp.1-99). The present paper reintroduces computability logic in a more compact and less technical way. It is written in a semitutorial style with a general computer science, logic or mathematics audience in mind. An Internet source on the subject is available at http://www.cis.upenn.edu/~giorgi/cl.html, and additional material at http://www.csc.villanova.edu/~japaridz/CL/gsoll.html .
△ Less
Submitted 10 December, 2004; v1 submitted 8 April, 2004;
originally announced April 2004.
-
Propositional computability logic I
Authors:
Giorgi Japaridze
Abstract:
In the same sense as classical logic is a formal theory of truth, the recently initiated approach called computability logic is a formal theory of computability. It understands (interactive) computational problems as games played by a machine against the environment, their computability as existence of a machine that always wins the game, logical operators as operations on computational problems…
▽ More
In the same sense as classical logic is a formal theory of truth, the recently initiated approach called computability logic is a formal theory of computability. It understands (interactive) computational problems as games played by a machine against the environment, their computability as existence of a machine that always wins the game, logical operators as operations on computational problems, and validity of a logical formula as being a scheme of "always computable" problems. The present contribution gives a detailed exposition of a soundness and completeness proof for an axiomatization of one of the most basic fragments of computability logic. The logical vocabulary of this fragment contains operators for the so called parallel and choice operations, and its atoms represent elementary problems, i.e. predicates in the standard sense. This article is self-contained as it explains all relevant concepts. While not technically necessary, however, familiarity with the foundational paper "Introduction to computability logic" [Annals of Pure and Applied Logic 123 (2003), pp.1-99] would greatly help the reader in understanding the philosophy, underlying motivations, potential and utility of computability logic, -- the context that determines the value of the present results. Online introduction to the subject is available at http://www.cis.upenn.edu/~giorgi/cl.html and http://www.csc.villanova.edu/~japaridz/CL/gsoll.html .
△ Less
Submitted 21 June, 2004; v1 submitted 8 April, 2004;
originally announced April 2004.
