EXTENDD

banner

PROJECT OVERVIEW

ExtenDD brings together two areas of intensive research that - surprisingly - so far have rarely come together: complex terms and proof theory. By complex terms we understand expressions that purport to denote objects like proper names, but that, unlike proper names, exhibit structure that contributes to their meaning. The most important examples of such expressions are definite descriptions. Proof theory is the mathematical study of proofs themselves. ExtenDD applies the tools of proof theory to proofs that appeal to propositions containing complex terms. A definite description is an expression of the form ‘the F’: the author of ‘On Denoting’, the author of Principia Mathematica, the present King of France. A definite descriptions aims to denote an object by virtue of a property that only it has: ‘the F’ aims to denote the sole F. The first example denotes Russell, as he was the sole author of ‘On Denoting’. Sometimes a definite description fails, because nothing or more than one thing has the property F, as in the second and third example: Principia Mathematica had two authors, Whitehead and Russell, and France is presently a republic. If a unique object has the property F, the definite description ‘the F’ is called proper; otherwise it is improper. Pride of place for the first formalisation of a theory of definite descriptions as part of a mathematical investigation belongs to Frege’s Grundgesetze der Arithmetik. But it was Russell who brought definite descriptions to prominence. Since his article ‘On Denoting’, in which Russell put forward his celebrated theory of definite descriptions, these expressions occupy a central place in philosophical research and many deep and detailed studies have been carried out in philosophical logic, epistemology, metaphysics and philosophy of language. Russell was prompted by reflections on improper definite descriptions: what do sentences like ‘The present King of France is bald’ mean? ‘The present King of France’ denotes no one, so the truth or falsity of ‘The present King of France is bald’ is not determined by whether the present King of France is bald or not. As there is no present King of France, ‘The present King of France is bald’ should not be true, as otherwise we are stating that a certain person has a certain property.

Russell accepted the principle of bivalence that every sentence is either true or false, hence the ‘The present King of France is bald’ should be false. But then it would appear that ‘The present King of France is not bald’ should be true and the same problem arises once more: if so, we are stating that a certain person fails to have a certain property. Russell concluded that sentences of the form ‘The F is G’ do not have the subject-predicate form they appear to have. According to Russell no meaning is assigned to the expression ‘the F’ standing alone, but only in the context of complete sentences in which it occurs. ‘The F is G’ means ‘There is exactly one F and it is G’. Thus the complex term ‘The F ’ disappears upon logical analysis. There are then two negations of ‘The F is G’: the external negation ‘It is not the case that the F is G’, meaning ‘It is not the case that there is exactly one F and it is G’, and the internal negation ‘The F is not G’, meaning ‘There is exactly one F and it is not G’. The former is true, the latter false. Russell’s problem is solved.

Russell’s theory of definite descriptions had enormous influence on the development of analytic philosophy in the twentieth century, as it was applied, by Russell himself and those influenced by him, to epistemology, metaphysics and philosophy of language. Scores of text books still use Russell’s theory as their official theory of definite descriptions. Despite its brilliance, Russell’s account has drawbacks. It appears to assign wrong truth values to sentences. Diogenes Laertius reports that Thales, having discovered his theorem, offered a sacrifice of oxen to the god at Delphi. According to Russell’s theory, what Diogenes reports is false, as it contains an improper definite description. That sounds wrong, if Thales did indeed offer a sacrifice at Delphi. Some philosophers, like Strawson, argued that ‘The present King of France is bald’ should be neither true nor false, as, due to the improper definite description, it is somehow defective. The second half of the 20th century saw the development of new approaches to definite descriptions. In Frege’s and Russell’s classical logic, it is assumed that every singular term denotes an object. In free logic, originating in the work of Hintikka and Lambert, this assumption is given up. Negative free logic takes a Russellian line according to which atomic formulas containing non-denoting terms are false. Neutral free logics pick up Strawson’s view that they are neither true nor false. Positive free logic permits them to be true. There is now a plethora of theories of definite descriptions, but very rarely have they been investigated from a proof theoretic perspective.

