The status of the equality predicate as a logical constant is problematic. In the paper we look at the problem from the proof-theoretic standpoint and survey several ways of treating equality in formal systems of different sorts. In particular, we focus on the framework of sequent calculus and examine equality in the light of criteria of logicality proposed by Hacking and Došen. Both attempts were formulated in terms of sequent calculus rules, although in the case of Došen it has a (...) nonstandard character. It will be shown that equality can be characterised in a way which satisfies Došen’s criteria of logicality. In the case of Hacking’s approach the fully satisfying result can be obtained only for languages with a nonempty, finite set of predicate constants other than equality. Otherwise, cut elimination theorem fails to hold. (shrink)

In the chapter “Information and Content” of their Impossible Worlds, Berto and Jago provide us with a semantic account of information in deductive reasoning such that we have an explanation for why some, but not all, logical deductions are informative. The framework Berto and Jago choose to make sense of the above-mentioned idea is a semantic interpretation of Sequent Calculus rules of inference for classical logic. I shall argue that although Berto and Jago’s idea and framework are hopeful, their definitions (...) do not capture what is intended. This is so because the definitions are solely based on the logical complexity of an argument and they fail to capture the richness of the non- logical content of that argument. Then I will suggest some amendments to address this problem. Finally, I will extend the application of the definitions to first-order logic. It shall be observed that in some classical deductions, applying contraction may lead to hiding some epistemic impossibilities. This happens when formulae which contribute different propositions to the proof get contracted at the quantified level. (shrink)

In this paper we use proof-theoretic methods, specifically sequent calculi, admissibility of cut within them and the resultant subformula property, to examine a range of philosophically-motivated deontic logics. We show that for all of those logics it is a (meta)theorem that the Special Hume Thesis holds, namely that no purely normative conclusion follows non-trivially from purely descriptive premises (nor vice versa). In addition to its interest on its own, this also illustrates one way in which proof theory sheds light on (...) philosophically substantial questions. (shrink)

This paper formulates a bilateral account of harmony that is an alternative to one proposed by Francez. It builds on an account of harmony for unilateral logic proposed by Kürbis and the observation that reading the rules for the connectives of bilateral logic bottom up gives the grounds and consequences of formulas with the opposite speech act. I formulate a process I call 'inversion' which allows the determination of assertive elimination rules from assertive introduction rules, and rejective elimination rules from (...) rejective introduction rules, and conversely. It corresponds to Francez's notion of vertical harmony. I also formulate a process I call 'conversion', which allows the determination of rejective introduction rules from assertive elimination rules and conversely, and the determination of assertive introduction rules from rejective elimination rules and conversely. It corresponds to Francez's notion of horizontal harmony. The account has a number of features that distinguish it from Francez's. (shrink)

One main goal of argumentation theory is to evaluate arguments and to determine whether they should be accepted or rejected. When there is no clear answer, a third option, being undecided, has to be taken into account. Indecision is often not considered explicitly, but rather taken to be a collection of all unclear or troubling cases. However, current philosophy makes a strong point for taking indecision itself to be a proper object of consideration. This paper aims at revealing parallels between (...) the findings concerning indecision in philosophy and the treatment of indecision in argumentation theory. By investigating what philosophical forms and norms of indecision are involved in argumentation theory, we can improve our understanding of the different uncertain evidential situations in argumentation theory. (shrink)

Inferentialism is a theory in the philosophy of language which claims that the meanings of expressions are constituted by inferential roles or relations. Instead of a traditional model-theoretic semantics, it naturally lends itself to a proof-theoretic semantics, where meaning is understood in terms of inference rules with a proof system. Most work in proof-theoretic semantics has focused on logical constants, with comparatively little work on the semantics of non-logical vocabulary. Drawing on Robert Brandom’s notion of material inference and Greg Restall’s (...) bilateralist interpretation of the multiple conclusion sequent calculus, I present a proof-theoretic semantics for atomic sentences and their constituent names and predicates. The resulting system has several interesting features: (1) the rules are harmonious and stable; (2) the rules create a structure analogous to familiar model-theoretic semantics; and (3) the semantics is compositional, in that the rules for atomic sentences are determined by those for their constituent names and predicates. (shrink)

