Hostname: page-component-586b7cd67f-t7czq Total loading time: 0 Render date: 2024-11-26T12:10:24.662Z Has data issue: false hasContentIssue false
  • English
  • Français

A natural extension of natural deduction

Published online by Cambridge University Press:  12 March 2014

Peter Schroeder-Heister
Peter Schroeder-Heister*
Affiliation:
Fachgruppe Philosophie, Universität Konstanz, Postfach 5560, 7750 Konstanz, Federal Republic of Germany
Get access Rights & Permissions [Opens in a new window]

Extract

One of the main ideas of calculi of natural deduction, as introduced by Jaśkowski and Gentzen, is that assumptions may be discharged in the course of a derivation. As regards sentential logic, this conception will be extended in so far as not only formulas but also rules may serve as assumptions which can be discharged. The resulting calculi and derivations with rules of any finite level are informally introduced in §1, while §§2 and 3 state formal definitions of the concepts involved and basic lemmata. Within this framework, a standard form for introduction and elimination rules for arbitrary n-ary sentential operators is motivated in §4, understood as a contribution to the theory of meaning for logical signs. §5 proves that the set {&, ∨, ⊃, ⋏} of standard intuitionistic connectives is complete, i.e. &, ∨, ⊃, and ⋏ suffice to express each n-ary sentential operator having rules of the standard form given in §4. §6 makes some remarks on related approaches. For an extension of the conception presented here to quantifier logic, see [11].

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 49 , Issue 4 , December 1984 , pp. 1284 - 1300
Copyright
Copyright © Association for Symbolic Logic 1984

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1]Belnap, N. D., Tonk, plonk and plink, Analysis, vol. 22 (1961–1962), pp. 130–134.CrossRefGoogle Scholar
[2]Došen, K., Logical constants. An essay in proof theory, D. Phil. Thesis, Oxford, 1980.Google Scholar
[3]Hendry, H. E., Does IPC have a binary indigenous Sheffer function?, Notre Dame Journal of Formal Logic, vol. 22 (1981), pp. 183–186.CrossRefGoogle Scholar
[4]Kreisel, G., Constructivist approaches to logic, Modern logic—a survey (Agazzi, E., editor), Reidel, Dordrecht, 1981, pp. 67–91.CrossRefGoogle Scholar
[5]Kutschera, F. v., Die Vollständigkeit des Operatorensystems. {¬,∧,∨, ⊃ für die intuitionistische Aussagenlogik im Rahmen der Gentzensemantik, Archiv für Mathematische Logik und Grundlagenforschung, vol. 11 (1968), pp. 3–16.CrossRefGoogle Scholar
[6]McCullough, D. P., Logical connectives for intuitionistic propositional logic, this Journal, vol. 36 (1971), pp. 15–20.Google Scholar
[7]Prawitz, D., Natural deduction. A proof-theoretical study, Almqvist & Wiksell, Stockholm, 1965.Google Scholar
[8]Prawitz, D., Proofs and the meaning and completeness of the logical constants, Essays on mathematical and philosophical logic (Hintikka, J.et al., editors), Reidel, Dordrecht, 1979, pp. 25–40; slightly revised German translation in Conceptus, vol. 16 (1982), no. 38, pp. 31–44.CrossRefGoogle Scholar
[9]Schroeder-Heister, P., Untersuchungen zur regellogischen Deutung von Aussagenverknüpfungen, Dissertation, Bonn, 1981.Google Scholar
[10]Schroeder-Heister, P., Logische Konstanten und Regeln. Zur Deutung von Aussagenoperatoren, Conceptus, vol. 16 (1982), no. 38, pp. 45–59.Google Scholar
[11]Schroeder-Heister, P., Generalized rules for quantifiers and the completeness of the intuitionistic operators &, ∨,⊃,⋏,∀,∃Logic Colloquium '83 (Richter, M. M.et al., editors), Lecture Notes in Mathematics, Springer-Verlag, Berlin (to appear).Google Scholar
[12]Tennant, N., Natural logic, Edinburgh University Press, Edinburgh, 1978.Google Scholar
[13]Zucker, J. I. and Tragesser, R. S., The adequacy problem for inferential logic, Journal of Philosophical Logic, vol. 7 (1978), pp. 501–516.Google Scholar