Proof Theory was founded by Hilbert at the beginning of the 20th century as the mathematical study of proofs. Initially it focused on axiomatisations of mathematical theories and proving their consistency. It was soon extended to the study of proofs outside mathematics, in particular to formal logic, which in turn was applied to the analysis of ordinary language and arguments in general. Gödel’s limitative results showed that the greatest ambition of Hilbert’s programme, to prove the consistency of arithmetic by finitary means, could not be achieved as envisaged. Gentzen’s groundbreaking work led to a substantial redefinition of the aims and tools of proof theory. It now occupies a centre stage in modern formal logic. His sequent calculus and systems of natural deduction represent the actual proofs carried out by logicians and mathematician much better than Hilbert’s axiomatic systems. These tools permit the deepest study of proofs and their properties. Following Gentzen’s work, a consensus developed over what constitutes a good proof system and the form rules of inference should take. The rules for each logical constant, expressions such as ‘not’, ‘all’ and ‘if-then’, exhibit a similar form, a remarkable systematic, as Gentzen notes. Each constant is governed by two kinds of rules for their use in proofs, and these rules govern only that constant. This form permits a precise study of where and how the logical constants are used, whether this use is essential or may be eschewed, and it is the basis for cut elimination in proofs in sequent calculus and normalisation of proofs in natural deduction. These results relate to a common phenomenon of mathematics: proofs are combined to establish new results, as lemmas are used in proofs of theorems from which corollaries are inferred in turn. Sometimes a theorem or corollary is simpler than the lemmas or theorems from which it is deduced. Gentzen’s Hauptsatz (cut elimination theorem) establishes that there is also a direct proof that proceeds from simple to complex ‘without detours’, as Gentzen says. As it is the latter in terms of which the correctness of proofs is defined, Gentzen’s result establishes that combining proofs in the said way is guaranteed to give a correct proof. In addition to these technical achievements, Gentzen’s ideas led also to the development of the more philosophically oriented proof-theoretic semantics, where the meanings of constants are defined in terms of their rules of inference.

ExtenDD will combine the paradigm of philosophy that is the theory of definite descriptions with the paradigm of proof theory that are Gentzen’s calculi. Despite the long history of research into definite descriptions, the methods developed by Gentzen have rarely been applied in research on definite descriptions. Only a small effort has so far been put into the adequate treatment of definite descriptions in this framework. The same counts for other complex singular terms such as set abstracts and number operators. ExtenDD fills this important gap in research. Applying the methods of proof theory to definite descriptions is profitable to both sides. Competing theories of definite descriptions and complex terms in general, their advantages and shortcomings, are shown in a new light. The behaviour of complex terms needs subtle syntactical analysis and requires enriching the toolkit of proof theory. ExtenDD deals with both challenges: it develops formal theories of definite descriptions and modifies the machinery of proof theory to cover new areas of application. ExtenDD will also formulate new theories of definite descriptions and other terms with an eye on proof-theoretic desiderata. ExtenDD aims to have a significant impact on proof theory, the philosophy of logic and language, linguistic, computer science and automated deduction.

TEAM

Andrzej Indrzejczak is a logician and philosopher working on non-classical logics and proof theory. He received his Ph.D. in 1997 and his habilitation in 2007 from the University of Lodz (Poland). Since 2015 he has been a full professor and the chair of the Department of Logic at the University of Łódź. Moreover, he is the editor-in-chief of the Bulletin of the Section of Logic, and the chairman of the editorial board of Studia Logica. He has published 8 books, including Natural Deduction, Hybrid Systems and Modal Logics (Springer 2010) and Sequents and Trees (Birkhäuser 2021), and numerous articles. Since 2008 he has organised ten editions of the conference Non-Classical Logics: Theory and Applications. Now he is the PI in the ERC project ExtenDD devoted to proof theory of definite descriptions and other complex terms and term-forming operators.

Nils Kürbis received his Ph.D. from King’s College London and his habilitation from the University of Bochum, where he was an Alexander von Humboldt Fellow and is an akademischer Oberrat. At the University of Lodz, besides being senior researcher in ExtenDD, he is an executive editor of the Bulletin of the Section of Logic. He’s also an honorary research fellow at University College London. His research is on proof theory and philosophical issues arising from proof theory, in particular proof theoretic semantics, where his focus was on negation, denial, falsehood and is now on proof theoretic harmony and modal operators, and definite descriptions. He has published a book Proof and Falsity. A Philosophical Investigation (Cambridge University Press 2019), edited Knowledge, Number and Reality. Encounters with the Work of Keith Hossack (Bloomsbury 2022), a Festschrift for his Doktorvater, and numerous articles on logic, philosophy of logic, philosophy of language, metaphysics and philosophical logic in ancient philosophy in leading specialist as well as generalist journals. 

 

Yaroslav Petrukhin

 is a logician working on proof theory: natural deduction and sequent calculi for many-valued, modal, multilattice, and classical logics. He has written his PhD under the supervision of prof. Andrzej Indrzejczak at the University of Łódź and is currently preparing for the viva. He is now an assistant professor at the Centre for the Philosophy of Nature, University of Łódź, a position sponsored by an ExtenDD grant. Now his research is devoted to the topics of the ERC project ExtenDD: proof theory of definite descriptions and other complex terms and term-forming operators.