Expressivism in logic is the view that logical vocabulary plays a primarily expressive role: that is, that logical vocabulary makes perspicuous in the object language structural features of inference and incompatibility (Brandom, 1994, 2008). I present a precise, technical criterion of expressivity for a logic (§2). I next present a logic that meets that criterion (§3). I further explore some interesting features of that logic: first, a representation theorem for capturing other logics (§3.1), and next some novel logical vocabulary for (...) expressing structural features of inference (§4). (shrink)

David Ripley ha argumentado extensamente a favor de una teoría no-transitiva de la verdad que abandona la regla de Corte para así evitar las pruebas de trivialidad causadas por paradojas como la del mentiroso. Sin embargo, es problemático comparar su teoría con varias teorías clásicas que se han ofrecido en la bibliografía. La tarea de formular esta teoría sobre la aritmética de Peano no es trivial, ya que Corte no es eliminable en la aritmética de Peano. En este artículo intento (...) cerrar esta brecha proponiendo una restricción adecuada para la regla de Corte. La restricción nos permite formular una teoría no-transitiva de la verdad sobre la aritmética de Peano que es, desde el punto de vista de la teoría de la prueba, tan fuerte como la teoría clásica de la verdad más fuerte conocida hasta el momento. (shrink)

It's natural to think that the principles expressed by the statements "Promises ought to be kept" and "We ought to help those in need" are defeasible. But how are we to make sense of this defeasibility? On one proposal, moral principles have hedges or built-in unless clauses specifying the conditions under which the principle doesn't apply. On another, such principles are contributory and, thus, do not specify which actions ought to be carried out, but only what counts in favor or (...) against them. Drawing on a defeasible logic framework, this paper sets up three models: one model for each proposal, as well as a third model capturing a mixed view on principles that combines them. It then explores the structural connections between the three models and establishes some equivalence results, suggesting that the seemingly different views captured by the models are closer than standardly thought. (shrink)

The book presents a thoroughly elaborated logical theory of generalized truth-values understood as subsets of some established set of truth values. After elucidating the importance of the very notion of a truth value in logic and philosophy, we examine some possible ways of generalizing this notion. The useful four-valued logic of first-degree entailment by Nuel Belnap and the notion of a bilattice constitute the basis for further generalizations. By doing so we elaborate the idea of a multilattice, and most notably, (...) a trilattice of truth values – a specific algebraic structure with information ordering and two distinct logical orderings, one for truth and another for falsity. Each logical order not only induces its own logical vocabulary, but determines also its own entailment relation. We consider both semantic and syntactic ways of formalizing these relations and construct various logical calculi. (shrink)

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. (shrink)

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. (shrink)

The paper presents a uniform proof-theoretic treatment of several kinds of free logic, including the logics of existence and definedness applied in constructive mathematics and computer science, and called here quasi-free logics. All free and quasi-free logics considered are formalised in the framework of sequent calculus, the latter for the first time. It is shown that in all cases remarkable simplifications of the starting systems are possible due to the special rule dealing with identity and existence predicate. Cut elimination is (...) proved in a constructive way for sequent calculi adequate for all logics under consideration. (shrink)

STIT logic is a prominent framework for the analysis of multi-agent choice-making. In the available deontic extensions of STIT, the principle of Ought-implies-Can (OiC) fulfills a central role. However, in the philosophical literature a variety of alternative OiC interpretations have been proposed and discussed. This paper provides a modular framework for deontic STIT that accounts for a multitude of OiC readings. In particular, we discuss, compare, and formalize ten such readings. We provide sound and complete sequent-style calculi for all of (...) the various STIT logics accommodating these OiC principles. We formally analyze the resulting logics and discuss how the different OiC principles are logically related. In particular, we propose an endorsement principle describing which OiC readings logically commit one to other OiC readings. (shrink)

In this paper, we investigate the possibility of translating a fragment of natural deduction system (NDS) for natural language semantics into modern type theory (MTT), originally suggested by Luo (2014). Our main goal will be to examine and translate the basic rules of NDS (namely, meta-rules, structural rules, identity rules, noun rules and rules for intersective and subsective adjectives) to MTT. Additionally, we will also consider some of their general features.

