Sequential operators in computability logic (Q999265)

The article is a continuation of a series of works of the author on computability logic (CL) as a formal-logic axiomatic system formalizing the process of computation considered as an interactive game between a machine and its environment. ``Truth'' is understood as existence of an algorithmic winning strategy. A sound and complete axiomatization of the propositional fragment of CL is given. CL is an extension of classical logic. \(\top\) and \(\bot\) are symbolic names for the players. Classical propositions and predicates \(p,q,r(x),s(x,y),\dots\) are viewed as elementary games that are won by the machine if true and lost if false. General atoms \(P,Q,R(x),S(x,y),\dots\) represent any other games. The operators \(\neg\), \(\wedge\), \(\vee\), \(\forall\), \(\exists\) are generalizations of the corresponding classical operators from elementary games to all games. Negation, \(\neg\), is a switch operation between \(\top\) and \(\bot\). The choice operations, \(\sqcup\) and \(\sqcap\), model decision in the course of interaction with disjunction and existential quantifier, meaning choices by \(\top\), and conjunction and universal quantifier, meaning \(\bot\)'s choices, respectively. The parallel operations, \(\wedge\) and \(\vee\), where \(A \wedge B\) or \(A \vee B\) means playing in parallel. In \(A \wedge B\), \(\top\) is considered the winner if it wins in both of the components, while in \(A \vee B\) it is sufficient to win in one of the components. The operation of reduction, \(\to\), where \(A \to B\) reduces \(B\) to \(A\). Blind operations produce games with imperfect information. Sequential conjunction \(A \bigtriangleup B\) gives a game that starts and proceeds as a play of \(A\). The branching operations come in the form of branching recurrence and its dual branching co-recurrence. The first-order level is outlined.