标题:Introduction to clarithmetic III
作者:Japaridze, G.
作者机构:[Japaridze, G] School of Computer Science and Technology, Shandong University, Middle Shunhua Road, Jinan, Shandong 25101, China, Department of Comput 更多
通讯作者:Japaridze, G
通讯作者地址:[Japaridze, G]Villanova Univ, Dept Comp Sci, 800 Lancaster Ave, Villanova, PA 19085 USA.
来源:Annals of Pure and Applied Logic
出版年:2014
卷:165
期:1
页码:241-252
DOI:10.1016/j.apal.2013.07.012
关键词:03D75;03F30;03F50;68T30;Computability logic;Constructive theories;Game semantics;Interactive computation;Peano arithmetic
摘要:The present paper constructs three new systems of clarithmetic (arithmetic based on computability logic): CLA8, CLA9 and CLA10. System CLA8 is shown to be sound and extensionally complete with respect to PA-provably recursive time computability. This is in the sense that an arithmetical problem A has a τ-time solution for some PA-provably recursive function τ iff A is represented by some theorem of CLA8. System CLA9 is shown to be sound and intensionally complete with respect to constructively PA-provable computability. This is in the sense that a sentence X is a theorem of CLA9 iff, for some particular machine M, PA proves that M computes (the problem represented by) X. And system CLA10 is shown to be sound and intensionally complete with respect to not-necessarily-constructively PA-provable computability. This means that a sentence X is a theorem of CLA10 iff PA proves that X is computable, even if PA does not \"know\" of any particular machine M that computes X.
收录类别:SCOPUS;SCIE
WOS核心被引频次:2
Scopus被引频次:2
资源类型:期刊论文
原文链接:https://www.scopus.com/inward/record.uri?eid=2-s2.0-84885304117&doi=10.1016%2fj.apal.2013.07.012&partnerID=40&md5=4b0059a36b4b2991c5f9f0bc54a251a2
TOP