Showing 1–13 of 13 results for author: Kürbis, N

A Cut-free, Sound and Complete Russellian Theory of Definite Descriptions

Authors: Andrzej Indrzejczak, Nils Kürbis

Abstract: We present a sequent calculus for first-order logic with lambda terms and definite descriptions. The theory formalised by this calculus is essentially Russellian, but avoids some of its well known drawbacks and treats definite description as genuine terms. A constructive proof of the cut elimination theorem and a Henkin-style proof of completeness are the main results of this contribution. We present a sequent calculus for first-order logic with lambda terms and definite descriptions. The theory formalised by this calculus is essentially Russellian, but avoids some of its well known drawbacks and treats definite description as genuine terms. A constructive proof of the cut elimination theorem and a Henkin-style proof of completeness are the main results of this contribution. △ Less

Submitted 4 December, 2024; originally announced December 2024.

Normalisation for Negative Free Logics without and with Definite Descriptions

Authors: Nils Kürbis

Abstract: This paper proves normalisation theorems for intuitionist and classical negative free logic, without and with the $\invertediota$ operator for definite descriptions. Rules specific to free logic give rise to new kinds of maximal formulas additional to those familiar from standard intuitionist and classical logic. When $\invertediota$ is added it must be ensured that reduction procedures involving… ▽ More This paper proves normalisation theorems for intuitionist and classical negative free logic, without and with the $\invertediota$ operator for definite descriptions. Rules specific to free logic give rise to new kinds of maximal formulas additional to those familiar from standard intuitionist and classical logic. When $\invertediota$ is added it must be ensured that reduction procedures involving replacements of parameters by terms do not introduce new maximal formulas of higher degree than the ones removed. The problem is solved by a rule that permits restricting these terms in the rules for $\forall$, $\exists$ and $\invertediota$ to parameters or constants. A restricted subformula property for deductions in systems without $\invertediota$ is considered. It is improved upon by an alternative formalisation of free logic building on an idea of Jaśkowski's. In the classical system the rules for $\invertediota$ require treatment known from normalisation for classical logic with $\lor$ or $\exists$. The philosophical significance of the results is also indicated. △ Less

Submitted 15 October, 2024; originally announced October 2024.

Comment on Mark Textor: Brentano's Positing Theory of Existence

Authors: Nils Kürbis

Abstract: This article is the text of a commentary on a talk delivered by Mark Textor entitled 'Brentano's Positing Theory of Existence' in December 2015. It contains ideas on implementing Textor's Neo-Brentanian theory of existence in a natural deduction proof system for negative free logic. This article is the text of a commentary on a talk delivered by Mark Textor entitled 'Brentano's Positing Theory of Existence' in December 2015. It contains ideas on implementing Textor's Neo-Brentanian theory of existence in a natural deduction proof system for negative free logic. △ Less

Submitted 17 April, 2023; originally announced April 2023.

Normalisation and subformula property for a system of intuitionistic logic with general introduction and elimination rules

Authors: Nils Kürbis

Abstract: This paper studies a formalisation of intuitionistic logic by Negri and von Plato which has general introduction and elimination rules. The philosophical importance of the system is expounded. Definitions of `maximal formula', `segment' and `maximal segment' suitable to the system are formulated and corresponding reduction procedures for maximal formulas and permutative reduction procedures for ma… ▽ More This paper studies a formalisation of intuitionistic logic by Negri and von Plato which has general introduction and elimination rules. The philosophical importance of the system is expounded. Definitions of `maximal formula', `segment' and `maximal segment' suitable to the system are formulated and corresponding reduction procedures for maximal formulas and permutative reduction procedures for maximal segments given. Alternatives to the main method used are also considered. It is shown that deductions in the system convert into normal form and that deductions in normal form have the subformula property. △ Less

Submitted 19 October, 2021; originally announced October 2021.

Comments: arXiv admin note: substantial text overlap with arXiv:2108.03939

Journal ref: Synthese 2021

A Binary Quantifier for Definite Descriptions for Cut Free Free Logics

Authors: Nils Kürbis

Abstract: This paper presents rules in sequent calculus for a binary quantifier $I$ to formalise definite descriptions: $Ix[F, G]$ means `The $F$ is $G$'. The rules are suitable to be added to a system of positive free logic. The paper extends the proof of a cut elimination theorem for this system by Indrzejczak by proving the cases for the rules of $I$. There are also brief comparisons of the present appro… ▽ More This paper presents rules in sequent calculus for a binary quantifier $I$ to formalise definite descriptions: $Ix[F, G]$ means `The $F$ is $G$'. The rules are suitable to be added to a system of positive free logic. The paper extends the proof of a cut elimination theorem for this system by Indrzejczak by proving the cases for the rules of $I$. There are also brief comparisons of the present approach to the more common one that formalises definite descriptions with a term forming operator. In the final section rules for $I$ for negative free and classical logic are also mentioned. △ Less

