91桃色

ExtenDD

Coming to Terms: Proof Theory Extended to Definite Descriptions and other Terms

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 鈥榯he F鈥�: the author of 鈥極n 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: 鈥榯he F鈥� aims to denote the sole F. The first example denotes Russell, as he was the sole author of 鈥極n 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 鈥榯he 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鈥檚 Grundgesetze der Arithmetik. But it was Russell who brought definite descriptions to prominence. Since his article 鈥極n 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 鈥楾he present King of France is bald鈥� mean? 鈥楾he present King of France鈥� denotes no one, so the truth or falsity of 鈥楾he 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, 鈥楾he 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 鈥楾he present King of France is bald鈥� should be false. But then it would appear that 鈥楾he 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 鈥楾he F is G鈥� do not have the subject-predicate form they appear to have. According to Russell no meaning is assigned to the expression 鈥榯he F鈥� standing alone, but only in the context of complete sentences in which it occurs. 鈥楾he F is G鈥� means 鈥楾here is exactly one F and it is G鈥�. Thus the complex term 鈥楾he F 鈥� disappears upon logical analysis. There are then two negations of 鈥楾he F is G鈥�: the external negation 鈥業t is not the case that the F is G鈥�, meaning 鈥業t is not the case that there is exactly one F and it is G鈥�, and the internal negation 鈥楾he F is not G鈥�, meaning 鈥楾here is exactly one F and it is not G鈥�. The former is true, the latter false. Russell鈥檚 problem is solved.

Russell鈥檚 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鈥檚 theory as their official theory of definite descriptions. Despite its brilliance, Russell鈥檚 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鈥檚 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 鈥楾he 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鈥檚 and Russell鈥檚 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鈥檚 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鈥檚 limitative results showed that the greatest ambition of Hilbert鈥檚 programme, to prove the consistency of arithmetic by finitary means, could not be achieved as envisaged. Gentzen鈥檚 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鈥檚 axiomatic systems. These tools permit the deepest study of proofs and their properties. Following Gentzen鈥檚 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 鈥榥ot鈥�, 鈥榓ll鈥� and 鈥榠f-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鈥檚 Hauptsatz (cut elimination theorem) establishes that there is also a direct proof that proceeds from simple to complex 鈥榳ithout detours鈥�, as Gentzen says. As it is the latter in terms of which the correctness of proofs is defined, Gentzen鈥檚 result establishes that combining proofs in the said way is guaranteed to give a correct proof. In addition to these technical achievements, Gentzen鈥檚 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鈥檚 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

