Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A propositional cirquent calculus for computability logic

Giorgi Japaridze

TL;DR

The main technical result of the article is a proof of the soundness and completeness of CL18, the basic propositional fragment of computability logic—the game-semantically conceived logic of computational resources and tasks.

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 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.

A propositional cirquent calculus for computability logic

TL;DR

The main technical result of the article is a proof of the soundness and completeness of CL18, the basic propositional fragment of computability logic—the game-semantically conceived logic of computational resources and tasks.

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 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.
Paper Structure (8 sections, 6 theorems, 18 equations)

This paper contains 8 sections, 6 theorems, 18 equations.

Table of Contents

  1. Introduction
  2. Games and interactive machines
  3. Syntax
  4. Semantics
  5. Axiomatics
  6. The preservation lemma
  7. Soundness and completeness
  8. From general-base to mixed-base formalism and back

Key Result

Lemma 6.1

1. Each application $\vec{A}\leadsto B$ of any of the rules of $\hbox{\bf CL18}$ preserves validity in the premise-to-conclusion direction, i.e., if all premises from $\vec{A}$ are valid, then so is the conclusion $B$. 2. Each application $\vec{A}\leadsto B$ of any of the rules of $\hbox{\bf CL18}$

Theorems & Definitions (18)

  • Definition 2.1
  • Definition 2.2
  • Definition 2.3
  • Definition 2.4
  • Definition 3.1
  • Definition 4.1
  • Definition 4.3
  • Example 5.1
  • Example 5.2
  • Example 5.3
  • ...and 8 more