Normal Modal Natural Deduction Proof Theory Of The Nature Of Exploration

The field of natural deduction in modal logics is not one of modal logics' research mainstreams, and these methods have never really flourished in modal logic. But this also is an important sub-tradition of modal logic—the syntactic tradition and the proof theory tradition. This article mainly discusses on these fields' questions. Firstly, we mainly discuss the research survey since the natural deduction methods were found by logicians such as G. Gentzen and others and we give some literature summaries of this text. And we discuss about the basic concepts, the definitions of natural deduction and features of natural deduction. Then we study about the natural deduction systems of the classical logic—Natural Deduction System and Sequent Deduction System, We study the structures and some correlative conclusions of these systems. In this foundation, we will inspect the natural deduction methods in some modal logics, here we will mainly research in normal modal logics like K, T, S4, S5 and other systems, and we will introduce the different research views and methods. We detailed research the soundness and completeness theories of these modal systems.The third chapter is very important part of this article. We mainly discuss the basic proof theoretical properties of classical logic and modal logic. In this part we discuss the properties and the study survey of proof theory, and we study the proof theoretical properties such as Gentzen theorem (i. e. cut elimination theory), sub-formula property and disjunction property. We obtain these properties of some classical logic systems and modal logic systems and also point out some systems that have not such properties.