Fregean Description Theory in Proof-Theoretical Setting

Andrzej Indrzejczak



We present a proof-theoretical analysis of the theory of definite descriptions which emerges from Frege’s approach and was formally developed by Kalish and Montague. This theory of definite descriptions is based on the assumption that all descriptions are treated as genuine terms. In particular, a special object is chosen as a designatum for all descriptions which fail to designate a unique object. Kalish and Montague provided a semantical treatment of such theory as well as complete axiomatic and natural deduction formalization. In the paper we provide a sequent calculus formalization of this logic and prove cut elimination theorem in the constructive manner.


sequent calculus; cut elimination; definite descriptions; Frege

Full Text:



Bencivenga, E., “Free logics”, pages 373–426 in: D. Gabbay, F. Guenthner (eds.), Handbook of Philosophical Logic, vol. III, Reidel Publishing Company, Dordrecht 1986. DOI:

Bencivenga, E., K. Lambert and B.C. van Fraasen, Logic, Bivalence and Denotation, Ridgeview, Atascadero 1991.

Bernays, P., Axiomatic Set Theory, North Holland, Amsterdam 1958.

Carnap, R., Meaning and Necessity, Chicago 1947.

Ciabattoni, A., G. Metcalfe and F. Montagna, “Algebraic and prooftheoretic characterizations of truth stressers for MTL and its extensions”, Fuzzy Sets and Systems 161, 3 (2010): 369–389. DOI:

Curry, H.B., Foundations of Mathematical Logic, McGraw-Hill, New York 1963.

Fitting, M., and R.L. Mendelsohn, First-Order Modal Logic, Kluwer, Dordrecht 1998. DOI:

Frege, G., “Über Sinn und Bedeutung”, Zeitschrift für Philosophie und Philosophische Kritik 100 (1892): 25–50.

Frege, G., Grundgesetze der Arithmetic I, Hermann Pohl, Jena 1893.

Garson, J.W., Modal Logic for Philosophers, Cambridge University Press, Cambridge 2006. DOI:

Hailperin, T., “Remarks on identity and description in first-order axiom systems”, Journal of Symbolic Logic 19 (1954): 14–20. DOI:

Indrzejczak, A., “Eliminability of cut in hypersequent calculi for some modal logics of linear frames”, Information Processing Letters 115, 2 (2015): 75–81. DOI:

Indrzejczak, A., “Simple cut elimination proof for hybrid logic”, Logic and Logical Philosophy 25, 2 (2016): 129–141. DOI:

Indrzejczak, A., ‘Rule-maker theorem and its applications’, submitted.

Kalish, D., and R. Montague, “Remarks on descriptions and natural deduction”, Archiv. für Mathematische Logik und Grundlagen Forschung 3 (1957): 50–64, 65–73

Kalish, D., and R. Montague, Logic. Techniques of Formal Reasoning, Harcourt, Brace & World, Inc., New York 1964.

Kurokawa, H., “Hypersequent calculi for modal logics extending S4”, pages 51–68 in New Frontiers in Artificial Intelligence (2013), Springer, 2014. DOI:

Metcalfe, G., N. Olivetti and D. Gabbay, Proof Theory for Fuzzy Logics, Springer, 2008.

Negri, S., and J. von Plato, Structural Proof Theory, CambridgeUniversity Press, Cambridge 2001. DOI:

Quine, W.V.O., Mathematical Logic, W. W. Norton and Company, New York 1940.

Rosser, J.B., Logic for Mathematicians, McGraw-Hill Book Company, Inc., New York 1953.

Russell, B., “On denoting”, Mind 14 (1905), 479–493.

Print ISSN: 1425-3305
Online ISSN: 2300-9802

Partnerzy platformy czasopism