Portal de Periódicos da CAPES

Analytic natural deduction

1965; Cambridge University Press; Volume: 30; Issue: 2 Linguagem: Inglês

10.2307/2270130

1943-5886

Raymond M. Smullyan,

Homotopy and Cohomology in Algebraic Topology

We consider some natural deduction systems for quantification theory whose only quantificational rules involve elimination of quantifiers. By imposing certain restrictions on the rules, we obtain a system which we term Analytic Natural Deduction ; it has the property that the only formulas used in the proof of a given formula X are either subformulas of X , or negations of subformulas of X . By imposing further restrictions, we obtain a canonical procedure which is bound to terminate, if the formula being tested is valid. The procedure (ultimately in the spirit of Herbrand [1]) can be thought of as a partial linearization of the method of semantical tableaux [2], [3]. A further linearization leads to a variant of Gentzen's system which we shall study in a sequel. The completeness theorem for semantical tableaux rests essentially on König's lemma on infinite graphs [4]. Our completeness theorem for natural deduction uses as a counterpart to König's lemma, a lemma on infinite “nest structures”, as they are to be defined. These structures can be looked at as the underlying combinatorial basis of a wide variety of natural deduction systems. In § 1 we study these nest structures in complete abstraction from quantification theory; the results of this section are of a purely combinatorial nature. The applications to quantification theory are given in § 2.