Przemysław Wałęga

 is a senior researcher in the Department of Computer Science, University of Oxford. He obtained his Ph.D. in logic from the Institute of Philosophy at the University of Warsaw (Poland), and his B.Eng. and M.S. degrees in Mechatronics from Warsaw University of Technology, and the B.A. degree in Philosophy from the Institute of Philosophy, University of Warsaw. His research interests include knowledge representation and reasoning, reasoning about time and space, logics in AI, stream reasoning, and computational complexity. He is mainly working on computational complexity and expressive power of various logics, e.g., temporal logics, interval logics, metric logics, modal logics, description logics, and Datalog.

 

Michał Zawidzki

 is an assistant professor in the Department of Logic at the University of Lodz (Poland). He received his Ph.D. in philosophical logic from the University of Lodz in 2013. Between June 2020 and June 2023 he worked as senior research associate in AI and semantic technologies at the Department of Computer Science at Oxford University. He has been a co-organiser of several editions of the Non-Classical Logics: Theory and Applications conference. His main research interests are in non-classical (mainly modal) logics, deductive systems and automated reasoning, decidability and complexity of logical theories.

 

PUBLICATIONS

  • Indrzejczak, A., Petrukhin, Y. (2023). A Uniform Formalisation of Three-Valued Logics in Bisequent Calculus. In: Pientka, B., Tinelli, C. (eds) Automated Deduction – CADE 29. CADE 2023. Lecture Notes in Computer Science, vol. 14132. Springer, Cham, 325–343. https://doi.org/10.1007/978-3-031-38499-8_19.
  • Indrzejczak, A., Zawidzki, M. Definite descriptions and hybrid tense logic. Synthese 202, 98 (2023). https://doi.org/10.1007/s11229-023-04319-8.
  • Indrzejczak, A., Kürbis, N. (2023). A Cut-Free, Sound and Complete Russellian Theory of Definite Descriptions. In: Ramanayake, R., Urban, J. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2023. Lecture Notes in Computer Science, vol. 14278. Springer, Cham, 112–130. https://doi.org/10.1007/978-3-031-43513-3_7.
  • Indrzejczak, A. (2023). Towards Proof-Theoretic Formulation of the General Theory of Term-Forming Operators. In: Ramanayake, R., Urban, J. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2023. Lecture Notes in Computer Science, vol. 14278. Springer, Cham, 131–149. https://doi.org/10.1007/978-3-031-43513-3_8.
  • Wałęga, P. A., Zawidzki, M. (2023). Hybrid Modal Operators for Definite Descriptions. In: Gaggl, S., Martinez, M.V., Ortiz, M. (eds), Logics in Artificial Intelligence. JELIA 2023. Lecture Notes in Computer Science, vol. 14281. Springer, Cham, 712–726. https://doi.org/10.1007/978-3-031-43619-2_48.
  • Indrzejczak A., Petrukhin Y. (2024). Uniform Cut-Free Bisequent Calculifor Three-Valued Logics. Logic and Logical Philosophy 33 (2024), 463–506. https://doi.org/10.12775/LLP.2024.019.
  • Kürbis, N. (2024). Normalisation for Negative Free Logics without and with Definite Descriptions. The Review of Symbolic Logic (accepted manuscript), 1–32. https://doi.org/10.1017/S1755020324000157.
  • Wałęga P. A. (2024). Expressive Power of Definite Descriptions in Modal Logics. In: Marquis, P., Ortiz, M., Pagnucco, M. (eds), Proceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning — Main Track. IJCAI Organization, 687–696. https://doi.org/10.24963/kr.2024/65.

SEMINAR

We aim to hold a seminar roughly every two weeks on Wednesdays from 16:15 to 18:00 CET during term time. It will be held online on Teams. There will be speakers from amongst the ExtenDD team as well as external speakers.

FORTHCOMING

  • 20th November 2024: Matthieu Fontaine (University of Sevilla), Abstract Artefacts in a Modal Framework
  • 4th December 2024: TBC
  • 18th December 2024: Elaine Pimentel (University College London), From axioms to synthetic inference rules via focusing
  • 8th January 2025: Christoph Benzmüller (University of Bamberg / Free University of Berlin), Utilizing proof assistant systems and the LogiKEy methodology for experiments on free logic in HOL
  • 22nd January 2025: Jiří Raclavský (Masaryk University, Brno), TBA