1

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 91桃色 (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.

1

Nils K眉rbis received his Ph.D. from King鈥檚 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 91桃色, besides being senior researcher in ExtenDD, he is an executive editor of the Bulletin of the Section of Logic. He鈥檚 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. 

1

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.

1

Micha艂 Socha艅ski received his Ph.D. from Adam Mickiewicz University in Pozna艅 (UAM), he also obtained M.Sc. degrees in philosophy and mathematics from the same university. In years 2019-2022 he was a post-doc in the project 鈥淒istributive Deductive Systems for Classical and Non-classical Logics. Proof theory supported with computational methods鈥� carried out at the Departmant of Logic and Cognitive Science, UAM, where his main duties were programming and data analysis. He also worked as a data analyst / data scientist in the private sector for many years. Micha艂 is now a research associate at the Centre for the Philosophy of Nature, University of 艁贸d藕, holding a position in the "ExtenDD" grant. His main research interests are in automated theorem proving and programming, but he also works on the philosophy of mathematics, diagrammatic reasoning, and application of combinatorics in proof theory.

1

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.

1

Micha艂 Zawidzki is an assistant professor in the Department of Logic at the 91桃色 (Poland). He received his Ph.D. in philosophical logic from the 91桃色 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. .
  • Indrzejczak, A., Zawidzki, M. Definite descriptions and hybrid tense logic. Synthese 202, 98 (2023). .
  • 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. .
  • 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. .
  • 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. .
  • Indrzejczak A., Petrukhin Y. (2024). Uniform Cut-Free Bisequent Calculifor Three-Valued Logics. Logic and Logical Philosophy 33 (2024), 463鈥�506. .
  • K眉rbis, N. (2024). Normalisation for Negative Free Logics without and with Definite Descriptions. The Review of Symbolic Logic 18(1) (2025), 240鈥�272. .
  • 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. .
  • Indrzejczak A., Petrukhin Y., Bisequent Calculi for Neutral Free Logic with Definite Descriptions. In: Benzm眉ller C., Otten J., Ramanayake R., Proceedings of the 5th International Workshop on Automated Reasoning in Quantified Non-Classical Logics, 48鈥�61. .
  • Indrzejczak A., When Epsilon meets Lambda: Extended Le艣niewski's Ontology. In: Benzm眉ller C., Otten J., Ramanayake R., Proceedings of the 5th International Workshop on Automated Reasoning in Quantified Non-Classical Logics, 62鈥�79. .
  • Petrukhin Y. A Binary Quantifier for Definite Descriptions in Nelsonian Free Logic. Electronic Proceedings in Theoretical Computer Science, 2024, vol. 415, pp. 5-15. .
  • Indrzejczak, A., Wa艂臋ga, P. A., Zawidzki, M. (2026). On Temporal References via Definite Descriptions in First-Order Monadic Logic of Order. In: Casini, G., Dundua, B., Kutsia, T. (eds) Logics in Artificial Intelligence. JELIA 2025. Lecture Notes in Computer Science, vol. 16094. Springer, Cham, 244鈥�262. .
  • Petrukhin, Y. (2026). On a Second-Order Version of Russellian Theory of Definite Descriptions. In: Casini, G., Dundua, B., Kutsia, T. (eds) Logics in Artificial Intelligence. JELIA 2025. Lecture Notes in Computer Science, vol. 16094. Springer, Cham, 313鈥�326. .
  • K眉rbis, N. (2026). Definite Descriptions. In: Nesi, H., Milin, P., Fontaine, M. (eds) The Encyclopedia of Language and Linguistics, 3rd Edition, Elsevier, 2026, online first, .
  • K眉rbis, N. (ed.) (2026). Synthese Topical Collection celebrating 120 Years of Russell's `On Denoting', 

Seminar

We aim to hold a seminar roughly every two weeks on Wednesdays from 12:00 to 14: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

  • 4th March 2026: (Anadolu University), TBA
  • 18th March 2026: (University of Oxford), The conjunction of predicates and modifiers in a Meaning-Dependent Grammar
  • 1st April 2026: (University of Waterloo), ARM & SQLP: Introducing a New Foundation for a Path-Aware Query Language to Bridge Relational and Graph Data (abstract)
    The talk will start at 13:00 CET.

PAST

  • 14th January 2026: (University of Waterloo), Referring Expressions in Knowledge Representation and Information Systems (abstract)
  • 7th January 2026: (KU Leuven), The Logical Geometry of Russell's Theory of Definite Descriptions (abstract)
  • 3rd December 2025: ,  (Free University of Bozen-Bolzano), Decidability in First-Order Modal Logic with Non-Rigid Constants and Definite Descriptions (slides)
  • 19th November 2025: (University of Oslo), Semantics and Reasoning for 蔚 Terms (abstract)
  • 5th November 2025: Micha艂 Socha艅ski, Przemys艂aw Wa艂臋ga, Micha艂 Zawidzki, Two types of definite descriptions in description logics (abstract)
  • 22nd October 2025: Yaroslav Petrukhin, A Paradefinite Version of Russellian Theory of Definite Descriptions (slides)
  • 8th October 2025: (Ludwig Maximilians Universit盲t, Munich), Conservative Extensions of Intuitionistic Logic by Epsilon Terms over Predicate Abstraction (slides)
  • 11th June 2025: Yaroslav Petrukhin, From Second-order Quantification to Second-order Definite Descriptions (slides)
  • 28th May 2025:  (Utrecht University), Vulcanology: descriptive names, invariant semantics, and dual predication (abstract)
  • 14th May 2025: Micha艂 Socha艅ski, Micha艂 Zawidzki, Modal Logic with Definite Descriptions, Tableaux, and Python (abstract)
  • 30th April 2025: (Free University Berlin), Free Higher-Order Logic and its Automation via a Semantical Embedding (slides)
  • 9th April 2025:  (Graduate Center, City University of New York), Nothing, everything, and paraconsistent mereology (work in progress)
  • 2nd April 2025: (The Ohio State University), Core systems of logic with single-barreled abstraction operators (slides)
  • 19th March 2025: (Stanford University), Definitions in a Hyperintensional Free QML (slides)
  • 5th March 2025:   (Victoria University of Wellington), Descriptions in Informational Semantics for Relevant Logic (slides)
  • 22nd January 2025:  (Masaryk University, Brno), Deduction with Non-referring Descriptions in Type-theoretic Partial Logic (abstract)
  • 8th January 2025: (University of Bamberg / Free University of Berlin), Utilizing proof assistant systems and the LogiKEy methodology for experiments on free logic in HOL (slides)
  • 18th December 2024:  (University College London), From axioms to synthetic inference rules via focusing (slides)
  • 4th December 2024: (University of Bologna), G3-style Sequent Calculi and Craig Interpolation Property for Logics with Russellian Definite Descriptions (slides)
  • 20th November 2024:  (University of Sevilla), Abstract Artefacts in a Modal Framework
  • 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: (Goethe Universit盲t, Frankfurt am Main), Incomplete descriptions and qualified definiteness (slides)
  • 9th October 2024: Andrzej Indrzejczak, Strict form of stratified set theories NF and NFU in the setting of sequent calculus (slides)
  • 5th June 2024: (Ludwig-Maximilians-University of Munich), Free Logic, Definite Descriptions, and Extensionality
  • 22nd May 2024: (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: (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: (Universidade Federal da Bahia), Free Theories of Definite Descriptions Based on FDE (slides)
  • 10th January 2024:  (Free University of Bozen-Bolzano),  (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 ()
  • 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)

First vacant slot are in Winter Term of the academic year 2025/2026, that is, on 22nd October and 5th November 2025.

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.

  • Nils K眉rbis, Proof Theoretic Semantics for Theories of Definite Descriptions, Symposium on Proof-theoretic Semantics, 9鈥�11 November 2022.
  • Andrzej Indrzejczak, The coming to terms project: Extending proof theory by ?, The second Bochum鈥揕odz Logic Workshop, Bochum and online, Germany, 17鈥�18 November 2022.
  • Nils K眉rbis, Definite descriptions via binary quantification, The second Bochum鈥揕odz Logic Workshop, Bochum and online, Germany, 17鈥�18 November 2022.
  • Yaroslav Petrukhin, Cut-free sequent calculi for some three-valued logics obtained via correspondence analysis, The second Bochum鈥揕odz Logic Workshop, Bochum and online, Germany, 17-18 November 2022.
  • Andrzej Indrzejczak, Proof systems for term-forming operators: theory and application, Research Seminar hosted by Software Systems Engineering group, School of Computer Science and Engineering, University of Westminster, London, UK, 25 January 2023.
  • Andrzej Indrzejczak, Micha艂 Zawidzki, Lambda meets iota: tableaux and interpolation, FM seminar, University of Manchester, Manchester, UK, 6 February 2023.
  • Andrzej Indrzejczak, Definite descriptions via term forming operators, CELL Workshop | Some Theories of Definite Descriptions from a Proof-Theoretic Perspective, London, UK, 8 February 2023.
  • Nils K眉rbis, Definite descriptions via binary quantification, CELL Workshop | Some Theories of Definite Descriptions from a Proof-Theoretic Perspective, London, UK, 8 February 2023.
  • Andrzej Indrzejczak, Teoria dowodu dla operator贸w formuj膮cych termy, Warsztaty Matematyczno-Filozoficzne, 艁贸d藕, Poland, Department of Logic, 13 March 2023.
  • Andrzej Indrzejczak, Towards a General Proof Theory of Term-Forming Operators, 26th Conference Applications of Logic in Philosophy and the Foundations of Mathematics, Szklarska Por臋ba, Poland, 8鈥�12 May 2023.
  • Nils K眉rbis, Some Systems for Formalising Sentences Containing Definite Descriptions by a Binary Quantifier, 26th Conference Applications of Logic in Philosophy and the Foundations of Mathematics, Szklarska Por臋ba, Poland, 8鈥�12 May 2023.
  • Yaroslav Petrukhin, Normalisation for Some FDE-Style Logics, 26th Conference Applications of Logic in Philosophy and the Foundations of Mathematics, Szklarska Por臋ba, Poland, 8鈥�12 May 2023.
  • Nils K眉rbis, Definite Descriptions in Modal Logic: Some Thoughts and a Proposal (inaugural lecture), Bochum, Germany. 14 June 2023.
  • Andrzej Indrzejczak, The prospects for classical logic with definite descriptions, Colloquia. Logic and Epistemology, Bochum, Germany. 15 June 2023.
  • Andrzej Indrzejczak, Proof-theoretic formulation of Quinean set theory NF,  Cracow Logic Conference (CLoCk) 2023, Krak贸w, Poland, 28鈥�30 June 2023.
  • Yaroslav Petrukhin, Normalisation for Segerberg's natural deduction system for Boolean n-ary connectives, Cracow Logic Conference (CLoCk) 2023, Krak贸w, Poland, 28-30 June 2023.
  • Andrzej Indrzejczak, Yaroslav Petrukhin, A Uniform Formalisation of Three-Valued Logics in Bisequent Calculus, Automated Deduction 鈥� CADE 29, 29th International Conference on Automated Deduction. Rome, Italy, 1鈥�4 July 2023.
  • Nils K眉rbis, Some Systems for Formalising Sentences Containing Definite Descriptions by a Binary Quantifier and some Thoughts on Modal Logic, CEFISES Logic & Philosophy seminar, Louvain la Neuve, Belgium, 4 July 2023. .
  • Andrzej Indrzejczak, Prezentacja wynik贸w wypracowanych do tej pory w ramach projektu 鈥滳oming to Terms: Proof Theory Extended to Definite Descriptions and other Terms鈥�, Twelfth Polish Congress of Philosophy, 艁贸d藕, Poland, 11鈥�16 September 2023.
  • Andrzej Indrzejczak , Micha艂 Zawidzki, Predicate Abstracts and Definite Descriptions, Twelfth Polish Congress of Philosophy, 艁贸d藕, Poland, 11鈥�16 September 2023.
  • Andrzej Indrzejczak, Yaroslav Petrukhin, A Uniform Formalisation of Three-Valued Logics in Bisequent Calculus, Twelfth Polish Congress of Philosophy, 艁贸d藕, Poland, 11鈥�16 September 2023.
  • Przemys艂aw Wa艂臋ga, Micha艂 Zawidzki, Definite Descriptions as Modal Operators, Twelfth Polish Congress of Philosophy, 艁贸d藕, Poland, 11鈥�16 September 2023.
  • Nils K眉rbis, A Theory of Definite Descriptions. Part I: Background.Motivation. Proof-Theory, Twelfth Polish Congress of Philosophy, 艁贸d藕, Poland, 11鈥�16 September 2023.
  • Nils K眉rbis, A Theory of Definite Descriptions. Part II: Iota Terms and Binary Quantifiers. Semantics. Some Thoughts on Modal Logic, Twelfth Polish Congress of Philosophy, 艁贸d藕, Poland, 11鈥�16 September 2023.
  • Yaroslav Petrukhin, Normalisation for Segerberg's natural deduction system for Boolean n-ary connectives, Twelfth Polish Congress of Philosophy, 艁贸d藕, Poland, 11-16 September 2023.
  • Andrzej Indrzejczak, Nils K眉rbis, A cut-free, sound and complete Russellian theory of definite descriptions, 32nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2023, Prague, Czech Republic, September 18鈥�21, 2023.
  • Andrzej Indrzejczak, Towards Proof-Theoretic Formulation of the General Theory of Term-Forming Operators, 32nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2023, Prague, Czech Republic, September 18鈥�21, 2023.
  • Przemys艂aw Wa艂臋ga, Micha艂 Zawidzki, Hybrid Modal Operators for Definite Descriptions, 18th Edition of the European Conference on Logics in Artificial Intelligence, JELIA 2023, Dresden, Germany, 20鈥�22 September 2023.
  • Nils K眉rbis, Deductive Semantics, Seminar of the University of Stirling, 28 September 2023.
  • Yaroslav Petrukhin, Definite descriptions in Nelson's logics, Trends in Logic XXIII. Bridges between Logic, Ethics and Social Sciences (BLESS). 70 years of STUDIA LOGICA, Toru艅, Poland, 22鈥�25 November 2023.
  • Andrzej Indrzejczak, Anselm鈥檚 God and theories of definite descriptions, Trends in Logic XXIII. Bridges between Logic, Ethics and Social Sciences (BLESS). 70 years of STUDIA LOGICA, Toru艅, Poland, 22鈥�25 November 2023.
  • Andrzej Indrzejczak, Prezentacja bada艅 Katedry Logiki i projektu ExtenDD, World Logic Day(s) in Poland 2024, 艁贸d藕, Poland, 15 January 2024.
  • Nils K眉rbis, Definite Descriptions. Russell and Beyond, World Logic Day(s) in Poland 2024, 艁贸d藕, Poland, 15 January 2024.
  • Yaroslav Petrukhin, The Recent Advances in Natural Deduction for Many-Valued Logic, World Logic Day(s) in Poland 2024, 艁贸d藕, Poland, 15 January 2024.
  • Andrzej Indrzejczak, Le艣niewski's Ontology Satisfies Interpolation, The Sixth Asian Workshop on Philosophical Logic (AWPL2024), Sapporo, Japan, 4鈥�6 March 2024.
  • Yaroslav Petrukhin, Definite Descriptions in Nelson's Logic (Online), The Sixth Asian Workshop on Philosophical Logic (AWPL2024), Sapporo, Japan, 4鈥�6 March 2024.
  • Andrzej Indrzejczak, Hybrid Logic Extended with Lambda and Iota Operators, Sapporo One-day Workshop on Hybrid Logic and Proof Theory, Sapporo, Japan, 7 March 2024.
  • Nils K眉rbis, A Theory of Definite Descriptions Formalised by Binary Quantification for Modal Logic, Sapporo One-day Workshop on Hybrid Logic and Proof Theory, Sapporo, Japan, 7 March 2024.
  • Andrzej Indrzejczak, Application of Bisequent Calculus to Neutral Free Logic with Definite Descriptions (A joint work with Yaroslav Petrukhin), LLAL@GSIS (II), Sendai, Japan, 9 March 2024.
  • Nils K眉rbis, Some Systems for Formalising Definite Descriptions with a Binary Quantifier in Free Logic, LLAL@GSIS (II), Sendai, Japan, 9 March 2024.
  • Andrzej Indrzejczak, When Epsilon meets Lambda; Extended Le艣niewski's Ontology, A Workshop on Russell, Le艣niewski and beyond, Tokyo, Japan, 13 March 2024.
  • Nils K眉rbis, Definite Descriptions formalised by Binary Quantifiers, A Workshop on Russell, Le艣niewski and beyond, Tokyo, Japan, 13 March 2024.
  • Nils K眉rbis, A Theory of Definite Descriptions Formalised by Binary Quantification for Modal Logic, Seminar at Stirling, 9 April 2024.
  • Andrzej Indrzejczak, Yaroslav Petrukhin, Bisequent Calculi for Neutral Free Logic with Definite Descriptions, 27th Conference Applications of Logic in Philosophy and the Foundations of Mathematics, 锘縎zklarska Por臋ba, 6鈥�10 May 2024.
  • Andrzej Indrzejczak, When Epsilon Meets Lambda: Extended Le艣niewski's Ontology, 27th Conference Applications of Logic in Philosophy and the Foundations of Mathematics, 锘縎zklarska Por臋ba, 6鈥�10 May 2024.
  • Przemys艂aw Wa艂臋ga, Referring to Modal Worlds via Definite Descriptions, 27th Conference Applications of Logic in Philosophy and the Foundations of Mathematics, 锘縎zklarska Por臋ba, 6鈥�10 May 2024.
  • Andrzej Indrzejczak, Russell, Definite Descriptions and Anselm鈥檚 God: Approaches to Concepts, Formal Methods and Science in Philosophy V, Dubrovnik, Croatia, 16鈥�18 May 2024.
  • Andrzej Indrzejczak, Yaroslav Petrukhin, Bisequent Calculi of Definite Descriptions in Neutral Free Logic, Formal Methods and Science in Philosophy V, Dubrovnik, Croatia, 16鈥�18 May 2024.
  • Andrzej Indrzejczak, Proof Systems for Hybrid Logic with Lambda and Iota Operators, Czech Gathering of Logicians 2024 and Kurt G枚del Day 2024, Brno, the Czech Republic, 27鈥�28 May 2024.
  • Yaroslav Petrukhin, Natural deduction for definite descriptions in strong Kleene free logic, Cracow Logic Conference feat. Trends in Logic 2024, Krak贸w, Poland, 18鈥�21 June 2024.
  • Andrzej Indrzejczak, Do theories of definite descriptions support Anselm's God?, Logic Colloquium 2024, Gothenburg, Sweden, 24鈥�28 June 2024
  • Yaroslav Petrukhin, Natural deduction for neutral free logic with definite descriptions, Logic Colloquium 2024, Gothenburg, Sweden, 24鈥�28 June 2024
  • Andrzej Indrzejczak, Yaroslav Petrukhin, Bisequent Calculi for Neutral Free Logic with Definite Descriptions, ARQNL 2024 Automated Reasoning in Quantified Non-Classical Logics 5th International Workshop (associated with IJCAR 2024), Nancy, France, 1 July 2024.
  • Andrzej Indrzejczak, When Epsilon meets Lambda: Extended Le艣niewski's Ontology. ARQNL 2024 Automated Reasoning in Quantified Non-Classical Logics 5th International Workshop (associated with IJCAR 2024), Nancy, France, 1 July 2024.
  • Andrzej Indrzejczak, Proof Theory extended to definite description & other terms, Proof Representations: From Theory to Applications, Dagstuhl Seminar 24341, Dagstuhl, Germany, 18鈥�23 August 2024. 
  • Nils K眉rbis, Normalisation for Negative Free Logic with Definite Descriptions, NCL'24: Non-Classical Logics. Theory and Applications 2024, 艁贸d藕, Poland, 5鈥�8 September 2024.
  • Nils K眉rbis, A Theory of Definite Descriptions, NCL'24: Non-Classical Logics. Theory and Applications 2024, 艁贸d藕, Poland, 5鈥�8 September 2024.
  • Andrzej Indrzejczak, Sequent Calculi for Logics of Classes, NCL'24: Non-Classical Logics. Theory and Applications 2024, 艁贸d藕, Poland, 5鈥�8 September 2024.
  • Przemys艂aw Wa艂臋ga, Micha艂 Zawidzki, Modal logic with definite descriptions: complexity, bisimulation, and tableaux, NCL'24: Non-Classical Logics. Theory and Applications 2024, 艁贸d藕, Poland, 5鈥�8 September 2024.
  • Yaroslav Petrukhin, Andrzej Indrzejczak, Bisequent Calculi for Neutral Free Logic with Definite Descriptions, NCL'24: Non-Classical Logics. Theory and Applications 2024, 艁贸d藕, Poland, 5鈥�8 September 2024.
  • Yaroslav Petrukhin, A Binary Quantifier for Definite Descriptions in Nelsonian Free Logic, NCL'24: Non-Classical Logics. Theory and Applications 2024, 艁贸d藕, Poland, 5鈥�8 September 2024.
  • Nils K眉rbis, A Theory of Definite Descriptions for Modal Logic, XXVI Deutscher Kongress f眉r Philosophie, Sektion Logik und Philosophie der Mathematik, M眉nster, Germany, 22鈥�26 September 2024. 
  • Przemys艂aw Wa艂臋ga, Expressive Power of Definite Descriptions in Modal Logics, KR 2024: 21st International Conference on Principles of Knowledge Representation and Reasoning, Hanoi, Vietnam, 2鈥�8 November 2024. 
  • Andrzej Indrzejczak, Proof Systems for Extensions of Hybrid Logic with Complex Terms, seminar of the Institute of Cybernetics of the Estonian Academy of Sciences, Tallin, Estonia, 10 January 2025.
  • Andrzej Indrzejczak, Bisequent Calculus and its Applications to Non-Classical Logics, World Logic Day 2025 in Tallin, Estonia, 11 January 2025. 
  • Micha艂 Zawidzki, Modal logic with definite description operators (in Polish), World Logic Day 2025 in 艁贸d藕, Poland, 15 January 2025. 
  • Yaroslav Petrukhin, Essence and accident modalities meet Belnapian truth values, World Logic Day 2025 in 艁贸d藕, Poland, 15 January 2025. 
  • Nils K眉rbis, 120 Years of On Denoting, World Logic Day 2025 in 艁贸d藕, Poland, 15 January 2025. 
  • Yaroslav Petrukhin, Second-order Definite Descriptions, Zagreb Logic Conference 2025, Zagreb, Croatia, 14鈥�17 February 2025. 
  • Nils K眉rbis, A Puzzle about Harmony and the Rules for Definite Descriptions, Bochum Logic and Epistemology Colloquium, Bochum, Germany, 24 April 2025.
  • Szymon Chlebowski, Yaroslav Petrukhin, Fregean Definite Descriptions in Non-Fregean Logic, 28th Conference Applications of Logic in Philosophy and the Foundations of Mathematics, Szklarska Por臋ba, Poland, 5鈥�9 May 2025. 
  • Yaroslav Petrukhin, Fregean Hypersequent Many-Valued Versions of Essence and Accident Modalities in FDE-Based Logics, 28th Conference Applications of Logic in Philosophy and the Foundations of Mathematics, Szklarska Por臋ba, Poland, 5鈥�9 May 2025. 
  • Nils K眉rbis, 120 Years of Russell鈥檚 鈥極n Denoting', 28th Conference Applications of Logic in Philosophy and the Foundations of Mathematics, Szklarska Por臋ba, Poland, 5鈥�9 May 2025. 
  • Andrzej Indrzejczak, Constructive Neologicism in the Theory of Classes, 28th Conference Applications of Logic in Philosophy and the Foundations of Mathematics, Szklarska Por臋ba, Poland, 5鈥�9 May 2025. 
  • Micha艂 Socha艅ski, Micha艂 Zawidzki, Modal Logic with Definite Descriptions, Tableaux, and Python, 28th Conference Applications of Logic in Philosophy and the Foundations of Mathematics, Szklarska Por臋ba, Poland, 5鈥�9 May 2025.
  • Przemys艂aw Wa艂臋ga, Graph Neural Networks, Modal Logics, and Definite Descriptions, 28th Conference Applications of Logic in Philosophy and the Foundations of Mathematics, Szklarska Por臋ba, Poland, 5鈥�9 May 2025. 
  • Andrzej Indrzejczak, How much of Set Theory can we derive from Logic?, special session at the workshop: Proof Representations: From Theory to Applications, Banff International Research Station, Canada, 1鈥�6 June 2025.
  • Nils K眉rbis, A Theory of Definite Descriptions for Modal Logic, Saul Kripke Center, New York, US, 11 June 2025.
  • Nils K眉rbis, Tennant on Deduction, Definite Descriptions and other Term Forming operators, conference Logic, Inference and Rationality. A Conference in Honour of Neil Tennant, Ohio State University, Columbus, US, 13鈥�14 June 2025.
  • Nils K眉rbis, Tennant on Deduction, A Puzzle about Harmony and the Rules for Definite Descriptions, Carl Friedrich von Weiz盲cker Kolloquium, University of T眉bingen, Germany, 25 June 2025.
  • Yaroslav Petrukhin, On a Second-order Generalisation of Russellian Theory of Definite Descriptions, Cracow Logic Conference (CLoCk) 2025, Krak贸w, Poland, 26鈥�27 June 2025. 
  • Yaroslav Petrukhin, From second-order quantification to second-order definite descriptions, Logic Colloquium 2025, Vienna, Austria, 7鈥�11 July 2025 
  • Nils K眉rbis, 120 Years of Russell鈥檚 'On Denoting鈥�, Logic Colloquium 2025, Vienna, Austria, 7鈥�11 July 2025. 
  • Andrzej Indrzejczak, Proof theoretic study of negative free logics with definite descriptions, Logic Colloquium 2025, Vienna, Austria, 7鈥�11 July 2025. 
  • Nils K眉rbis, Russell, On Denoting and Definite Descriptions formalised via Binary Quantification, Center for Mathematical Philosophy, University of Munich, Germany, 24 July 2025. 
  • Andrzej Indrzejczak, Cut Elimination for Negative Free Logics with Definite Descriptions, CADE-30: 30th International Conference on Automated Deduction, Stuttgart, Germany, 28 July鈥�2 August, 2025. 
  • Yaroslav Petrukhin, On a Second-Order Version of Russellian Theory of Definite Descriptions, JELIA 2025: 19th edition of the European Conference on Logics in Artificial Intelligence. Kutaisi, Georgia, 1鈥�4 September 2025. 
  • Andrzej Indrzejczak, Przemys艂aw Wa艂臋ga, Micha艂 Zawidzki, On Temporal References via Definite Descriptions in First-Order Monadic Logic of Order, JELIA 2025: 19th edition of the European Conference on Logics in Artificial Intelligence, Kutaisi, Georgia, 1鈥�4 September 2025. 
  • Micha艂 Socha艅ski, Przemys艂aw Wa艂臋ga, Micha艂 Zawidzki, Two Types of Definite Descriptions: Theory and Implementation, DL 2025: 38th International Workshop on Description Logics, Opole, Poland, 3鈥�6 September 2025. 
  • Andrzej Indrzejczak, How much set theory is in logic? On some applications of proof theory in the logic of classes (in Polish: Ile teorii mnogo艣ci zawiera logika? O pewnych zastosowaniach teorii dowodu w logice klas), invited talk, 10th Forum of Polish Mathematicians, Bia艂ystok, Poland, 8鈥�12 September, 2025. 
  • Yaroslav Petrukhin, From second-order quantification to second-order definite descriptions, Polish Congress of Logic, 22鈥�26 September 2025, Toru艅, Poland. 
  • Nils K眉rbis, Formal Theories of Definite Descriptions. Part I, Polish Congress of Logic, 22鈥�26 September 2025, Toru艅, Poland. 
  • Nils K眉rbis, Definite Descriptions in Free Core Logic, Polish Congress of Logic, 22鈥�26 September 2025, Toru艅, Poland. 
  • Szymon Chlebowski, Yaroslav Petrukhin, Fregean Definite Descriptions in Non-Fregean Logic, Polish Congress of Logic, 3rd Workshop on Non-Fregean Logics, 22鈥�26 September 2025, Toru艅, Poland. 
  • Andrzej Indrzejczak, Ontology of Le艣niewski in the Proof-Theoretic Setting, invited talk, Polish Congress of Logic, 22鈥�26 September 2025, Toru艅, Poland. 
  • Andrzej Indrzejczak, Formal Theories of Definite Descriptions. Part III, Polish Congress of Logic, 22鈥�26 September 2025, Toru艅, Poland. 
  • Micha艂 Zawidzki, Formal Theories of Definite Descriptions. Part II, Polish Congress of Logic, 22鈥�26 September 2025, Toru艅, Poland. 
  • Nils K眉rbis, Definite Descriptions in Free Core Logic, 6th Taiwan Philosophical Logic Conference, National Taiwan University, Taipei, Taiwan, 23鈥�25 October 2025.

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

ul. Narutowicza 68, 90-136 艁贸d藕
NIP: 724 000 32 43
KONTAKT鈥嬧赌嬧赌嬧赌嬧赌嬧赌嬧赌�

© 2009-2026, 91桃色