Much has been said about intuitionistic and classical logical systems since Gentzen’s seminal work. Recently, Prawitz and others have been discussing how to put together Gentzen’s systems for classical and intuitionistic logic in a single unified system. We call Prawitz’ proposal the Ecumenical System, following the terminology introduced by Pereira and Rodriguez. In this work we present an Ecumenical sequent calculus, as opposed to the original natural deduction version, and state some proof theoretical properties of the system. We reason that (...) sequent calculi are more amenable to extensive investigation using the tools of proof theory, such as cut-elimination and rule invertibility, hence allowing a full analysis of the notion of Ecumenical entailment. We then present some extensions of the Ecumenical sequent system and show that interesting systems arise when restricting such calculi to specific fragments. This approach of a unified system enabling both classical and intuitionistic features sheds some light not only on the logics themselves, but also on their semantical interpretations as well as on the proof theoretical properties that can arise from combining logical systems. (shrink)

Conditional logics were originally developed for the purpose of modeling intuitively correct modes of reasoning involving conditional—especially counterfactual—expressions in natural language. While the debate over the logic of conditionals is as old as propositional logic, it was the development of worlds semantics for modal logic in the past century that catalyzed the rapid maturation of the field. Moreover, like modal logic, conditional logic has subsequently found a wide array of uses, from the traditional (e.g. counterfactuals) to the exotic (e.g. conditional (...) obligation). Despite the close connections between conditional and modal logic, both the technical development and philosophical exploitation of the latter has outstripped that of the former, with the result that noticeable lacunae exist in the literature on conditional logic. My dissertation addresses a number of these underdeveloped frontiers, producing new technical insights and philosophical applications. -/- I contribute to the solution of a problem posed by Priest of finding sound and complete labeled tableaux for systems of conditional logic from Lewis' V-family. To develop these tableaux, I draw on previous work on labeled tableaux for modal and conditional logic; errors and shortcomings in recent work on this problem are identified and corrected. While modal logic has by now been thoroughly studied in non-classical contexts, e.g. intuitionistic and relevant logic, the literature on conditional logic is still overwhelmingly classical. Another contribution of my dissertation is a thorough analysis of intuitionistic conditional logic, in which I utilize both algebraic and worlds semantics, and investigate how several novel embedding results might shed light on the philosophical interpretation of both intuitionistic logic and conditional logic extensions thereof. -/- My dissertation examines deontic and connexive conditional logic as well as the underappreciated history of connexive notions in the analysis of conditional obligation. The possibility of interpreting deontic modal logics in such systems (via embedding results) serves as an important theoretical guide. A philosophically motivated proscription on impossible obligations is shown to correspond to, and justify, certain (weak) connexive theses. Finally, I contribute to the intensifying debate over counterpossibles, counterfactuals with impossible antecedents, and take—in contrast to Lewis and Williamson—a non-vacuous line. Thus, in my view, a counterpossible like "If there had been a counterexample to the law of the excluded middle, Brouwer would not have been vindicated" is false, not (vacuously) true, although it has an impossible antecedent. I exploit impossible (non-normal) worlds—originally developed to model non-normal modal logics—to provide non-vacuous semantics for counterpossibles. I buttress the case for non-vacuous semantics by making recourse to both novel technical results and theoretical considerations. (shrink)

This book examines the philosophical conception of abductive reasoning as developed by Charles S. Peirce, the founder of American pragmatism. It explores the historical and systematic connections of Peirce's original ideas and debates about their interpretations. Abduction is understood in a broad sense which covers the discovery and pursuit of hypotheses and inference to the best explanation. The analysis presents fresh insights into this notion of reasoning, which derives from effects to causes or from surprising observations to explanatory theories. The (...) author outlines some logical and AI approaches to abduction as well as studies various kinds of inverse problems in astronomy, physics, medicine, biology, and human sciences to provide examples of retroductions and abductions. The discussion covers also everyday examples with the implication of this notion in detective stories, one of Peirce’s own favorite themes. The author uses Bayesian probabilities to argue that explanatory abduction is a method of confirmation. He uses his own account of truth approximation to reformulate abduction as inference which leads to the truthlikeness of its conclusion. This allows a powerful abductive defense of scientific realism. This up-to-date survey and defense of the Peircean view of abduction may very well help researchers, students, and philosophers better understand the logic of truth-seeking. (shrink)