PAST

  • 6th November 2024:Nils Kürbis, Definite Descriptions in Positive Free Logic and a New Theory of Definite Descriptions based on Proof Theoretic Considerations (abstract)
  • 23rd October 2024: Bartosz Wieckowski (Goethe Universität, Frankfurt am Main), Incomplete descriptions and qualified definiteness (slides)
  • 9th September 2024: Andrzej Indrzejczak, Strict form of stratified set theories NF and NFU in the setting of sequent calculus (slides)
  • 5th June 2024:  Norbert Gratzl (Ludwig-Maximilians-University of Munich), Free Logic, Definite Descriptions, and Extensionality
  • 22nd May 2024:  Eugenio Orlandelli (University of Bologna), Nested sequents for quantified modal logics (slides)
  • 24th April 2024:  Yaroslav Petrukhin, Andrzej Indrzejczak, Bisequent Calculi for Neutral Free Logic with Definite Descriptions (slides)
  • 10th April 2024: Melvin Fitting (City University of New York), First-Order Modal Logic: Predicate Abstracts and Definite Descriptions (slides)
  • 20th March 2024: Andrzej Indrzejczak, When Epsilon Meets Lambda: Extended Leśniewski's Ontology (slides)
  • 28th February 2024: Michał Zawidzki, Definite Descriptions in First-Order Temporal Setting (slides)
  • 24th January 2024: Henrique Antunes (Universidade Federal da Bahia), Free Theories of Definite Descriptions Based on FDE (slides)
  • 10th January 2024: Alessandro Artale (Free University of Bozen-Bolzano), Andrea Mazzullo (University of Trento), Temporal and Modal Free Description Logics with Definite Descriptions (slides)
  • 13th December 2023: Nils Kürbis, Some Thoughts on Formalising Definite Descriptions with Binary Quantifiers in Modal Logic (slides)
  • 29th November 2023: Przemysław Wałęga, Bisimulation for Propositional Modal logic with Definite Descriptions (slides)
  • 15th November 2023: Andrzej Indrzejczak, Russellian Logic of Definite Descriptions and Anselm's God (slides)
  • 25th October 2023:  Andrzej Indrzejczak, Constructive Proof of the Craig Interpolation Theorem for Russellian Logic of Definite Descriptions (slides)
  • 20th June 2023: Przemysław Wałęga, Michał Zawidzki, Andrzej Indrzejczak, Definite Descriptions in Modal and Temporal Logics (slides)
  • 30th May 2023: Nils Kürbis, Normalisation for Negative Free Logics with Definite Descriptions (paper)
  • 2nd May 2023: Andrzej Indrzejczak, Prospects for Classical Theory of Definite Descriptions (slides)
  • 18th April 2023:  Andrzej Indrzejczak, Towards a General Proof Theory of Term-Forming Operators 2 (slides)
  • 4th April 2023: Nils Kürbis, A Survey of Systems Formalising Definite Descriptions by Binary Quantification (slides)
  • 21st March 2023: Andrzej Indrzejczak, Towards a general proof theory of term-forming operators (slides)

The first vacant slot is in Winter Term of the academic year 2024/2025, namely on 4th December.

If you wish to participate, please email Yaroslav Petrukhin (yaroslav.petrukhin@gmail.com) to register your interest. You will then receive a link to the Teams Meeting and regular updates on the seminar series.

If, on the other hand, you would like to give a talk in one of seminar meetings, please contact Andrzej Indrzejczak (andrzej.indrzejczak@filhist.uni.lodz.pl) to discuss the details.

RELATED EVENTS

Below we present a list of all events where the ExtenDD team was presenting topics related to the project.

Funded by the European Union (ERC, ExtenDD, project number: 101054714). Views and opinions expressed are however those of the team members only and do not necessarily reflect those of the European Union or the European Research Council. Neither the European Union nor the granting authority can be held responsible for them.

ERC_EU_logo.jpg

Niezbędne pliki cookie umożliwiają podstawowe funkcje i są niezbędne do prawidłowego działania witryny.

Statystyczne pliki cookie zbierają informacje anonimowo. Informacje te pomagają nam zrozumieć, w jaki sposób nasi goście korzystają z naszej strony internetowej.

Nasza strona internetowa używa plików cookies (tzw. ciasteczka) w celach statystycznych, reklamowych oraz funkcjonalnych. Dzięki nim możemy indywidualnie dostosować stronę do Twoich potrzeb. Każdy może zaakceptować pliki cookies albo ma możliwość wyłączenia ich w przeglądarce, dzięki czemu nie będą zbierane żadne informacje
Przejdź do strony polityka prywatności