E. W. Beth. Remarks on natural deduction. Koninklijke Nederlandse Akademie van Wetenschappen, Proceedings, series A, Vol. 58 (1955), pp. 322–325; also Indagationes mathematicae, vol. 17 (1955) pp. 322–325. - E. W. Beth. Semantic entailment and formal derivability. Mededelingen der Koninklijke Nederlandse Akademie van Wetenschappen, Afd. letterkunde, n.s. vol. 18 no. 13 (1955), pp. 309–342. - K. Jaakko J. Hintikka. A new approach to sentential logic. Societas Scientiarum Fennica, Commentationes physico-mathematicae, vol. 17 no. 2 (1953), 14 pp. - K. Jaakko J. Hintikka. Form and content in quantification theory. Two papers on symbolic logic, Acta philosophica Fennica no. 8, Helsinki1955, pp. 7–55. - K. Jaakko J. Hintikka. Notes on quantification theory. Societas Scientiarum Fennica, Commentationes physico-mathematicae, vol. 17 no. 12 (1955), 13 pp.

1957 ◽  
Vol 22 (4) ◽  
pp. 360-363
Author(s):  
William Craig
Keyword(s):  
Natural Deduction ◽  
Symbolic Logic ◽  
Quantification Theory ◽  
New Approach ◽  
Sentential Logic

A system of implicit quantification

1968 ◽  
Vol 32 (4) ◽  
pp. 480-504 ◽  
Author(s):  
J. Jay Zeman
Keyword(s):  
Subject Matter ◽  
Traditional Method ◽  
Natural Deduction ◽  
Propositional Calculus ◽  
Axiom System ◽  
Symbolic Logic ◽  
Quantification Theory ◽  
The Subject

The “traditional” method of presenting the subject-matter of symbolic logic involves setting down, first of all, a basis for a propositional calculus—which basis might be a system of natural deduction, an axiom system, or a rule concerning tautologous formulas. The next step, ordinarily, consists of the introduction of quantifiers into the symbol-set of the system, and the stating of axioms or rules for quantification. In this paper I shall propose a system somewhat different from the ordinary; this system has rules for quantification and is, indeed, equivalent to classical quantification theory. It departs from the usual, however, in that it has no primitive quantifiers.

H. Hiż. Inferential equivalence and natural deduction. The journal of symbolic logic, vol. 22 (1957), pp. 237–240.

1970 ◽  
Vol 35 (2) ◽  
pp. 325-325
Author(s):  
Henry W. Johnstone
Keyword(s):  
Natural Deduction ◽  
Symbolic Logic

Analytic natural deduction

1965 ◽  
Vol 30 (2) ◽  
pp. 123-139 ◽  
Author(s):  
Raymond M. Smullyan
Keyword(s):  
Natural Deduction ◽  
Completeness Theorem ◽  
Infinite Graphs ◽  
Quantification Theory ◽  
Partial Linearization ◽  
König’S Lemma

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.

Irving M. Copi. Another variant of natural deduction. The journal of symbolic logic, vol. 21 (1956), pp. 52–55.

1957 ◽  
Vol 22 (3) ◽  
pp. 298-299
Author(s):  
Paul Bernays
Keyword(s):  
Natural Deduction ◽  
Symbolic Logic

On natural deduction

1950 ◽  
Vol 15 (2) ◽  
pp. 93-102 ◽  
Author(s):  
W. V. Quine
Keyword(s):  
Natural Deduction ◽  
The Other ◽  
Quantification Theory ◽  
Other Hand ◽  
Derived Rules

For Gentzen's natural deduction, a formalized method of deduction in quantification theory dating from 1934, these important advantages may be claimed: it corresponds more closely than other methods of formalized quantification theory to habitual unformalized modes of reasoning, and it consequently tends to minimize the false moves involved in seeking to construct proofs. The object of this paper is to present and justify a simplification of Gentzen's method, to the end of enhancing the advantages just claimed. No acquaintance with Gentzen's work will be presupposed.A further advantage of Gentzen's method, also somewhat enhanced in my revision of the method, is relative brevity of proofs. In the more usual systematizations of quantification theory, theorems are derived from axiom schemata by proofs which, if rendered in full, would quickly run to unwieldy lengths. Consequently an abbreviative expedient is usually adopted which consists in preserving and numbering theorems for reference in proofs of subsequent theorems. Further brevity is commonly gained by establishing metatheorems, or derived rules, for reference in proving subsequent theorems. In natural deduction, on the other hand, proofs tend to be so short that the abbreviative expedients just now mentioned may conveniently be dispensed with—at least until theorems of extraordinary complexity are embarked upon. In natural deduction accordingly it is customary to start each argument from scratch, without benefit of accumulated theorems or derived rules.

Sign in / Sign up

Export Citation Format

Share Document