This work contributes to the theory of judgement aggregation by discussing a number of significant non-classical logics. After adapting the standard framework of judgement aggregation to cope with non-classical logics, we discuss in particular results for the case of Intuitionistic Logic, the Lambek calculus, Linear Logic and Relevant Logics. The motivation for studying judgement aggregation in non-classical logics is that they offer a number of modelling choices to represent agents’ reasoning in aggregation problems. By studying judgement aggregation in logics that (...) are weaker than classical logic, we investigate whether some well-known impossibility results, that were tailored for classical logic, still apply to those weak systems. (shrink)

Philosophy and Phenomenological Research, EarlyView.

The article concerns two axiom systems of Słupecki for the functionally complete three-valued propositional logic: W1–W6 and A1–A9. The article proves that both of them are inadequate—W1–W6 is semantically incomplete, on the other hand, A1–A9 governs a functionally incomplete calculus, and thus, it cannot be a semantically complete axiom system for the functionally complete three-valued logic.

Rejecting the Cut rule has been proposed as a strategy to avoid both the usual semantic paradoxes and the so-called v-Curry paradox. In this paper we consider if a Cut-free theory is capable of accurately representing its own notion of validity. We claim that the standard rules governing the validity predicate are too weak for this purpose and we show that although it is possible to strengthen these rules, the most obvious way of doing so brings with it a serious (...) problem: an internalized version of Cut can be proved for a Curry-like sentence. We also evaluate a number of possible ways of escaping this difficulty. (shrink)

We present two proof systems for first-order logic with identity and without function symbols. The first one is an extension of the Rasiowa-Sikorski system with the rules for identity. This system is a validity checker. The rules of this system preserve and reflect validity of disjunctions of their premises and conclusions. The other is a Tableau system, which is an unsatisfiability checker. Its rules preserve and reflect unsatisfiability of conjunctions of their premises and conclusions. We show that the two systems (...) are dual to each other. The duality is expressed in a formal way which enables us to define a transformation of proofs in one of the systems into the proofs of the other. (shrink)

A general method for generating contraction- and cut-free sequent calculi for a large family of normal modal logics is presented. The method covers all modal logics characterized by Kripke frames determined by universal or geometric properties and it can be extended to treat also Gödel-Löb provability logic. The calculi provide direct decision methods through terminating proof search. Syntactic proofs of modal undefinability results are obtained in the form of conservativity theorems.

Many prominent writers on the philosophy of logic, including Michael Dummett, Dag Prawitz, Neil Tennant, have held that the introduction and elimination rules of a logical connective must be ‘in harmony ’ if the connective is to possess a sense. This Harmony Thesis has been used to justify the choice of logic: in particular, supposed violations of it by the classical rules for negation have been the basis for arguments for switching from classical to intuitionistic logic. The Thesis has also (...) had an influence on the philosophy of language: some prominent writers in that area, notably Dummett and Robert Brandom, have taken it to be a special case of a more general requirement that the grounds for asserting a statement must cohere with its consequences. This essay considers various ways of making the Harmony Thesis precise and scrutinizes the most influential arguments for it. The verdict is negative: all the extant arguments for the Thesis are weak, and no version of it is remotely plausible. (shrink)

Logical orthodoxy has it that classical first-order logic, or some extension thereof, provides the right extension of the logical consequence relation. However, together with naïve but intuitive principles about semantic notions such as truth, denotation, satisfaction, and possibly validity and other naïve logical properties, classical logic quickly leads to inconsistency, and indeed triviality. At least since the publication of Kripke’s Outline of a theory of truth , an increasingly popular diagnosis has been to restore consistency, or at least non-triviality, by (...) restricting some classical rules. Our modest aim in this note is to briefly introduce the main strands of the current debate on paradox and logical revision, and point to some of the potential challenges revisionary approaches might face, with reference to the nine contributions to the present volume.For a recent introduction to non-classical theories of truth and other semantic notions, see the excellent Beall a .. (shrink)

