期刊
FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES (FOSSACS 2017)
卷 10203, 期 -, 页码 283-300出版社
SPRINGER INTERNATIONAL PUBLISHING AG
DOI: 10.1007/978-3-662-54458-7_17
关键词
-
资金
- Air Force Office of Scientific Research, Air Force Materiel Command, USAF [FA9550-14-1-0096]
Cyclic proof provides a style of proof for logics with inductive (and coinductive) definitions, in which proofs are cyclic graphs representing a form of argument by infinite descent. It is easily shown that cyclic proof subsumes proof by (co) induction. So cyclic proof systems are at least as powerful as the corresponding proof systems with explicit (co) induction rules. Whether or not the converse inclusion holds is a non-trivial question. In this paper, we resolve this question in one interesting case. We show that a cyclic formulation of first-order arithmetic is equivalent in power to Peano Arithmetic. The proof involves formalising the meta-theory of cyclic proof in a subsystem of second-order arithmetic.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据