The parallel versus branching recurrences in computability logic (Q1934954)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | The parallel versus branching recurrences in computability logic |
scientific article |
Statements
The parallel versus branching recurrences in computability logic (English)
0 references
30 January 2013
0 references
Computability logic ( CoL) is a formal theory of interactive computational problems understood as games between a machine and its environment. CoL has a game semantics. The signature of CoL is \(\mathrm{SU} =(\neg,\wedge,\vee,\downarrow,\uparrow)\), where \(\neg,\wedge,\vee\) are ordinary logical operators and \(\downarrow,\uparrow\) are operators of \textit{uncountable branching recurrence}. If \(F\) is a formula in signature SU, then the formula \(\uparrow F=\neg\downarrow\neg F\) is dual for the formula \(\downarrow F\). The \textit{basic logic} in signature SU (BLinSU) is the set of all formulas in signature SU. \(\mathbf{CL15}\) is a sound and complete axiomatization for the basic (\(\neg,\wedge,\vee,\downarrow,\uparrow\))-fragment of computability logic. \(\mathbf{CL15}\) is a system built in cirquent calculus. Resource semantics are described. The parallel recurrence \(\curlywedge\) and its dual \(\curlyvee\) are considered for which \(\curlyvee F =\neg\curlywedge\neg F\). Three statements are proved. Theorem 1. The basic logic in the signature (\(\neg,\wedge,\vee,\curlywedge,\curlyvee\)) is a proper superset of the basic logic in the signature (\(\neg,\wedge,\vee,\downarrow,\uparrow\)). Theorem 2. The axiomatic system \(\mathbf{CL15}\) with \(\curlywedge,\curlyvee\) instead of \(\downarrow,\uparrow\) is sound but not complete (a conjecture of Japaridze). Theorem 3. The operator \(\curlywedge\) is strictly weaker than \(\downarrow\), that is, \(\downarrow F\) logically implies \(\curlywedge F\), but the reverse does not hold.
0 references
computability logic
0 references
cirquent calculus
0 references
interactive computation
0 references
game semantics
0 references
resource semantics
0 references