A comparison is given between two conditions used to define logical constants: Belnap's uniqueness and Hacking's deducibility of identicals. It is shown that, in spite of some surface similarities, there is a deep difference between them. On the one hand, deducibility of identicals turns out to be a weaker and less demanding condition than uniqueness. On the other hand, deducibility of identicals is shown to be more faithful to the inferentialist perspective, permitting definition of genuinely proof-theoretical concepts. This kind of (...) analysis is driven by exploiting the Curry–Howard correspondence. In particular, deducibility of identicals is shown to correspond to the computational property of eta expansion, which is essential in the characterization of propositional identity. (shrink)

Argumentation mining aims to automatically detect, classify and structure argumentation in text. Therefore, argumentation mining is an important part of a complete argumentation analyisis, i.e. understanding the content of serial arguments, their linguistic structure, the relationship between the preceding and following arguments, recognizing the underlying conceptual beliefs, and understanding within the comprehensive coherence of the specific topic. We present different methods to aid argumentation mining, starting with plain argumentation detection and moving forward to a more structural analysis of the detected (...) argumentation. Different state-of-the-art techniques on machine learning and context free grammars are applied to solve the challenges of argumentation mining. We also highlight fundamental questions found during our research and analyse different issues for future research on argumentation mining. (shrink)

Various sources in the literature claim that the deduction theorem does not hold for normal modal or epistemic logic, whereas others present versions of the deduction theorem for several normal modal systems. It is shown here that the apparent problem arises from an objectionable notion of derivability from assumptions in an axiomatic system. When a traditional Hilbert-type system of axiomatic logic is generalized into a system for derivations from assumptions, the necessitation rule has to be modified in a way that (...) restricts its use to cases in which the premiss does not depend on assumptions. This restriction is entirely analogous to the restriction of the rule of universal generalization of first-order logic. A necessitation rule with this restriction permits a proof of the deduction theorem in its usual formulation. Other suggestions presented in the literature to deal with the problem are reviewed, and the present solution is argued to be preferable to the other alternatives. A contraction-and cut-free sequent calculus equivalent to the Hubert system for basic modal logic shows the standard failure argument untenable by proving the underivability of DA from A. (shrink)

The method of Socratic proofs (SP-method) simulates the solving of logical problem by pure questioning. An outcome of an application of the SP-method is a sequence of questions, called a Socratic transformation. Our aim is to give a method of translation of Socratic transformations into trees. We address this issue both conceptually and by providing certain algorithms. We show that the trees which correspond to successful Socratic transformations—that is, to Socratic proofs—may be regarded, after a slight modification, as Gentzen-style proofs. (...) Thus proof-search for some Gentzen-style calculi can be performed by means of the SP-method. At the same time the method seems promising as a foundation for automated deduction. (shrink)

This paper presents and defends a way to add a transparent truth predicate to classical logic, such that and A are everywhere intersubstitutable, where all T-biconditionals hold, and where truth can be made compositional. A key feature of our framework, called STTT (for Strict-Tolerant Transparent Truth), is that it supports a non-transitive relation of consequence. At the same time, it can be seen that the only failures of transitivity STTT allows for arise in paradoxical cases.

The axiomatic presentation of modal systems and the standard formulations of natural deduction and sequent calculus for modal logic are reviewed, together with the difficulties that emerge with these approaches. Generalizations of standard proof systems are then presented. These include, among others, display calculi, hypersequents, and labelled systems, with the latter surveyed from a closer perspective.

A proof-theoretical treatment of collectively accepted group beliefs is presented through a multi-agent sequent system for an axiomatization of the logic of acceptance. The system is based on a labelled sequent calculus for propositional multi-agent epistemic logic with labels that correspond to possible worlds and a notation for internalized accessibility relations between worlds. The system is contraction- and cut-free. Extensions of the basic system are considered, in particular with rules that allow the possibility of operative members or legislators. Completeness with (...) respect to the underlying Kripke semantics follows from a general direct and uniform argument for labelled sequent calculi extended with mathematical rules for frame properties. As an example of the use of the calculus we present an analysis of the discursive dilemma. (shrink)

A good argument is one whose conclusions follow from its premises; its conclusions are consequences of its premises. But in what sense do conclusions follow from premises? What is it for a conclusion to be a consequence of premises? Those questions, in many respects, are at the heart of logic (as a philosophical discipline). Consider the following argument: 1. If we charge high fees for university, only the rich will enroll. We charge high fees for university. Therefore, only the rich (...) will enroll. There are many different things one can say about this argument, but many agree that if we do not equivocate (if the terms mean the same thing in the premises and the conclusion) then the argument is valid, that is, the conclusion follows deductively from the premises. This does not mean that the conclusion is true. Perhaps the premises are not true. However, if the premises are true, then the conclusion is also true, as a matter of logic. This entry is about the relation between premises and conclusions in valid arguments. (shrink)