Submitted 22 August, 2021; originally announced August 2021.

Journal ref: Studia Logica 2021

Normalisation for Bilateral Classical Logic with some Philosophical Remarks, and a Note on it

Authors: Nils Kürbis

Abstract: Bilateralists hold that the meanings of the connectives are determined by rules of inference for their use in deductive reasoning with asserted and denied formulas. This paper presents two bilateral connectives comparable to Prior's tonk, for which, unlike for tonk, there are reduction steps for the removal of maximal formulas arising from introducing and eliminating formulas with those connective… ▽ More Bilateralists hold that the meanings of the connectives are determined by rules of inference for their use in deductive reasoning with asserted and denied formulas. This paper presents two bilateral connectives comparable to Prior's tonk, for which, unlike for tonk, there are reduction steps for the removal of maximal formulas arising from introducing and eliminating formulas with those connectives as main operators. Adding either of them to bilateral classical logic results in an incoherent system. One way around this problem is to count formulas as maximal that are the conclusion of reductio and major premise of an elimination rule and to require their removability from deductions. The main part of the paper consists in a proof of a normalisation theorem for bilateral logic. The closing sections address philosophical concerns whether the proof provides a satisfactory solution to the problem at hand and confronts bilateralists with the dilemma that a bilateral notion of stability sits uneasily with the core bilateral thesis. The Note corrects an error in one of the reduction steps in the paper. △ Less

Submitted 12 August, 2021; originally announced August 2021.

Journal ref: Journal of Applied Logics 8/2 (2021): 531-556; Journal of Applied Logics 8/7 (2021): 2259-2261

Proof-Theory and Semantics for a Theory of Definite Descriptions

Authors: Nils Kürbis

Abstract: This paper presents a sequent calculus and a dual domain semantics for a theory of definite descriptions in which these expressions are formalised in the context of complete sentences by a binary quantifier $I$. $I$ forms a formula from two formulas. $Ix[F, G]$ means `The $F$ is $G$'. This approach has the advantage of incorporating scope distinctions directly into the notation. Cut elimination is… ▽ More This paper presents a sequent calculus and a dual domain semantics for a theory of definite descriptions in which these expressions are formalised in the context of complete sentences by a binary quantifier $I$. $I$ forms a formula from two formulas. $Ix[F, G]$ means `The $F$ is $G$'. This approach has the advantage of incorporating scope distinctions directly into the notation. Cut elimination is proved for a system of classical positive free logic with $I$ and it is shown to be sound and complete for the semantics. The system has a number of novel features and is briefly compared to the usual approach of formalising `the $F$' by a term forming operator. It does not coincide with Hintikka's and Lambert's preferred theories, but the divergence is well-motivated and attractive. △ Less

Submitted 9 August, 2021; originally announced August 2021.

Report number: Anupam Das, Sara Negri (eds.): Automated Reasoning with Analytic Tableaux and Related Methods. Proceedings of the 30th International Conference Tableaux 2021. (Berlin, Heidelberg: Springer 2021)

Normalisation and Subformula Property for a System of Classical Logic with Tarski's Rule, and a Correction

Authors: Nils Kürbis

Abstract: This paper considers a formalisation of classical logic using general introduction rules and general elimination rules. It proposes a definition of `maximal formula', `segment' and `maximal segment' suitable to the system, and gives reduction procedures for them. It is then shown that deductions in the system convert into normal form, i.e. deductions that contain neither maximal formulas nor maxim… ▽ More This paper considers a formalisation of classical logic using general introduction rules and general elimination rules. It proposes a definition of `maximal formula', `segment' and `maximal segment' suitable to the system, and gives reduction procedures for them. It is then shown that deductions in the system convert into normal form, i.e. deductions that contain neither maximal formulas nor maximal segments, and that deductions in normal form satisfy the subformula property. Tarski's Rule is treated as a general introduction rule for implication. The general introduction rule for negation has a similar form. Maximal formulas with implication or negation as main operator require reduction procedures of a more intricate kind not present in normalisation for intuitionist logic. The Correction added to the end of the paper corrects an error: Theorem 2 is mistaken, and so is a corollary drawn from it as well as a corollary that was concluded by the same mistake. Luckily this does not affect the main result of the paper. △ Less

Submitted 24 April, 2023; v1 submitted 9 August, 2021; originally announced August 2021.

Journal ref: Archive for Mathematical Logic 2021

Definite Descriptions in Intuitionist Positive Free Logic

Authors: Nils Kürbis

Abstract: 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… ▽ More 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'. △ Less

Submitted 4 August, 2021; originally announced August 2021.

Journal ref: Logic and Logical Philosophy 30/2 (2021): 327-358

