Abstract
As has often been claimed, the introduction (I) and elimination (E) rules of intuitionistic natural deduction systems stand in a certain harmony with each other. This can be understood in such a way that once the I rules are given the E rules are uniquely determined and vice versa. The following is an attempt to elaborate this claim. More precisely, we define two notions of validity, one based on I rules (valid+) and one based on E rules (valid−), and show: the E rules generate a maximal valid+ extension of the I rules, and the I rules generate a maximal valid− extension of the E rules. That is to say, the calculus consisting of I and E rules (i.e., intuitionistic logic) is sound and complete with respect to both validity+ and validity−. This does not mean that the syntactical form of E rules is determined by the I rules and vice versa, but that the deductive power which E rules bring about in addition to I rules is exactly what can be justified from I rules and vice versa. Concerning the approach based on I rules this was already claimed by Gentzen who considered I rules to give meanings to the logical signs and the E rules to be consequences thereof (Gentzen, 1935, p. 189).
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Došen, K. and Schroeder-Heister, P., 1984, Conservativeness and Uniqueness. Submitted for publication.
Gentzen, G., 1935, Untersuchungen über das logische Schließen, Math. Zeitschr., 39:176–210 and 405–431.
Lorenzen, P., 1955, “Einführung in die operative Logik und Mathematik,” Springer, Berlin. (2nd edition 969).
Prawitz, D., 1965, “Natural Deduction. A Proof-Theoretical Study,” Almqvist & Wiksell, Stockholm.
Prawitz, D., 1971, Ideas and Results in Proof Theory, in: “Proceedings of the 2nd Scandinavian Logic Symposium,” J. E. Fenstad, ed., North-Holland, Amsterdam.
Prawitz, D., 1973, Towards a Foundation of a General Proof Theory, in: “Logic, Methodology and Philosophy of Science, IV,” P. Suppes. L. Henkin, A, Joja and Gr. C. Moisil, eds., North-Holland, Amsterdam.
Prawitz, D., 1974, On the Idea of a General Proof Theory, Synthese, 27:63–77.
Prawitz, D., 1984, Remarks on some Approaches to the Concept of Logical Consequence (forthcoming).
Schroeder-Heister, P., 1981, “Untersuchungen zur regellogischen Deutung von Aussagenverknüpfungen,” Ph. Diss., Bonn.
Schroeder-Heister, P., 1983a, The Completeness of Intuitionistic Logic with Respect to a Validity Concept Based on an Inversion Principle, J. Philos. Log., 12:359–377.
Schroeder-Heister, P., 1983b, Inversion Principles and the Completeness of Intuitionistic Natural Deduction Systems, in: “Abstracts of the 7th International Congress of Logic, Methodology and Philosophy of Science, Salzburg 1983, Vol. 5.” Salzburg.
Schroeder-Heister, P., 1984a, A Natural Extension of Natural Deduction, J. Symb. Log. (to appear).
Schroeder-Heister, P., 1984b, Generalized Rules for Quantifiers and the Completeness of the Intuitionistic Operators &, v, ⊃, ³, ∀, ∃, in; “Logic Colloquium’ 83,” M. M. Richter, ed., Springer, Berlin (to appear).
Tennant, N., 1978, “Natural Logic,” Edinburgh University Press.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1985 Springer Science+Business Media New York
About this chapter
Cite this chapter
Schroeder-Heister, P. (1985). Proof-theoretic Validity and the Completeness of Intuitionistic Logic. In: Dorn, G., Weingartner, P. (eds) Foundations of Logic and Linguistics. Springer, Boston, MA. https://doi.org/10.1007/978-1-4899-0548-2_4
Download citation
DOI: https://doi.org/10.1007/978-1-4899-0548-2_4
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4899-0550-5
Online ISBN: 978-1-4899-0548-2
eBook Packages: Springer Book Archive