Arithmetical Completeness of the Intuitionistic Logic of Proofs

被引：6
|
作者：
Dashkov, Evgenij [1 ]
机构：
[1] Moscow MV Lomonosov State Univ, Dept Math Log & Theory Algorithms, Fac Mech & Math, Moscow 119992, Russia
来源：
JOURNAL OF LOGIC AND COMPUTATION | 2011年 / 21卷 / 04期
基金：
美国国家科学基金会;
关键词：
Logic of proofs; intuitionistic arithmetic; admissible rules;
D O I：
10.1093/logcom/exp041
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
Classical logic of proofs LP naturally extends propositional calculus to the language enriched with formulas meaning t is a proof of formula F. Intuitionistic logic of proofs iLP introduced by Artemov and Iemhoff was conjectured to be complete with respect to intuitionistic arithmetic HA. The article presents a proof of this conjecture.
引用
收藏
页码：665 / 682
页数：18
相关论文
共 50 条
12345