Abstract
In this paper, we develop a proof-theoretic framework for the treatment of arbitrary quantifiers binding m variables in n formulas. In particular, we motivate a schema for introduction and elimination rules for such quantifiers based on a concept of ‘derivation’ that allows rules as assumptions which may be discharged. With respect to this schema, the system of the standard operators of intuitionistic quantifier logic turns out to be complete.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
M. Beeson, Recursive Models for Constructive Set Theories, Annals of Mathematical Logic 23 (1982), 127–178.
B. R. Boričić, Prilog teoriji intermedijalnih iskaznih logika, Dissertation, Beograd 1983.
L. Borkowski, On Proper Quantifiers I, Studia Logica 8 (1958), 65–129.
K. Došen, Logical Constants. An Essay in Proof Theory, Dissertation, Oxford 1980.
K. Došen, Sequent-Systems for Modal Logic (forthcoming).
M. Dummett, Elements of Intuitionism, Oxford 1977.
G. Gentzen, Untersuchungen über das logische Schließen, Mathematische Zeitschrift 39 (1935), 176–210, 405–431.
D. Kalish and R. Montague, Logic. Techniques of Formal Reasoning, New York 1964.
F. v. Kutschera, Ein verallgemeinerter Widerlegungsbegriff für Gentzenkalküle, Archiv für mathematische Logik und Grundlagenforschung 12 (1969), 104–118.
P. Lorenzen, Einfürung in die operative Logik und Mathematik, Berlin 1955, 2nd edition 1969.
P. Martin-Löf, Constructive Mathematics and Computer Programming. In: L. J. Cohen, J. Los, H. Pfeiffer and K. P. Podewski (eds.), Logic, Methodology and Philosophy of Science VI, Amsterdam 1982, 153–175.
D. Prawitz, Angående konstruktiv logik och implikationsbegreppet. In: Sju filosofiska studier tillägnade Anders Wedberg, Stockholm 1963, 9–32.
D. Prawitz, Natural Deduction. A Proof-Theoretical Study, Stockholm 1965.
D. Prawitz, Towards a Foundation of a General Proof Theory, In: P. Suppes, L. Henkin, A. Joja, G. C. Moisil (eds.), Logic, Methodology and Philosophy of Science IV, Amsterdam 1973, 225–250.
D. Prawitz, Remarks on Some Approaches to the Concept of Logical Consequence (forthcoming).
H. A. Schmidt, Mathematische Gesetze der Logik I. Vorlesungen über Aussagenlogik, Berlin 1960.
P. Schroeder-Heister, Untersuchungen zur regellogischen Deutung von Aussagenverknüpfungen, Dissertation, Bonn 1981.
P. Schroeder-Heister, A Natural Extension of Natural Deduction (to appear in The Journal of Symbolic Logic).
D. J. Shoesmith and T. J. Smiley, Multiple-Conclusion Logic, Cambridge 1978.
J. I. Zucker and R. S. Tragesser, The Adequacy Problem for Inferential Logic, Journal of Philosophical Logic 7 (1978), 501–516.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1984 Springer-Verlag
About this paper
Cite this paper
Schroeder-Heister, P. (1984). Generalized rules for quantifiers and the completeness of the intuitionistic operators &, ν, ⊃, λ, ∀, ε. In: Börger, E., Oberschelp, W., Richter, M.M., Schinzel, B., Thomas, W. (eds) Computation and Proof Theory. Lecture Notes in Mathematics, vol 1104. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0099494
Download citation
DOI: https://doi.org/10.1007/BFb0099494
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-13901-0
Online ISBN: 978-3-540-39119-7
eBook Packages: Springer Book Archive