Abstract
A working definition of the distinction intended in the title is this. Proof theory is principally interested in what is traditionally called the essence or, equivalently, ‘defining property’ of proofs, namely their being valid arguments. This property of validity, which — like most notions and questions of traditional philosophy — occurs to us at a very early stage of experience, is regarded as basic in proof theory. And general proof theory develops such refinements as the distinction between different kinds of validity, for example, logical or constructive validity (and others familiar from the foundational literature). In contrast, the theory of proofs questions the utility of these distinctions compared to taking for granted the validity at least of currently used principles. Instead, this theory studies such structural features as the length of proofs, and especially relations between proofs and other things, so to speak, the ‘role’ of proofs. With this different emphasis, the classifications needed in the theory of proofs are often demonstrably in conflict with the basic distinctions of proof theory, and not, as has sometimes been thought, refinements of the latter.
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
S. Feferman, ‘Ordinals and functionals in proof theory’, in vol. 1, pp. 229-233 of Actes du Congrès Int. Math . 1970, Gauthier-Villars, Paris, 1971. Reviewed in JSL 40 (1975), 625–626.
H. Friedman, ‘Programs and results in logic I’, Notices A.M.S. 22 (1975), 476.
H. Friedman, ‘Systems of second order arithmetic with restricted induction’ (abstracts), JSL 41 (1976), 557–559.
K. Gödel, ‘Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes’, Dialectica 12 (1958), 280–287.
R. L. Goodstein, Recursive Analysis, North-Holland, Amsterdam, 1961.
R. B. Jensen, ‘The fine structure of L’, Ann. Math. Logic 4 (1972), 229–308.
G. M. Kelley and S. MacLane, ‘Coherence in closed categories’, J. Pure Appl. Algebra 1 (1971), 97–140.
G. Kreisel, ‘On the interpretation of non-finitist proofs’, JSL 16 (1951), 241–267.
G. Kreisel, ‘A survey of proof theory’,JSL 33 (1968), 321–388. 8
G. Kreisel, ‘A survey of proof theory IF’, in Proc. Second Scand. Logic Symp., ed.
J. E. Fenstad, North-Holland, Amsterdam, 1971.
G. Kreisel, ‘What have we learnt from Hilbert’s second problem?’, Proc. Symp. Pure Math.28 (1976), 93–130. (A)
G. Kreisel, ‘Der unheilvolle Einbruch der Logik in the Mathematik’, Acta Phil. Fennica 28 (1976), 166–187.9 (B)
G. Kreisel, ‘L. E. J. Brouwer, Collected Works’ (review), Bull. A.M.S. 83 (1977), 86–93. (A)
G. Kreisel, ‘On the kind of data needed for a theory of proofs’, in R. O. Gandy and J. E. M. Hyland (eds.), Logic Colloquium ’76, North-Holland, Amsterdam, 1977. (B)
G. Kreisel, ‘Wie die Beweistheorie zu ihren Ordinalzahlen kam und kommt’, Jber. d. Dt. Math.-Verein. 78 (1977), 177–223. (C)
G. Kreisel, ‘The motto of “Investigations” and the philosophy of proofs and rules’ (to appear: A).
G. Kreisel and J.-L. Krivine, Elements of Model Theory, 2nd. ed. North-Holland, Amsterdam, 1971.
G. Kreisel, G. E. Mints and S. G. Simpson, ‘The use of abstract language in elementary metamathematics: some pedagogic examples’, Springer Lecture Notes 453 (1975), 38–131.
G. Kreisel and W. W. Tait, ‘Finite definability of number theoretic functions and parametric completeness of equation calculi’, Z. Math. Logik Grundlagen Math. 1 (1961), 28–38.
G. Kreisel and G. Takeuti, ‘Formally self-referential propositions for cut-free analysis and related systems’, Diss. Math. 118 (1974).
E. G. K. Lopez-Escobar, ‘On an extremely restricted ω-rule’, Fund. Math. 90 (1976), 159–172.
P. Lorenzen, Differential und Integral; Eine konstruktive Einfuhrung in die klassische Analysis, Akad. Verlagsges., Frankfurt, 1965.
G. E. Mints, ‘A theorem on cut elimination for relevant logic’, Zap. Nauc~h. Sent. LOM1 32 (1972), 90–97. This appears in translation in J. Soviet Math. 6 (1976), 422–428.
G. E. Mints, ‘Finite investigation of infinite derivations’, ibid. 49 (1975), 67–122.
G. E. Mints, ‘Universality of canonical trees’, Dokl. Akad. Nauk SSSR 227 (1976), 808–812.
G. E. Mints, ‘Closed categories and the theory of proofs’, Zap. Nauc~n. Sem. LOMI 68 (1977), 83–114.
W. C. Powell, ‘Extending Godel’s negative interpretation to ZF’, JSL 40 (1975), 221–229
D. Prawitz, ‘Ideas and results in proof theory’, in Proc. Second Scand. Logic Symp., ed. J. E. Fenstad, North-Holland, Amsterdam, 1971.
D. Prawitz, ‘Towards a foundation of general proof theory’, in Logic, Methodology and Philosophy of Science IV, North-Holland, Amsterdam, 1973.
R. Statman, Structural complexity of proofs, Ph.D.Thesis, Stanford University, Stanford, 1974.
R. Statman, ‘Herbrand’s theorem and Gentzen’s notion of direct proof’ in J. Barwise (ed.), Handbook of Mathematical Logic, North-Holland, Amsterdam, 1977.
W. W. Tait, ‘The substitution method’, JSL 30 (1965), 175–192.
G. Takeuti, ‘Two applications of logic to mathematics’ (to appear, A).
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1979 D. Reidel Publishing Company, Dordrecht, Holland
About this chapter
Cite this chapter
Kreisel, G. (1979). Some Facts from the Theory of Proofs and Some Fictions from General Proof Theory. In: Hintikka, J., Niiniluoto, I., Saarinen, E. (eds) Essays on Mathematical and Philosophical Logic. Synthese Library, vol 122. Springer, Dordrecht. https://doi.org/10.1007/978-94-009-9825-4_1
Download citation
DOI: https://doi.org/10.1007/978-94-009-9825-4_1
Publisher Name: Springer, Dordrecht
Print ISBN: 978-94-009-9827-8
Online ISBN: 978-94-009-9825-4
eBook Packages: Springer Book Archive