The intuitionistic fragment of computability logic at the propositional level (Q2373697)

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