Definite Descriptions in Intuitionist Positive Free Logic

Nils Kürbis



This paper presents rules of inference for a binary quantifier I for the formalisation of sentences containing definite descriptions within intuitionist positive free logic. I binds one variable and forms a formula from two formulas. Ix[F,G] means ‘The F is G’. The system is shown to have desirable proof-theoretic properties: it is proved that deductions in it can be brought into normal form. The discussion is rounded up by comparisons between the approach to the formalisation of definite descriptions recommended here and the more usual approach that uses a term-forming operator ι, where ιxF means ‘the F’. 


free logic; definite descriptions; proof theory; normalisation; intuitionist logic; binary quantifiers; term forming operators

Full Text:



Bencivenga, E., 1986, “Free logics”, pages 373–426 in D. Gabbay and F. Guenther (eds.), Handbook of Philosophical Logic. Volume III: Alternatives to Classical Logic, Dortrecht: Springer. DOI:

Bostock, D., 1997, Intermediate Logic, Oxford: Clarendon Press.

Czermak, J., 1974, “A logical calculus with definite descriptions”, Journal of Philosophical Logic 3 (3): 211–228. DOI:

Dummett, M., 1978, “The justification of deduction”, pages 290–318 in Truth and Other Enigmas, London: Duckworth.

Dummett, M., 1981, Frege. Philosophy of Language, 2 ed., London: Duckworth.

Dummett, M., 1993, The Logical Basis of Metaphysics, Cambridge, Mass.: Harvard University Press.

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

Francez, N., and R. Dyckhoff, 2012, “A note on harmony”, Journal of Philosophical Logic 41 (3): 613–628. DOI:

Garson, J.W., 2013, Modal Logic for Philosophers, 2 ed., Cambridge University Press. DOI:

Gratzl, N., 2015, “Incomplete symbols – definite descriptions revisited”, Journal of Philosophical Logic 44 (5): 489–506. DOI:

Indrzejczak, A., 2018, “Cut-free modal theory of definite descriptions”, pages 359–378 in G.M.G. Bezhanishvili, G. D’Agostino and T. Studer (eds.), Advances in Modal Logic, vol. 12, London: College Publications.

Indrzejczak, A., 2019, “Fregean description theory in proof-theoretical setting”, Logic and Logical Philosophy 28 (1): 137–155. DOI:

Indrzejczak, A., 2020a, “Existence, definedness and definite descriptions in hybrid modal logic”, pages 349–368 in N. Olivetti, R. Verbrugge, S. Negri and G. Sandu (eds.), Advances in Modal Logic 13, Rickmansworth: College Publications.

Indrzejczak, A., 2020b, “Free definite description theory - sequent calculi and cut elimination”, Logic and Logical Philosophy, 29 (4): 505–539. DOI:

Indrzejczak, A., 2020c, “Free logics are cut free”, forthcoming in Studia Logica. DOI:

Kürbis, N., 2007, “Harmony, normality and stability”.

Kürbis, N., 2015, “Proof-theoretic semantics, a problem with negation and prospects for modality”, The Journal of Philosophical Logic 44: 713–727. DOI:

Kürbis, N., 2019a, “A binary quantifier for definite descriptions in intuitionist negative free logic: Natural deduction and normalisation”, Bulletin of the Section of Logic 48 (2): 81–97. DOI:

Kürbis, N., 2019b, Proof and Falsity. A Logical Investigation, Cambridge University Press. DOI:

Kürbis, N., 2019c, “Two treatments of definite descriptions in intuitionist negative free logic”, Bulletin of the Section of Logic 48 (4): 299–318. DOI:

Lambert, K., 2001, “Free logic and definite descriptions”, in E. Morscher and A. Hieke (eds.), New Essays in Free Logic in Honour of Karel Lambert, Dordrecht: Kluwer. DOI:

Lambert, K., and E. Bencivenga, 1986, “A free logic with simple and complex predicates”, Notre Dame Journal of Formal Logic 27 (2): 247–256. DOI:

Prawitz, D., 1965, Natural Deduction, Stockholm, Göteborg, Uppsala: Almqvist and Wiksell.

Prawitz, D., 1979, “Proofs and the meaning and completeness of the logical constants”, pages 25–40 in J. Hintikka et al. (ed.), Essays on Mathematical and Philosophical Logic, Dordrecht: Reidel. DOI:

Prawitz, D., 1987, “Dummett on a theory of meaning and its impact on logic”, pages 117–165 in B. Taylor (ed.), Michael Dummett: Contributions to Philosophy, Dordrecht: Nijhoff.

Prawitz, D., 2006, “Meaning approached via proofs”, Synthese 148: 507–524. DOI:

Read, S., 2010, “General-elimination harmony and the meaning of the logical constants”, Journal of Philosophical Logic 39: 557–576. DOI:

Schroeder-Heister, P., 1984, “A natural extension of natural deduction”, Journal of Symbolic Logic 49: 1284–1300. DOI:

Tennant, N., 1978, Natural Logic, Edinburgh: Edinburgh University Press.

Tennant, N., 2004, “A general theory of abstraction operators”, The Philosophical Quarterly 54 (214): 105–133. DOI:

Troestra, A., and H. Schwichtenberg, 2000, Basic Proof Theory, 2 ed., Cambridge University Press. DOI:

van Fraassen, B.C., and K. Lambert, 1967, “On free description theory”, Zeitschrift für mathematische Logik und Grundlagen der Mathematik 13: 225–240.

Whitehead, A.N., and B. Russell, 1997, Principia Mathematica to ∗56, Cambridge University Press.

ISSN: 1425-3305 (print version)

ISSN: 2300-9802 (electronic version)

Partnerzy platformy czasopism