This open access book is a superb collection of some fifteen chapters inspired by Schroeder-Heister's groundbreaking work, written by leading experts in the field, plus an extensive autobiography and comments on the various contributions by Schroeder-Heister himself. For several decades, Peter Schroeder-Heister has been a central figure in proof-theoretic semantics, a field of study situated at the interface of logic, theoretical computer science, natural-language semantics, and the philosophy of language. -/- The chapters of which this book is composed discuss the (...) subject from a rich variety of angles, including the history of logic, the proper interpretation of logical validity, natural deduction rules, the notions of harmony and of synonymy, the structure of proofs, the logical status of equality, intentional phenomena, and the proof theory of second-order arithmetic. All chapters relate directly to questions that have driven Schroeder-Heister's own research agenda and to which he has made seminal contributions. The extensive autobiographical chapter not only provides a fascinating overview of Schroeder-Heister's career and the evolution of his academic interests but also constitutes a contribution to the recent history of logic in its own right, painting an intriguing picture of the philosophical, logical, and mathematical institutional landscape in Germany and elsewhere since the early 1970s. The papers collected in this book are illuminatingly put into a unified perspective by Schroeder-Heister's comments at the end of the book. Both graduate students and established researchers in the field will find this book an excellent resource for future work in proof-theoretic semantics and related areas. (shrink)

This is a contribution to the idea that some proofs in first-order logic are synthetic. Syntheticity is understood here in its classical geometrical sense. Starting from Jaakko Hintikka’s original idea and Allen Hazen’s insights, this paper develops a method to define the ‘graphical form’ of formulae in monadic and dyadic fraction of first-order logic. Then a synthetic inferential step in Natural Deduction is defined. A proof is defined as synthetic if it includes at least one synthetic inferential step. Finally, it (...) will be shown that the proposed definition is not sensitive to different ways of driving the same conclusion from the same assumptions. (shrink)

Against the backdrop of the frequent comparison of theories of truth in the literature on semantic paradoxes with regard to which inferences and metainferences are deemed valid, this paper develops a novel approach to defining a binary predicate for representing the valid inferences and metainferences of a theory within the theory itself under the assumption that the theory is defined with a classical meta-theory. The aim with the approach is to obtain a tool which facilitates the comparison between a theory (...) and its competitors within the theory itself, thereby expressing the disagreement between the theories within the theories. After discussing what we can and should require of an object-linguistic representation of a theory for that purpose, this paper proposes to restrict the representation of valid metainferences to locally valid metainferences, a requirement which turns out to be \-consistent and conservative over classical first-order arithmetic. This approach is then applied to four theories definable on strong Kleene models using a labelled nested sequent calculus. (shrink)

I consider two cognitive phenomena: inquiring and justifying, as complementary processes running in opposite directions. I explain on an example that the former process is driven by questions and the latter is a codification of the results of the first one. Traditionally, proof theory focuses on the latter process, and thus describes the former, at best, as an example of a backward proof search. I argue that this is not the best way to analyze cognitive processes driven by questions, and (...) that proof-theoretical analysis of questions can bring mutual benefits for both proof theory and erotetic logic. In the second part of my paper (sect. 6.3) I introduce the structural rules of weakening and contraction. Results concerning their admissibility are discussed. I also sketch an erotetic interpretation of the rule of weakening as reducing information noise, and that of contraction as securing information. (shrink)

Proof-theoretic semantics is an alternative to model-theoretic semantics. It aims at explaining the meaning of the logical constants in terms of the inference rules that govern their behaviour in proofs. We argue that this must be construed as the task of explaining these meanings relative to a logic, i.e., to a consequence relation. Alas, there is no agreed set of properties that a relation must have in order to qualify as a consequence relation. Moreover, the association of a consequence relation (...) to a logical calculus is not as straightforward as it may seem. We show that these facts are problematic for the proof-theoretic project but the problems can be solved. Our thesis is that the consequence relation relevant for proof-theoretic semantics is the one given by the sequent-to-sequent derivability relation in Gentzen systems. (shrink)

