The intuitionistic fragment of computability logic at the propositional level

Subsystems of classical logic (including intuitionistic logic) (03B20) Logic in computer science (03B70) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

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

Review text

Propositional axiomatic intuitionistic calculus (INT), Kripke semantics, and computability-logic semantics are considered. Intuitionistic formulas are built from propositional variables, the sign \(\natural\) for the false, and logical operations in the standard way. INT is described in the form of intuitionistic Gentzen-style natural inference for intuitionistic sequents. The expression Int \(\vdash{F}\) means formula \(F\) is provable in Int. A Kripke model is a triple \(K= (W,R,\mid\!\equiv)\), where 1) \(W\) is the set \(\{1,\dots,n\}\) of the first \(n\geq 1\) natural numbers (the worlds of \(K\)); 2) \(R\) is a binary (transitive, reflexive, antisymmetric) accessibility relation between worlds; 3) \(\mid\!\equiv\) is the forcing relation of \(K\) between worlds and formulas. If \(p\) is in \(W\) and \(F\) is a formula, then \(p\mid\!\equiv F\) means \(p\) forces \(F\). The expression \(K\parallel\!\equiv F\) means \(1\mid\!\equiv F\). The expression \(\parallel\!\equiv F\) means \(K\parallel\!\equiv F\) for every Kripke model \(K\). Theorem (Kripke). \(\text{Int}\vdash F\) if (completeness) and only if (soundness) \(\parallel\!\equiv F\). Let 1) a \(\Sigma_1\)-predicate be a predicate of the form \(\exists{zA}\) for some decidable finitary predicate (elementary game) \(A\); 2) a Boolean combination of \(\Sigma_1\)-predicates be a \(\neg\), \(\wedge\), \(\vee\)-combination of such games; 3) \(\Sigma_1^B\) be the set of all Boolean combinations of \(\Sigma_1\) predicates; 4) \(\bigsqcup\Sigma_{1}^{B}\) be the set of all games of the form \(\bigsqcup\, xA\), where \(A \in\Sigma_1^B\); 5) \(^*\) be an interpretation and \(C\) a set of static games, such as \(\Sigma_1^B\) or \(\bigsqcup\Sigma_1^B\). Interpretation \(^*\) is of complexity \(C\) iff 1) for every nonlogical atom \(P\), \(P^*\) is in \(C\); 2) the base \(\natural^*\) is also in \(C\). A formula \(K\) in computability logic is an interactive computational problem, formalized as a game between a machine and its environment. Let the expressions \(\parallel\!\!\!-K\) and \(\mid\mid\mid\!\!\!-K\) mean formula \(K\) is valid and \(K\) is uniformly valid, respectively. Main theorem (Japaridze). 1. For any formula \(K\), \(\text{Int}\vdash K\) iff \(\parallel\!\!\!-K\) iff \(\mid\mid\mid\!\!\!-K\). 2. (Soundness). There is an effective procedure that takes an arbitrary INT-proof of an arbitrary formula \(K\) and construct a uniform solution for \(K\). 3. (Completeness). If an INT-formula \(K\) is not provable in INT, then \(K^*\) is not computable for some interpretation \(^*\) of complexity \(\bigsqcup\Sigma_1^B\).

Recommendations

Cites work

Cited in

(26)

This page was built for publication: The intuitionistic fragment of computability logic at the propositional level

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2373697)