Normality, Non-contamination and Logical Depth in Classical Natural Deduction
Studia Logica(2019)
摘要
In this paper we provide a detailed proof-theoretical analysis of a natural deduction system for classical propositional logic that (i) represents classical proofs in a more natural way than standard Gentzen-style natural deduction, (ii) admits of a simple normalization procedure such that normal proofs enjoy the Weak Subformula Property, (iii) provides the means to prove a Non-contamination Property of normal proofs that is not satisfied by normal proofs in the Gentzen tradition and is useful for applications, especially in formal argumentation, (iv) naturally leads to defining a notion of depth of a proof, to the effect that, for every fixed natural k , normal k -depth deducibility is a tractable problem and converges to classical deducibility as k tends to infinity.
更多查看译文
关键词
Natural deduction,Classical propositional logic,Normal proofs,Non-contamination,Tractable reasoning
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络