Two Treatments of Definite Descriptions in Intuitionist Negative Free Logic

Authors: Nils Kürbis

Abstract: Sentences containing definite descriptions, expressions of the form `The $F$', can be formalised using a binary quantifier $ι$ that forms a formula out of two predicates, where $ιx[F, G]$ is read as `The $F$ is $G$'. This is an innovation over the usual formalisation of definite descriptions with a term forming operator. The present paper compares the two approaches. After a brief overview of the… ▽ More Sentences containing definite descriptions, expressions of the form `The $F$', can be formalised using a binary quantifier $ι$ that forms a formula out of two predicates, where $ιx[F, G]$ is read as `The $F$ is $G$'. This is an innovation over the usual formalisation of definite descriptions with a term forming operator. The present paper compares the two approaches. After a brief overview of the system $\mathbf{INF}^ι$ of intuitionist negative free logic extended by such a quantifier, which was presented in \citep{kurbisiotaI}, $\mathbf{INF}^ι$ is first compared to a system of Tennant's and an axiomatic treatment of a term forming $ι$ operator within intuitionist negative free logic. Both systems are shown to be equivalent to the subsystem of $\mathbf{INF}^ι$ in which the $G$ of $ιx[F, G]$ is restricted to identity. $\mathbf{INF}^ι$ is then compared to an intuitionist version of a system of Lambert's which in addition to the term forming operator has an operator for predicate abstraction for indicating scope distinctions. The two systems will be shown to be equivalent through a translation between their respective languages. Advantages of the present approach over the alternatives are indicated in the discussion. △ Less

Submitted 4 August, 2021; originally announced August 2021.

Journal ref: Bulletin of the Section of Logic 48/4 (2019): 299-317

A Binary Quantifier for Definite Descriptions in Intuitionist Negative Free Logic: Natural Deduction and Normalisation

Authors: Nils Kürbis

Abstract: This paper presents a way of formalising definite descriptions with a binary quantifier $ι$, where $ιx[F, G]$ is read as `The $F$ is $G$'. Introduction and elimination rules for $ι$ in a system of intuitionist negative free logic are formulated. Procedures for removing maximal formulas of the form $ιx[F, G]$ are given, and it is shown that deductions in the system can be brought into normal form. This paper presents a way of formalising definite descriptions with a binary quantifier $ι$, where $ιx[F, G]$ is read as `The $F$ is $G$'. Introduction and elimination rules for $ι$ in a system of intuitionist negative free logic are formulated. Procedures for removing maximal formulas of the form $ιx[F, G]$ are given, and it is shown that deductions in the system can be brought into normal form. △ Less

Submitted 4 August, 2021; originally announced August 2021.

Journal ref: Bulletin of the Section of Logic 48/2 (2019): 81-97

Proof-Theoretic Semantics, a Problem with Negation and Prospects for Modality

Authors: Nils Kürbis

Abstract: This paper discusses proof-theoretic semantics, the project of specifying the meanings of the logical constants in terms of rules of inference governing them. I concentrate on Michael Dummett's and Dag Prawitz' philosophical motivations and give precise characterisations of the crucial notions of harmony and stability, placed in the context of proving normalisation results in systems of natural de… ▽ More This paper discusses proof-theoretic semantics, the project of specifying the meanings of the logical constants in terms of rules of inference governing them. I concentrate on Michael Dummett's and Dag Prawitz' philosophical motivations and give precise characterisations of the crucial notions of harmony and stability, placed in the context of proving normalisation results in systems of natural deduction. I point out a problem for defining the meaning of negation in this framework and prospects for an account of the meanings of modal operators in terms of rules of inference. △ Less

Submitted 29 July, 2021; originally announced July 2021.

Journal ref: Journal of Philosophical Logic 44/6 (2015): 713-727

A Sketch of a Proof-Theoretic Semantics for Necessity

Authors: Nils Kürbis

Abstract: This paper considers proof-theoretic semantics for necessity within Dummett's and Prawitz's framework. Inspired by a system of Pfenning's and Davies's, the language of intuitionist logic is extended by a higher order operator which captures a notion of validity. A notion of relative necessary is defined in terms of it, which expresses a necessary connection between the assumptions and the conclusi… ▽ More This paper considers proof-theoretic semantics for necessity within Dummett's and Prawitz's framework. Inspired by a system of Pfenning's and Davies's, the language of intuitionist logic is extended by a higher order operator which captures a notion of validity. A notion of relative necessary is defined in terms of it, which expresses a necessary connection between the assumptions and the conclusion of a deduction. △ Less

Submitted 29 July, 2021; originally announced July 2021.

Report number: Advances in Modal Logic 13. Booklet of Short Papers, ed. by Sara Negri, Nicola Olivetti, Rineke Verbrugge (Helsinki 2020): 37-43