Sequents and Trees
Sequents and Trees
复制标题
序列和树
DOI：
10.1007/978-3-030-57145-0
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Andrzej Indrzejczak
中科院分区：
文献类型：
--
作者：
Andrzej Indrzejczak
以各种形式的序列演算(SC)作为基本形式系统的证明论已经有了许多优秀的工作。这本书的性质不同。它不是用序列演算对证明论的系统阐述，而是对序列演算本身的方法论研究。当然，不可能介绍序列演算及其应用，也不可能避免介绍证明理论中的重要问题。然而，我们的目标是将重点放在工具上，而不是结果上；后者将作为在顺序演算框架内发展的证明技术的例子。在我看来，顺序演算确实是一种令人惊叹的形式系统，它们值得单独研究。在接下来的内容中，我们将介绍规则和微积分的几种变体，描述它们的优点，并集中在它们的应用上。特别是，我们将详细介绍几种证明最重要的结果的方法，如割消去定理、完备性、可判断性、插值法。这本书是初级的，自成体系的。所有技术细节将包括正式介绍和非正式解释。校样将被详细介绍，但留有许多空白，作为细心读者的练习。由于我们的目的是展示如何使用序列演算，我们必须在这里强调，做大多数练习是必要的，以获得所给方法的实用知识。在当代作品中，有一种趋势是呈现非常笼统的结果。这在理论上是有价值的，但对于新手来说，可能很难跟上。在这本书中，我们选择了一条不同的路线；我们提供了几个更容易掌握的案例研究。经过对这种特殊情况的仔细研究，可以更容易地发展出对大类类似问题的一般和统一的处理。我们专注于证据。关于SC中的校样就不多了，因为它们的构造相当简单，任何使用过Tableau系统的读者在SC中进行校样搜索应该没有问题。我们更关注关于SC的最深刻结果的证明。我们还想展示一下我们有多容易
There are a lot of excellent works in proof theory using various forms of Sequent Calculi (SC) as the basic formal systems. 1 This book is of a different character. It is not a systematic exposition of proof theory using sequent calculus but it is a methodological study of sequent calculi as such. Of course it is not possible to present sequent calculi and their applications and to avoid a presentation of important issues in proof theory. However, our aim is to focus on the tools not on the results; the latter will serve as examples illustrating proof techniques developed in the framework of sequent calculi. In my opinion sequent calculi are truly amazing kind of formal systems and they deserve a separate study. In what follows we will present several variants of rules and calculi, describe their merits and focus on their applications. In particular, we will present in detail several methods of proving the most important results like the cut-elimination theorem, completeness, decidability, interpolation.The book is elementary and self-contained. All technical details will be introduced both formally and with informal explanations. Proofs will be presented in detail but with a lot of gaps left as exercises for the careful reader. As our aim is to show how to use sequent calculi we must underline here that it is essential to do most of the exercises to gain a working knowledge of the methods presented. There is a tendency in contemporary works to present very general results. This is theoretically valuable but for a novice it may be hard to follow. In this book we opt for a different route; we rather present several case studies which are much simpler to grasp. After careful study of such special cases, the general and uniform treatment of broad classes of similar problems may be developed more easily. We focus on proofs. Not so much on proofs in SC since their construction is rather simple and any reader who has worked with tableau systems should have no problem with proof search in SC. We rather focus on proofs of the most profound results concerning SC. We also want to show how easily