Sequential operators in computability logic (Q999265)

From MaRDI portal
Revision as of 14:29, 10 July 2023 by Importer (talk | contribs) (‎Created a new Item)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
scientific article
Language Label Description Also known as
English
Sequential operators in computability logic
scientific article

    Statements

    Sequential operators in computability logic (English)
    0 references
    0 references
    3 February 2009
    0 references
    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.
    0 references
    computability logic
    0 references
    interactive computation
    0 references
    game semantics
    0 references
    linear logic
    0 references
    constructive logic
    0 references

    Identifiers