The origins of proof-theoretic semantics lie in the question of what constitutes the meaning of the logical connectives and its response: the rules of inference that govern the use of the connective. However, what if we go a step further and ask about the meaning of a proof as a whole? In this paper we address this question and lay out a framework to distinguish sense and denotation of proofs. Two questions are central here. First of all, if we have (...) two different derivations, does this always lead to a difference, firstly, in sense, and secondly, in denotation? The other question is about the relation between different kinds of proof systems with respect to this distinction. Do the different forms of representing a proof necessarily correspond to a difference in how the inferential steps are given? In our framework it will be possible to identify denotation as well as sense of proofs not only within one proof system but also between different kinds of proof systems. Thus, we give an account to distinguish a mere syntactic divergence from a divergence in meaning and a divergence in meaning from a divergence of proof objects analogous to Frege’s distinction for singular terms and sentences. (shrink)

In this dissertation, we shall investigate whether Tennant's criterion for paradoxicality(TCP) can be a correct criterion for genuine paradoxes and whether the requirement of a normal derivation(RND) can be a proof-theoretic solution to the paradoxes. Tennant’s criterion has two types of counterexamples. The one is a case which raises the problem of overgeneration that TCP makes a paradoxical derivation non-paradoxical. The other is one which generates the problem of undergeneration that TCP renders a non-paradoxical derivation paradoxical. Chapter 2 deals with (...) the problem of undergeneration and Chapter 3 concerns the problem of overgeneration. Chapter 2 discusses that Tenant’s diagnosis of the counterexample which applies CR−rule and causes the undergeneration problem is not correct and presents a solution to the problem of undergeneration. Chapter 3 argues that Tennant’s diagnosis of the counterexample raising the overgeneration problem is wrong and provides a solution to the problem. Finally, Chapter 4 addresses what should be explicated in order for RND to be a proof-theoretic solution to the paradoxes. (shrink)

This paper presents a sound and complete five-sided sequent calculus for first-order weak Kleene valuations which permits not only elegant representations of four logics definable on first-order weak Kleene valuations, but also admissibility of five cut rules by proof analysis.

Starting from a proof-theoretic perspective, where meaning is determined by the inference rules governing logical operators, in this paper we primarily aim at developing a proof-theoretic alternative to the model-theoretic meaning-invariant logical pluralism discussed in Beall and Restall. We will also outline how this framework can be easily extended to include a form of meaning-variant logical pluralism. In this respect, the framework developed in this paper—which we label two-level proof-theoretic pluralism—is much broader in scope than the one discussed in Beall (...) and Restall’s book. (shrink)

Proof-theoretic semantics is an alternative to model-theoretic semantics. It aims at explaining the meaning of the logical constants in terms of the inference rules that govern their behaviour in proofs. We argue that this must be construed as the task of explaining these meanings relative to a logic, i.e., to a consequence relation. Alas, there is no agreed set of properties that a relation must have in order to qualify as a consequence relation. Moreover, the association of a consequence relation (...) to a logical calculus is not as straightforward as it may seem. We show that these facts are problematic for the proof-theoretic project but the problems can be solved. Our thesis is that the consequence relation relevant for proof-theoretic semantics is the one given by the sequent-to-sequent derivability relation in Gentzen systems. (shrink)

Intra-theoretical logical pluralism is a form of meaning-invariant pluralism about logic, articulated recently by Hjortland :355–373, 2013). This version of pluralism relies on it being possible to define several distinct notions of provability relative to the same logical calculus. The present paper picks up and explores this theme: How can a single logical calculus express several different consequence relations? The main hypothesis articulated here is that the divide between the internal and external consequence relations in Gentzen systems generates a form (...) of intra-theoretical logical pluralism. (shrink)

Nonclassical theories of truth have in common that they reject principles of classical logic to accommodate an unrestricted truth predicate. However, different nonclassical strategies give up different classical principles. The paper discusses one criterion we might use in theory choice when considering nonclassical rivals: the maxim of minimal mutilation.

We give a simple sequent calculus presentation of R.B. Angell’s logic of analytic containment, recently championed by Kit Fine as a plausible logic of partial content.